pretty.ml 16.9 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 46 47 48 49
  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 58
  let sanitizer n = "'" ^ n in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
59

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

69
let forget_var vs = forget_id iprinter vs.vs_name
70

71 72
(* theory names always start with an upper case letter *)
let print_th fmt th =
73 74
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
75

76 77
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
78

79
let print_ls fmt ls =
80 81 82 83 84
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
85

86
let print_pr fmt pr =
87
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
88 89 90 91 92

(** Types *)

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

93 94 95 96
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
97
  | Tyapp (ts, l) -> fprintf fmt "(%a)@ %a"
98
      (print_list ns_comma print_ty) l print_ts ts
99 100 101 102 103 104 105 106 107 108

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
109
    | Tyvar u when tv_equal u v -> true
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
    | _ -> 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

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

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

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

150 151 152 153 154 155
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
156

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

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

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

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

231
and print_tbranch fmt br =
232
  let pl,t = t_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
233 234
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_term t;
235
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
236

237
and print_fbranch fmt br =
238
  let pl,f = f_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
239 240
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma print_pat) pl print_fmla f;
241
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
242

243
and print_tl fmt tl =
244
  if tl = [] then () else fprintf fmt "@ [%a]"
245
    (print_list alt (print_list comma print_expr)) tl
246

247
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
248 249 250

(** Declarations *)

251
let print_constr fmt cs =
252
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
253
    (print_paren_l print_ty) cs.ls_args
254

255
let print_ty_args fmt = function
256
  | [] -> ()
257 258
  | [tv] -> fprintf fmt " %a" print_tv tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l
259

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

274
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
275

276
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
277

278 279 280 281 282 283 284 285 286 287 288 289 290
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 ()
291

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

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

301 302 303 304 305 306 307
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
308

309 310 311 312 313
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 ()

314 315 316 317 318 319
let print_decl fmt d = match d.d_node with
  | 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
  | Dprop p   -> print_prop_decl fmt p

320 321 322 323 324 325 326 327
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

let print_inst_ls fmt (ls1,ls2) =
  fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2

let print_inst_pr fmt (pr1,pr2) =
  fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
328

329
let print_meta_arg fmt = function
330 331 332 333 334
  | MAts ts -> fprintf fmt "type %a" print_ts ts
  | MAls ls -> fprintf fmt "logic %a" print_ls ls
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
335 336 337

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
338
      print_decl fmt d
339
  | Use th ->
340
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
341 342 343 344 345 346 347 348
  | Clone (th,tm,lm,pm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) tm [] in
      let lm = Mls.fold (fun x y a -> (x,y)::a) lm [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) pm [] in
      fprintf fmt "@[<hov 2>(* clone %a with %a,%a,%a *)@]"
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
349 350 351 352 353 354 355
  | Meta (t,al) ->
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
        t (print_list space print_meta_arg) al

let print_theory fmt th =
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
    print_th th (print_list newline2 print_tdecl) th.th_decls
356

357 358 359
let print_task fmt task =
  fprintf fmt "@[<hov>%a@]@."
    (print_list newline2 print_decl) (task_decls task)
360

361 362
let print_named_task fmt name task =
  fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
363
    name (print_list newline2 print_tdecl) (task_tdecls task)
364

365 366
module NsTree = struct
  type t =
367
    | Namespace of string * namespace * known_map
368 369
    | Leaf      of string

370 371
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
372
    let add_pr s p  acc =
373 374
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
375 376 377 378 379 380 381 382 383 384 385 386 387 388
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
      if s = "infix <>" && ls_equal ls ps_neq then acc else
        Leaf ("logic " ^ s) :: acc
    in
    let add_ts s ts acc =
      if s = "int"  && ts_equal ts ts_int  then acc else
      if s = "real" && ts_equal ts ts_real then acc else
        Leaf ("type " ^ s) :: acc
    in
    let acc = Mnm.fold add_ns ns.ns_ns []  in
    let acc = Mnm.fold add_pr ns.ns_pr acc in
    let acc = Mnm.fold add_ls ns.ns_ls acc in
    let acc = Mnm.fold add_ts ns.ns_ts acc in acc
389 390

  let decomp = function
391 392
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
393 394
end

395
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
396
  let module P = Print_tree.Make(NsTree) in
397
  fprintf fmt "@[<hov>%a@]@." P.print
398
    (NsTree.Namespace (name, th.th_export, th.th_known))
399

400 401 402 403 404 405 406 407 408 409 410 411
(* Exception reporting *)

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | Ty.TypeMismatch (t1,t2) ->
      fprintf fmt "Type mismatch between %a and %a"
        print_ty t1 print_ty t2
  | Ty.BadTypeArity (ts, ts_arg, app_arg) ->
      fprintf fmt "Bad type arity: type symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ts ts ts_arg app_arg
  | Ty.DuplicateTypeVar tv ->
412 413 414
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450
  | Term.BadArity (ls, ls_arg, app_arg) ->
      fprintf fmt "Bad arity: symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ls ls ls_arg app_arg
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
  | Term.FunctionSymbolExpected ls ->
      fprintf fmt "Not a function symbol: %a" print_ls ls
  | Term.PredicateSymbolExpected ls ->
      fprintf fmt "Not a predicate symbol: %a" print_ls ls
  | Term.NoMatch ->
      fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
  | Pattern.ConstructorExpected ls ->
      fprintf fmt "The symbol %a is not a constructor"
        print_ls ls
  | Pattern.NonExhaustive pl ->
      fprintf fmt "Non-exhaustive pattern list:@\n@[<hov 2>%a@]"
        (print_list newline print_pat) pl
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
        print_pr pr
  | Decl.TooSpecificIndDecl (_ls, pr, t) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          has too type-specific conclusion %a"
        print_pr pr print_term t
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          contains a negative occurrence of dependent symbol %a"
        print_pr pr print_ls ls1
  | Decl.BadLogicDecl (id1,id2) ->
      fprintf fmt "Ill-formed definition: idents %s and %s are different"
        id1.id_string id2.id_string
451 452
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
453 454 455 456
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
457 458 459 460
  | Decl.EmptyAlgDecl ts ->
      fprintf fmt "Algebraic type %a has no constructors" print_ts ts
  | Decl.EmptyIndDecl ls ->
      fprintf fmt "Inductive predicate %a has no constructors" print_ls ls
461 462 463 464 465 466 467 468 469 470 471 472 473 474
  | Decl.KnownIdent id ->
      fprintf fmt "Ident %s is already declared" id.id_string
  | Decl.UnknownIdent id ->
      fprintf fmt "Ident %s is not yet declared" id.id_string
  | Decl.RedeclaredIdent id ->
      fprintf fmt "Ident %s is already declared, with a different declaration"
        id.id_string
  | Decl.NonExhaustiveExpr (pl, e) ->
      fprintf fmt
        "Non-exhaustive pattern list:@\n@[<hov 2>%a@]@\nin expression %a"
        (print_list newline print_pat) pl print_expr e
  | _ -> raise exn
  end