pretty.ml 20.4 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
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
let debug_print_labels = Debug.register_flag "print_labels"
31
let debug_print_locs = Debug.register_flag "print_locs"
32

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

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

50
let tv_set = ref Sid.empty
51

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

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

67
let forget_var vs = forget_id iprinter vs.vs_name
68

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

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

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

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

96 97 98 99
let print_ls fmt ls =
  if ls.ls_name.id_string = "mixfix []" then fprintf fmt "([])" else
  if ls.ls_name.id_string = "mixfix [<-]" then fprintf fmt "([<-])" else
  match extract_op ls with
100
  | Some s -> fprintf fmt "(%s)" (escape_op s)
101
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
102 103 104

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

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

(** Types *)

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

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

let print_const fmt = function
125 126 127 128
  | ConstInt (IConstDecimal s) -> fprintf fmt "%s" s
  | ConstInt (IConstHexa s) -> fprintf fmt "0x%s" s
  | ConstInt (IConstOctal s) -> fprintf fmt "0o%s" s
  | ConstInt (IConstBinary s) -> fprintf fmt "0b%s" s
129 130 131 132 133 134 135
  | 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
136
    | Tyvar u when tv_equal u v -> true
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
144
  option_apply true inspect fs.ls_value
145 146 147

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
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
169

170 171
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
172 173

let print_quant fmt = function
174 175
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
176

177 178 179
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
Andrei Paskevich's avatar
Andrei Paskevich committed
180 181
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
182 183
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
184

185
let prio_binop = function
186 187 188 189
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
190

191
let print_label fmt l =
192
  if l = "" then () else fprintf fmt "\"%s\"" l
193

194 195 196 197
let print_loc fmt l =
  let (f,l,b,e) = Loc.get l in
  fprintf fmt "#\"%s\" %d %d %d#" f l b e

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199 200
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
201 202 203
  else ();
  if Debug.test_flag debug_print_locs then
    Util.option_iter (fun l -> fprintf fmt " %a" print_loc l) id.id_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
204 205
  else ()

206

MARCHE Claude's avatar
MARCHE Claude committed
207 208 209
let rec print_term fmt t = print_lterm 0 fmt t

and print_lterm pri fmt t =
210 211
  if Debug.test_flag debug_print_locs then
    Util.option_iter (fun l -> fprintf fmt "%a " print_loc l) t.t_loc;
MARCHE Claude's avatar
MARCHE Claude committed
212
  match t.t_label with
213 214
  | _ when Debug.nottest_flag debug_print_labels
       -> print_tnode pri fmt t
215 216 217
  | [] -> print_tnode pri fmt t
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_tnode 0) t
218

219 220 221 222
and print_app pri ls fmt tl = match extract_op ls, tl with
  | _, [] ->
      print_ls fmt ls
  | Some s, [t1] when tight_op s ->
223 224
      fprintf fmt (protect_on (pri > 7) "%s%a")
        s (print_lterm 7) t1
225 226 227 228 229 230
  | 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
231 232 233 234 235 236
  | _, [t1;t2] when ls.ls_name.id_string = "mixfix []" ->
      fprintf fmt (protect_on (pri > 6) "%a[%a]")
        (print_lterm 6) t1 print_term t2
  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
      fprintf fmt (protect_on (pri > 6) "%a[%a <- %a]")
        (print_lterm 6) t1 (print_lterm 5) t2 (print_lterm 5) t3
237 238 239 240
  | _, tl ->
      fprintf fmt (protect_on (pri > 5) "%a@ %a")
        print_ls ls (print_list space (print_lterm 6)) tl

241
and print_tnode pri fmt t = match t.t_node with
242
  | Tvar v ->
243
      print_vs fmt v
244 245
  | Tconst c ->
      print_const fmt c
Andrei Paskevich's avatar
Andrei Paskevich committed
246 247
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
248
  | Tapp (fs, tl) when unambig_fs fs ->
249
      print_app pri fs fmt tl
250
  | Tapp (fs, tl) ->
251
      fprintf fmt (protect_on (pri > 0) "%a:%a")
252
        (print_app 5 fs) tl print_ty (t_type t)
253
  | Tif (f,t1,t2) ->
254
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
255
        print_term f print_term t1 print_term t2
256 257
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
258
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
259
        print_vs v (print_lterm 4) t1 print_term t2;
260
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
261
  | Tcase (t1,bl) ->
262
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
263
        print_term t1 (print_list newline print_tbranch) bl
264
  | Teps fb ->
265
      let v,f = t_open_bound fb in
266
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
267
        print_vsty v print_term f;
268
      forget_var v
269 270
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
271
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
272
        (print_list comma print_vsty) vl print_tl tl print_term f;
273
      List.iter forget_var vl
274
  | Ttrue ->
275
      fprintf fmt "true"
276
  | Tfalse ->
277
      fprintf fmt "false"
278
  | Tbinop (b,f1,f2) ->
279
      let asym = List.mem Term.asym_label t.t_label in
280 281
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
282
        (print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
283
  | Tnot f ->
284
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) 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_tl fmt tl =
292
  if tl = [] then () else fprintf fmt "@ [%a]"
293
    (print_list alt (print_list comma print_term)) tl
294 295 296

(** Declarations *)

297 298 299 300
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

301 302 303 304
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
305
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
306
    (print_list nothing print_ty_arg) tl
307

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

326
let print_type_decl fst fmt d = print_type_decl fst fmt d; forget_tvs ()
327

328
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
329

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

332
let print_logic_decl fst fmt (ls,ld) = match ld with
333 334
  | Some ld ->
      let vl,e = open_ls_defn ld in
335
      fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
336
        (if fst then ls_kind ls else "with") print_ls ls
337
        print_ident_labels ls.ls_name
338
        (print_list nothing print_vs_arg) vl
339
        (print_option print_ls_type) ls.ls_value print_term e;
340 341
      List.iter forget_var vl
  | None ->
342
      fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
343
        (if fst then ls_kind ls else "with") print_ls ls
344
        print_ident_labels ls.ls_name
345
        (print_list nothing print_ty_arg) ls.ls_args
346 347
        (print_option print_ls_type) ls.ls_value

348
let print_logic_decl fst fmt d = print_logic_decl fst fmt d; forget_tvs ()
349

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

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

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

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

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

374 375 376 377 378 379
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

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

386 387 388 389 390 391 392
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

393 394 395 396
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
397
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
398 399 400

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

402
let print_meta_arg_type fmt = function
403
  | MTty       -> fprintf fmt "[type]"
404
  | MTtysymbol -> fprintf fmt "[type symbol]"
Andrei Paskevich's avatar
Andrei Paskevich committed
405
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
406 407 408 409
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

410
let print_meta_arg fmt = function
411
  | MAty ty -> fprintf fmt "type %a" print_ty ty
412
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
413
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
414 415 416
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
417 418 419

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

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

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

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

452 453
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
454
    let add_pr s p  acc =
455 456
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
457 458
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
Andrei Paskevich's avatar
Andrei Paskevich committed
459
        Leaf (ls_kind ls ^ " " ^ s) :: acc
460 461 462 463 464 465
    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
466 467 468 469
    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
470 471

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

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

481 482 483 484 485 486 487 488 489 490 491 492
(* 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 ->
493 494 495
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
496 497
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
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
  | 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
512
  | Term.TermExpected t ->
513
      fprintf fmt "Not a term: %a" print_term t
514 515
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
516 517 518 519 520 521 522 523 524 525
  | 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
526 527
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
528
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
529
      fprintf fmt "Constructor %a \
530 531
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
532
  | Decl.InvalidIndDecl (_ls, pr) ->
533
      fprintf fmt "Ill-formed inductive clause %a"
534 535
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
536 537
      fprintf fmt "Inductive clause %a contains \
          a negative occurrence of symbol %a"
538
        print_pr pr print_ls ls1
539 540 541
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
542 543
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
544 545 546 547
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
548 549 550 551
  | 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
552 553 554 555 556 557 558
  | 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
559 560
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
561
  | Decl.NonExhaustiveCase (pl, e) ->
562
      fprintf fmt "Pattern @[%a@] is not covered in expression:@\n  @[%a@]"
563
        (print_list comma print_pat) pl print_term e
564 565 566
  | _ -> raise exn
  end