pretty.ml 20.4 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
  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,
44
  create_ident_printer bl ~sanitizer:isanitize
45 46 47 48

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
49
  forget_all pprinter
50

51
let tv_set = ref Sid.empty
52

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

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

68
let forget_var vs = forget_id iprinter vs.vs_name
69

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

84 85 86 87 88
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

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

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

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

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

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

(** Types *)

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

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

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

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

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

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

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

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

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

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

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

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

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

255 256
and print_fnode pri fmt f = match f.t_node with
  | Tapp (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
  | Tif (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
  | Tlet (t,f) ->
277
      let v,f = t_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
281
  | Tcase (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
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
285

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

291
and print_fbranch fmt br =
292
  let p,f = t_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
293 294
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
  Svs.iter forget_var p.pat_vars
295

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

300
and print_expr fmt = e_map (print_term fmt) (print_fmla fmt)
301 302 303

(** Declarations *)

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

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

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

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

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

337
let print_logic_decl fst fmt (ls,ld) = match ld with
338 339
  | Some ld ->
      let vl,e = open_ls_defn ld in
340 341 342
      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
343 344 345
        (print_option print_ls_type) ls.ls_value print_expr e;
      List.iter forget_var vl
  | None ->
346 347 348
      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
349 350
        (print_option print_ls_type) ls.ls_value

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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