pretty.ml 20.7 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13

open Format
open Pp
14
open Stdlib
15
open Number
16 17 18
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
19
open Decl
20
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
21
open Task
22

23
let debug_print_labels = Debug.register_info_flag "print_labels"
24
  ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
25
let debug_print_locs = Debug.register_info_flag "print_locs"
26
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
27

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

41 42 43
let forget_tvs () =
  forget_all aprinter

44 45
let forget_all () =
  forget_all iprinter;
46
  forget_all aprinter;
47
  forget_all tprinter;
48
  forget_all pprinter
49

50 51 52 53 54 55 56 57 58 59 60 61
let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label

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

let print_ident_labels fmt id =
  if Debug.test_flag debug_print_labels &&
      not (Slab.is_empty id.id_label) then
    fprintf fmt "@ %a" print_labels id.id_label;
  if Debug.test_flag debug_print_locs then
62
    Opt.iter (fprintf fmt "@ %a" print_loc) id.id_loc
63

64 65
(* type variables always start with a quote *)
let print_tv fmt tv =
66
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
67 68 69

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
70
  let id = vs.vs_name in
71
  let sanitizer = String.uncapitalize in
72 73
  fprintf fmt "%s" (id_unique iprinter ~sanitizer id);
  print_ident_labels fmt id
74

75
let forget_var vs = forget_id iprinter vs.vs_name
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90
(* 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 = "?"

91 92 93 94 95
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

96 97
(* theory names always start with an upper case letter *)
let print_th fmt th =
98 99
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
100

101 102
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
103

104 105 106 107
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
108
  | Some s -> fprintf fmt "(%s)" (escape_op s)
109
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
110 111 112

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

115
let print_pr fmt pr =
116
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
117 118 119

(** Types *)

120
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
121

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

let print_const fmt = function
133 134 135 136 137 138 139 140
  | ConstInt (IConstDec s) -> fprintf fmt "%s" s
  | ConstInt (IConstHex s) -> fprintf fmt "0x%s" s
  | ConstInt (IConstOct s) -> fprintf fmt "0o%s" s
  | ConstInt (IConstBin s) -> fprintf fmt "0b%s" s
  | ConstReal (RConstDec (i,f,None)) -> fprintf fmt "%s.%s" i f
  | ConstReal (RConstDec (i,f,Some e)) -> fprintf fmt "%s.%se%s" i f e
  | ConstReal (RConstHex (i,f,Some e)) -> fprintf fmt "0x%s.%sp%s" i f e
  | ConstReal (RConstHex (i,f,None)) -> fprintf fmt "0x%s.%s" i f
141 142 143 144

(* 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
145
    | Tyvar u when tv_equal u v -> true
146 147 148 149 150 151 152
    | _ -> 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
153
  Opt.fold (fun _ -> inspect) true fs.ls_value
154 155 156

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
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
178

179 180
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
181 182

let print_quant fmt = function
183 184
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
185

186 187 188
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
Andrei Paskevich's avatar
Andrei Paskevich committed
189 190
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
191 192
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
193

194
let prio_binop = function
195 196 197 198
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
199

200

MARCHE Claude's avatar
MARCHE Claude committed
201 202 203
let rec print_term fmt t = print_lterm 0 fmt t

and print_lterm pri fmt t =
204
  let print_tlab pri fmt t =
205
    if Debug.test_flag debug_print_labels && not (Slab.is_empty t.t_label)
206
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
207
      print_labels t.t_label (print_tnode 0) t
208 209
    else print_tnode pri fmt t in
  let print_tloc pri fmt t =
210
    if Debug.test_flag debug_print_locs && t.t_loc <> None
211
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
212 213 214
      (print_option print_loc) t.t_loc (print_tlab 0) t
    else print_tlab pri fmt t in
  print_tloc pri fmt t
215

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

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

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

288
and print_tl fmt tl =
289
  if tl = [] then () else fprintf fmt "@ [%a]"
290
    (print_list alt (print_list comma print_term)) tl
291 292 293

(** Declarations *)

294 295 296 297
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

298 299 300 301 302 303
let print_constr fmt (cs,pjl) =
  let add_pj pj ty pjl = (pj,ty)::pjl in
  let print_pj fmt (pj,ty) = match pj with
    | Some ls -> fprintf fmt "@ (%a:@,%a)" print_ls ls print_ty ty
    | None -> print_ty_arg fmt ty
  in
304 305
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
    print_ident_labels cs.ls_name
306 307
    (print_list nothing print_pj)
    (List.fold_right2 add_pj pjl cs.ls_args [])
308

309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
let print_ty_decl fmt ts =
  let print_def fmt = function
    | None -> ()
    | Some ty -> fprintf fmt " =@ %a" print_ty ty
  in
  fprintf fmt "@[<hov 2>type %a%a%a%a@]"
    print_ts ts print_ident_labels ts.ts_name
    (print_list nothing print_tv_arg) ts.ts_args
    print_def ts.ts_def;
  forget_tvs ()

let print_data_decl fst fmt (ts,csl) =
  fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]"
    (if fst then "type" else "with") print_ts ts
    print_ident_labels ts.ts_name
    (print_list nothing print_tv_arg) ts.ts_args
    (print_list newline print_constr) csl;
  forget_tvs ()
327

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

330 331 332
let ls_kind ls =
  if ls.ls_value = None then "predicate"
  else if ls.ls_args = [] then "constant" else "function"
Andrei Paskevich's avatar
Andrei Paskevich committed
333

334 335 336 337 338 339 340
let print_param_decl fmt ls =
  fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
    (ls_kind ls) print_ls ls
    print_ident_labels ls.ls_name
    (print_list nothing print_ty_arg) ls.ls_args
    (print_option print_ls_type) ls.ls_value;
  forget_tvs ()
341

342 343 344 345 346 347 348 349 350
let print_logic_decl fst fmt (ls,ld) =
  let vl,e = open_ls_defn ld in
  fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]"
    (if fst then ls_kind ls else "with") print_ls ls
    print_ident_labels ls.ls_name
    (print_list nothing print_vs_arg) vl
    (print_option print_ls_type) ls.ls_value print_term e;
  List.iter forget_var vl;
  forget_tvs ()
351

352
let print_ind fmt (pr,f) =
353
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
354
    print_pr pr print_ident_labels pr.pr_name print_term f
355

356 357 358 359 360
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

let print_ind_decl s fst fmt (ps,bl) =
361
  fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]"
362
    (if fst then ind_sign s else "with") print_ls ps
363
    print_ident_labels ps.ls_name
364
    (print_list nothing print_ty_arg) ps.ls_args
365 366
    (print_list newline print_ind) bl;
  forget_tvs ()
367

368 369 370 371 372 373 374
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

376
let print_prop_decl fmt (k,pr,f) =
377
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
378
    print_pr pr print_ident_labels pr.pr_name print_term f;
379 380
  forget_tvs ()

381 382 383 384 385 386
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

387
let print_decl fmt d = match d.d_node with
388 389 390
  | Dtype ts  -> print_ty_decl fmt ts
  | Ddata tl  -> print_list_next newline print_data_decl fmt tl
  | Dparam ls -> print_param_decl fmt ls
391
  | Dlogic ll -> print_list_next newline print_logic_decl fmt ll
392
  | Dind (s, il) -> print_list_next newline (print_ind_decl s) fmt il
393 394
  | Dprop p   -> print_prop_decl fmt p

395 396
let print_next_data_decl  = print_data_decl false
let print_data_decl       = print_data_decl true
397 398
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
399 400
let print_next_ind_decl   = print_ind_decl Ind false
let print_ind_decl fmt s  = print_ind_decl s true fmt
401

402 403 404 405
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
406
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
407 408 409

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

411
let print_meta_arg_type fmt = function
412
  | MTty       -> fprintf fmt "[type]"
413
  | MTtysymbol -> fprintf fmt "[type symbol]"
Andrei Paskevich's avatar
Andrei Paskevich committed
414
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
415 416 417 418
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

419
let print_meta_arg fmt = function
420
  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
421
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
422
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
423 424 425
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
426

427 428 429 430 431 432
let print_qt fmt th =
  if th.th_path = [] then print_th fmt th else
  fprintf fmt "%a.%a"
    (print_list (constant_string ".") string) th.th_path
    print_th th

433 434
let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
435
      print_decl fmt d
436
  | Use th ->
437
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
438
  | Clone (th,sm) when is_empty_sm sm ->
439
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
440 441 442 443
  | 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
444
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
445
        print_qt th (print_list comma print_inst_ts) tm
446 447
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
448
  | Meta (m,al) ->
449
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
450
        m.meta_name (print_list comma print_meta_arg) al
451 452

let print_theory fmt th =
453 454 455
  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
456

457
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
458
  forget_all ();
459 460
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
461

462 463
module NsTree = struct
  type t =
464
    | Namespace of string * namespace * known_map
465 466
    | Leaf      of string

467 468
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
469
    let add_pr s p  acc =
470 471
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
472 473
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
Andrei Paskevich's avatar
Andrei Paskevich committed
474
        Leaf (ls_kind ls ^ " " ^ s) :: acc
475 476 477 478 479 480
    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
481 482 483 484
    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
485 486

  let decomp = function
487 488
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
489 490
end

491
let print_namespace fmt name th =
492
  let module P = Print_tree.Make(NsTree) in
493
  fprintf fmt "@[<hov>%a@]@." P.print
494
    (NsTree.Namespace (name, th.th_export, th.th_known))
495

496 497 498 499 500 501 502
(* 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
503
  | Ty.BadTypeArity (ts, app_arg) ->
504 505
      fprintf fmt "Bad type arity: type symbol %a must be applied \
                   to %i arguments, but is applied to %i"
506
        print_ts ts (List.length ts.ts_args) app_arg
507
  | Ty.DuplicateTypeVar tv ->
508 509 510
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
511 512
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
513
  | Term.BadArity (ls, app_arg) ->
514 515
      fprintf fmt "Bad arity: symbol %a must be applied \
                   to %i arguments, but is applied to %i"
516
        print_ls ls (List.length ls.ls_args) app_arg
517 518
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
519 520
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
521 522
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
523 524 525 526
  | 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
527 528 529
  | Term.ConstructorExpected ls ->
      fprintf fmt "Symbol %a is not a constructor"
        print_ls ls
530
  | Term.TermExpected t ->
531
      fprintf fmt "Not a term: %a" print_term t
532 533
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
534 535 536
  | Pattern.ConstructorExpected (ls,ty) ->
      fprintf fmt "Symbol %a is not a constructor of type %a"
        print_ls ls print_ty ty
537
  | Pattern.NonExhaustive pl ->
538 539
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
        print_pat (List.hd pl)
540 541 542 543
  | Decl.BadConstructor ls ->
      fprintf fmt "Bad constructor symbol: %a" print_ls ls
  | Decl.BadRecordField ls ->
      fprintf fmt "Not a record field: %a" print_ls ls
544 545 546 547
  | Decl.RecordFieldMissing (_cs,ls) ->
      fprintf fmt "Field %a is missing" print_ls ls
  | Decl.DuplicateRecordField (_cs,ls) ->
      fprintf fmt "Field %a is used twice in the same constructor" print_ls ls
548 549 550 551
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
552 553
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
554
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
555
      fprintf fmt "Constructor %a \
556 557
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
558
  | Decl.InvalidIndDecl (_ls, pr) ->
559
      fprintf fmt "Ill-formed inductive clause %a"
560 561
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
562
      fprintf fmt "Inductive clause %a contains \
MARCHE Claude's avatar
MARCHE Claude committed
563
          a non strictly positive occurrence of symbol %a"
564
        print_pr pr print_ls ls1
565 566 567
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
568 569
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
570 571 572 573
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
574 575 576 577
  | 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
578 579 580 581 582 583 584
  | 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
585 586
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
587 588 589
  | _ -> raise exn
  end