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

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

76
let forget_var vs = forget_id iprinter vs.vs_name
77

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

83
let print_ts fmt ts =
84
  Hid.replace thash ts.ts_name ts;
85
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
86

87
let print_ls fmt ls =
88
  Hid.replace lhash ls.ls_name ls;
89 90 91 92 93 94
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
  Hid.replace lhash ls.ls_name ls;
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
95

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

(** Types *)

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

104 105 106 107
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
108
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
109
      (print_list ns_comma print_ty) l print_ts ts
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 136

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

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

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

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

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

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

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

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

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

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

245
and print_fbranch fmt br =
246
  let pl,f = f_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
247 248
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_fmla f;
249
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
250

251
and print_tl fmt tl =
252
  if tl = [] then () else fprintf fmt "@ [%a]"
253
    (print_list alt (print_list comma print_expr)) tl
254

255
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
256 257 258

(** Declarations *)

259
let print_constr fmt cs =
260
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
261
    (print_paren_l print_ty) cs.ls_args
262

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

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

282
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
283

284
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
285

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

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

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

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

314 315 316 317 318
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 ()

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

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

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

347 348 349
let print_task fmt task =
  fprintf fmt "@[<hov>%a@]@."
    (print_list newline2 print_decl) (task_decls task)
350

351 352 353 354 355 356 357 358 359 360 361 362
let print_named_task fmt name task =
  fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
    name (print_list newline2 print_tdecl) (task_tdecls task)

let print_th_tdecl fmt = function
  | Theory.Decl d ->
      print_decl fmt d
  | Theory.Use th ->
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
  | Theory.Clone (th,inst) ->
      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
        print_th th (print_list comma print_inst) inst
363

364
let print_theory fmt th =
365
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
366
    print_th th (print_list newline2 print_th_tdecl) th.th_decls
367

368 369 370 371 372 373 374 375 376
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
377
    let acc = Mnm.fold (add_s "prop ")  ns.ns_pr acc in
378
    let acc = Mnm.fold (add_s "logic ") ns.ns_ls acc in
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
379
    let acc = Mnm.fold (add_s "type ")  ns.ns_ts acc in acc
380 381 382 383 384 385 386 387

  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
388
  fprintf fmt "@[<hov>%a@]@." P.print (NsTree.Namespace (name, ns))
389