pretty.ml 12.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
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 iprinter,tprinter,lprinter,cprinter,pprinter =
29
30
31
32
33
34
35
  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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
  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,
  create_ident_printer bl ~sanitizer:usanitize

let thash = Hid.create 63
let lhash = Hid.create 63
let phash = Hid.create 63

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
  forget_all cprinter;
  forget_all pprinter;
  Hid.clear thash;
  Hid.clear lhash;
  Hid.clear phash
58

59
let tv_set = ref Sid.empty
60

61
62
63
(* type variables always start with a quote *)
let print_tv fmt tv =
  tv_set := Sid.add tv !tv_set;
64
  let sanitize n = "'" ^ n in
65
  let n = id_unique iprinter ~sanitizer:sanitize tv 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
87
88
let print_ts fmt ts =
  Hid.replace thash ts.ts_name ts;
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
89

90
91
let print_ls fmt ls =
  Hid.replace lhash ls.ls_name ls;
Andrei Paskevich's avatar
Andrei Paskevich committed
92
93
  if ls.ls_constr then fprintf fmt "%s" (id_unique cprinter ls.ls_name)
                  else fprintf fmt "%s" (id_unique lprinter ls.ls_name)
94

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

(** Types *)

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

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

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

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

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

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

160
161
162
163
164
165
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
166

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

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

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

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

236
and print_tbranch fmt br =
237
  let pat,svs,t = t_open_branch br in
238
239
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_term t;
  Svs.iter forget_var svs
240

241
and print_fbranch fmt br =
242
  let pat,svs,f = f_open_branch br in
243
244
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_fmla f;
  Svs.iter forget_var svs
245

246
and print_tl fmt tl =
247
  if tl = [] then () else fprintf fmt "@ [%a]"
248
    (print_list alt (print_list comma print_tr)) tl
249

250
251
252
and print_tr fmt = function
  | TrTerm t -> print_term fmt t
  | TrFmla f -> print_fmla fmt f
253
254
255

(** Declarations *)

256
257
258
let print_constr fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
    (print_paren_l print_ty) cs.ls_args
259

260
let print_ty_args fmt = function
261
  | [] -> ()
262
263
  | [tv] -> fprintf fmt " %a" print_tv tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l
264

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

279
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
280

281
let print_logic_decl fmt = function
282
283
  | Lfunction (fs,None) ->
      fprintf fmt "@[<hov 2>logic %a%a :@ %a@]"
284
285
        print_ls fs (print_paren_l print_ty) fs.ls_args
          print_ty (of_option fs.ls_value)
286
287
  | Lpredicate (ps,None) ->
      fprintf fmt "@[<hov 2>logic %a%a@]"
288
        print_ls ps (print_paren_l print_ty) ps.ls_args
289
290
291
  | Lfunction (fs,Some fd) ->
      let _,vl,t = open_fs_defn fd in
      fprintf fmt "@[<hov 2>logic %a%a :@ %a =@ %a@]"
292
293
294
        print_ls fs (print_paren_l print_vsty) vl
        print_ty t.t_ty print_term t;
      List.iter forget_var vl
295
296
297
  | Lpredicate (ps,Some fd) ->
      let _,vl,f = open_ps_defn fd in
      fprintf fmt "@[<hov 2>logic %a%a =@ %a@]"
298
299
        print_ls ps (print_paren_l print_vsty) vl print_fmla f;
      List.iter forget_var vl
300

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

303
304
let print_prop fmt pr =
  fprintf fmt "%a : %a" print_pr pr print_fmla pr.pr_fmla
305

306
let print_ind fmt pr = fprintf fmt "@[<hov 4>| %a@]" print_prop pr
307

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

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

319
320
321
let print_inst fmt (id1,id2) =
  if Hid.mem thash id2 then
    let n = id_unique tprinter id1 in
322
    fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
323
324
  else if Hid.mem lhash id2 then
    let n = id_unique lprinter id1 in
325
    fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
326
327
  else if Hid.mem phash id2 then
    let n = id_unique pprinter id1 in
328
    fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
329
330
331
  else assert false

let print_decl fmt d = match d.d_node with
332
333
334
  | 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
335
  | Dprop (k,pr) ->
336
337
      fprintf fmt "@[<hov 2>%a %a@]" print_pkind k print_prop pr;
      forget_tvs ()
338
339
340
341
  | Duse th ->
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
  | Dclone (th,inst) ->
      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
342
        print_th th (print_list comma print_inst) inst
343

344
let print_decls fmt dl =
345
  fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl
346

347
let print_context fmt ctxt = print_decls fmt (Context.get_decls ctxt)
348

349
let print_theory fmt th =
350
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@\n@."
351
    print_th th print_context th.th_ctxt
352

353
let print_named_context fmt name ctxt =
354
  fprintf fmt "@[<hov 2>context %s@\n%a@]@\nend@\n@."
355
    name print_context ctxt
356