alt_ergo.ml 18.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  *)
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
(********************************************************************)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
11

Francois Bobot's avatar
Francois Bobot committed
12 13
(** Alt-ergo printer *)

14 15
open Format
open Pp
16
open Wstdlib
17 18 19
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
20
open Decl
21
open Printer
22
open Cntexmp_printer
23

24
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
  ~desc:"Specify@ that@ a@ symbol@ is@ associative@ and@ commutative."

27 28
let meta_printer_option =
  Theory.register_meta "printer_option" [Theory.MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
29
    ~desc:"Pass@ additional@ parameters@ to@ the@ pretty-printer."
30

31 32 33 34
let meta_invalid_trigger =
  Theory.register_meta "invalid trigger" [Theory.MTlsymbol]
  ~desc:"Specify@ that@ a@ symbol@ is@ not@ allowed@ in@ a@ trigger."

35 36 37
type info = {
  info_syn : syntax_map;
  info_ac  : Sls.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
38
  info_show_attrs : bool;
39
  info_type_casts : bool;
40 41 42
  info_csm : lsymbol list Mls.t;
  info_pjs : Sls.t;
  info_axs : Spr.t;
43
  info_inv_trig : Sls.t;
44
  info_printer : ident_printer;
45 46 47
  mutable info_model: S.t;
  info_vc_term: vc_term_info;
  mutable info_in_goal: bool;
48
  mutable list_projs: Ident.ident Mstr.t;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
49
  mutable list_field_def: Ident.ident Mstr.t;
50
  meta_model_projection: Sls.t;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
51
  meta_record_def : Sls.t;
52
  info_cntexample: bool
53
  }
54

55
let ident_printer () =
56
  let bls = [
Guillaume Melquiond's avatar
Guillaume Melquiond committed
57
    "abs_int"; "abs_real"; "ac"; "and"; "array"; "as"; "axiom";
58 59
    "bitv"; "bool"; "case_split"; "check"; "cut"; "distinct";
    "else"; "end"; "exists"; "extends";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
60 61 62 63 64 65 66 67 68 69 70 71
    "false"; "float"; "float32"; "float32d"; "float64"; "float64d";
    "forall"; "fpa_rounding_mode"; "function";
    "goal";
    "if"; "in"; "include"; "int"; "int_ceil"; "int_floor";
    "integer_log2"; "integer_round"; "is_theory_constant"; "inversion";
    "let"; "linear_dependency"; "logic";
    "max_int"; "max_real"; "min_int"; "min_real";
    "not"; "not_theory_constant"; "or";
    "parameter"; "predicate"; "pow_real_int"; "pow_real_real";
    "prop";
    "real"; "real_of_int"; "rewriting";
    "select"; "sqrt_real"; "sqrt_real_default"; "sqrt_real_excess"; "store";
72
    "then"; "theory"; "true"; "type"; "unit"; "void"; "with";
Guillaume Melquiond's avatar
Guillaume Melquiond committed
73 74 75
    "Aw"; "Down"; "Od";
    "NearestTiesToAway"; "NearestTiesToEven"; "Nd"; "No"; "Nu"; "Nz";
    "ToZero"; "Up";
76
  ]
77
  in
78
  let san = sanitizer char_to_alpha char_to_alnumus in
79
  create_ident_printer bls ~sanitizer:san
80

81 82
let print_ident info fmt id =
  fprintf fmt "%s" (id_unique info.info_printer id)
83

Andrei Paskevich's avatar
Andrei Paskevich committed
84
let print_attr fmt l = fprintf fmt "\"%s\"" l.attr_string
MARCHE Claude's avatar
MARCHE Claude committed
85

Andrei Paskevich's avatar
Andrei Paskevich committed
86 87
let print_ident_attr info fmt id =
  if info.info_show_attrs then
88
    fprintf fmt "%s %a"
89
      (id_unique info.info_printer id)
Andrei Paskevich's avatar
Andrei Paskevich committed
90
      (print_list space print_attr) (Sattr.elements id.id_attrs)
91
  else
92
    print_ident info fmt id
93

94
let forget_var info v = forget_id info.info_printer v.vs_name
95

96
let collect_model_ls info ls =
97
  if Sls.mem ls info.meta_model_projection then
98 99
    info.list_projs <- Mstr.add (sprintf "%a" (print_ident info) ls.ls_name)
        ls.ls_name info.list_projs;
100
  if ls.ls_args = [] && relevant_for_counterexample ls.ls_name then
101 102 103
    let t = t_app ls [] ls.ls_value in
    info.info_model <-
      add_model_element
Andrei Paskevich's avatar
Andrei Paskevich committed
104
      (t_attr_set ?loc:ls.ls_name.id_loc ls.ls_name.id_attrs t) info.info_model
105

106
(*
107 108 109 110 111
let tv_printer =
  let san = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:san

let print_tvsymbol fmt tv =
112
  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)
113 114

let forget_tvs () = forget_all tv_printer
115 116 117 118 119
*)

(* work around a "duplicate type variable" bug of Alt-Ergo 0.94 *)
let print_tvsymbol, forget_tvs =
  let htv = Hid.create 5 in
120
  (fun info fmt tv ->
121
    Hid.replace htv tv.tv_name ();
122 123 124
    fprintf fmt "'%s" (id_unique info.info_printer tv.tv_name)),
  (fun info ->
    Hid.iter (fun id _ -> forget_id info.info_printer id) htv;
125
    Hid.clear htv)
126

127
let rec print_type info fmt ty = match ty.ty_node with
128
  | Tyvar id ->
129
      print_tvsymbol info fmt id
130
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
131
      | Some s -> syntax_arguments s (print_type info) fmt tl
132 133
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl
          (print_ident info) ts.ts_name
134 135
    end

136
and print_tyapp info fmt = function
137
  | [] -> ()
138 139
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
140

141 142 143 144 145 146 147 148 149 150 151 152 153
(* 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 tv_equal 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 (Opt.get fs.ls_value)

154 155 156 157 158 159 160 161 162 163 164 165 166
let number_format = {
    Number.long_int_support = `Default;
    Number.negative_int_support = `Default;
    Number.dec_int_support = `Default;
    Number.hex_int_support = `Unsupported;
    Number.oct_int_support = `Unsupported;
    Number.bin_int_support = `Unsupported;
    Number.negative_real_support = `Default;
    Number.dec_real_support = `Default;
    Number.hex_real_support = `Default;
    Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
  }

167
let rec print_term info fmt t =
168
  if check_for_counterexample t then
169 170 171 172 173
    info.info_model <- add_model_element t info.info_model;

  check_enter_vc_term t info.info_in_goal info.info_vc_term;

  let () = match t.t_node with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174
  | Tconst c ->
175
      Number.print number_format fmt c
176
  | Tvar { vs_name = id } ->
177
      print_ident info fmt id
178 179 180 181 182
  | Tapp (ls, tl) ->
     begin
       match query_syntax info.info_syn ls.ls_name with
       | Some s -> syntax_arguments s (print_term info) fmt tl
       | None ->
183 184 185 186 187 188 189 190
	  begin
	    if (tl = []) then
	      begin
		let vc_term_info = info.info_vc_term in
		if vc_term_info.vc_inside then begin
		  match vc_term_info.vc_loc with
		  | None -> ()
		  | Some loc ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
191 192 193 194 195 196 197 198
                    let attrs = (*match vc_term_info.vc_func_name with
                      | None ->*)
                          ls.ls_name.id_attrs
                      (*| Some _ ->
                          model_trace_for_postcondition ~attrs:ls.ls_name.id_attrs info.info_vc_term
                       *)
                    in
                    let _t_check_pos = t_attr_set ~loc attrs t in
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224
		      (* TODO: temporarily disable collecting variables inside the term triggering VC *)
		      (*info.info_model <- add_model_element t_check_pos info.info_model;*)
		      ()
		end
	      end;
	  end;
	  if (Mls.mem ls info.info_csm) then
	    begin
              let print_field fmt ({ls_name = id},t) =
		fprintf fmt "%a =@ %a" (print_ident info) id (print_term info) t in
              fprintf fmt "{@ %a@ }" (print_list semi print_field)
		(List.combine (Mls.find ls info.info_csm) tl)
	    end
	  else if (Sls.mem ls info.info_pjs) then
	    begin
              fprintf fmt "%a.%a" (print_tapp info) tl (print_ident info) ls.ls_name
	    end
	  else if (unambig_fs ls || not info.info_type_casts) then
	    begin
              fprintf fmt "%a%a" (print_ident info) ls.ls_name (print_tapp info) tl
	    end
	  else
	    begin
	      fprintf fmt "(%a%a : %a)" (print_ident info) ls.ls_name
		(print_tapp info) tl (print_type info) (t_type t)
	    end
225
     end
226
  | Tlet _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
227
      "alt-ergo: you must eliminate let in term"
228
  | Tif _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
229
      "alt-ergo: you must eliminate if_then_else"
230
  | Tcase _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
231
      "alt-ergo: you must eliminate match"
232
  | Teps _ -> unsupportedTerm t
Andrei Paskevich's avatar
Andrei Paskevich committed
233
      "alt-ergo: you must eliminate epsilon"
234
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
235 236 237
  in
  check_exit_vc_term t info.info_in_goal info.info_vc_term;

238

239
and print_tapp info fmt = function
240
  | [] -> ()
241
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
242

243
let rec print_fmla info fmt f =
244
  if check_for_counterexample f then
245 246 247 248
    info.info_model <- add_model_element f info.info_model;

  check_enter_vc_term f info.info_in_goal info.info_vc_term;

Andrei Paskevich's avatar
Andrei Paskevich committed
249 250
  let () = if info.info_show_attrs then
    match Sattr.elements f.t_attrs with
251 252 253
      | [] -> print_fmla_node info fmt f
      | l ->
        fprintf fmt "(%a : %a)"
Andrei Paskevich's avatar
Andrei Paskevich committed
254
          (print_list colon print_attr) l
255 256 257
          (print_fmla_node info) f
  else
    print_fmla_node info fmt f
258 259
  in
  check_exit_vc_term f info.info_in_goal info.info_vc_term
260 261

and print_fmla_node info fmt f = match f.t_node with
262
  | Tapp ({ ls_name = id }, []) ->
263
      print_ident info fmt id
264
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
265
      | Some s -> syntax_arguments s (print_term info) fmt tl
266
      | None -> fprintf fmt "%a(%a)" (print_ident info) ls.ls_name
267
                    (print_list comma (print_term info)) tl
268
    end
269 270
  | Tquant (q, fq) ->
      let vl, tl, f = t_open_quant fq in
271 272
      let q, tl = match q with
        | Tforall -> "forall", tl
273
        | Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
274
      in
275
      let forall fmt v =
Andrei Paskevich's avatar
Andrei Paskevich committed
276
        fprintf fmt "%s %a:%a" q (print_ident_attr info) v.vs_name
277
          (print_type info) v.vs_ty
278
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
279
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
280
        (print_triggers info) tl (print_fmla info) f;
281
      List.iter (forget_var info) vl
282
  | Tbinop (Tand, f1, f2) ->
283
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
284
  | Tbinop (Tor, f1, f2) ->
285
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
286
  | Tbinop (Timplies, f1, f2) ->
287
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
288
  | Tbinop (Tiff, f1, f2) ->
289
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
290
  | Tnot f ->
291
      fprintf fmt "(not %a)" (print_fmla info) f
292
  | Ttrue ->
293
      fprintf fmt "true"
294
  | Tfalse ->
295
      fprintf fmt "false"
296
  | Tif (f1, f2, f3) ->
297
      fprintf fmt "((%a and@ %a)@ or@ (not@ %a and@ %a))"
298
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
299
        f1 (print_fmla info) f3
300
  | Tlet _ -> unsupportedTerm f
301
      "alt-ergo: you must eliminate let in formula"
302
  | Tcase _ -> unsupportedTerm f
303
      "alt-ergo: you must eliminate match"
304
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
305

306 307
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
308

309
and print_triggers info fmt tl =
310
  let filter = function
Andrei Paskevich's avatar
Andrei Paskevich committed
311
    | { t_ty = Some _ } -> true
312
    | { t_node = Tapp (ps,_) } -> not (Sls.mem ps info.info_inv_trig)
313
    | _ -> false in
314
  let tl = List.map (List.filter filter) tl in
315
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316
  if tl = [] then () else fprintf fmt "@ [%a]"
317
    (print_list alt (print_list comma (print_expr info))) tl
318

319
let print_logic_binder info fmt v =
320
  fprintf fmt "%a: %a" (print_ident info) v.vs_name (print_type info) v.vs_ty
321

322
let print_type_decl info fmt ts = match ts.ts_args with
Andrei Paskevich's avatar
Andrei Paskevich committed
323
  | [] -> fprintf fmt "type %a"
324
      (print_ident info) ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
325
  | [tv] -> fprintf fmt "type %a %a"
326
      (print_tvsymbol info) tv (print_ident info) ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
327
  | tl -> fprintf fmt "type (%a) %a"
328
      (print_list comma (print_tvsymbol info)) tl (print_ident info) ts.ts_name
329

330 331 332
let print_enum_decl info fmt ts csl =
  let print_cs fmt (ls,_) = print_ident info fmt ls.ls_name in
  fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" (print_ident info) ts.ts_name
333
    (print_list alt2 print_cs) csl
334

335
let print_ty_decl info fmt ts =
Clément Fumex's avatar
Clément Fumex committed
336
  if is_alias_type_def ts.ts_def then () else
337
  if Mid.mem ts.ts_name info.info_syn then () else
338
  (fprintf fmt "%a@\n@\n" (print_type_decl info) ts; forget_tvs info)
339 340 341

let print_data_decl info fmt = function
  | ts, csl (* monomorphic enumeration *)
342
    when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
343
      print_enum_decl info fmt ts csl
344
  | ts, [cs,_] (* non-recursive records *)
Andrei Paskevich's avatar
Andrei Paskevich committed
345 346 347
    when Mls.mem cs info.info_csm ->
      let pjl = Mls.find cs info.info_csm in
      let print_field fmt ls =
348
        fprintf fmt "%a@ :@ %a" (print_ident info) ls.ls_name
349
          (print_type info) (Opt.get ls.ls_value) in
350
      fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" (print_type_decl info) ts
Andrei Paskevich's avatar
Andrei Paskevich committed
351
        (print_list semi print_field) pjl
352
  | _, _ -> unsupported
Andrei Paskevich's avatar
Andrei Paskevich committed
353
      "alt-ergo: algebraic datatype are not supported"
354

MARCHE Claude's avatar
MARCHE Claude committed
355
let print_data_decl info fmt ((ts, _csl) as p) =
356 357 358
  if Mid.mem ts.ts_name info.info_syn then () else
  print_data_decl info fmt p

359 360 361
let print_param_decl info fmt ls =
  let sac = if Sls.mem ls info.info_ac then "ac " else "" in
  fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n@\n"
362
    sac (print_ident info) ls.ls_name
363 364 365 366
    (print_list comma (print_type info)) ls.ls_args
    (if ls.ls_args = [] then "" else " -> ")
    (print_option_or_default "prop" (print_type info)) ls.ls_value

Andrei Paskevich's avatar
Andrei Paskevich committed
367 368
let print_param_decl info fmt ls =
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
369
    then () else (print_param_decl info fmt ls; forget_tvs info)
Andrei Paskevich's avatar
Andrei Paskevich committed
370

371
let print_logic_decl info fmt ls ld =
372
  collect_model_ls info ls;
373 374 375 376 377
  let vl,e = open_ls_defn ld in
  begin match e.t_ty with
    | Some _ ->
        (* TODO AC? *)
        fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n@\n"
378
          (print_ident info) ls.ls_name
379
          (print_list comma (print_logic_binder info)) vl
380
          (print_type info) (Opt.get ls.ls_value)
381
          (print_term info) e
382
    | None ->
383
        fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
384
          (print_ident info) ls.ls_name
385 386 387
          (print_list comma (print_logic_binder info)) vl
          (print_fmla info) e
  end;
388
  List.iter (forget_var info) vl
389

390
let print_logic_decl info fmt (ls,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
391
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
392
    then () else (print_logic_decl info fmt ls ld; forget_tvs info)
393

394
let print_info_model info =
395 396
  (* Prints the content of info.info_model *)
  let info_model = info.info_model in
397
  if not (S.is_empty info_model) && info.info_cntexample then
398 399 400
    begin
      let model_map =
	S.fold (fun f acc ->
401
          let s = asprintf "%a" (print_fmla info) f in
402
	  Mstr.add s f acc)
403
	info_model
404
	Mstr.empty in ();
405 406 407 408 409 410 411

      (* Printing model has modification of info.info_model as undesirable
	 side-effect. Revert it back. *)
      info.info_model <- info_model;
      model_map
    end
  else
412
    Mstr.empty
413

414
let print_prop_decl vc_loc args info fmt k pr f =
415
  match k with
416 417
  | Paxiom ->
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
418
        (print_ident info) pr.pr_name (print_fmla info) f
419
  | Pgoal ->
420
      let model_list = print_info_model info in
421 422
      args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
				vc_term_loc = vc_loc;
423
				queried_terms = model_list;
424
                                list_projections = info.list_projs;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
425
                                list_fields = info.list_field_def;
426
                                list_records = Mstr.empty;
427 428
                                noarg_constructors = [];
                                set_str = Mstr.empty};
429
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
430
        (print_ident info) pr.pr_name (print_fmla info) f
431
  | Plemma -> assert false
432

433
let print_prop_decl vc_loc args info fmt k pr f =
Andrei Paskevich's avatar
Andrei Paskevich committed
434
  if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
435
    then () else (print_prop_decl vc_loc args info fmt k pr f; forget_tvs info)
436

437
let print_decl vc_loc args info fmt d = match d.d_node with
438 439 440 441 442
  | Dtype ts ->
      print_ty_decl info fmt ts
  | Ddata dl ->
      print_list nothing (print_data_decl info) fmt dl
  | Dparam ls ->
443
      collect_model_ls info ls;
444
      print_param_decl info fmt ls
445
  | Dlogic dl ->
446
      print_list nothing (print_logic_decl info) fmt dl
447
  | Dind _ -> unsupportedDecl d
448
      "alt-ergo: inductive definitions are not supported"
449
  | Dprop (k,pr,f) -> print_prop_decl vc_loc args info fmt k pr f
450

451 452 453 454 455 456 457 458
let add_projection (csm,pjs,axs) = function
  | [Theory.MAls ls; Theory.MAls cs; Theory.MAint ind; Theory.MApr pr] ->
      let csm = try Array.set (Mls.find cs csm) ind ls; csm
      with Not_found ->
        Mls.add cs (Array.make (List.length cs.ls_args) ls) csm in
      csm, Sls.add ls pjs, Spr.add pr axs
  | _ -> assert false

459
let check_options ((show,cast) as acc) = function
Andrei Paskevich's avatar
Andrei Paskevich committed
460
  | [Theory.MAstr "show_attrs"] -> true, cast
461
  | [Theory.MAstr "no_type_cast"] -> show, false
462 463 464
  | [Theory.MAstr _] -> acc
  | _ -> assert false

465
let print_task args ?old:_ fmt task =
466 467 468 469 470
  let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
    add_projection (Mls.empty,Sls.empty,Spr.empty) task in
  let inv_trig = Task.on_tagged_ls meta_invalid_trigger task in
  let show,cast = Task.on_meta meta_printer_option
    check_options (false,true) task in
MARCHE Claude's avatar
MARCHE Claude committed
471
  let cntexample = Inlining.get_counterexmp task in
472 473
  let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
  let vc_info = {vc_inside = false; vc_loc = None; vc_func_name = None} in
474 475 476
  let info = {
    info_syn = Discriminate.get_syntax_map task;
    info_ac  = Task.on_tagged_ls meta_ac task;
Andrei Paskevich's avatar
Andrei Paskevich committed
477
    info_show_attrs = show;
478 479 480 481 482
    info_type_casts = cast;
    info_csm = Mls.map Array.to_list csm;
    info_pjs = pjs;
    info_axs = axs;
    info_inv_trig = Sls.add ps_equ inv_trig;
483 484 485
    info_printer = ident_printer ();
    info_model = S.empty;
    info_vc_term = vc_info;
486
    info_in_goal = false;
487
    list_projs = Mstr.empty;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
488
    list_field_def = Mstr.empty;
MARCHE Claude's avatar
MARCHE Claude committed
489
    meta_model_projection = Task.on_tagged_ls Theory.meta_projection task;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
490
    meta_record_def = Task.on_tagged_ls Theory.meta_record task;
491
    info_cntexample = cntexample;
492
  } in
493 494
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
495 496 497 498 499
  let rec print_decls = function
    | Some t ->
        print_decls t.Task.task_prev;
        begin match t.Task.task_decl.Theory.td_node with
        | Theory.Decl d ->
500
            begin try print_decl vc_loc args info fmt d
501 502 503 504
            with Unsupported s -> raise (UnsupportedDecl (d,s)) end
        | _ -> () end
    | None -> () in
  print_decls task;
505
  pp_print_flush fmt ()
506 507

let () = register_printer "alt-ergo" print_task
Andrei Paskevich's avatar
Andrei Paskevich committed
508
  ~desc:"Printer for the Alt-Ergo theorem prover."