pretty.ml 13 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
43
44
45
  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,
  create_ident_printer bl ~sanitizer:lsanitize,
  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
  let sanitize n = "'" ^ n in
65
  let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
66
67
  fprintf fmt "%s" n

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

78
let forget_var vs = forget_id iprinter vs.vs_name
79

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

86
let print_ts fmt ts =
87
  Hid.replace thash ts.ts_name ts;
88
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
89

90
let print_ls fmt ls =
91
  Hid.replace lhash ls.ls_name ls;
92
93
94
95
96
  let n = if ls.ls_constr
    then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
    else id_unique lprinter ls.ls_name
  in
  fprintf fmt "%s" n
97

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

(** Types *)

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

106
107
108
109
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
110
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
111
      (print_list ns_comma print_ty) l print_ts ts
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138

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
    | Tyvar u when u == v -> true
    | _ -> 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

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

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

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

163
164
165
166
167
168
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
169

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

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

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

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

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

247
and print_fbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
248
249
250
  let pl,svs,f = f_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_fmla f;
251
  Svs.iter forget_var svs
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
let print_constr fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
    (print_paren_l print_ty) cs.ls_args
264

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

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

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

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

288
289
290
291
292
293
294
295
296
297
298
299
300
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 ()
301

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

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

let print_pkind fmt = function
  | Paxiom -> fprintf fmt "axiom"
  | Plemma -> fprintf fmt "lemma"
  | Pgoal  -> fprintf fmt "goal"

316
317
318
319
320
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 ()

321
322
323
324
325
326
327
328
329
330
let print_inst fmt (id1,id2) =
  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)
331
  else
332
    fprintf fmt "ident %s = %s" id1.id_long id2.id_long
333

334
let print_decl fmt d = match d.d_node with
335
336
337
  | 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
338
  | Dprop p   -> print_prop_decl fmt p
Andrei Paskevich's avatar
Andrei Paskevich committed
339
340
341
342
343

let print_tdecl fmt = function
  | Decl d ->
      print_decl fmt d
  | Use th ->
344
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
345
346
347
  | Clone (th,inst) ->
      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
        print_th th (print_list comma print_inst) inst
348

349
let print_decls fmt dl =
350
  fprintf fmt "@[<hov>%a@]@." (print_list newline2 print_decl) dl
351

Andrei Paskevich's avatar
Andrei Paskevich committed
352
let print_task fmt task = print_decls fmt (task_decls task)
353

354
let print_theory fmt th =
355
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
Andrei Paskevich's avatar
Andrei Paskevich committed
356
    print_th th (print_list newline2 print_tdecl) th.th_decls
357

Andrei Paskevich's avatar
Andrei Paskevich committed
358
let print_named_task fmt name task =
359
  fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
Andrei Paskevich's avatar
Andrei Paskevich committed
360
    name print_task task
361

362
363
364
365
366
367
368
369
370
module NsTree = struct
  type t =
    | Namespace of string * namespace
    | Leaf      of string

  let contents ns =
    let add_ns s ns acc = Namespace (s, ns) :: acc in
    let add_s k s _ acc = Leaf (k ^ s) :: acc in
    let acc = Mnm.fold add_ns           ns.ns_ns []  in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
371
    let acc = Mnm.fold (add_s "prop ")  ns.ns_pr acc in
372
    let acc = Mnm.fold (add_s "logic ") ns.ns_ls acc in
Andrei Paskevich's avatar
minor    
Andrei Paskevich committed
373
    let acc = Mnm.fold (add_s "type ")  ns.ns_ts acc in acc
374
375
376
377
378
379
380
381

  let decomp = function
    | Namespace (s,ns) -> s, contents ns
    | Leaf s           -> s, []
end

let print_namespace fmt name ns =
  let module P = Prtree.Make(NsTree) in
382
  fprintf fmt "@[<hov>%a@]@." P.print (NsTree.Namespace (name, ns))
383