pretty.ml 17.4 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
33
34
35
36
37
  let bl = ["theory"; "type"; "logic"; "inductive";
            "axiom"; "lemma"; "goal"; "use"; "clone";
            "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:isanitize,
44
45
  create_ident_printer bl ~sanitizer:usanitize

46
47
48
49
let thash = Hid.create 63
let lhash = Hid.create 63
let phash = Hid.create 63

50
51
52
53
let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
54
55
56
57
  forget_all pprinter;
  Hid.clear thash;
  Hid.clear lhash;
  Hid.clear phash
58

59
let tv_set = ref Sid.empty
60

61
62
(* type variables always start with a quote *)
let print_tv fmt tv =
63
  tv_set := Sid.add tv.tv_name !tv_set;
64
65
  let sanitizer n = "'" ^ n in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
66

67
68
69
70
71
72
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 =
73
74
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
75

76
let forget_var vs = forget_id iprinter vs.vs_name
77

78
79
(* theory names always start with an upper case letter *)
let print_th fmt th =
80
81
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
82

83
let print_ts fmt ts =
84
  Hid.replace thash ts.ts_name ts;
85
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
86

87
let print_ls fmt ls =
88
  Hid.replace lhash ls.ls_name ls;
89
90
91
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
92
  Hid.replace lhash ls.ls_name ls;
93
94
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
95

96
let print_pr fmt pr =
97
  Hid.replace phash pr.pr_name pr;
98
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
99
100
101
102
103

(** Types *)

let rec ns_comma fmt () = fprintf fmt ",@,"

104
105
106
107
let rec print_ty fmt ty = match ty.ty_node with
  | Tyvar v -> print_tv fmt v
  | Tyapp (ts, []) -> print_ts fmt ts
  | Tyapp (ts, [t]) -> fprintf fmt "%a@ %a" print_ty t print_ts ts
108
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
109
      (print_list ns_comma print_ty) l print_ts ts
110
111
112
113
114
115
116
117
118
119

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
120
    | Tyvar u when tv_equal u v -> true
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
    | _ -> 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 *)

let lparen_l fmt () = fprintf fmt "@ ("
let lparen_r fmt () = fprintf fmt "(@,"
let print_paren_l fmt x = print_list_delim lparen_l rparen comma fmt x
let print_paren_r fmt x = print_list_delim lparen_r rparen comma fmt x

137
let rec print_pat fmt p = match p.pat_node with
138
  | Pwild -> fprintf fmt "_"
139
140
  | Pvar v -> print_vs fmt v
  | Pas (p,v) -> fprintf fmt "%a as %a" print_pat p print_vs v
141
  | Papp (cs,pl) -> fprintf fmt "%a%a"
142
      print_cs cs (print_paren_r print_pat) pl
143

144
145
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160

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 "<->"

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

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

161
162
163
164
165
166
let rec print_term fmt t = print_lrterm false false fmt t
and     print_fmla fmt f = print_lrfmla false false fmt f
and print_opl_term fmt t = print_lrterm true  false fmt t
and print_opl_fmla fmt f = print_lrfmla true  false fmt f
and print_opr_term fmt t = print_lrterm false true  fmt t
and print_opr_fmla fmt f = print_lrfmla false true  fmt f
167

168
169
and print_lrterm opl opr fmt t = match t.t_label with
  | [] -> print_tnode opl opr fmt t
170
  | ll -> fprintf fmt "(%a %a)"
171
      (print_list space print_label) ll (print_tnode false false) t
172

173
174
and print_lrfmla opl opr fmt f = match f.f_label with
  | [] -> print_fnode opl opr fmt f
175
  | ll -> fprintf fmt "(%a %a)"
176
      (print_list space print_label) ll (print_fnode false false) f
177

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

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

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

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

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

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

(** Declarations *)

262
let print_constr fmt cs =
263
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
264
    (print_paren_l print_ty) cs.ls_args
265

266
let print_ty_args fmt = function
267
  | [] -> ()
268
269
  | [tv] -> fprintf fmt " %a" print_tv tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l
270

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

285
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
286

287
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
288

289
290
291
292
293
294
295
296
297
298
299
300
301
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@]"
        print_ls ls (print_paren_l print_vsty) vl
        (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@]"
        print_ls ls (print_paren_l print_ty) ls.ls_args
        (print_option print_ls_type) ls.ls_value

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

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

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

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

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

320
321
322
323
324
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 ()

325
326
327
328
329
330
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

331
let print_inst fmt (id1,id2) =
332
333
334
335
336
337
338
339
340
341
342
  if Hid.mem thash id2 then
    let n = id_unique tprinter id1 in
    fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
  else if Hid.mem lhash id2 then
    let n = id_unique lprinter id1 in
    fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
  else if Hid.mem phash id2 then
    let n = id_unique pprinter id1 in
    fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
  else
    fprintf fmt "ident %s = %s" id1.id_string id2.id_string
343

344
let print_meta_arg fmt = function
345
346
347
348
349
350
351
352
353
  | MARid id ->
      if Hid.mem thash id then
        fprintf fmt "type %a" print_ts (Hid.find thash id)
      else if Hid.mem lhash id then
        fprintf fmt "logic %a" print_ls (Hid.find lhash id)
      else if Hid.mem phash id then
        fprintf fmt "prop %a" print_pr (Hid.find phash id)
      else
        fprintf fmt "ident %s" id.id_string
354
355
356
357
358
  | MARstr s -> fprintf fmt "\"%s\"" s
  | MARint i -> fprintf fmt "%d" i

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
359
      print_decl fmt d
360
  | Use th ->
361
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
362
363
  | Clone (th,inst) ->
      let inst = Mid.fold (fun x y a -> (x,y)::a) inst [] in
364
365
      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
        print_th th (print_list comma print_inst) inst
366
367
368
369
370
371
372
  | Meta (t,al) ->
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
        t (print_list space print_meta_arg) al

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
373

374
375
376
let print_task fmt task =
  fprintf fmt "@[<hov>%a@]@."
    (print_list newline2 print_decl) (task_decls task)
377

378
379
let print_named_task fmt name task =
  fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
380
    name (print_list newline2 print_tdecl) (task_tdecls task)
381

382
383
module NsTree = struct
  type t =
384
    | Namespace of string * namespace * known_map
385
386
    | Leaf      of string

387
388
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
389
    let add_pr s p  acc = 
390
391
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
392
393
394
395
396
397
398
399
400
401
402
403
404
405
    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
406
407

  let decomp = function
408
409
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
410
411
end

412
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
413
  let module P = Print_tree.Make(NsTree) in
414
  fprintf fmt "@[<hov>%a@]@." P.print 
415
    (NsTree.Namespace (name, th.th_export, th.th_known))
416

417
418
419
420
421
422
423
424
425
426
427
428
(* 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 ->
429
430
431
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
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
459
460
461
462
463
464
465
466
467
  | 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
468
469
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
470
471
472
473
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
474
475
476
477
  | 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
478
479
480
481
482
483
484
485
486
487
488
489
490
491
  | 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