pretty.ml 23.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11 12 13

open Format
open Pp
14
open Stdlib
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
let debug_print_labels = Debug.register_info_flag "print_labels"
Andrei Paskevich's avatar
Andrei Paskevich committed
23
  ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
Andrei Paskevich's avatar
Andrei Paskevich committed
24

25
let debug_print_locs = Debug.register_info_flag "print_locs"
Andrei Paskevich's avatar
Andrei Paskevich committed
26
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
27

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

31
let iprinter,aprinter,tprinter,pprinter =
32
  let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
Andrei Paskevich's avatar
Andrei Paskevich committed
33
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
34
            "scope"; "import"; "export"; "end";
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36
            "forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ] in
37 38 39 40
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
41
  create_ident_printer bl ~sanitizer:lsanitize,
42
  create_ident_printer bl ~sanitizer:isanitize
43

44 45 46
let forget_tvs () =
  forget_all aprinter

47 48
let forget_all () =
  forget_all iprinter;
49
  forget_all aprinter;
50
  forget_all tprinter;
51
  forget_all pprinter
52

Mário Pereira's avatar
Mário Pereira committed
53 54
let label_coercion = create_label "coercion"

55 56 57 58 59 60 61
let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label

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
62
let print_id_labels fmt id =
63 64 65 66
  if Debug.test_flag debug_print_labels &&
      not (Slab.is_empty id.id_label) then
    fprintf fmt "@ %a" print_labels id.id_label;
  if Debug.test_flag debug_print_locs then
67
    Opt.iter (fprintf fmt "@ %a" print_loc) id.id_loc
68

69 70
(* type variables always start with a quote *)
let print_tv fmt tv =
71
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
72 73 74

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
75
  let sanitizer = Strings.uncapitalize in
76
  pp_print_string fmt (id_unique iprinter ~sanitizer vs.vs_name)
77

78
let forget_var vs = forget_id iprinter vs.vs_name
79

80 81 82 83
(* pretty-print infix and prefix logic symbols *)

let extract_op ls =
  let s = ls.ls_name.id_string in
84 85
  try Some (Strings.remove_prefix "infix " s) with Not_found ->
  try Some (Strings.remove_prefix "prefix " s) with Not_found ->
86 87
  None

88 89
let tight_op s =
  s <> "" && (let c = String.get s 0 in c = '!' || c = '?')
90

91
let escape_op s =
92
  let s = if Strings.has_prefix "*" s then " " ^ s else s in
93
  let s = if Strings.has_suffix "*" s then s ^ " " else s in
94 95
  s

96 97
(* theory names always start with an upper case letter *)
let print_th fmt th =
98
  let sanitizer = Strings.capitalize in
99
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
100

101 102
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
103

104 105 106 107 108 109
let print_ls fmt ({ls_name = {id_string = nm}} as ls) =
  if nm = "mixfix []" then pp_print_string fmt "([])" else
  if nm = "mixfix [<-]" then pp_print_string fmt "([<-])" else
  if nm = "mixfix [_..]" then pp_print_string fmt "([_..])" else
  if nm = "mixfix [.._]" then pp_print_string fmt "([.._])" else
  if nm = "mixfix [_.._]" then pp_print_string fmt "([_.._])" else
110
  match extract_op ls with
111
  | Some s -> fprintf fmt "(%s)" (escape_op s)
112
  | None   -> fprintf fmt "%s" (id_unique iprinter ls.ls_name)
113 114

let print_cs fmt ls =
115
  let sanitizer = Strings.capitalize in
116
  fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
117

118
let print_pr fmt pr =
119
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
120 121 122

(** Types *)

123
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
124

125
let rec print_ty_node pri fmt ty = match ty.ty_node with
126
  | Tyvar v -> print_tv fmt v
127 128 129
  | Tyapp (ts, [t1;t2]) when ts_equal ts Ty.ts_func ->
      fprintf fmt (protect_on (pri > 0) "%a@ ->@ %a")
        (print_ty_node 1) t1 (print_ty_node 0) t2
130 131
  | Tyapp (ts, []) when is_ts_tuple ts ->
      fprintf fmt "unit"
132 133
  | Tyapp (ts, tl) when is_ts_tuple ts ->
      fprintf fmt "(%a)" (print_list comma (print_ty_node 0)) tl
134
  | Tyapp (ts, []) -> print_ts fmt ts
135 136
  | Tyapp (ts, tl) -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
      print_ts ts (print_list space (print_ty_node 2)) tl
137

138
let print_ty fmt ty = print_ty_node 0 fmt ty
139

140 141 142 143 144 145 146 147
let print_vsty fmt v =
  fprintf fmt "%a%a:@,%a" print_vs v
    print_id_labels v.vs_name print_ty v.vs_ty

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

148 149 150
(* 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
151
    | Tyvar u when tv_equal u v -> true
152 153 154 155 156 157 158
    | _ -> 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
159
  Opt.fold (fun _ -> inspect) true fs.ls_value
160 161 162

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
163 164 165 166
let rec print_pat_node pri fmt p = match p.pat_node with
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
167
      print_vs fmt v; print_id_labels fmt v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
168
  | Pas (p, v) ->
169 170
      fprintf fmt (protect_on (pri > 1) "%a as %a%a")
        (print_pat_node 1) p print_vs v print_id_labels v.vs_name
Andrei Paskevich's avatar
Andrei Paskevich committed
171 172 173 174 175 176 177 178 179 180 181 182 183
  | 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
184 185

let print_quant fmt = function
186 187
  | Tforall -> fprintf fmt "forall"
  | Texists -> fprintf fmt "exists"
188

189 190 191
let print_binop ~asym fmt = function
  | Tand when asym -> fprintf fmt "&&"
  | Tor when asym -> fprintf fmt "||"
Andrei Paskevich's avatar
Andrei Paskevich committed
192 193
  | Tand -> fprintf fmt "/\\"
  | Tor -> fprintf fmt "\\/"
194 195
  | Timplies -> fprintf fmt "->"
  | Tiff -> fprintf fmt "<->"
196

197
let prio_binop = function
198 199
  | Tand -> 4
  | Tor -> 3
200 201
  | Timplies -> 1
  | Tiff -> 1
202

203

MARCHE Claude's avatar
MARCHE Claude committed
204 205 206
let rec print_term fmt t = print_lterm 0 fmt t

and print_lterm pri fmt t =
207
  let print_tlab pri fmt t =
208
    if Debug.test_flag debug_print_labels && not (Slab.is_empty t.t_label)
209
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
210
      print_labels t.t_label (print_tnode 0) t
211 212
    else print_tnode pri fmt t in
  let print_tloc pri fmt t =
213
    if Debug.test_flag debug_print_locs && t.t_loc <> None
214
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
215 216 217
      (print_option print_loc) t.t_loc (print_tlab 0) t
    else print_tlab pri fmt t in
  print_tloc pri fmt t
218

219 220 221 222
and print_app pri ls fmt tl = match extract_op ls, tl with
  | _, [] ->
      print_ls fmt ls
  | Some s, [t1] when tight_op s ->
223 224
      fprintf fmt (protect_on (pri > 8) "%s%a")
        s (print_lterm 8) t1
225
  | Some s, [t1] ->
226 227
      fprintf fmt (protect_on (pri > 5) "%s %a")
        s (print_lterm 6) t1
228
  | Some s, [t1;t2] ->
229 230
      fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a %s@ %a@]")
        (print_lterm 6) t1 s (print_lterm 6) t2
231
  | _, [t1;t2] when ls.ls_name.id_string = "mixfix []" ->
232 233
      fprintf fmt (protect_on (pri > 7) "%a[%a]")
        (print_lterm 7) t1 print_term t2
234
  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
235 236
      fprintf fmt (protect_on (pri > 7) "%a[%a <- %a]")
        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
237
  | _, [t1;t2] when ls.ls_name.id_string = "mixfix [_..]" ->
238 239
      fprintf fmt (protect_on (pri > 7) "%a[%a..]")
        (print_lterm 7) t1 print_term t2
240
  | _, [t1;t2] when ls.ls_name.id_string = "mixfix [.._]" ->
241 242
      fprintf fmt (protect_on (pri > 7) "%a[..%a]")
        (print_lterm 7) t1 print_term t2
243
  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [_.._]" ->
244 245
      fprintf fmt (protect_on (pri > 7) "%a[%a..%a]")
        (print_lterm 7) t1 (print_lterm 6) t2 (print_lterm 6) t3
246
  | _, tl ->
247 248
      fprintf fmt (protect_on (pri > 6) "@[<hov 1>%a@ %a@]")
        print_ls ls (print_list space (print_lterm 7)) tl
249

250
and print_tnode pri fmt t = match t.t_node with
251
  | Tvar v ->
252
      print_vs fmt v
253
  | Tconst c ->
Clément Fumex's avatar
Clément Fumex committed
254
      Number.print_constant fmt c
Mário Pereira's avatar
Mário Pereira committed
255 256 257
  | Tapp (_, [t1]) when Slab.mem label_coercion t.t_label &&
                        Debug.test_noflag debug_print_coercions ->
      print_lterm pri fmt (t_label t1.t_label t1)
Andrei Paskevich's avatar
Andrei Paskevich committed
258 259
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
260
  | Tapp (fs, tl) when unambig_fs fs ->
261
      print_app pri fs fmt tl
262
  | Tapp (fs, tl) ->
263
      fprintf fmt (protect_on (pri > 0) "%a:%a")
264
        (print_app 5 fs) tl print_ty (t_type t)
265
  | Tif (f,t1,t2) ->
266
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
267
        print_term f print_term t1 print_term t2
268 269
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
270
      fprintf fmt (protect_on (pri > 0) "let %a%a = @[%a@] in@ %a")
271
        print_vs v print_id_labels v.vs_name (print_lterm 5) t1 print_term t2;
272
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
273
  | Tcase (t1,bl) ->
274
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
275
        print_term t1 (print_list newline print_tbranch) bl
276
  | Teps fb ->
277 278 279 280 281 282 283
      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
284 285
        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;
286 287
        List.iter forget_var vl
      end
288 289
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
290
      fprintf fmt (protect_on (pri > 0) "@[<hov 1>%a %a%a.@ %a@]") print_quant q
291
        (print_list comma print_vsty) vl print_tl tl print_term f;
292
      List.iter forget_var vl
293
  | Ttrue ->
294
      fprintf fmt "true"
295
  | Tfalse ->
296
      fprintf fmt "false"
297
  | Tbinop (Tand,f1,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) })
298
    when Slab.mem Term.asym_split f2.t_label ->
299 300
      fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a so@ %a@]")
        (print_lterm 2) f1 (print_lterm 1) f2
301
  | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },f1)
302
    when Slab.mem Term.asym_split f2.t_label ->
303 304
      fprintf fmt (protect_on (pri > 1) "@[<hov 1>%a by@ %a@]")
        (print_lterm 2) f1 (print_lterm 1) f2
305
  | Tbinop (b,f1,f2) ->
306
      let asym = Slab.mem Term.asym_split f1.t_label in
307
      let p = prio_binop b in
308
      fprintf fmt (protect_on (pri > p) "@[<hov 1>%a %a@ %a@]")
309
        (print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
310
  | Tnot f ->
311
      fprintf fmt (protect_on (pri > 5) "not %a") (print_lterm 5) f
312

313
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
314 315 316
  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
317

318
and print_tl fmt tl =
319
  if tl = [] then () else fprintf fmt "@ [%a]"
320
    (print_list alt (print_list comma print_term)) tl
321 322 323

(** Declarations *)

324 325 326 327 328 329
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
330
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
Andrei Paskevich's avatar
Andrei Paskevich committed
331
    print_id_labels cs.ls_name
332 333
    (print_list nothing print_pj)
    (List.fold_right2 add_pj pjl cs.ls_args [])
334

335 336
let print_ty_decl fmt ts =
  let print_def fmt = function
Clément Fumex's avatar
Clément Fumex committed
337 338 339 340
    | NoDef -> ()
    | Alias ty -> fprintf fmt " =@ %a" print_ty ty
    | Range _  -> fprintf fmt " =@ <range ...>" (* TODO *)
    | Float _  -> fprintf fmt " =@ <float ...>" (* TODO *)
341 342
  in
  fprintf fmt "@[<hov 2>type %a%a%a%a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
343
    print_ts ts print_id_labels ts.ts_name
344 345 346 347 348 349 350
    (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
351
    print_id_labels ts.ts_name
352 353 354
    (print_list nothing print_tv_arg) ts.ts_args
    (print_list newline print_constr) csl;
  forget_tvs ()
355

356
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
357

358 359 360
let ls_kind ls =
  if ls.ls_value = None then "predicate"
  else if ls.ls_args = [] then "constant" else "function"
Andrei Paskevich's avatar
Andrei Paskevich committed
361

362 363 364
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
365
    print_id_labels ls.ls_name
366 367 368
    (print_list nothing print_ty_arg) ls.ls_args
    (print_option print_ls_type) ls.ls_value;
  forget_tvs ()
369

370 371 372 373
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
374
    print_id_labels ls.ls_name
375 376 377 378
    (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 ()
379

380
let print_ind fmt (pr,f) =
381
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
382
    print_pr pr print_id_labels pr.pr_name print_term f
383

384 385 386 387 388
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

let print_ind_decl s fst fmt (ps,bl) =
389
  fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]"
390
    (if fst then ind_sign s else "with") print_ls ps
Andrei Paskevich's avatar
Andrei Paskevich committed
391
    print_id_labels ps.ls_name
392
    (print_list nothing print_ty_arg) ps.ls_args
393 394
    (print_list newline print_ind) bl;
  forget_tvs ()
395

396 397 398 399 400 401
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"

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

403
let print_prop_decl fmt (k,pr,f) =
404
  fprintf fmt "@[<hov 2>%a %a%a :@ %a@]" print_pkind k
Andrei Paskevich's avatar
Andrei Paskevich committed
405
    print_pr pr print_id_labels pr.pr_name print_term f;
406 407
  forget_tvs ()

408 409 410 411 412 413
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

414
let print_decl fmt d = match d.d_node with
415 416 417
  | 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
418
  | Dlogic ll -> print_list_next newline print_logic_decl fmt ll
419
  | Dind (s, il) -> print_list_next newline (print_ind_decl s) fmt il
420 421
  | Dprop p   -> print_prop_decl fmt p

422 423
let print_next_data_decl  = print_data_decl false
let print_data_decl       = print_data_decl true
424 425
let print_next_logic_decl = print_logic_decl false
let print_logic_decl      = print_logic_decl true
426 427
let print_next_ind_decl   = print_ind_decl Ind false
let print_ind_decl fmt s  = print_ind_decl s true fmt
428

429
let print_inst_ty fmt (ts1,ty2) =
430 431 432
  fprintf fmt "type %a%a = %a" print_ts ts1
    (print_list_pre space print_tv) ts1.ts_args
    print_ty ty2; forget_tvs ()
433

434 435 436
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

437
let print_inst_ls fmt (ls1,ls2) =
Andrei Paskevich's avatar
Andrei Paskevich committed
438
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
439 440 441

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

443
let print_meta_arg_type fmt = function
444
  | MTty       -> fprintf fmt "[type]"
445
  | MTtysymbol -> fprintf fmt "[type symbol]"
Andrei Paskevich's avatar
Andrei Paskevich committed
446
  | MTlsymbol  -> fprintf fmt "[function/predicate symbol]"
447 448 449 450
  | MTprsymbol -> fprintf fmt "[proposition]"
  | MTstring   -> fprintf fmt "[string]"
  | MTint      -> fprintf fmt "[integer]"

451
let print_meta_arg fmt = function
452
  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
453
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
454
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
455 456 457
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
458

459 460 461 462 463 464
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

465 466
let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
467
      print_decl fmt d
468
  | Use th ->
469
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
470 471
  | Clone (th,sm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
472
      let ym = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ty [] in
473 474
      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
475 476 477 478 479
      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
480
  | Meta (m,al) ->
481
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
482
        m.meta_name (print_list comma print_meta_arg) al
483 484

let print_theory fmt th =
Andrei Paskevich's avatar
Andrei Paskevich committed
485
  fprintf fmt "@[<hov 2>theory %a%a@\n%a@]@\nend@."
Andrei Paskevich's avatar
Andrei Paskevich committed
486
    print_th th print_id_labels th.th_name
Andrei Paskevich's avatar
Andrei Paskevich committed
487
    (print_list newline2 print_tdecl) th.th_decls
488

489
let print_task fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
490
  forget_all ();
491 492
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
493

494 495
module NsTree = struct
  type t =
496
    | Namespace of string * namespace * known_map
497 498
    | Leaf      of string

499 500
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
501
    let add_pr s p  acc =
502 503
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
504 505
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
Andrei Paskevich's avatar
Andrei Paskevich committed
506
        Leaf (ls_kind ls ^ " " ^ s) :: acc
507 508 509 510 511 512
    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
513 514 515 516
    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
517 518

  let decomp = function
519 520
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
521 522
end

523
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
524
  let module P = Print_tree.Make(NsTree) in
525
  fprintf fmt "@[<hov>%a@]@." P.print
526
    (NsTree.Namespace (name, th.th_export, th.th_known))
527

528 529 530 531 532 533 534
(* 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
535 536
  | Ty.BadTypeArity ({ts_args = []} as ts, _) ->
      fprintf fmt "Type symbol %a expects no arguments" print_ts ts
537
  | Ty.BadTypeArity (ts, app_arg) ->
538 539 540
      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
541
  | Ty.DuplicateTypeVar tv ->
542 543 544
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
545 546
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
Clément Fumex's avatar
Clément Fumex committed
547 548 549 550 551 552
  | 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"
553 554 555
  | 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
556
  | Term.BadArity (ls, app_arg) ->
557 558
      let i = List.length ls.ls_args in
      fprintf fmt "%s %a expects %i argument%s but is applied to %i"
559
        (if ls.ls_value = None then "Predicate" else "Function")
560
        print_ls ls i (if i = 1 then "" else "s") app_arg
561 562
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
563 564
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
565 566
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
567 568 569 570
  | 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
571
  | Term.ConstructorExpected ls ->
572 573
      fprintf fmt "%s %a is not a constructor"
        (if ls.ls_value = None then "Predicate" else "Function") print_ls ls
574
  | Term.TermExpected t ->
575
      fprintf fmt "Not a term: %a" print_term t
576 577
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" print_term t
Clément Fumex's avatar
Clément Fumex committed
578 579
  | Term.InvalidLiteralType ty ->
      fprintf fmt "Type %a cannot be used for a numeric literal" print_ty ty
580
  | Pattern.ConstructorExpected (ls,ty) ->
581 582 583
      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
584
  | Pattern.NonExhaustive pl ->
585 586
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
        print_pat (List.hd pl)
587
  | Decl.BadConstructor ls ->
588
      fprintf fmt "Bad constructor: %a" print_ls ls
589 590
  | Decl.BadRecordField ls ->
      fprintf fmt "Not a record field: %a" print_ls ls
591
  | Decl.RecordFieldMissing ls ->
592
      fprintf fmt "Field %a is missing" print_ls ls
593
  | Decl.DuplicateRecordField ls ->
594
      fprintf fmt "Field %a is used twice in the same constructor" print_ls ls
595 596 597 598
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
599 600
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" print_ts ts
601
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
602
      fprintf fmt "Constructor %a \
603 604
          contains a non strictly positive occurrence of type %a"
        print_ls ls print_ty ty
605
  | Decl.InvalidIndDecl (_ls, pr) ->
606
      fprintf fmt "Ill-formed inductive clause %a"
607 608
        print_pr pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
609
      fprintf fmt "Inductive clause %a contains \
MARCHE Claude's avatar
MARCHE Claude committed
610
          a non strictly positive occurrence of symbol %a"
611
        print_pr pr print_ls ls1
612 613 614
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        print_ls ls1 print_ls ls2
615 616
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
617 618 619 620
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
621 622 623 624
  | 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
625 626 627 628 629 630 631
  | 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
632 633
  | Decl.NoTerminationProof ls ->
      fprintf fmt "Cannot prove the termination of %a" print_ls ls
634 635
  | _ -> raise exn
  end