pretty.ml 21 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,aprinter,tprinter,pprinter =
34
  let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
Andrei Paskevich's avatar
Andrei Paskevich committed
35
            "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:lsanitize,
44
  create_ident_printer bl ~sanitizer:isanitize
45

46 47 48
let forget_tvs () =
  forget_all aprinter

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

55 56
(* type variables always start with a quote *)
let print_tv fmt tv =
57
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
58 59 60

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
61 62
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
63

64
let forget_var vs = forget_id iprinter vs.vs_name
65

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

80 81 82 83 84
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

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

90 91
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
92

93 94 95 96
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
97
  | Some s -> fprintf fmt "(%s)" (escape_op s)
98
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
99 100 101

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

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

(** Types *)

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

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

let print_const fmt = function
122 123 124 125
  | 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
126 127 128 129 130 131 132
  | 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
133
    | Tyvar u when tv_equal u v -> true
134 135 136 137 138 139 140
    | _ -> 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
141
  option_apply true inspect fs.ls_value
142 143 144

(** Patterns, terms, and formulas *)

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

167 168
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
169 170

let print_quant fmt = function
171 172
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
173

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

182
let prio_binop = function
183 184 185 186
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
187

188
let print_label fmt l =
Andrei Paskevich's avatar
Andrei Paskevich committed
189
  fprintf fmt "\"%s\"" l.lab_string
190

191 192 193 194
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
195
let print_ident_labels fmt id =
196
  if Debug.test_flag debug_print_labels && id.id_label <> [] then
197
    fprintf fmt "@ %a" (print_list space print_label) id.id_label;
198
  if Debug.test_flag debug_print_locs then
199
    Util.option_iter (fprintf fmt "@ %a" print_loc) id.id_loc
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 && t.t_label <> []
206
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
207 208 209
      (print_list space print_label) t.t_label (print_tnode 0) t
    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 = List.mem Term.asym_label t.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
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
302 303
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
    print_ident_labels cs.ls_name
304
    (print_list nothing print_ty_arg) tl
305

306
let print_type_decl fst fmt (ts,def) = match def with
307 308
  | Tabstract -> begin match ts.ts_def with
      | None ->
309
          fprintf fmt "@[<hov 2>%s %a%a%a@]"
310
            (if fst then "type" else "with") print_ts ts
311
            print_ident_labels ts.ts_name
312
            (print_list nothing print_tv_arg) ts.ts_args
313
      | Some ty ->
314
          fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]"
315
            (if fst then "type" else "with") print_ts ts
316
            print_ident_labels ts.ts_name
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
      fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]"
322
        (if fst then "type" else "with") print_ts ts
323
        print_ident_labels ts.ts_name
324
        (print_list nothing print_tv_arg) ts.ts_args
325
        (print_list newline (print_constr ty)) csl
326

327 328
let print_type_decl first fmt d =
  print_type_decl first fmt d; forget_tvs ()
329

330
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
331

332 333 334
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
335

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

352 353
let print_logic_decl first fmt d =
  print_logic_decl first fmt d; forget_tvs ()
354

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

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

let print_ind_decl first fmt d =
  print_ind_decl first fmt d; forget_tvs ()
368

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

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

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

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

388
let print_decl fmt d = match d.d_node with
389 390 391
  | 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
392 393
  | Dprop p   -> print_prop_decl fmt p

394 395 396 397 398 399 400
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

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

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

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

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

426 427 428 429 430 431
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

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

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
452 453 454
  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
455

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

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

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

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

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

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