pretty.ml 11.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
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
46
47
48
49
  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

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
  let sanitize n = "'" ^ n in
58
  let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
59
60
  fprintf fmt "%s" n

61
62
63
64
65
66
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 =
67
  let sanitize = String.uncapitalize in
68
  let n = id_unique iprinter ~sanitizer:sanitize vs.vs_name in
69
70
  fprintf fmt "%s" n

71
let forget_var vs = forget_id iprinter vs.vs_name
72

73
74
75
76
(* 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
77
78
  fprintf fmt "%s" n

79
80
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
81

82
let print_ls fmt ls =
83
84
85
86
87
  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
88

89
let print_pr fmt pr =
90
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
91
92
93
94
95

(** Types *)

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

96
97
98
99
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
100
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
101
      (print_list ns_comma print_ty) l print_ts ts
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

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

129
let rec print_pat fmt p = match p.pat_node with
130
  | Pwild -> fprintf fmt "_"
131
132
  | Pvar v -> print_vs fmt v
  | Pas (p,v) -> fprintf fmt "%a as %a" print_pat p print_vs v
133
  | Papp (cs,pl) -> fprintf fmt "%a%a"
134
      print_ls cs (print_paren_r print_pat) pl
135

136
137
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152

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

153
154
155
156
157
158
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
159

160
161
and print_lrterm opl opr fmt t = match t.t_label with
  | [] -> print_tnode opl opr fmt t
162
  | ll -> fprintf fmt "(%a %a)"
163
      (print_list space print_label) ll (print_tnode false false) t
164

165
166
and print_lrfmla opl opr fmt f = match f.f_label with
  | [] -> print_fnode opl opr fmt f
167
  | ll -> fprintf fmt "(%a %a)"
168
      (print_list space print_label) ll (print_fnode false false) f
169

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

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

229
and print_tbranch fmt br =
230
  let pat,svs,t = t_open_branch br in
231
232
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_term t;
  Svs.iter forget_var svs
233

234
and print_fbranch fmt br =
235
  let pat,svs,f = f_open_branch br in
236
237
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_fmla f;
  Svs.iter forget_var svs
238

239
and print_tl fmt tl =
240
  if tl = [] then () else fprintf fmt "@ [%a]"
241
    (print_list alt (print_list comma print_expr)) tl
242

243
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
244
245
246

(** Declarations *)

247
248
249
let print_constr fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
    (print_paren_l print_ty) cs.ls_args
250

251
let print_ty_args fmt = function
252
  | [] -> ()
253
254
  | [tv] -> fprintf fmt " %a" print_tv tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l
255

256
let print_type_decl fmt (ts,def) = match def with
257
258
259
  | Tabstract -> begin match ts.ts_def with
      | None ->
          fprintf fmt "@[<hov 2>type%a %a@]"
260
            print_ty_args ts.ts_args print_ts ts
261
262
      | Some ty ->
          fprintf fmt "@[<hov 2>type%a %a =@ %a@]"
263
            print_ty_args ts.ts_args print_ts ts print_ty ty
264
265
266
      end
  | Talgebraic csl ->
      fprintf fmt "@[<hov 2>type%a %a =@\n@[<hov>%a@]@]"
267
268
        print_ty_args ts.ts_args print_ts ts
        (print_list newline print_constr) csl
269

270
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
271

272
let print_ls_defn fmt ld =
273
  let vl,e = open_ls_defn ld in
274
  fprintf fmt " =@ %a" print_expr e;
275
276
  List.iter forget_var vl

277
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
278
279
280
281

let print_logic_decl fmt (ls,ld) =
  fprintf fmt "@[<hov 2>logic %a%a%a%a@]"
    print_ls ls (print_paren_l print_ty) ls.ls_args
282
283
    (print_option print_ls_type) ls.ls_value
    (print_option print_ls_defn) ld;
284
  forget_tvs ()
285

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

289
let print_ind_decl fmt (ps,bl) =
290
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
291
292
    print_ls ps (print_paren_l print_ty) ps.ls_args
    (print_list newline print_ind) bl;
293
  forget_tvs ()
294
295
296
297
298
299

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

300
301
302
303
304
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 ()

305
let print_decl fmt d = match d.d_node with
306
307
308
  | 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
309
  | Dprop p   -> print_prop_decl fmt p
Andrei Paskevich's avatar
Andrei Paskevich committed
310
311
312
313
314

let print_tdecl fmt = function
  | Decl d ->
      print_decl fmt d
  | Use th ->
315
316
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th

317
let print_decls fmt dl =
318
  fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl
319

Andrei Paskevich's avatar
Andrei Paskevich committed
320
let print_task fmt task = print_decls fmt (task_decls task)
321

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

Andrei Paskevich's avatar
Andrei Paskevich committed
326
327
328
let print_named_task fmt name task =
  fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@\n@."
    name print_task task
329