pretty.ml 29.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13

open Format
open Pp
14
open Wstdlib
15 16 17
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
18
open Decl
19
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Task
21

22 23 24
let why3_keywords =
  ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
   "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
25
   "scope"; "import"; "export"; "end";
26 27 28
   "forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
   "let"; "in"; "match"; "with"; "as"; "epsilon" ]

Andrei Paskevich's avatar
Andrei Paskevich committed
29
let coercion_attr = create_attribute "coercion"
30

MARCHE Claude's avatar
MARCHE Claude committed
31
module type Printer = sig
MARCHE Claude's avatar
MARCHE Claude committed
32

33 34 35
    val tprinter : ident_printer  (* type symbols *)
    val aprinter : ident_printer  (* type variables *)
    val sprinter : ident_printer  (* variables and functions *)
36
    val pprinter : ident_printer  (* proposition names *)
37

MARCHE Claude's avatar
MARCHE Claude committed
38 39 40 41
    val forget_all : unit -> unit     (* flush id_unique *)
    val forget_tvs : unit -> unit     (* flush id_unique for type vars *)
    val forget_var : vsymbol -> unit  (* flush id_unique for a variable *)

Andrei Paskevich's avatar
Andrei Paskevich committed
42
    val print_id_attrs : formatter -> ident -> unit   (* attributes and location *)
MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46 47 48 49 50 51 52 53 54 55

    val print_tv : formatter -> tvsymbol -> unit      (* type variable *)
    val print_vs : formatter -> vsymbol -> unit       (* variable *)

    val print_ts : formatter -> tysymbol -> unit      (* type symbol *)
    val print_ls : formatter -> lsymbol -> unit       (* logic symbol *)
    val print_cs : formatter -> lsymbol -> unit       (* constructor symbol *)
    val print_pr : formatter -> prsymbol -> unit      (* proposition name *)
    val print_th : formatter -> theory -> unit        (* theory name *)

    val print_ty : formatter -> ty -> unit            (* type *)
    val print_vsty : formatter -> vsymbol -> unit     (* variable : type *)

56 57 58 59 60 61 62
    val print_ts_qualified : formatter -> tysymbol -> unit
    val print_ls_qualified : formatter -> lsymbol -> unit
    val print_cs_qualified : formatter -> lsymbol -> unit
    val print_pr_qualified : formatter -> prsymbol -> unit
    val print_th_qualified : formatter -> theory -> unit
    val print_ty_qualified : formatter -> ty -> unit

MARCHE Claude's avatar
MARCHE Claude committed
63 64 65 66 67
    val print_quant : formatter -> quant -> unit      (* quantifier *)
    val print_binop : asym:bool -> formatter -> binop -> unit (* binary operator *)
    val print_pat : formatter -> pattern -> unit      (* pattern *)
    val print_term : formatter -> term -> unit        (* term *)

Andrei Paskevich's avatar
Andrei Paskevich committed
68
    val print_attr : formatter -> attribute -> unit
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
    val print_loc : formatter -> Loc.position -> unit
    val print_pkind : formatter -> prop_kind -> unit
    val print_meta_arg : formatter -> meta_arg -> unit
    val print_meta_arg_type : formatter -> meta_arg_type -> unit

    val print_ty_decl : formatter -> tysymbol -> unit
    val print_data_decl : formatter -> data_decl -> unit
    val print_param_decl : formatter -> lsymbol -> unit
    val print_logic_decl : formatter -> logic_decl -> unit
    val print_ind_decl : formatter -> ind_sign -> ind_decl -> unit
    val print_next_data_decl : formatter -> data_decl -> unit
    val print_next_logic_decl : formatter -> logic_decl -> unit
    val print_next_ind_decl : formatter -> ind_decl -> unit
    val print_prop_decl : formatter -> prop_decl -> unit

    val print_decl : formatter -> decl -> unit
    val print_tdecl : formatter -> tdecl -> unit

    val print_task : formatter -> task -> unit
    val print_sequent : formatter -> task -> unit

    val print_theory : formatter -> theory -> unit

    val print_namespace : formatter -> string -> theory -> unit

  end

96
let debug_print_attrs = Debug.register_info_flag "print_attributes"
Andrei Paskevich's avatar
Andrei Paskevich committed
97
    ~desc:"Print@ attributes@ of@ identifiers@ and@ expressions."
Andrei Paskevich's avatar
Andrei Paskevich committed
98

99
let debug_print_locs = Debug.register_info_flag "print_locs"
100
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
101

Mário Pereira's avatar
Mário Pereira committed
102 103 104
let debug_print_coercions = Debug.register_info_flag "print_coercions"
  ~desc:"Print@ coercions@ in@ logical@ formulas."

105 106 107 108
(* always print qualified?
let debug_print_qualifs = Debug.register_info_flag "print_qualifs"
  ~desc:"Print@ qualifiers@ of@ identifiers@ in@ error@ messages."*)

109
let create sprinter aprinter tprinter pprinter do_forget_all =
110
  (module (struct
111

112
let forget_tvs () =
113 114
  (* we always forget type variables between each declaration *)
  (* if do_forget_all then *) forget_all aprinter
115

116
let forget_all () =
117
  if do_forget_all then forget_all sprinter;
118 119 120
  if do_forget_all then forget_all aprinter;
  if do_forget_all then forget_all tprinter;
  if do_forget_all then forget_all pprinter
Mário Pereira's avatar
Mário Pereira committed
121

Andrei Paskevich's avatar
Andrei Paskevich committed
122 123
let print_attr fmt a = fprintf fmt "[@%s]" a.attr_string
let print_attrs = print_iter1 Sattr.iter space print_attr
124 125 126 127 128

let print_loc fmt l =
  let (f,l,b,e) = Loc.get l in
  fprintf fmt "#\"%s\" %d %d %d#" f l b e

Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132
let print_id_attrs fmt id =
  if Debug.test_flag debug_print_attrs &&
      not (Sattr.is_empty id.id_attrs) then
    fprintf fmt "@ %a" print_attrs id.id_attrs;
133
  if Debug.test_flag debug_print_locs then
134
    Opt.iter (fprintf fmt "@ %a" print_loc) id.id_loc
135

136 137
(* type variables always start with a quote *)
let print_tv fmt tv =
138
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
139 140 141

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
142
  let sanitizer = Strings.uncapitalize in
143
  Ident.print_decoded fmt (id_unique sprinter ~sanitizer vs.vs_name)
144

145
let forget_var vs = forget_id sprinter vs.vs_name
146

147 148
(* theory names always start with an upper case letter *)
let print_th fmt th =
149
  let sanitizer = Strings.capitalize in
150
  pp_print_string fmt (id_unique sprinter ~sanitizer th.th_name)
151

152
let print_ts fmt ts =
153 154 155
  if ts_equal ts ts_func then pp_print_string fmt "(->)" else
  pp_print_string fmt (id_unique tprinter ts.ts_name)

156
let print_cs fmt ls =
157
  let sanitizer = Strings.capitalize in
158
  pp_print_string fmt (id_unique sprinter ~sanitizer ls.ls_name)
159

160
let print_ls fmt ls =
161
  Ident.print_decoded fmt (id_unique sprinter ls.ls_name)
162

163
let print_pr fmt pr =
164
  Ident.print_decoded fmt (id_unique pprinter pr.pr_name)
165

166 167 168 169
let print_qualified decode fmt id =
(* if Debug.test_noflag debug_print_qualifs then raise Not_found; *)
  let dot fmt () =
    pp_print_char fmt '.'; pp_print_cut fmt () in
170 171 172
  let str fmt s =
    if String.contains s ' ' || String.contains s '.' then begin
      pp_print_char fmt '"'; pp_print_string fmt s; pp_print_char fmt '"'
173 174 175 176 177 178 179 180 181 182 183 184 185 186 187
    end else pp_print_string fmt s;
    dot fmt () in
  let lp, tn, qn = Theory.restore_path id (* raises Not_found *) in
  let qn = match lp with
    | "why3"::_ -> if qn = [] then [tn] (* theory *) else qn
    | _ -> print_list Pp.nothing str fmt lp; tn::qn in
  if decode then match List.rev qn with
    | [sn] ->
        Ident.print_decoded fmt sn
    | sn::qn ->
        print_list dot pp_print_string fmt (List.rev qn); dot fmt ();
        Ident.print_decoded fmt sn
    | [] -> ()
  else
    print_list dot pp_print_string fmt qn
188 189

let print_th_qualified fmt th =
190
  try print_qualified false fmt th.th_name with Not_found -> print_th fmt th
191 192 193

let print_ts_qualified fmt ts =
  if ts_equal ts ts_func then pp_print_string fmt "(->)" else
194
  try print_qualified false fmt ts.ts_name with Not_found -> print_ts fmt ts
195 196

let print_cs_qualified fmt ls =
197
  try print_qualified false fmt ls.ls_name with Not_found -> print_cs fmt ls
198 199

let print_ls_qualified fmt ls =
200
  try print_qualified true fmt ls.ls_name with Not_found -> print_ls fmt ls
201 202

let print_pr_qualified fmt pr =
203
  try print_qualified true fmt pr.pr_name with Not_found -> print_pr fmt pr
204

205 206
(** Types *)

207
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
208

209
let rec print_ty_node q pri fmt ty = match ty.ty_node with
210
  | Tyvar v -> print_tv fmt v
211 212
  | Tyapp (ts, [t1;t2]) when ts_equal ts Ty.ts_func ->
      fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
213
        (print_ty_node q 1) t1 (print_ty_node q 0) t2
214 215
  | Tyapp (ts, []) when is_ts_tuple ts ->
      fprintf fmt "unit"
216
  | Tyapp (ts, tl) when is_ts_tuple ts ->
217 218 219
      fprintf fmt "(%a)" (print_list comma (print_ty_node q 0)) tl
  | Tyapp (ts, []) ->
      if q then print_ts_qualified fmt ts else print_ts fmt ts
220
  | Tyapp (ts, tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
221 222 223 224
      (if q then print_ts_qualified else print_ts) ts
      (print_list space (print_ty_node q 2)) tl

let print_ty fmt ty = print_ty_node false 0 fmt ty
225

226
let print_ty_qualified fmt ty = print_ty_node true 0 fmt ty
227

228 229
let print_vsty fmt v =
  fprintf fmt "%a%a:@,%a" print_vs v
Andrei Paskevich's avatar
Andrei Paskevich committed
230
    print_id_attrs v.vs_name print_ty v.vs_ty
231 232

let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
233
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node false 2) ty
234 235
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs

236 237 238
(* 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
239
    | Tyvar u when tv_equal u v -> true
240 241 242 243 244 245 246
    | _ -> 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
247
  Opt.fold (fun _ -> inspect) true fs.ls_value
248 249 250

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
251 252 253 254
let rec print_pat_node pri fmt p = match p.pat_node with
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
Andrei Paskevich's avatar
Andrei Paskevich committed
255
      print_vs fmt v; print_id_attrs fmt v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
256
  | Pas (p, v) ->
257
      fprintf fmt (protect_on (pri > 1) "%a as %a%a")
Andrei Paskevich's avatar
Andrei Paskevich committed
258
        (print_pat_node 1) p print_vs v print_id_attrs v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
259 260 261 262 263 264 265 266 267 268 269 270 271
  | Por (p, q) ->
      fprintf fmt (protect_on (pri > 0) "%a | %a")
        (print_pat_node 0) p (print_pat_node 0) q
  | Papp (cs, pl) when is_fs_tuple cs ->
      fprintf fmt (protect_on (pri > 0) "%a")
        (print_list comma (print_pat_node 1)) pl
  | Papp (cs, []) ->
      print_cs fmt cs
  | Papp (cs, pl) ->
      fprintf fmt (protect_on (pri > 1) "%a@ %a")
        print_cs cs (print_list space (print_pat_node 2)) pl

let print_pat = print_pat_node 0
272 273

let print_quant fmt = function
274 275
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
276

277 278 279
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
280 281
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
282 283
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
284

285
let prio_binop = function
286 287
  | Tand -> 4
  | Tor -> 3
288 289
  | Timplies -> 1
  | Tiff -> 1
290

291 292 293
let rec print_term fmt t = print_lterm 0 fmt t

and print_lterm pri fmt t =
Andrei Paskevich's avatar
Andrei Paskevich committed
294 295
  let print_tattr pri fmt t =
    if Debug.test_flag debug_print_attrs && not (Sattr.is_empty t.t_attrs)
296
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
Andrei Paskevich's avatar
Andrei Paskevich committed
297
      print_attrs t.t_attrs (print_tnode 0) t
298 299
    else print_tnode pri fmt t in
  let print_tloc pri fmt t =
300
    if Debug.test_flag debug_print_locs && t.t_loc <> None
301
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
Andrei Paskevich's avatar
Andrei Paskevich committed
302 303
      (print_option print_loc) t.t_loc (print_tattr 0) t
    else print_tattr pri fmt t in
304
  print_tloc pri fmt t
305

306 307
and print_app pri ls fmt tl =
  if tl = [] then print_ls fmt ls else
308
  let s = id_unique sprinter ls.ls_name in
309
  match Ident.sn_decode s, tl with
310
  | Ident.SNtight s, [t1] ->
311
      fprintf fmt (protect_on (pri > 8) "@[%s%a@]")
312
        s (print_lterm 8) t1
313
  | Ident.SNprefix s, [t1] ->
314
      fprintf fmt (protect_on (pri > 5) "@[%s %a@]")
315
        s (print_lterm 6) t1
316
  | Ident.SNinfix s, [t1;t2] ->
317
      fprintf fmt (protect_on (pri > 5) "@[%a@ %s %a@]")
318
        (print_lterm 6) t1 s (print_lterm 6) t2
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
  | Ident.SNget s, [t1;t2] ->
      fprintf fmt (protect_on (pri > 7) "@[%a@,[%a]%s@]")
        (print_lterm 7) t1 print_term t2 s
  | Ident.SNupdate s, [t1;t2;t3] ->
      fprintf fmt (protect_on (pri > 7) "@[%a@,[%a <-@ %a]%s@]")
        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3 s
  | Ident.SNset s, [t1;t2;t3] ->
      fprintf fmt (protect_on (pri > 5) "@[%a@,[%a]%s <-@ %a@]")
        (print_lterm 6) t1 print_term t2 s (print_lterm 6) t3
  | Ident.SNcut s, [t1;t2;t3] ->
      fprintf fmt (protect_on (pri > 7) "%a[%a..%a]%s")
        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3 s
  | Ident.SNrcut s, [t1;t2] ->
      fprintf fmt (protect_on (pri > 7) "%a[%a..]%s")
        (print_lterm 7) t1 print_term t2 s
  | Ident.SNlcut s, [t1;t2] ->
      fprintf fmt (protect_on (pri > 7) "%a[..%a]%s")
        (print_lterm 7) t1 print_term t2 s
  | Ident.SNword s, tl ->
      fprintf fmt (protect_on (pri > 6) "@[%s@ %a@]")
        s (print_list space (print_lterm 7)) tl
  | _, tl -> (* do not fail, just print the string *)
      fprintf fmt (protect_on (pri > 6) "@[%s@ %a@]")
        s (print_list space (print_lterm 7)) tl
343

344
and print_tnode pri fmt t = match t.t_node with
345
  | Tvar v ->
346
      print_vs fmt v
347
  | Tconst c ->
MARCHE Claude's avatar
MARCHE Claude committed
348 349 350 351 352 353 354 355 356
     begin
       match t.t_ty with
       | Some {ty_node = Tyapp (ts,[])}
            when ts_equal ts ts_int || ts_equal ts ts_real ->
          Number.print_constant fmt c
       | Some ty -> fprintf fmt "(%a:%a)" Number.print_constant c
                            print_ty ty
       | None -> assert false
     end
Andrei Paskevich's avatar
Andrei Paskevich committed
357
  | Tapp (_, [t1]) when Sattr.mem coercion_attr t.t_attrs &&
Mário Pereira's avatar
Mário Pereira committed
358
                        Debug.test_noflag debug_print_coercions ->
Andrei Paskevich's avatar
Andrei Paskevich committed
359
      print_lterm pri fmt (t_attr_set t1.t_attrs t1)
Andrei Paskevich's avatar
Andrei Paskevich committed
360 361
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
362
  | Tapp (fs, tl) when unambig_fs fs ->
363
      print_app pri fs fmt tl
364
  | Tapp (fs, tl) ->
365
      fprintf fmt (protect_on (pri > 0) "@[%a:@ %a@]")
366
        (print_app 5 fs) tl print_ty (t_type t)
367
  | Tif (f,t1,t2) ->
368
      fprintf fmt (protect_on (pri > 0) "@[if %a@ then %a@ else %a@]")
369
        print_term f print_term t1 print_term t2
370 371
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
372 373
      fprintf fmt (protect_on (pri > 0)
                              "@[@[<hv 0>let %a%a =@;<1 2>%a@;<1 0>in@]@ %a@]")
Andrei Paskevich's avatar
Andrei Paskevich committed
374
        print_vs v print_id_attrs v.vs_name (print_lterm 5) t1 print_term t2;
375
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
376
  | Tcase (t1,bl) ->
377
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
378
        print_term t1 (print_list newline print_tbranch) bl
379
  | Teps fb ->
380 381 382 383 384 385 386
      let vl,tl,e = t_open_lambda t in
      if vl = [] then begin
        let v,f = t_open_bound fb in
        fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
          print_vsty v print_term f;
        forget_var v
      end else begin
387 388
        fprintf fmt (protect_on (pri > 0) "@[<hov 1>fun%a%a ->@ %a@]")
          (print_list nothing print_vs_arg) vl print_tl tl print_term e;
389 390
        List.iter forget_var vl
      end
391 392
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
393
      fprintf fmt (protect_on (pri > 0) "@[<hov 1>%a %a%a.@ %a@]") print_quant q
394
        (print_list comma print_vsty) vl print_tl tl print_term f;
395
      List.iter forget_var vl
396
  | Ttrue ->
397
      fprintf fmt "true"
398
  | Tfalse ->
399
      fprintf fmt "false"
400
  | Tbinop (Tand,f1,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) })
Andrei Paskevich's avatar
Andrei Paskevich committed
401
    when Sattr.mem Term.asym_split f2.t_attrs ->
402 403
      fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a so@ %a@]")
        (print_lterm 2) f1 (print_lterm 1) f2
404
  | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },f1)
Andrei Paskevich's avatar
Andrei Paskevich committed
405
    when Sattr.mem Term.asym_split f2.t_attrs ->
406 407
      fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a by@ %a@]")
        (print_lterm 2) f1 (print_lterm 1) f2
408
  | Tbinop (b,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
409
      let asym = Sattr.mem Term.asym_split f1.t_attrs in
410
      let p = prio_binop b in
411
      fprintf fmt (protect_on (pri > p) "@[%a %a@ %a@]")
412
        (print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
413
  | Tnot f ->
414
      fprintf fmt (protect_on (pri > 5) "not %a") (print_lterm 5) f
415

416
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
417 418 419
  let p,t = t_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
  Svs.iter forget_var p.pat_vars
420

421
and print_tl fmt tl =
422
  if tl = [] then () else fprintf fmt "@ [%a]"
423
    (print_list alt (print_list comma print_term)) tl
424 425 426

(** Declarations *)

427 428 429 430 431 432
let print_constr fmt (cs,pjl) =
  let add_pj pj ty pjl = (pj,ty)::pjl in
  let print_pj fmt (pj,ty) = match pj with
    | Some ls -> fprintf fmt "@ (%a:@,%a)" print_ls ls print_ty ty
    | None -> print_ty_arg fmt ty
  in
433
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
Andrei Paskevich's avatar
Andrei Paskevich committed
434
    print_id_attrs cs.ls_name
435 436
    (print_list nothing print_pj)
    (List.fold_right2 add_pj pjl cs.ls_args [])
437

438 439
let print_ty_decl fmt ts =
  let print_def fmt = function
440 441 442
    | NoDef     -> ()
    | Alias ty  -> fprintf fmt " =@ %a" print_ty ty
    | Range ir  ->
Sylvain Dailler's avatar
Sylvain Dailler committed
443
        fprintf fmt " =@ <range %s %s>"
444 445 446 447 448 449
          (BigInt.to_string ir.Number.ir_lower)
          (BigInt.to_string ir.Number.ir_upper)
    | Float irf ->
        fprintf fmt " =@ <float %d %d>"
          irf.Number.fp_exponent_digits
          irf.Number.fp_significand_digits
450 451
  in
  fprintf fmt "@[<hov 2>type %a%a%a%a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
452
    print_ts ts print_id_attrs ts.ts_name
453 454 455 456 457 458 459
    (print_list nothing print_tv_arg) ts.ts_args
    print_def ts.ts_def;
  forget_tvs ()

let print_data_decl fst fmt (ts,csl) =
  fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]"
    (if fst then "type" else "with") print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
460
    print_id_attrs ts.ts_name
461 462 463
    (print_list nothing print_tv_arg) ts.ts_args
    (print_list newline print_constr) csl;
  forget_tvs ()
464

465
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
466

467 468 469
let ls_kind ls =
  if ls.ls_value = None then "predicate"
  else if ls.ls_args = [] then "constant" else "function"
470

471 472 473
let print_param_decl fmt ls =
  fprintf fmt "@[<hov 2>%s %a%a%a%a@]"
    (ls_kind ls) print_ls ls
Andrei Paskevich's avatar
Andrei Paskevich committed
474
    print_id_attrs ls.ls_name
475 476 477
    (print_list nothing print_ty_arg) ls.ls_args
    (print_option print_ls_type) ls.ls_value;
  forget_tvs ()
478

479 480 481 482
let print_logic_decl fst fmt (ls,ld) =
  let vl,e = open_ls_defn ld in
  fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]"
    (if fst then ls_kind ls else "with") print_ls ls
Andrei Paskevich's avatar
Andrei Paskevich committed
483
    print_id_attrs ls.ls_name
484 485 486 487
    (print_list nothing print_vs_arg) vl
    (print_option print_ls_type) ls.ls_value print_term e;
  List.iter forget_var vl;
  forget_tvs ()
488

489
let print_ind fmt (pr,f) =
490
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
491
    print_pr pr print_id_attrs pr.pr_name print_term f
492

493 494 495 496 497
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

let print_ind_decl s fst fmt (ps,bl) =
498
  fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]"
499
    (if fst then ind_sign s else "with") print_ls ps
Andrei Paskevich's avatar
Andrei Paskevich committed
500
    print_id_attrs ps.ls_name
501
    (print_list nothing print_ty_arg) ps.ls_args
502 503
    (print_list newline print_ind) bl;
  forget_tvs ()
504

505 506 507 508 509 510
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"

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

512
let print_prop_decl fmt (k,pr,f) =
513
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
Andrei Paskevich's avatar
Andrei Paskevich committed
514
    print_pr pr print_id_attrs pr.pr_name print_term f;
515 516
  forget_tvs ()

517 518 519 520 521 522
let print_list_next sep print fmt = function
  | [] -> ()
  | [x] -> print true fmt x
  | x :: r -> print true fmt x; sep fmt ();
      print_list sep (print false) fmt r

523
let print_decl fmt d = match d.d_node with
524 525 526
  | Dtype ts  -> print_ty_decl fmt ts
  | Ddata tl  -> print_list_next newline print_data_decl fmt tl
  | Dparam ls -> print_param_decl fmt ls
527
  | Dlogic ll -> print_list_next newline print_logic_decl fmt ll
528
  | Dind (s, il) -> print_list_next newline (print_ind_decl s) fmt il
529 530
  | Dprop p   -> print_prop_decl fmt p

531 532
let print_next_data_decl  = print_data_decl false
let print_data_decl       = print_data_decl true
533 534
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
535 536
let print_next_ind_decl   = print_ind_decl Ind false
let print_ind_decl fmt s  = print_ind_decl s true fmt
537

538
let print_inst_ty fmt (ts1,ty2) =
539 540 541
  fprintf fmt "type %a%a = %a" print_ts ts1
    (print_list_pre space print_tv) ts1.ts_args
    print_ty ty2; forget_tvs ()
542

543 544 545
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

546
let print_inst_ls fmt (ls1,ls2) =
547
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
548 549 550

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

552
let print_meta_arg_type fmt = function
553
  | MTty       -> fprintf fmt "[type]"
554
  | MTtysymbol -> fprintf fmt "[type symbol]"
555
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
556 557 558
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
559
  | MTid    -> fprintf fmt "[identifier]"
560

561
let print_meta_arg fmt = function
562
  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
563
  | MAts ts -> fprintf fmt "type %a" print_ts ts
564
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
565 566 567
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
568
  | MAid i -> fprintf fmt "%a" Ident.print_decoded (id_unique sprinter i)
569

570 571 572 573 574 575
let print_qt fmt th =
  if th.th_path = [] then print_th fmt th else
  fprintf fmt "%a.%a"
    (print_list (constant_string ".") string) th.th_path
    print_th th

576 577
let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
578
      print_decl fmt d
579
  | Use th ->
580
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
581 582
  | Clone (th,sm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
583
      let ym = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ty [] in
584 585
      let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) sm.sm_pr [] in
586 587 588 589 590
      fprintf fmt "@[<hov 2>(* clone %a with %a%a%a%a *)@]"
        print_qt th (print_list_suf comma print_inst_ts) tm
                    (print_list_suf comma print_inst_ty) ym
                    (print_list_suf comma print_inst_ls) lm
                    (print_list_suf comma print_inst_pr) pm
591
  | Meta (m,al) ->
592
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
593
        m.meta_name (print_list comma print_meta_arg) al
594 595

let print_theory fmt th =
596
  fprintf fmt "@[<hov 2>theory %a%a@\n%a@]@\nend@."
Andrei Paskevich's avatar
Andrei Paskevich committed
597
    print_th th print_id_attrs th.th_name
598
    (print_list newline2 print_tdecl) th.th_decls
599

600
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
601
  forget_all ();
602 603
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
604

605 606
module NsTree = struct
  type t =
607
    | Namespace of string * namespace * known_map
608 609
    | Leaf      of string

610 611
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
612
    let add_pr s p  acc =
613 614
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
615
    let add_ls s ls acc =
616
      if ls_equal ls ps_equ then acc else
617
        Leaf (ls_kind ls ^ " " ^ s) :: acc
618 619
    in
    let add_ts s ts acc =
620 621
      if ts_equal ts ts_int  then acc else
      if ts_equal ts ts_real then acc else
622 623
        Leaf ("type " ^ s) :: acc
    in
624 625 626 627
    let acc = Mstr.fold add_ns ns.ns_ns []  in
    let acc = Mstr.fold add_pr ns.ns_pr acc in
    let acc = Mstr.fold add_ls ns.ns_ls acc in
    let acc = Mstr.fold add_ts ns.ns_ts acc in acc
628 629

  let decomp = function
630 631
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
632 633
end

634
let print_namespace fmt name th =
635
  let module P = Print_tree.Make(NsTree) in
636
  fprintf fmt "@[<hov>%a@]@." P.print
637
    (NsTree.Namespace (name, th.th_export, th.th_known))
638

639 640 641

(* print task under the form of a sequent, with only local context, for the IDE *)

642
(*
643 644 645 646
let print_goal fmt d =
   match d.d_node with
   | Dprop (Pgoal,_pr,f) -> fprintf fmt "@[%a@]@\n" print_term f
   | _ -> assert false
647
*)
648 649 650

let print_sequent fmt task =
  let ut = Task.used_symbols (Task.used_theories task) in
651
  let ld = Task.local_decls task ut in
652 653
  let rec aux fmt l =
    match l with
654
      | [] -> ()
655
      | [_] -> ()
656 657 658 659
      | d :: r ->
         fprintf fmt "@[%a@]@\n@\n" print_decl d;
         aux fmt r
  in
660 661 662 663 664 665 666 667
  let rec last fmt l =
    match l with
      | [] -> ()
      | [d] ->
         fprintf fmt "@[%a@]@\n@\n" print_decl d
      | _ :: r ->
         last fmt r
  in
668
  fprintf fmt "--------------------------- Local Context ---------------------------@\n@\n";
669
  fprintf fmt "@[<v 0>%a@]" aux ld;
670
  fprintf fmt "------------------------------- Goal --------------------------------@\n@\n";
671
  fprintf fmt "@[<v 0>%a@]" last ld
672

673 674 675 676
let sprinter = sprinter
let aprinter = aprinter
let tprinter = tprinter
let pprinter = pprinter
677

MARCHE Claude's avatar
MARCHE Claude committed
678
            end) : Printer) (* end of the first class module *)
679 680 681


module LegacyPrinter =
682
  (val (let sprinter,aprinter,tprinter,pprinter =
683 684 685 686 687
    let same = fun x -> x in
    create_ident_printer why3_keywords ~sanitizer:same,
    create_ident_printer why3_keywords ~sanitizer:same,
    create_ident_printer why3_keywords ~sanitizer:same,
    create_ident_printer why3_keywords ~sanitizer:same
688
  in
689
  create sprinter aprinter tprinter pprinter true))
690 691 692 693

include LegacyPrinter


694 695 696 697 698 699
(* 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"
700
        print_ty_qualified t1 print_ty_qualified t2
701 702
  | Ty.BadTypeArity ({ts_args = []} as ts, _) ->
      fprintf fmt "Type symbol %a expects no arguments" print_ts ts
703
  | Ty.BadTypeArity (ts, app_arg) ->
704 705 706
      let i = List.length ts.ts_args in
      fprintf fmt "Type symbol %a expects %i argument%s but is applied to %i"
        print_ts ts i (if i = 1 then "" else "s") app_arg
707
  | Ty.DuplicateTypeVar tv ->
708 709 710
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
711 712
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
Clément Fumex's avatar
Clément Fumex committed
713 714 715 716 717 718
  | Ty.EmptyRange ->
      fprintf fmt "Empty integer range"
  | Ty.BadFloatSpec ->
      fprintf fmt "Invalid floating point format"
  | Ty.IllegalTypeParameters ->
      fprintf fmt "This type cannot have type parameters"
719 720 721
  | Term.BadArity ({ls_args = []} as ls, _) ->
      fprintf fmt "%s %a expects no arguments"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
722
  | Term.BadArity (ls, app_arg) ->
723 724
      let i = List.length ls.ls_args in
      fprintf fmt "%s %a expects %i argument%s but is applied to %i"
725
        (if ls.ls_value = None then "Predicate" else "Function")
726
        print_ls ls i (if i = 1 then "" else "s") app_arg
727 728
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
729 730
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
731 732
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
733 734 735 736
  | 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
737
  | Term.ConstructorExpected ls ->
738 739
      fprintf fmt "%s %a is not a constructor"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
740
  | Term.TermExpected t ->
741
      fprintf fmt "Not a term: %a" print_term t
742 743
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
MARCHE Claude's avatar
MARCHE Claude committed
744 745 746 747
  | Term.InvalidIntegerLiteralType ty ->
      fprintf fmt "Cannot cast an integer literal to type %a" print_ty ty
  | Term.InvalidRealLiteralType ty ->
      fprintf fmt "Cannot cast a real literal to type %a" print_ty ty
748
  | Pattern.ConstructorExpected (ls,ty) ->
749 750 751
      fprintf fmt "%s %a is not a constructor of type %a"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
        print_ty ty
752
  | Pattern.NonExhaustive pl ->
753 754
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
        print_pat (List.hd pl)
755
  | Decl.BadConstructor ls ->
756
      fprintf fmt "Bad constructor: %a" print_ls ls
757 758
  | Decl.BadRecordField ls ->
      fprintf fmt "Not a record field: %a" print_ls ls
759
  | Decl.RecordFieldMissing ls ->
760
      fprintf fmt "Field %a is missing" print_ls ls
761
  | Decl.DuplicateRecordField ls ->
762
      fprintf fmt "Field %a is used twice in the same constructor" print_ls ls
763 764 765 766
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
767 768
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
769
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
770
      fprintf fmt "Constructor %a \
771 772
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
773
  | Decl.InvalidIndDecl (_ls, pr) ->
774
      fprintf fmt "Ill-formed inductive clause %a"
775 776
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
777
      fprintf fmt "Inductive clause %a contains \
778
          a non strictly positive occurrence of symbol %a"
779
        print_pr pr print_ls ls1
780 781 782
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
783 784
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
785
  | Decl.ClashIdent id ->
786
      fprintf fmt "Ident %a is defined twice" Ident.print_decoded id.id_string
787 788
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
789 790 791 792
  | 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
793 794 795 796 797 798 799
  | Decl.KnownIdent {id_string = s} ->
      fprintf fmt "Ident %a is already declared" Ident.print_decoded s
  | Decl.UnknownIdent {id_string = s} ->
      fprintf fmt "Ident %a is not yet declared" Ident.print_decoded s
  | Decl.RedeclaredIdent {id_string = s} ->
      fprintf fmt "Ident %a is already declared, with a different declaration"
        Ident.print_decoded s
800
  | Decl.NoTerminationProof ls ->
801
      fprintf fmt "Cannot prove termination for %a" print_ls ls
802 803
  | _ -> raise exn
  end