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