pretty.ml 19.2 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Pp
open Util
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Decl
27
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
28
open Task
29

30 31
let debug_print_labels = Debug.register_flag "print_labels"

32
let iprinter,tprinter,pprinter =
Andrei Paskevich's avatar
Andrei Paskevich committed
33 34
  let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
35
            "namespace"; "import"; "export"; "end";
Andrei Paskevich's avatar
Andrei Paskevich committed
36 37
            "forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ] in
38 39 40 41
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
42
  create_ident_printer bl ~sanitizer:isanitize
43 44 45 46

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
47
  forget_all pprinter
48

49
let tv_set = ref Sid.empty
50

51 52
(* type variables always start with a quote *)
let print_tv fmt tv =
53
  tv_set := Sid.add tv.tv_name !tv_set;
54 55
  let sanitizer n = "'" ^ n in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
56

57 58 59 60 61 62
let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
63 64
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
65

66
let forget_var vs = forget_id iprinter vs.vs_name
67

68 69 70 71 72 73 74 75 76 77 78 79 80 81
(* pretty-print infix and prefix logic symbols *)

let extract_op ls =
  let s = ls.ls_name.id_string in
  let len = String.length s in
  if len < 7 then None else
  let inf = String.sub s 0 6 in
  if inf = "infix "  then Some (String.sub s 6 (len - 6)) else
  let prf = String.sub s 0 7 in
  if prf = "prefix " then Some (String.sub s 7 (len - 7)) else
  None

let tight_op s = let c = String.sub s 0 1 in c = "!" || c = "?"

82 83 84 85 86
let escape_op s =
  let s = Str.replace_first (Str.regexp "^\\*.") " \\0" s in
  let s = Str.replace_first (Str.regexp ".\\*$") "\\0 " s in
  s

87 88
(* theory names always start with an upper case letter *)
let print_th fmt th =
89 90
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
91

92 93
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
94

95
let print_ls fmt ls = match extract_op ls with
96
  | Some s -> fprintf fmt "(%s)" (escape_op s)
97
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
98 99 100

let print_cs fmt ls =
  let sanitizer = String.capitalize in
101
  fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
102

103
let print_pr fmt pr =
104
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
105 106 107

(** Types *)

108
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
109

110
let rec print_ty_node inn fmt ty = match ty.ty_node with
111
  | Tyvar v -> print_tv fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
112 113
  | Tyapp (ts, tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
      (print_list comma (print_ty_node false)) tl
114
  | Tyapp (ts, []) -> print_ts fmt ts
115 116 117 118
  | Tyapp (ts, tl) -> fprintf fmt (protect_on inn "%a@ %a")
      print_ts ts (print_list space (print_ty_node true)) tl

let print_ty = print_ty_node false
119 120 121 122 123 124 125 126 127 128

let print_const fmt = function
  | ConstInt s -> fprintf fmt "%s" s
  | ConstReal (RConstDecimal (i,f,None)) -> fprintf fmt "%s.%s" i f
  | ConstReal (RConstDecimal (i,f,Some e)) -> fprintf fmt "%s.%se%s" i f e
  | ConstReal (RConstHexa (i,f,e)) -> fprintf fmt "0x%s.%sp%s" i f e

(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
  let rec lookup v ty = match ty.ty_node with
129
    | Tyvar u when tv_equal u v -> true
130 131 132 133 134 135 136
    | _ -> ty_any (lookup v) ty
  in
  let lookup v = List.exists (lookup v) fs.ls_args in
  let rec inspect ty = match ty.ty_node with
    | Tyvar u when not (lookup u) -> false
    | _ -> ty_all inspect ty
  in
137
  option_apply true inspect fs.ls_value
138 139 140

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
let rec print_pat_node pri fmt p = match p.pat_node with
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
      print_vs fmt v
  | Pas (p, v) ->
      fprintf fmt (protect_on (pri > 1) "%a as %a")
        (print_pat_node 1) p print_vs v
  | Por (p, q) ->
      fprintf fmt (protect_on (pri > 0) "%a | %a")
        (print_pat_node 0) p (print_pat_node 0) q
  | Papp (cs, pl) when is_fs_tuple cs ->
      fprintf fmt (protect_on (pri > 0) "%a")
        (print_list comma (print_pat_node 1)) pl
  | Papp (cs, []) ->
      print_cs fmt cs
  | Papp (cs, pl) ->
      fprintf fmt (protect_on (pri > 1) "%a@ %a")
        print_cs cs (print_list space (print_pat_node 2)) pl

let print_pat = print_pat_node 0
162

163 164
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
165 166

let print_quant fmt = function
167 168
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
169 170

let print_binop fmt = function
Andrei Paskevich's avatar
Andrei Paskevich committed
171 172
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
173 174
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
175

176
let prio_binop = function
177 178 179 180
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
181

182
let print_label fmt l =
183
  if l = "" then () else fprintf fmt "\"%s\"" l
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185 186 187 188 189
let print_ident_labels fmt id =
  if Debug.test_flag debug_print_labels && id.id_label <> []
  then fprintf fmt " %a" (print_list space print_label) id.id_label
  else ()

190
let rec print_term fmt t = print_lterm 0 fmt t
191

192
and print_lterm pri fmt t = match t.t_label with
193 194
  | _ when Debug.nottest_flag debug_print_labels
       -> print_tnode pri fmt t
195 196 197
  | [] -> print_tnode pri fmt t
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_tnode 0) t
198

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
and print_app pri ls fmt tl = match extract_op ls, tl with
  | _, [] ->
      print_ls fmt ls
  | Some s, [t1] when tight_op s ->
      fprintf fmt (protect_on (pri > 6) "%s%a")
        s (print_lterm 6) t1
  | Some s, [t1] ->
      fprintf fmt (protect_on (pri > 4) "%s %a")
        s (print_lterm 5) t1
  | Some s, [t1;t2] ->
      fprintf fmt (protect_on (pri > 4) "%a %s@ %a")
        (print_lterm 5) t1 s (print_lterm 5) t2
  | _, tl ->
      fprintf fmt (protect_on (pri > 5) "%a@ %a")
        print_ls ls (print_list space (print_lterm 6)) tl

215
and print_tnode pri fmt t = match t.t_node with
216
  | Tvar v ->
217
      print_vs fmt v
218 219
  | Tconst c ->
      print_const fmt c
Andrei Paskevich's avatar
Andrei Paskevich committed
220 221
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
222
  | Tapp (fs, tl) when unambig_fs fs ->
223
      print_app pri fs fmt tl
224
  | Tapp (fs, tl) ->
225
      fprintf fmt (protect_on (pri > 0) "%a:%a")
226
        (print_app 5 fs) tl print_ty (t_type t)
227
  | Tif (f,t1,t2) ->
228
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
229
        print_term f print_term t1 print_term t2
230 231
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
232
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
233
        print_vs v (print_lterm 4) t1 print_term t2;
234
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
235
  | Tcase (t1,bl) ->
236
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
237
        print_term t1 (print_list newline print_tbranch) bl
238
  | Teps fb ->
239
      let v,f = t_open_bound fb in
240
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
241
        print_vsty v print_term f;
242
      forget_var v
243 244
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
245
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
246
        (print_list comma print_vsty) vl print_tl tl print_term f;
247
      List.iter forget_var vl
248
  | Ttrue ->
249
      fprintf fmt "true"
250
  | Tfalse ->
251
      fprintf fmt "false"
252
  | Tbinop (b,f1,f2) ->
253 254
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
255
        (print_lterm (p + 1)) f1 print_binop b (print_lterm p) f2
256
  | Tnot f ->
257
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
258

259
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
260 261 262
  let p,t = t_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
  Svs.iter forget_var p.pat_vars
263

264
and print_tl fmt tl =
265
  if tl = [] then () else fprintf fmt "@ [%a]"
266
    (print_list alt (print_list comma print_term)) tl
267 268 269

(** Declarations *)

270 271 272 273
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node true) ty
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs

274 275 276 277
let print_constr ty fmt cs =
  let ty_val = of_option cs.ls_value in
  let m = ty_match Mtv.empty ty_val ty in
  let tl = List.map (ty_inst m) cs.ls_args in
278
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
279
    (print_list nothing print_ty_arg) tl
280

281
let print_type_decl fst fmt (ts,def) = match def with
282 283
  | Tabstract -> begin match ts.ts_def with
      | None ->
284 285
          fprintf fmt "@[<hov 2>%s %a%a@]"
            (if fst then "type" else "with") print_ts ts
286
            (print_list nothing print_tv_arg) ts.ts_args
287
      | Some ty ->
288 289
          fprintf fmt "@[<hov 2>%s %a%a =@ %a@]"
            (if fst then "type" else "with") print_ts ts
290
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
291 292
      end
  | Talgebraic csl ->
293
      let ty = ty_app ts (List.map ty_var ts.ts_args) in
294 295 296
      fprintf fmt "@[<hov 2>%s %a%a =@\n@[<hov>%a@]@]"
        (if fst then "type" else "with") print_ts ts
        (print_list nothing print_tv_arg) ts.ts_args
297
        (print_list newline (print_constr ty)) csl
298

299
let print_type_decl fst fmt d = print_type_decl fst fmt d; forget_tvs ()
300

301
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
302

Andrei Paskevich's avatar
Andrei Paskevich committed
303 304
let ls_kind ls = if ls.ls_value = None then "predicate" else "function"

305
let print_logic_decl fst fmt (ls,ld) = match ld with
306 307
  | Some ld ->
      let vl,e = open_ls_defn ld in
308
      fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
309
        (if fst then ls_kind ls else "with") print_ls ls
310
        (print_list nothing print_vs_arg) vl
311
        (print_option print_ls_type) ls.ls_value print_term e;
312 313
      List.iter forget_var vl
  | None ->
314
      fprintf fmt "@[<hov 2>%s %a%a%a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
315
        (if fst then ls_kind ls else "with") print_ls ls
316
        (print_list nothing print_ty_arg) ls.ls_args
317 318
        (print_option print_ls_type) ls.ls_value

319
let print_logic_decl fst fmt d = print_logic_decl fst fmt d; forget_tvs ()
320

321
let print_ind fmt (pr,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
322
  fprintf fmt "@[<hov 4>| %a%a : %a@]"
323
    print_pr pr print_ident_labels pr.pr_name print_term f
324

325 326 327 328
let print_ind_decl fst fmt (ps,bl) =
  fprintf fmt "@[<hov 2>%s %a%a =@ @[<hov>%a@]@]"
    (if fst then "inductive" else "with") print_ls ps
    (print_list nothing print_ty_arg) ps.ls_args
329
    (print_list newline print_ind) bl;
330
  forget_tvs ()
331

332 333 334 335 336 337 338
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
339

340
let print_prop_decl fmt (k,pr,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
341
  fprintf fmt "@[<hov 2>%a %a%a : %a@]" print_pkind k
342
    print_pr pr print_ident_labels pr.pr_name print_term f;
343 344
  forget_tvs ()

345 346 347 348 349 350
let print_list_next sep print fmt = function
  | [] -> ()
  | [x] -> print true fmt x
  | x :: r -> print true fmt x; sep fmt ();
      print_list sep (print false) fmt r

351
let print_decl fmt d = match d.d_node with
352 353 354
  | Dtype tl  -> print_list_next newline print_type_decl fmt tl
  | Dlogic ll -> print_list_next newline print_logic_decl fmt ll
  | Dind il   -> print_list_next newline print_ind_decl fmt il
355 356
  | Dprop p   -> print_prop_decl fmt p

357 358 359 360 361 362 363
let print_next_type_decl  = print_type_decl false
let print_type_decl       = print_type_decl true
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
let print_next_ind_decl   = print_ind_decl false
let print_ind_decl        = print_ind_decl true

364 365 366 367
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

let print_inst_ls fmt (ls1,ls2) =
Andrei Paskevich's avatar
Andrei Paskevich committed
368
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
369 370 371

let print_inst_pr fmt (pr1,pr2) =
  fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
372

373
let print_meta_arg_type fmt = function
374
  | MTty       -> fprintf fmt "[type]"
375
  | MTtysymbol -> fprintf fmt "[type symbol]"
Andrei Paskevich's avatar
Andrei Paskevich committed
376
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
377 378 379 380
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

381
let print_meta_arg fmt = function
382
  | MAty ty -> fprintf fmt "type %a" print_ty ty
383
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
384
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
385 386 387
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
388 389 390

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
391
      print_decl fmt d
392
  | Use th ->
393
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
394
  | Clone (th,sm) when is_empty_sm sm ->
395
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
396 397 398 399
  | Clone (th,sm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
      let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) sm.sm_pr [] in
400
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
401 402 403
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
404
  | Meta (m,al) ->
405
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
406
        m.meta_name (print_list comma print_meta_arg) al
407 408

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
409 410 411
  fprintf fmt "@[<hov 2>theory %a%a@\n%a@]@\nend@."
    print_th th print_ident_labels th.th_name
    (print_list newline2 print_tdecl) th.th_decls
412

413
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
414
  forget_all ();
415 416
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
417

418 419
module NsTree = struct
  type t =
420
    | Namespace of string * namespace * known_map
421 422
    | Leaf      of string

423 424
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
425
    let add_pr s p  acc =
426 427
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
428 429
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
Andrei Paskevich's avatar
Andrei Paskevich committed
430
        Leaf (ls_kind ls ^ " " ^ s) :: acc
431 432 433 434 435 436
    in
    let add_ts s ts acc =
      if s = "int"  && ts_equal ts ts_int  then acc else
      if s = "real" && ts_equal ts ts_real then acc else
        Leaf ("type " ^ s) :: acc
    in
437 438 439 440
    let acc = Mstr.fold add_ns ns.ns_ns []  in
    let acc = Mstr.fold add_pr ns.ns_pr acc in
    let acc = Mstr.fold add_ls ns.ns_ls acc in
    let acc = Mstr.fold add_ts ns.ns_ts acc in acc
441 442

  let decomp = function
443 444
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
445 446
end

447
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
448
  let module P = Print_tree.Make(NsTree) in
449
  fprintf fmt "@[<hov>%a@]@." P.print
450
    (NsTree.Namespace (name, th.th_export, th.th_known))
451

452 453 454 455 456 457 458 459 460 461 462 463
(* Exception reporting *)

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | Ty.TypeMismatch (t1,t2) ->
      fprintf fmt "Type mismatch between %a and %a"
        print_ty t1 print_ty t2
  | Ty.BadTypeArity (ts, ts_arg, app_arg) ->
      fprintf fmt "Bad type arity: type symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ts ts ts_arg app_arg
  | Ty.DuplicateTypeVar tv ->
464 465 466
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
467 468
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
469 470 471 472
  | Term.BadArity (ls, ls_arg, app_arg) ->
      fprintf fmt "Bad arity: symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ls ls ls_arg app_arg
473 474
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
475 476
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
477 478
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
479 480 481 482
  | Term.FunctionSymbolExpected ls ->
      fprintf fmt "Not a function symbol: %a" print_ls ls
  | Term.PredicateSymbolExpected ls ->
      fprintf fmt "Not a predicate symbol: %a" print_ls ls
483
  | Term.TermExpected t ->
484
      fprintf fmt "Not a term: %a" print_term t
485 486
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
487 488 489 490 491 492 493 494 495 496
  | Pattern.ConstructorExpected ls ->
      fprintf fmt "The symbol %a is not a constructor"
        print_ls ls
  | Pattern.NonExhaustive pl ->
      fprintf fmt "Non-exhaustive pattern list:@\n@[<hov 2>%a@]"
        (print_list newline print_pat) pl
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
497 498
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
499
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
500
      fprintf fmt "Constructor %a \
501 502
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
503
  | Decl.InvalidIndDecl (_ls, pr) ->
504
      fprintf fmt "Ill-formed inductive clause %a"
505 506
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
507 508
      fprintf fmt "Inductive clause %a contains \
          a negative occurrence of symbol %a"
509
        print_pr pr print_ls ls1
510 511 512
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
513 514
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
515 516 517 518
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
519 520 521 522
  | Decl.EmptyAlgDecl ts ->
      fprintf fmt "Algebraic type %a has no constructors" print_ts ts
  | Decl.EmptyIndDecl ls ->
      fprintf fmt "Inductive predicate %a has no constructors" print_ls ls
523 524 525 526 527 528 529
  | Decl.KnownIdent id ->
      fprintf fmt "Ident %s is already declared" id.id_string
  | Decl.UnknownIdent id ->
      fprintf fmt "Ident %s is not yet declared" id.id_string
  | Decl.RedeclaredIdent id ->
      fprintf fmt "Ident %s is already declared, with a different declaration"
        id.id_string
530 531
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
532
  | Decl.NonExhaustiveCase (pl, e) ->
533
      fprintf fmt "Pattern @[%a@] is not covered in expression:@\n  @[%a@]"
534
        (print_list comma print_pat) pl print_term e
535 536 537
  | _ -> raise exn
  end