pretty.ml 21.3 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
(*    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
27
open Decl
28
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
29
open Task
30

31
let debug_print_labels = Debug.register_flag "print_labels"
32
let debug_print_locs = Debug.register_flag "print_locs"
33

34
let iprinter,aprinter,tprinter,pprinter =
35
  let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
Andrei Paskevich's avatar
Andrei Paskevich committed
36
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
37
            "namespace"; "import"; "export"; "end";
Andrei Paskevich's avatar
Andrei Paskevich committed
38 39
            "forall"; "exists"; "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:lsanitize,
45
  create_ident_printer bl ~sanitizer:isanitize
46

47 48 49
let forget_tvs () =
  forget_all aprinter

50 51
let forget_all () =
  forget_all iprinter;
52
  forget_all aprinter;
53
  forget_all tprinter;
54
  forget_all pprinter
55

56 57 58 59 60 61 62 63 64 65 66 67 68 69
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
    Util.option_iter (fprintf fmt "@ %a" print_loc) id.id_loc

70 71
(* type variables always start with a quote *)
let print_tv fmt tv =
72
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
73 74 75

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
76
  let id = vs.vs_name in
77
  let sanitizer = String.uncapitalize in
78 79
  fprintf fmt "%s" (id_unique iprinter ~sanitizer id);
  print_ident_labels fmt id
80

81
let forget_var vs = forget_id iprinter vs.vs_name
82

83 84 85 86 87 88 89 90 91 92 93 94 95 96
(* 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 = "?"

97 98 99 100 101
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

102 103
(* theory names always start with an upper case letter *)
let print_th fmt th =
104 105
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
106

107 108
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
109

110 111 112 113
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
114
  | Some s -> fprintf fmt "(%s)" (escape_op s)
115
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
116 117 118

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

121
let print_pr fmt pr =
122
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
123 124 125

(** Types *)

126
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
127

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

let print_const fmt = function
139 140 141 142
  | 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
143 144 145 146 147 148 149
  | 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
150
    | Tyvar u when tv_equal u v -> true
151 152 153 154 155 156 157
    | _ -> 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
158
  option_apply true inspect fs.ls_value
159 160 161

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
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
183

184 185
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
186 187

let print_quant fmt = function
188 189
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
190

191 192 193
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
Andrei Paskevich's avatar
Andrei Paskevich committed
194 195
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
196 197
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
198

199
let prio_binop = function
200 201 202 203
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
204

205

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

and print_lterm pri fmt t =
209
  let print_tlab pri fmt t =
210
    if Debug.test_flag debug_print_labels && not (Slab.is_empty t.t_label)
211
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
212
      print_labels t.t_label (print_tnode 0) t
213 214
    else print_tnode pri fmt t in
  let print_tloc pri fmt t =
215
    if Debug.test_flag debug_print_locs && t.t_loc <> None
216
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
217 218 219
      (print_option print_loc) t.t_loc (print_tlab 0) t
    else print_tlab pri fmt t in
  print_tloc pri fmt t
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 ->
225 226
      fprintf fmt (protect_on (pri > 7) "%s%a")
        s (print_lterm 7) t1
227 228 229 230
  | Some s, [t1] ->
      fprintf fmt (protect_on (pri > 4) "%s %a")
        s (print_lterm 5) t1
  | Some s, [t1;t2] ->
231
      fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
232
        (print_lterm 5) t1 s (print_lterm 5) t2
233 234 235 236 237 238
  | _, [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
239
  | _, tl ->
240
      fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
241 242
        print_ls ls (print_list space (print_lterm 6)) tl

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

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

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

(** Declarations *)

299 300 301 302
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

303 304 305 306 307 308
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
309 310
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
    print_ident_labels cs.ls_name
311 312
    (print_list nothing print_pj)
    (List.fold_right2 add_pj pjl cs.ls_args [])
313

314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
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 ()
332

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

335 336 337
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
338

339 340 341 342 343 344 345
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 ()
346

347 348 349 350 351 352 353 354 355
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 ()
356

357
let print_ind fmt (pr,f) =
358
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
359
    print_pr pr print_ident_labels pr.pr_name print_term f
360

361 362 363 364 365
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

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

373 374 375 376 377 378 379
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

381
let print_prop_decl fmt (k,pr,f) =
382
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
383
    print_pr pr print_ident_labels pr.pr_name print_term f;
384 385
  forget_tvs ()

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

392
let print_decl fmt d = match d.d_node with
393 394 395
  | 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
396
  | Dlogic ll -> print_list_next newline print_logic_decl fmt ll
397
  | Dind (s, il) -> print_list_next newline (print_ind_decl s) fmt il
398 399
  | Dprop p   -> print_prop_decl fmt p

400 401
let print_next_data_decl  = print_data_decl false
let print_data_decl       = print_data_decl true
402 403
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
404 405
let print_next_ind_decl   = print_ind_decl Ind false
let print_ind_decl fmt s  = print_ind_decl s true fmt
406

407 408 409 410
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
411
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
412 413 414

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

416
let print_meta_arg_type fmt = function
417
  | MTty       -> fprintf fmt "[type]"
418
  | MTtysymbol -> fprintf fmt "[type symbol]"
Andrei Paskevich's avatar
Andrei Paskevich committed
419
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
420 421 422 423
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

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

432 433 434 435 436 437
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

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

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
458 459 460
  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
461

462
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
463
  forget_all ();
464 465
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
466

467 468
module NsTree = struct
  type t =
469
    | Namespace of string * namespace * known_map
470 471
    | Leaf      of string

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

  let decomp = function
492 493
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
494 495
end

496
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
497
  let module P = Print_tree.Make(NsTree) in
498
  fprintf fmt "@[<hov>%a@]@." P.print
499
    (NsTree.Namespace (name, th.th_export, th.th_known))
500

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