pretty.ml 13.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
26
27
(**************************************************************************)
(*                                                                        *)
(*  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
open Theory

28
let printer () =
29
30
31
32
33
34
35
36
  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
  let sanitize = sanitizer char_to_alpha char_to_alnumus in
37
  create_ident_printer bl ~sanitizer:sanitize
38

39
40
41
42
let printer_debug = printer ()

let print_id ?(printer=printer_debug) fmt id = 
  Format.fprintf fmt "%s" (id_unique printer id)
43
44

(* some idents must be put in upper case *)
45
let print_uc ?(printer=printer_debug) fmt id =
46
47
48
49
50
  let sanitize = String.capitalize in
  let n = id_unique printer ~sanitizer:sanitize id in
  fprintf fmt "%s" n

(* and some in lower *)
51
let print_lc ?(printer=printer_debug) fmt id =
52
53
54
55
56
57
  let sanitize = String.uncapitalize in
  let n = id_unique printer ~sanitizer:sanitize id in
  fprintf fmt "%s" n

let tv_set = ref Sid.empty

58
let forget_tvs ?(printer=printer_debug) () =
59
60
61
62
  Sid.iter (forget_id printer) !tv_set;
  tv_set := Sid.empty

(* type variables always start with a quote *)
63
let print_tv ?(printer=printer_debug) fmt v =
64
65
66
67
68
  tv_set := Sid.add v !tv_set;
  let sanitize n = String.concat "" ["'"; n] in
  let n = id_unique printer ~sanitizer:sanitize v in
  fprintf fmt "%s" n

69
70
let print_ts ?printer fmt ts = print_lc ?printer fmt ts.ts_name
let print_vs ?printer fmt vs = print_lc ?printer fmt vs.vs_name
71

72
73
74
let print_ls ?printer fmt ls =
  if ls.ls_constr then print_uc ?printer fmt ls.ls_name
                  else print_lc ?printer fmt ls.ls_name
75

76
let forget_var ?(printer=printer_debug) v = forget_id printer v.vs_name
77
78
79
80
81

(** Types *)

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

82
83
84
85
let rec print_ty ?printer fmt ty = match ty.ty_node with
  | Tyvar v -> print_tv ?printer fmt v
  | Tyapp (ts, []) -> print_ts ?printer fmt ts
  | Tyapp (ts, [t]) -> fprintf fmt "%a@ %a" (print_ty ?printer) t (print_ts ?printer) ts
86
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
87
      (print_list ns_comma (print_ty ?printer)) l (print_ts ?printer) ts
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

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

115
let rec print_pat ?printer fmt p = match p.pat_node with
116
  | Pwild -> fprintf fmt "_"
117
118
  | Pvar v -> print_vs ?printer fmt v
  | Pas (p,v) -> fprintf fmt "%a as %a" (print_pat ?printer) p (print_vs ?printer) v
119
  | Papp (cs,pl) -> fprintf fmt "%a%a"
120
      (print_ls ?printer) cs (print_paren_r (print_pat ?printer)) pl
121

122
123
let print_vsty ?printer fmt v =
  fprintf fmt "%a:@,%a" (print_vs ?printer) v (print_ty ?printer) v.vs_ty
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138

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

139
140
141
142
143
144
let rec print_term ?printer fmt t = print_lrterm ?printer false false fmt t
and     print_fmla ?printer fmt f = print_lrfmla ?printer false false fmt f
and print_opl_term ?printer fmt t = print_lrterm ?printer true  false fmt t
and print_opl_fmla ?printer fmt f = print_lrfmla ?printer true  false fmt f
and print_opr_term ?printer fmt t = print_lrterm ?printer false true  fmt t
and print_opr_fmla ?printer fmt f = print_lrfmla ?printer false true  fmt f
145

146
147
and print_lrterm ?printer opl opr fmt t = match t.t_label with
  | [] -> print_tnode ?printer opl opr fmt t
148
  | ll -> fprintf fmt "(%a %a)"
149
      (print_list space print_label) ll (print_tnode ?printer false false) t
150

151
152
and print_lrfmla ?printer opl opr fmt f = match f.f_label with
  | [] -> print_fnode ?printer opl opr fmt f
153
  | ll -> fprintf fmt "(%a %a)"
154
      (print_list space print_label) ll (print_fnode ?printer false false) f
155

156
and print_tnode ?printer opl opr fmt t = match t.t_node with
157
158
159
  | Tbvar _ ->
      assert false
  | Tvar v ->
160
      print_vs ?printer fmt v
161
162
163
  | Tconst c ->
      print_const fmt c
  | Tapp (fs, tl) when unambig_fs fs ->
164
165
      fprintf fmt "%a%a" (print_ls ?printer) fs (print_paren_r 
                                                   (print_term ?printer)) tl
166
167
  | Tapp (fs, tl) ->
      fprintf fmt (protect_on opl "%a%a:%a")
168
169
        (print_ls ?printer) fs (print_paren_r (print_term ?printer)) tl 
        (print_ty ?printer) t.t_ty
170
171
172
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
      fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
173
174
175
        (print_vs ?printer) v (print_opl_term ?printer) t1 
        (print_opl_term ?printer) t2;
      (forget_var ?printer) v
176
177
  | Tcase (t1,bl) ->
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
178
        (print_term ?printer) t1 (print_list newline (print_tbranch ?printer)) bl
179
180
181
  | Teps fb ->
      let v,f = f_open_bound fb in
      fprintf fmt (protect_on opr "epsilon %a in@ %a")
182
183
        (print_vsty ?printer) v (print_opl_fmla ?printer) f;
      (forget_var ?printer) v
184

185
and print_fnode ?printer opl opr fmt f = match f.f_node with
186
187
  | Fapp (ps,[t1;t2]) when ps = ps_equ ->
      fprintf fmt (protect_on (opl || opr) "%a =@ %a")
188
        (print_opr_term ?printer) t1 (print_opl_term ?printer) t2
189
  | Fapp (ps,tl) ->
190
191
      fprintf fmt "%a%a" (print_ls ?printer) ps
        (print_paren_r (print_term ?printer)) tl
192
193
194
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
      fprintf fmt (protect_on opr "%a %a%a.@ %a") print_quant q
195
196
197
        (print_list comma (print_vsty ?printer)) vl (print_tl ?printer) tl 
        (print_fmla ?printer) f;
      List.iter (forget_var ?printer) vl
198
199
200
201
202
203
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
204
        (print_opr_fmla ?printer) f1 print_binop b (print_opl_fmla ?printer) f2
205
  | Fnot f ->
206
      fprintf fmt (protect_on opr "not %a") (print_opl_fmla ?printer) f
207
208
209
  | Flet (t,f) ->
      let v,f = f_open_bound f in
      fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
210
211
212
        (print_vs ?printer) v (print_opl_term ?printer) t 
        (print_opl_fmla ?printer) f;
      forget_var ?printer v
213
  | Fcase (t,bl) ->
214
215
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend" (print_term ?printer) t
        (print_list newline (print_fbranch ?printer)) bl
216
217
  | Fif (f1,f2,f3) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
218
        (print_fmla ?printer) f1 (print_fmla ?printer) f2 (print_opl_fmla ?printer) f3
219

220
and print_tbranch ?printer fmt br =
221
  let pat,svs,t = t_open_branch br in
222
223
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat ?printer) pat (print_term ?printer) t;
  Svs.iter (forget_var ?printer) svs
224

225
and print_fbranch ?printer fmt br =
226
  let pat,svs,f = f_open_branch br in
227
228
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat ?printer) pat (print_fmla ?printer) f;
  Svs.iter (forget_var ?printer) svs
229

230
and print_tl ?printer fmt tl =
231
  if tl = [] then () else fprintf fmt "@ [%a]"
232
    (print_list alt (print_list comma (print_tr ?printer))) tl
233

234
235
236
and print_tr  ?printer fmt = function
  | TrTerm t -> print_term ?printer fmt t
  | TrFmla f -> print_fmla ?printer fmt f
237
238
239

(** Declarations *)

240
241
242
let print_constr ?printer fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" (print_ls ?printer) cs
    (print_paren_l (print_ty ?printer)) cs.ls_args
243

244
let print_ty_args ?printer fmt = function
245
  | [] -> ()
246
247
  | [tv] -> fprintf fmt " %a" (print_tv ?printer) tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma (print_tv ?printer)) l
248

249
let print_type_decl ?printer fmt (ts,def) = match def with
250
251
252
  | Tabstract -> begin match ts.ts_def with
      | None ->
          fprintf fmt "@[<hov 2>type%a %a@]"
253
            (print_ty_args ?printer) ts.ts_args (print_ts ?printer) ts
254
255
      | Some ty ->
          fprintf fmt "@[<hov 2>type%a %a =@ %a@]"
256
            (print_ty_args ?printer) ts.ts_args (print_ts ?printer) ts (print_ty ?printer) ty
257
258
259
      end
  | Talgebraic csl ->
      fprintf fmt "@[<hov 2>type%a %a =@\n@[<hov>%a@]@]"
260
261
        (print_ty_args ?printer) ts.ts_args (print_ts ?printer) ts
        (print_list newline (print_constr ?printer)) csl
262

263
264
let print_type_decl ?printer fmt d = print_type_decl ?printer fmt d; 
  forget_tvs  ?printer ()
265

266
let print_logic_decl ?printer fmt = function
267
268
  | Lfunction (fs,None) ->
      fprintf fmt "@[<hov 2>logic %a%a :@ %a@]"
269
270
        (print_ls ?printer) fs (print_paren_l (print_ty ?printer)) fs.ls_args
          (print_ty ?printer)(of_option fs.ls_value)
271
272
  | Lpredicate (ps,None) ->
      fprintf fmt "@[<hov 2>logic %a%a@]"
273
        (print_ls ?printer) ps (print_paren_l (print_ty ?printer)) ps.ls_args
274
275
276
  | Lfunction (fs,Some fd) ->
      let _,vl,t = open_fs_defn fd in
      fprintf fmt "@[<hov 2>logic %a%a :@ %a =@ %a@]"
277
278
279
        (print_ls ?printer) fs (print_paren_l (print_vsty ?printer)) vl
        (print_ty ?printer) t.t_ty (print_term ?printer) t;
      List.iter (forget_var ?printer) vl
280
281
282
  | Lpredicate (ps,Some fd) ->
      let _,vl,f = open_ps_defn fd in
      fprintf fmt "@[<hov 2>logic %a%a =@ %a@]"
283
284
        (print_ls ?printer) ps (print_paren_l (print_vsty ?printer)) vl (print_fmla ?printer) f;
      List.iter (forget_var ?printer) vl
285

286
287
let print_logic_decl ?printer fmt d = print_logic_decl ?printer fmt d; 
  forget_tvs ?printer ()
288

289
290
291
let print_prop ?printer fmt pr =
  fprintf fmt "%a : %a" (print_uc ?printer) pr.pr_name (print_fmla ?printer)
    pr.pr_fmla
292

293
294
let print_ind ?printer fmt pr = 
  fprintf fmt "@[<hov 4>| %a@]" (print_prop ?printer) pr
295

296
let print_ind_decl ?printer fmt (ps,bl) =
297
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
298
299
300
     (print_ls ?printer) ps (print_paren_l (print_ty ?printer)) ps.ls_args
     (print_list newline (print_ind ?printer)) bl;
  forget_tvs ?printer ()
301
302
303
304
305
306

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

307
308
let print_inst ?printer fmt (id1,id2) =
  fprintf fmt "%a = %a" (print_id ?printer) id1 (print_id ?printer) id2
309
310
311

let print_th fmt th = fprintf fmt "%s" th.th_name.id_long

312
313
314
315
let print_decl ?printer fmt d = match d.d_node with
  | Dtype tl  -> print_list newline2 (print_type_decl ?printer) fmt tl
  | Dlogic ll -> print_list newline2 (print_logic_decl ?printer) fmt ll
  | Dind il   -> print_list newline2 (print_ind_decl ?printer) fmt il
316
  | Dprop (k,pr) ->
317
318
      fprintf fmt "@[<hov 2>%a %a@]" print_pkind k (print_prop ?printer) pr;
      forget_tvs ?printer ()
319
320
321
322
  | Duse th ->
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
  | Dclone (th,inst) ->
      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
323
        print_th th (print_list comma (print_inst ?printer)) inst
324

325
326
let print_decls ?printer fmt dl =
  fprintf fmt "@[<hov>%a@]" (print_list newline2 (print_decl ?printer)) dl
327

328
let print_context ?printer fmt ctxt = print_decls ?printer fmt (Context.get_decls ctxt)
329

330
let print_theory ?printer fmt th =
331
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@\n@."
332
    print_th th (print_context ?printer) th.th_ctxt
333

334
let print_named_context ?printer fmt name ctxt =
335
  fprintf fmt "@[<hov 2>context %s@\n%a@]@\nend@\n@."
336
    name (print_context ?printer) ctxt
337