pretty.ml 21.4 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
(* TODO: Is it not an example of register_stop_flag? *)
32
let debug_print_labels = Debug.register_flag "print_labels"
33
34
  ~desc:"Control if ident labels are printed."

35
let debug_print_locs = Debug.register_flag "print_locs"
36
  ~desc:"Control if ident location are printed."
37

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

51
52
53
let forget_tvs () =
  forget_all aprinter

54
55
let forget_all () =
  forget_all iprinter;
56
  forget_all aprinter;
57
  forget_all tprinter;
58
  forget_all pprinter
59

60
61
62
63
64
65
66
67
68
69
70
71
72
73
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

74
75
(* type variables always start with a quote *)
let print_tv fmt tv =
76
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
77
78
79

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

85
let forget_var vs = forget_id iprinter vs.vs_name
86

87
88
89
90
91
92
93
94
95
96
97
98
99
100
(* 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 = "?"

101
102
103
104
105
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

106
107
(* theory names always start with an upper case letter *)
let print_th fmt th =
108
109
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
110

111
112
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
113

114
115
116
117
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
118
  | Some s -> fprintf fmt "(%s)" (escape_op s)
119
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
120
121
122

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

125
let print_pr fmt pr =
126
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
127
128
129

(** Types *)

130
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
131

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

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

(** Patterns, terms, and formulas *)

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

188
189
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
190
191

let print_quant fmt = function
192
193
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
194

195
196
197
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
Andrei Paskevich's avatar
Andrei Paskevich committed
198
199
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
200
201
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
202

203
let prio_binop = function
204
205
206
207
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
208

209

MARCHE Claude's avatar
MARCHE Claude committed
210
211
212
let rec print_term fmt t = print_lterm 0 fmt t

and print_lterm pri fmt t =
213
  let print_tlab pri fmt t =
214
    if Debug.test_flag debug_print_labels && not (Slab.is_empty t.t_label)
215
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
216
      print_labels t.t_label (print_tnode 0) t
217
218
    else print_tnode pri fmt t in
  let print_tloc pri fmt t =
219
    if Debug.test_flag debug_print_locs && t.t_loc <> None
220
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
221
222
223
      (print_option print_loc) t.t_loc (print_tlab 0) t
    else print_tlab pri fmt t in
  print_tloc pri fmt t
224

225
226
227
228
and print_app pri ls fmt tl = match extract_op ls, tl with
  | _, [] ->
      print_ls fmt ls
  | Some s, [t1] when tight_op s ->
229
230
      fprintf fmt (protect_on (pri > 7) "%s%a")
        s (print_lterm 7) t1
231
232
233
234
  | Some s, [t1] ->
      fprintf fmt (protect_on (pri > 4) "%s %a")
        s (print_lterm 5) t1
  | Some s, [t1;t2] ->
235
      fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
236
        (print_lterm 5) t1 s (print_lterm 5) t2
237
238
239
240
241
242
  | _, [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
243
  | _, tl ->
244
      fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
245
246
        print_ls ls (print_list space (print_lterm 6)) tl

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

292
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
293
294
295
  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
296

297
and print_tl fmt tl =
298
  if tl = [] then () else fprintf fmt "@ [%a]"
299
    (print_list alt (print_list comma print_term)) tl
300
301
302

(** Declarations *)

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

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

318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
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 ()
336

337
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
338

339
340
341
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
342

343
344
345
346
347
348
349
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 ()
350

351
352
353
354
355
356
357
358
359
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 ()
360

361
let print_ind fmt (pr,f) =
362
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
363
    print_pr pr print_ident_labels pr.pr_name print_term f
364

365
366
367
368
369
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

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

377
378
379
380
381
382
383
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

385
let print_prop_decl fmt (k,pr,f) =
386
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
387
    print_pr pr print_ident_labels pr.pr_name print_term f;
388
389
  forget_tvs ()

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

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

404
405
let print_next_data_decl  = print_data_decl false
let print_data_decl       = print_data_decl true
406
407
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
408
409
let print_next_ind_decl   = print_ind_decl Ind false
let print_ind_decl fmt s  = print_ind_decl s true fmt
410

411
412
413
414
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
415
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
416
417
418

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

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

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

436
437
438
439
440
441
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

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

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
462
463
464
  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
465

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

471
472
module NsTree = struct
  type t =
473
    | Namespace of string * namespace * known_map
474
475
    | Leaf      of string

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

  let decomp = function
496
497
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
498
499
end

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

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