pretty.ml 17.2 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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 iprinter,tprinter,lprinter,pprinter =
31
32
  let bl = ["theory"; "type"; "logic"; "inductive"; "meta";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop";
33
34
35
36
37
            "namespace"; "import"; "export"; "end";
            "forall"; "exists"; "and"; "or"; "not";
            "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ]
  in
38
39
40
41
42
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
43
  create_ident_printer bl ~sanitizer:lsanitize,
44
45
46
47
48
49
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
50
  forget_all pprinter
51

52
let tv_set = ref Sid.empty
53

54
55
(* type variables always start with a quote *)
let print_tv fmt tv =
56
  tv_set := Sid.add tv.tv_name !tv_set;
57
58
  let sanitizer n = "'" ^ n in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
59

60
61
62
63
64
65
let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

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

69
let forget_var vs = forget_id iprinter vs.vs_name
70

71
72
(* theory names always start with an upper case letter *)
let print_th fmt th =
73
74
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
75

76
77
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
78

79
let print_ls fmt ls =
80
81
82
83
84
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
85

86
let print_pr fmt pr =
87
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
88
89
90

(** Types *)

91
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
92

93
let rec print_ty_node inn fmt ty = match ty.ty_node with
94
95
  | Tyvar v -> print_tv fmt v
  | Tyapp (ts, []) -> print_ts fmt ts
96
97
98
99
  | 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
100
101
102
103
104
105
106
107
108
109

let print_const fmt = function
  | ConstInt s -> fprintf fmt "%s" s
  | 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
110
    | Tyvar u when tv_equal u v -> true
111
112
113
114
115
116
117
118
119
120
121
    | _ -> 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
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

122
let rec print_pat_node inn fmt p = match p.pat_node with
123
  | Pwild -> fprintf fmt "_"
124
  | Pvar v -> print_vs fmt v
125
126
127
128
129
130
131
  | Pas (p,v) -> fprintf fmt (protect_on inn "%a as %a")
      (print_pat_node false) p print_vs v
  | Papp (cs,[]) -> print_cs fmt cs
  | Papp (cs,pl) -> fprintf fmt (protect_on inn "%a@ %a")
      print_cs cs (print_list space (print_pat_node true)) pl

let print_pat = print_pat_node false
132

133
134
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
135
136
137
138
139
140
141
142
143
144
145

let print_quant fmt = function
  | Fforall -> fprintf fmt "forall"
  | Fexists -> fprintf fmt "exists"

let print_binop fmt = function
  | Fand -> fprintf fmt "and"
  | For -> fprintf fmt "or"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

146
147
148
149
150
let prio_binop = function
  | Fand -> 3
  | For -> 2
  | Fimplies -> 1
  | Fiff -> 1
151

152
let print_label fmt l = fprintf fmt "\"%s\"" l
153

154
155
let rec print_term fmt t = print_lterm 0 fmt t
and     print_fmla fmt f = print_lfmla 0 fmt f
156

157
158
159
160
and print_lterm pri fmt t = match t.t_label with
  | [] -> print_tnode pri fmt t
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_tnode 0) t
161

162
163
164
165
and print_lfmla pri fmt f = match f.f_label with
  | [] -> print_fnode pri fmt f
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_fnode 0) f
166

167
and print_tnode pri fmt t = match t.t_node with
168
169
170
  | Tbvar _ ->
      assert false
  | Tvar v ->
171
      print_vs fmt v
172
173
  | Tconst c ->
      print_const fmt c
174
175
176
177
178
  | Tapp (fs, []) when unambig_fs fs ->
      print_ls fmt fs
  | Tapp (fs, []) ->
      fprintf fmt (protect_on (pri > 0) "%a:%a")
        print_ls fs print_ty t.t_ty
179
  | Tapp (fs, tl) when unambig_fs fs ->
180
181
      fprintf fmt (protect_on (pri > 4) "%a@ %a")
        print_ls fs (print_list space (print_lterm 5)) tl
182
  | Tapp (fs, tl) ->
183
184
185
      fprintf fmt (protect_on (pri > 0) "%a@ %a:%a")
        print_ls fs (print_list space (print_lterm 5)) tl
          print_ty t.t_ty
186
  | Tif (f,t1,t2) ->
187
188
      fprintf fmt (protect_on (pri > 0) "if %a@ then %a@ else %a")
        print_fmla f print_term t1 print_term t2
189
190
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
191
192
      fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
        print_vs v (print_lterm 4) t1 print_term t2;
193
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
194
  | Tcase (tl,bl) ->
195
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
196
197
        (print_list comma print_term) tl
        (print_list newline print_tbranch) bl
198
199
  | Teps fb ->
      let v,f = f_open_bound fb in
200
201
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
        print_vsty v print_fmla f;
202
      forget_var v
203

204
and print_fnode pri fmt f = match f.f_node with
205
  | Fapp (ps,[t1;t2]) when ps = ps_equ ->
206
207
208
209
      fprintf fmt (protect_on (pri > 4) "%a =@ %a")
        (print_lterm 4) t1 (print_lterm 4) t2
  | Fapp (ps,[]) ->
      print_ls fmt ps
210
  | Fapp (ps,tl) ->
211
212
      fprintf fmt (protect_on (pri > 4) "%a@ %a")
        print_ls ps (print_list space (print_lterm 5)) tl
213
214
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
215
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
216
217
        (print_list comma print_vsty) vl print_tl tl print_fmla f;
      List.iter forget_var vl
218
219
220
221
222
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
223
224
225
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
        (print_lfmla (p + 1)) f1 print_binop b (print_lfmla p) f2
226
  | Fnot f ->
227
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
228
  | Fif (f1,f2,f3) ->
229
230
      fprintf fmt (protect_on (pri > 0) "if %a@ then %a@ else %a")
        print_fmla f1 print_fmla f2 print_fmla f3
231
232
  | Flet (t,f) ->
      let v,f = f_open_bound f in
233
234
      fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
        print_vs v (print_lterm 4) t print_fmla f;
235
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
236
237
238
  | Fcase (tl,bl) ->
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
        (print_list comma print_term) tl
239
        (print_list newline print_fbranch) bl
240

241
and print_tbranch fmt br =
242
  let pl,t = t_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
243
244
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_term t;
245
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
246

247
and print_fbranch fmt br =
248
  let pl,f = f_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
249
250
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_fmla f;
251
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
252

253
and print_tl fmt tl =
254
  if tl = [] then () else fprintf fmt "@ [%a]"
255
    (print_list alt (print_list comma print_expr)) tl
256

257
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
258
259
260

(** Declarations *)

261
262
263
264
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

265
let print_constr fmt cs =
266
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
267
    (print_list nothing print_ty_arg) cs.ls_args
268

269
let print_type_decl fmt (ts,def) = match def with
270
271
  | Tabstract -> begin match ts.ts_def with
      | None ->
272
273
          fprintf fmt "@[<hov 2>type %a%a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args
274
      | Some ty ->
275
276
          fprintf fmt "@[<hov 2>type %a%a =@ %a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
277
278
      end
  | Talgebraic csl ->
279
280
      fprintf fmt "@[<hov 2>type %a%a =@\n@[<hov>%a@]@]"
        print_ts ts (print_list nothing print_tv_arg) ts.ts_args
281
        (print_list newline print_constr) csl
282

283
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
284

285
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
286

287
288
289
290
let print_logic_decl fmt (ls,ld) = match ld with
  | Some ld ->
      let vl,e = open_ls_defn ld in
      fprintf fmt "@[<hov 2>logic %a%a%a =@ %a@]"
291
        print_ls ls (print_list nothing print_vs_arg) vl
292
293
294
295
        (print_option print_ls_type) ls.ls_value print_expr e;
      List.iter forget_var vl
  | None ->
      fprintf fmt "@[<hov 2>logic %a%a%a@]"
296
        print_ls ls (print_list nothing print_ty_arg) ls.ls_args
297
298
299
        (print_option print_ls_type) ls.ls_value

let print_logic_decl fmt d = print_logic_decl fmt d; forget_tvs ()
300

301
302
let print_ind fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr print_fmla f
303

304
let print_ind_decl fmt (ps,bl) =
305
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
306
    print_ls ps (print_list nothing print_ty_arg) ps.ls_args
307
    (print_list newline print_ind) bl;
308
  forget_tvs ()
309

310
311
312
313
314
315
316
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

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

318
319
320
321
322
let print_prop_decl fmt (k,pr,f) =
  fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
    print_pr pr print_fmla f;
  forget_tvs ()

323
324
325
326
327
328
let print_decl fmt d = match d.d_node with
  | Dtype tl  -> print_list newline print_type_decl fmt tl
  | Dlogic ll -> print_list newline print_logic_decl fmt ll
  | Dind il   -> print_list newline print_ind_decl fmt il
  | Dprop p   -> print_prop_decl fmt p

329
330
331
332
333
334
335
336
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) =
  fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2

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

338
let print_meta_arg fmt = function
339
340
341
342
343
  | MAts ts -> fprintf fmt "type %a" print_ts ts
  | MAls ls -> fprintf fmt "logic %a" print_ls ls
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
344
345
346

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
347
      print_decl fmt d
348
  | Use th ->
349
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
350
351
352
  | Clone (th,tm,lm,pm)
    when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm ->
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
353
354
355
356
  | Clone (th,tm,lm,pm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) tm [] in
      let lm = Mls.fold (fun x y a -> (x,y)::a) lm [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) pm [] in
357
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
358
359
360
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
361
362
  | Meta (t,al) ->
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
363
        t (print_list comma print_meta_arg) al
364
365
366
367

let print_theory fmt th =
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
    print_th th (print_list newline2 print_tdecl) th.th_decls
368

369
let print_task fmt task =
370
371
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
372

373
374
module NsTree = struct
  type t =
375
    | Namespace of string * namespace * known_map
376
377
    | Leaf      of string

378
379
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
380
    let add_pr s p  acc =
381
382
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
383
384
385
386
387
388
389
390
391
392
393
394
395
396
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
      if s = "infix <>" && ls_equal ls ps_neq then acc else
        Leaf ("logic " ^ s) :: acc
    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
    let acc = Mnm.fold add_ns ns.ns_ns []  in
    let acc = Mnm.fold add_pr ns.ns_pr acc in
    let acc = Mnm.fold add_ls ns.ns_ls acc in
    let acc = Mnm.fold add_ts ns.ns_ts acc in acc
397
398

  let decomp = function
399
400
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
401
402
end

403
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
404
  let module P = Print_tree.Make(NsTree) in
405
  fprintf fmt "@[<hov>%a@]@." P.print
406
    (NsTree.Namespace (name, th.th_export, th.th_known))
407

408
409
410
411
412
413
414
415
416
417
418
419
(* 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 ->
420
421
422
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
  | 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
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
  | 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
  | Term.NoMatch ->
      fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
  | 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
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
        print_pr pr
  | Decl.TooSpecificIndDecl (_ls, pr, t) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          has too type-specific conclusion %a"
        print_pr pr print_term t
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          contains a negative occurrence of dependent symbol %a"
        print_pr pr print_ls ls1
  | Decl.BadLogicDecl (id1,id2) ->
      fprintf fmt "Ill-formed definition: idents %s and %s are different"
        id1.id_string id2.id_string
459
460
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
461
462
463
464
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
465
466
467
468
  | 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
469
470
471
472
473
474
475
476
477
478
479
480
481
482
  | 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
  | Decl.NonExhaustiveExpr (pl, e) ->
      fprintf fmt
        "Non-exhaustive pattern list:@\n@[<hov 2>%a@]@\nin expression %a"
        (print_list newline print_pat) pl print_expr e
  | _ -> raise exn
  end