pretty.ml 18.6 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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
let iprinter,tprinter,lprinter,pprinter =
31
32
  let bl = ["theory"; "type"; "logic"; "inductive"; "meta";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop";
33
34
35
36
37
            "namespace"; "import"; "export"; "end";
            "forall"; "exists"; "and"; "or"; "not";
            "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ]
  in
38
39
40
41
42
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  create_ident_printer bl ~sanitizer:isanitize,
44
45
46
47
48
49
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
50
  forget_all pprinter
51

52
let tv_set = ref Sid.empty
53

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

60
61
62
63
64
65
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 =
66
67
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
68

69
let forget_var vs = forget_id iprinter vs.vs_name
70

71
72
73
74
75
76
77
78
79
80
81
82
83
84
(* 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 = "?"

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

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

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

let print_cs fmt ls =
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
100

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

(** Types *)

106
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
107

108
let rec print_ty_node inn fmt ty = match ty.ty_node with
109
  | Tyvar v -> print_tv fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
110
111
  | Tyapp (ts, tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
      (print_list comma (print_ty_node false)) tl
112
  | Tyapp (ts, []) -> print_ts fmt ts
113
114
115
116
  | 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
117
118
119
120
121
122
123
124
125
126

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
127
    | Tyvar u when tv_equal u v -> true
128
129
130
131
132
133
134
135
136
137
138
    | _ -> 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
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
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
160

161
162
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
163
164
165
166
167
168
169
170
171
172
173

let print_quant fmt = function
  | Fforall -> fprintf fmt "forall"
  | Fexists -> fprintf fmt "exists"

let print_binop fmt = function
  | Fand -> fprintf fmt "and"
  | For -> fprintf fmt "or"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

174
175
176
177
178
let prio_binop = function
  | Fand -> 3
  | For -> 2
  | Fimplies -> 1
  | Fiff -> 1
179

180
let print_label fmt (l,_) = fprintf fmt "\"%s\"" l
181

182
183
let rec print_term fmt t = print_lterm 0 fmt t
and     print_fmla fmt f = print_lfmla 0 fmt f
184

185
186
187
188
and print_lterm pri fmt t = match t.t_label with
  | [] -> print_tnode pri fmt t
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_tnode 0) t
189

190
191
192
193
and print_lfmla pri fmt f = match f.f_label with
  | [] -> print_fnode pri fmt f
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_fnode 0) f
194

195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
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

211
and print_tnode pri fmt t = match t.t_node with
212
213
214
  | Tbvar _ ->
      assert false
  | Tvar v ->
215
      print_vs fmt v
216
217
  | Tconst c ->
      print_const fmt c
Andrei Paskevich's avatar
Andrei Paskevich committed
218
219
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
220
  | Tapp (fs, tl) when unambig_fs fs ->
221
      print_app pri fs fmt tl
222
  | Tapp (fs, tl) ->
223
224
      fprintf fmt (protect_on (pri > 0) "%a:%a")
        (print_app 5 fs) tl print_ty t.t_ty
225
  | Tif (f,t1,t2) ->
226
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
227
        print_fmla f print_term t1 print_term t2
228
229
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
230
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
231
        print_vs v (print_lterm 4) t1 print_term t2;
232
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
233
  | Tcase (t1,bl) ->
234
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
235
        print_term t1 (print_list newline print_tbranch) bl
236
237
  | Teps fb ->
      let v,f = f_open_bound fb in
238
239
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
        print_vsty v print_fmla f;
240
      forget_var v
241

242
and print_fnode pri fmt f = match f.f_node with
243
  | Fapp (ps,tl) ->
244
      print_app pri ps fmt tl
245
246
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
247
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
248
249
        (print_list comma print_vsty) vl print_tl tl print_fmla f;
      List.iter forget_var vl
250
251
252
253
254
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
255
256
257
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
        (print_lfmla (p + 1)) f1 print_binop b (print_lfmla p) f2
258
  | Fnot f ->
259
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
260
  | Fif (f1,f2,f3) ->
261
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
262
        print_fmla f1 print_fmla f2 print_fmla f3
263
264
  | Flet (t,f) ->
      let v,f = f_open_bound f in
265
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
266
        print_vs v (print_lterm 4) t print_fmla f;
267
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
268
  | Fcase (t,bl) ->
269
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
270
        print_term t (print_list newline print_fbranch) bl
271

272
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
273
274
275
  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
276

277
and print_fbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
278
279
280
  let p,f = f_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
  Svs.iter forget_var p.pat_vars
281

282
and print_tl fmt tl =
283
  if tl = [] then () else fprintf fmt "@ [%a]"
284
    (print_list alt (print_list comma print_expr)) tl
285

286
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
287
288
289

(** Declarations *)

290
291
292
293
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

294
295
296
297
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
298
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
299
    (print_list nothing print_ty_arg) tl
300

301
let print_type_decl fmt (ts,def) = match def with
302
303
  | Tabstract -> begin match ts.ts_def with
      | None ->
304
305
          fprintf fmt "@[<hov 2>type %a%a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args
306
      | Some ty ->
307
308
          fprintf fmt "@[<hov 2>type %a%a =@ %a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
309
310
      end
  | Talgebraic csl ->
311
      let ty = ty_app ts (List.map ty_var ts.ts_args) in
312
313
      fprintf fmt "@[<hov 2>type %a%a =@\n@[<hov>%a@]@]"
        print_ts ts (print_list nothing print_tv_arg) ts.ts_args
314
        (print_list newline (print_constr ty)) csl
315

316
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
317

318
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
319

320
321
322
323
let print_logic_decl fmt (ls,ld) = match ld with
  | Some ld ->
      let vl,e = open_ls_defn ld in
      fprintf fmt "@[<hov 2>logic %a%a%a =@ %a@]"
324
        print_ls ls (print_list nothing print_vs_arg) vl
325
326
327
328
        (print_option print_ls_type) ls.ls_value print_expr e;
      List.iter forget_var vl
  | None ->
      fprintf fmt "@[<hov 2>logic %a%a%a@]"
329
        print_ls ls (print_list nothing print_ty_arg) ls.ls_args
330
331
332
        (print_option print_ls_type) ls.ls_value

let print_logic_decl fmt d = print_logic_decl fmt d; forget_tvs ()
333

334
335
let print_ind fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr print_fmla f
336

337
let print_ind_decl fmt (ps,bl) =
338
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
339
    print_ls ps (print_list nothing print_ty_arg) ps.ls_args
340
    (print_list newline print_ind) bl;
341
  forget_tvs ()
342

343
344
345
346
347
348
349
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

351
352
353
354
355
let print_prop_decl fmt (k,pr,f) =
  fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
    print_pr pr print_fmla f;
  forget_tvs ()

356
357
358
359
360
361
let print_decl fmt d = match d.d_node with
  | Dtype tl  -> print_list newline print_type_decl fmt tl
  | Dlogic ll -> print_list newline print_logic_decl fmt ll
  | Dind il   -> print_list newline print_ind_decl fmt il
  | Dprop p   -> print_prop_decl fmt p

362
363
364
365
366
367
368
369
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) =
  fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2

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

371
372
373
374
375
376
377
let print_meta_arg_type fmt = function
  | MTtysymbol -> fprintf fmt "[type symbol]"
  | MTlsymbol  -> fprintf fmt "[logic symbol]"
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

378
let print_meta_arg fmt = function
379
380
381
382
383
  | MAts ts -> fprintf fmt "type %a" print_ts ts
  | MAls ls -> fprintf fmt "logic %a" print_ls ls
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
384
385
386

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

let print_theory fmt th =
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
    print_th th (print_list newline2 print_tdecl) th.th_decls
408

409
let print_task fmt task =
410
411
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
412

413
414
module NsTree = struct
  type t =
415
    | Namespace of string * namespace * known_map
416
417
    | Leaf      of string

418
419
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
420
    let add_pr s p  acc =
421
422
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
423
424
425
426
427
428
429
430
431
432
433
434
435
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
        Leaf ("logic " ^ s) :: acc
    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
    let acc = Mnm.fold add_ns ns.ns_ns []  in
    let acc = Mnm.fold add_pr ns.ns_pr acc in
    let acc = Mnm.fold add_ls ns.ns_ls acc in
    let acc = Mnm.fold add_ts ns.ns_ts acc in acc
436
437

  let decomp = function
438
439
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
440
441
end

442
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
443
  let module P = Print_tree.Make(NsTree) in
444
  fprintf fmt "@[<hov>%a@]@." P.print
445
    (NsTree.Namespace (name, th.th_export, th.th_known))
446

447
448
449
450
451
452
453
454
455
456
457
458
(* 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 ->
459
460
461
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
462
463
464
465
  | 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
466
467
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
468
469
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
470
471
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
  | 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
  | Term.NoMatch ->
      fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
  | 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
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
        print_pr pr
  | Decl.TooSpecificIndDecl (_ls, pr, t) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          has too type-specific conclusion %a"
        print_pr pr print_term t
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          contains a negative occurrence of dependent symbol %a"
        print_pr pr print_ls ls1
  | Decl.BadLogicDecl (id1,id2) ->
      fprintf fmt "Ill-formed definition: idents %s and %s are different"
        id1.id_string id2.id_string
502
503
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
504
505
506
507
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
508
509
510
511
  | 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
512
513
514
515
516
517
518
519
  | 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
  | Decl.NonExhaustiveExpr (pl, e) ->
520
521
      fprintf fmt "Pattern @[%a@] is not covered in expression:@\n  @[%a@]"
        (print_list comma print_pat) pl print_expr e
522
523
524
  | _ -> raise exn
  end