pretty.ml 20.1 KB
Newer Older
1
2
3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
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 =
33
34
  let bl = ["theory"; "type"; "logic"; "inductive"; "meta";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop";
35
36
37
38
39
            "namespace"; "import"; "export"; "end";
            "forall"; "exists"; "and"; "or"; "not";
            "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ]
  in
40
41
42
43
44
45
46
47
48
49
  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,
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
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
87
88
89
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

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

95
96
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
97

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

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

106
let print_pr fmt pr =
107
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
108
109
110

(** Types *)

111
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
112

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

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
132
    | Tyvar u when tv_equal u v -> true
133
134
135
136
137
138
139
140
141
142
143
    | _ -> 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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
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
165

166
167
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
168
169
170
171
172
173
174
175
176
177
178

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 "<->"

179
180
181
182
183
let prio_binop = function
  | Fand -> 3
  | For -> 2
  | Fimplies -> 1
  | Fiff -> 1
184

185
let print_label fmt l =
186
  if l = "" then () else fprintf fmt "\"%s\"" l
187

Andrei Paskevich's avatar
Andrei Paskevich committed
188
189
190
191
192
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 ()

193
194
let rec print_term fmt t = print_lterm 0 fmt t
and     print_fmla fmt f = print_lfmla 0 fmt f
195

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

203
and print_lfmla pri fmt f = match f.f_label with
204
205
  | _ when Debug.nottest_flag debug_print_labels
       -> print_fnode pri fmt f
206
207
208
  | [] -> print_fnode pri fmt f
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_fnode 0) f
209

210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
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

226
and print_tnode pri fmt t = match t.t_node with
227
  | Tvar v ->
228
      print_vs fmt v
229
230
  | Tconst c ->
      print_const fmt c
Andrei Paskevich's avatar
Andrei Paskevich committed
231
232
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
233
  | Tapp (fs, tl) when unambig_fs fs ->
234
      print_app pri fs fmt tl
235
  | Tapp (fs, tl) ->
236
237
      fprintf fmt (protect_on (pri > 0) "%a:%a")
        (print_app 5 fs) tl print_ty t.t_ty
238
  | Tif (f,t1,t2) ->
239
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
240
        print_fmla f print_term t1 print_term t2
241
242
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
243
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
244
        print_vs v (print_lterm 4) t1 print_term t2;
245
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
246
  | Tcase (t1,bl) ->
247
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
248
        print_term t1 (print_list newline print_tbranch) bl
249
250
  | Teps fb ->
      let v,f = f_open_bound fb in
251
252
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
        print_vsty v print_fmla f;
253
      forget_var v
254

255
and print_fnode pri fmt f = match f.f_node with
256
  | Fapp (ps,tl) ->
257
      print_app pri ps fmt tl
258
259
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
260
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
261
262
        (print_list comma print_vsty) vl print_tl tl print_fmla f;
      List.iter forget_var vl
263
264
265
266
267
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
268
269
270
      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
271
  | Fnot f ->
272
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
273
  | Fif (f1,f2,f3) ->
274
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
275
        print_fmla f1 print_fmla f2 print_fmla f3
276
277
  | Flet (t,f) ->
      let v,f = f_open_bound f in
278
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
279
        print_vs v (print_lterm 4) t print_fmla f;
280
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
281
  | Fcase (t,bl) ->
282
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
283
        print_term t (print_list newline print_fbranch) bl
284

285
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
286
287
288
  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
289

290
and print_fbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
291
292
293
  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
294

295
and print_tl fmt tl =
296
  if tl = [] then () else fprintf fmt "@ [%a]"
297
    (print_list alt (print_list comma print_expr)) tl
298

299
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
300
301
302

(** Declarations *)

303
304
305
306
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

307
308
309
310
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
311
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
312
    (print_list nothing print_ty_arg) tl
313

314
let print_type_decl fst fmt (ts,def) = match def with
315
316
  | Tabstract -> begin match ts.ts_def with
      | None ->
317
318
          fprintf fmt "@[<hov 2>%s %a%a@]"
            (if fst then "type" else "with") print_ts ts
319
            (print_list nothing print_tv_arg) ts.ts_args
320
      | Some ty ->
321
322
          fprintf fmt "@[<hov 2>%s %a%a =@ %a@]"
            (if fst then "type" else "with") print_ts ts
323
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
324
325
      end
  | Talgebraic csl ->
326
      let ty = ty_app ts (List.map ty_var ts.ts_args) in
327
328
329
      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
330
        (print_list newline (print_constr ty)) csl
331

332
let print_type_decl fst fmt d = print_type_decl fst fmt d; forget_tvs ()
333

334
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
335

336
let print_logic_decl fst fmt (ls,ld) = match ld with
337
338
  | Some ld ->
      let vl,e = open_ls_defn ld in
339
340
341
      fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]"
        (if fst then "logic" else "with") print_ls ls
        (print_list nothing print_vs_arg) vl
342
343
344
        (print_option print_ls_type) ls.ls_value print_expr e;
      List.iter forget_var vl
  | None ->
345
346
347
      fprintf fmt "@[<hov 2>%s %a%a%a@]"
        (if fst then "logic" else "with") print_ls ls
        (print_list nothing print_ty_arg) ls.ls_args
348
349
        (print_option print_ls_type) ls.ls_value

350
let print_logic_decl fst fmt d = print_logic_decl fst fmt d; forget_tvs ()
351

352
let print_ind fmt (pr,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
353
354
  fprintf fmt "@[<hov 4>| %a%a : %a@]"
    print_pr pr print_ident_labels pr.pr_name print_fmla f
355

356
357
358
359
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
360
    (print_list newline print_ind) bl;
361
  forget_tvs ()
362

363
364
365
366
367
368
369
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

371
let print_prop_decl fmt (k,pr,f) =
Andrei Paskevich's avatar
Andrei Paskevich committed
372
373
  fprintf fmt "@[<hov 2>%a %a%a : %a@]" print_pkind k
    print_pr pr print_ident_labels pr.pr_name print_fmla f;
374
375
  forget_tvs ()

376
377
378
379
380
381
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

382
let print_decl fmt d = match d.d_node with
383
384
385
  | 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
386
387
  | Dprop p   -> print_prop_decl fmt p

388
389
390
391
392
393
394
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

395
396
397
398
399
400
401
402
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
403

404
let print_meta_arg_type fmt = function
405
  | MTty       -> fprintf fmt "[type]"
406
407
408
409
410
411
  | MTtysymbol -> fprintf fmt "[type symbol]"
  | MTlsymbol  -> fprintf fmt "[logic symbol]"
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

412
let print_meta_arg fmt = function
413
  | MAty ty -> fprintf fmt "type %a" print_ty ty
414
415
416
417
418
  | 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
419
420
421

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
422
      print_decl fmt d
423
  | Use th ->
424
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
425
  | Clone (th,sm) when is_empty_sm sm ->
426
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
427
428
429
430
  | 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
431
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
432
433
434
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
435
  | Meta (m,al) ->
436
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
437
        m.meta_name (print_list comma print_meta_arg) al
438
439

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
440
441
442
  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
443

444
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
445
  forget_all ();
446
447
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
448

449
450
module NsTree = struct
  type t =
451
    | Namespace of string * namespace * known_map
452
453
    | Leaf      of string

454
455
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
456
    let add_pr s p  acc =
457
458
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
459
460
461
462
463
464
465
466
467
468
469
470
471
    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
472
473

  let decomp = function
474
475
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
476
477
end

478
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
479
  let module P = Print_tree.Make(NsTree) in
480
  fprintf fmt "@[<hov>%a@]@." P.print
481
    (NsTree.Namespace (name, th.th_export, th.th_known))
482

483
484
485
486
487
488
489
490
491
492
493
494
(* 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 ->
495
496
497
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
498
499
500
501
  | 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
502
503
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
504
505
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
506
507
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
  | 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
524
525
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
526
527
528
529
  | Decl.NonPositiveTypeDecl (_ts, ls, ts1) ->
      fprintf fmt "Constructor %a \
          contains a non strictly positive occurrence of type symbol %a"
        print_ls ls print_ts ts1
530
  | Decl.InvalidIndDecl (_ls, pr) ->
531
      fprintf fmt "Ill-formed inductive clause %a"
532
533
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
534
535
      fprintf fmt "Inductive clause %a contains \
          a negative occurrence of symbol %a"
536
        print_pr pr print_ls ls1
537
538
539
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
540
541
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
542
543
544
545
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
546
547
548
549
  | 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
550
551
552
553
554
555
556
  | 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
557
558
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
559
  | Decl.NonExhaustiveExpr (pl, e) ->
560
561
      fprintf fmt "Pattern @[%a@] is not covered in expression:@\n  @[%a@]"
        (print_list comma print_pat) pl print_expr e
562
563
564
  | _ -> raise exn
  end