pretty.ml 21.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
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"
Andrei Paskevich's avatar
Andrei Paskevich committed
24
  ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
Andrei Paskevich's avatar
Andrei Paskevich committed
25

26
let debug_print_locs = Debug.register_info_flag "print_locs"
Andrei Paskevich's avatar
Andrei Paskevich committed
27
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
28

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

42
43
44
let forget_tvs () =
  forget_all aprinter

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

51
52
53
54
55
56
57
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

Andrei Paskevich's avatar
Andrei Paskevich committed
58
let print_id_labels fmt id =
59
60
61
62
  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
63
    Opt.iter (fprintf fmt "@ %a" print_loc) id.id_loc
64

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

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
71
  let sanitizer = String.uncapitalize in
72
  pp_print_string fmt (id_unique iprinter ~sanitizer vs.vs_name)
73

74
let forget_var vs = forget_id iprinter vs.vs_name
75

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

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

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

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

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

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

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

(** Types *)

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

121
let rec print_ty_node pri fmt ty = match ty.ty_node with
122
  | Tyvar v -> print_tv fmt v
123
124
125
126
127
  | Tyapp (ts, [t1;t2]) when ts_equal ts Ty.ts_func ->
      fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
        (print_ty_node 1) t1 (print_ty_node 0) t2
  | Tyapp (ts, tl) when is_ts_tuple ts ->
      fprintf fmt "(%a)" (print_list comma (print_ty_node 0)) tl
128
  | Tyapp (ts, []) -> print_ts fmt ts
129
130
  | Tyapp (ts, tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
      print_ts ts (print_list space (print_ty_node 2)) tl
131

132
let print_ty fmt ty = print_ty_node 0 fmt ty
133
134

let print_const fmt = function
135
136
137
138
139
140
141
142
  | 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
143
144
145
146

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

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
159
160
161
162
let rec print_pat_node pri fmt p = match p.pat_node with
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
163
      print_vs fmt v; print_id_labels fmt v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
164
  | Pas (p, v) ->
165
166
      fprintf fmt (protect_on (pri > 1) "%a as %a%a")
        (print_pat_node 1) p print_vs v print_id_labels v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
167
168
169
170
171
172
173
174
175
176
177
178
179
  | 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
180

181
let print_vsty fmt v =
182
183
  fprintf fmt "%a%a:@,%a" print_vs v
    print_id_labels v.vs_name print_ty v.vs_ty
184
185

let print_quant fmt = function
186
187
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
188

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

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

203

MARCHE Claude's avatar
MARCHE Claude committed
204
205
206
let rec print_term fmt t = print_lterm 0 fmt t

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

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

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

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

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

(** Declarations *)

304
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
305
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node 2) ty
306
307
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs

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

319
320
321
322
323
324
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@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
325
    print_ts ts print_id_labels ts.ts_name
326
327
328
329
330
331
332
    (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
Andrei Paskevich's avatar
Andrei Paskevich committed
333
    print_id_labels ts.ts_name
334
335
336
    (print_list nothing print_tv_arg) ts.ts_args
    (print_list newline print_constr) csl;
  forget_tvs ()
337

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

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

344
345
346
let print_param_decl fmt ls =
  fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
    (ls_kind ls) print_ls ls
Andrei Paskevich's avatar
Andrei Paskevich committed
347
    print_id_labels ls.ls_name
348
349
350
    (print_list nothing print_ty_arg) ls.ls_args
    (print_option print_ls_type) ls.ls_value;
  forget_tvs ()
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
Andrei Paskevich's avatar
Andrei Paskevich committed
356
    print_id_labels ls.ls_name
357
358
359
360
    (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 ()
361

362
let print_ind fmt (pr,f) =
363
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
364
    print_pr pr print_id_labels pr.pr_name print_term f
365

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

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

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

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

386
let print_prop_decl fmt (k,pr,f) =
387
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
Andrei Paskevich's avatar
Andrei Paskevich committed
388
    print_pr pr print_id_labels pr.pr_name print_term f;
389
390
  forget_tvs ()

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

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

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

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

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

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

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

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

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

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
463
  fprintf fmt "@[<hov 2>theory %a%a@\n%a@]@\nend@."
Andrei Paskevich's avatar
Andrei Paskevich committed
464
    print_th th print_id_labels th.th_name
Andrei Paskevich's avatar
Andrei Paskevich committed
465
    (print_list newline2 print_tdecl) th.th_decls
466

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

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

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

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

501
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
502
  let module P = Print_tree.Make(NsTree) in
503
  fprintf fmt "@[<hov>%a@]@." P.print
504
    (NsTree.Namespace (name, th.th_export, th.th_known))
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
513
514
  | Ty.BadTypeArity ({ts_args = []} as ts, _) ->
      fprintf fmt "Type symbol %a expects no arguments" print_ts ts
515
  | Ty.BadTypeArity (ts, app_arg) ->
516
517
518
      let i = List.length ts.ts_args in
      fprintf fmt "Type symbol %a expects %i argument%s but is applied to %i"
        print_ts ts i (if i = 1 then "" else "s") app_arg
519
  | Ty.DuplicateTypeVar tv ->
520
521
522
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
523
524
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
525
526
527
  | Term.BadArity ({ls_args = []} as ls, _) ->
      fprintf fmt "%s %a expects no arguments"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
528
  | Term.BadArity (ls, app_arg) ->
529
530
      let i = List.length ls.ls_args in
      fprintf fmt "%s %a expects %i argument%s but is applied to %i"
531
        (if ls.ls_value = None then "Predicate" else "Function")
532
        print_ls ls i (if i = 1 then "" else "s") app_arg
533
534
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
535
536
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
537
538
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
539
540
541
542
  | 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
543
  | Term.ConstructorExpected ls ->
544
545
      fprintf fmt "%s %a is not a constructor"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
546
  | Term.TermExpected t ->
547
      fprintf fmt "Not a term: %a" print_term t
548
549
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
550
  | Pattern.ConstructorExpected (ls,ty) ->
551
552
553
      fprintf fmt "%s %a is not a constructor of type %a"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
        print_ty ty
554
  | Pattern.NonExhaustive pl ->
555
556
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
        print_pat (List.hd pl)
557
  | Decl.BadConstructor ls ->
558
      fprintf fmt "Bad constructor: %a" print_ls ls
559
560
  | Decl.BadRecordField ls ->
      fprintf fmt "Not a record field: %a" print_ls ls
561
562
563
564
  | 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
565
566
567
568
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
569
570
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
571
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
572
      fprintf fmt "Constructor %a \
573
574
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
575
  | Decl.InvalidIndDecl (_ls, pr) ->
576
      fprintf fmt "Ill-formed inductive clause %a"
577
578
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
579
      fprintf fmt "Inductive clause %a contains \
MARCHE Claude's avatar
MARCHE Claude committed
580
          a non strictly positive occurrence of symbol %a"
581
        print_pr pr print_ls ls1
582
583
584
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
585
586
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
587
588
589
590
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
591
592
593
594
  | 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
595
596
597
598
599
600
601
  | 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
602
603
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
604
605
  | _ -> raise exn
  end