alt_ergo.ml 18 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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
(********************************************************************)
Jean-Christophe Filliâtre's avatar
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 38
type info = {
  info_syn : syntax_map;
  info_ac  : Sls.t;
  info_show_labels : 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: Sstr.t;
49
  meta_model_projection: Sls.t;
50
  info_cntexample: bool
51
  }
52

53
let ident_printer () =
54
  let bls = [
55
    "abs_int"; "abs_real"; "ac"; "and"; "array"; "as"; "axiom";
56 57
    "bitv"; "bool"; "case_split"; "check"; "cut"; "distinct";
    "else"; "end"; "exists"; "extends";
58 59 60 61 62 63 64 65 66 67 68 69
    "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";
70
    "then"; "theory"; "true"; "type"; "unit"; "void"; "with";
71 72 73
    "Aw"; "Down"; "Od";
    "NearestTiesToAway"; "NearestTiesToEven"; "Nd"; "No"; "Nu"; "Nz";
    "ToZero"; "Up";
74
  ]
75
  in
76
  let san = sanitizer char_to_alpha char_to_alnumus in
77
  create_ident_printer bls ~sanitizer:san
78

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

MARCHE Claude's avatar
MARCHE Claude committed
82 83
let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string

84 85
let print_ident_label info fmt id =
  if info.info_show_labels then
86
    fprintf fmt "%s %a"
87
      (id_unique info.info_printer id)
88 89
      (print_list space print_label) (Slab.elements id.id_label)
  else
90
    print_ident info fmt id
91

92
let forget_var info v = forget_id info.info_printer v.vs_name
93

94
let collect_model_ls info ls =
95
  if Sls.mem ls info.meta_model_projection then
96
    info.list_projs <- Sstr.add (sprintf "%a" (print_ident info) ls.ls_name) info.list_projs;
97 98 99 100 101 102
  if ls.ls_args = [] && Slab.mem model_label ls.ls_name.id_label then
    let t = t_app ls [] ls.ls_value in
    info.info_model <-
      add_model_element
      (t_label ?loc:ls.ls_name.id_loc ls.ls_name.id_label t) info.info_model

103
(*
104 105 106 107 108
let tv_printer =
  let san = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:san

let print_tvsymbol fmt tv =
109
  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)
110 111

let forget_tvs () = forget_all tv_printer
112 113 114 115 116
*)

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

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

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

138 139 140 141 142 143 144 145 146 147 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
    | 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)

151 152 153 154 155 156 157
let rec print_term info fmt t =
  if Slab.mem model_label t.t_label then
    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
158
  | Tconst c ->
159
      let number_format = {
160
          Number.long_int_support = true;
161
          Number.extra_leading_zeros_support = true;
162
          Number.negative_int_support = Number.Number_default;
163 164 165 166 167
          Number.dec_int_support = Number.Number_default;
          Number.hex_int_support = Number.Number_unsupported;
          Number.oct_int_support = Number.Number_unsupported;
          Number.bin_int_support = Number.Number_unsupported;
          Number.def_int_support = Number.Number_unsupported;
168
          Number.negative_real_support = Number.Number_default;
169 170 171 172
          Number.dec_real_support = Number.Number_default;
          Number.hex_real_support = Number.Number_default;
          Number.frac_real_support = Number.Number_unsupported;
          Number.def_real_support = Number.Number_unsupported;
173
        } in
174
      Number.print number_format fmt c
175
  | Tvar { vs_name = id } ->
176
      print_ident info fmt id
177 178
  | Tapp (ls, tl) -> begin
      (match query_syntax info.info_syn ls.ls_name with
179
      | Some s -> syntax_arguments s (print_term info) fmt tl
180
      | None ->
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
	  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 ->
		      let labels = match vc_term_info.vc_func_name with
		      | None ->
			  ls.ls_name.id_label
		      | Some _ ->
			  model_trace_for_postcondition ~labels:ls.ls_name.id_label info.info_vc_term in
		      let _t_check_pos = t_label ~loc labels t in
		      (* 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
      ) end
222
  | Tlet _ -> unsupportedTerm t
223
      "alt-ergo: you must eliminate let in term"
224
  | Tif _ -> unsupportedTerm t
225
      "alt-ergo: you must eliminate if_then_else"
226
  | Tcase _ -> unsupportedTerm t
227
      "alt-ergo: you must eliminate match"
228
  | Teps _ -> unsupportedTerm t
229
      "alt-ergo: you must eliminate epsilon"
230
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
231 232 233
  in
  check_exit_vc_term t info.info_in_goal info.info_vc_term;

234

235
and print_tapp info fmt = function
236
  | [] -> ()
237
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
238

239
let rec print_fmla info fmt f =
240 241 242 243 244 245
  if Slab.mem model_label f.t_label then
    info.info_model <- add_model_element f info.info_model;

  check_enter_vc_term f info.info_in_goal info.info_vc_term;

  let () = if info.info_show_labels then
246 247 248 249 250 251 252 253
    match Slab.elements f.t_label with
      | [] -> print_fmla_node info fmt f
      | l ->
        fprintf fmt "(%a : %a)"
          (print_list colon print_label) l
          (print_fmla_node info) f
  else
    print_fmla_node info fmt f
254 255
  in
  check_exit_vc_term f info.info_in_goal info.info_vc_term
256 257

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

302 303
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
304

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

315
let print_logic_binder info fmt v =
316
  fprintf fmt "%a: %a" (print_ident info) v.vs_name (print_type info) v.vs_ty
317

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

326 327 328
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
329
    (print_list alt2 print_cs) csl
330

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

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

MARCHE Claude's avatar
MARCHE Claude committed
351
let print_data_decl info fmt ((ts, _csl) as p) =
352 353 354
  if Mid.mem ts.ts_name info.info_syn then () else
  print_data_decl info fmt p

355 356 357
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"
358
    sac (print_ident info) ls.ls_name
359 360 361 362
    (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
363 364
let print_param_decl info fmt ls =
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
365
    then () else (print_param_decl info fmt ls; forget_tvs info)
Andrei Paskevich's avatar
Andrei Paskevich committed
366

367
let print_logic_decl info fmt ls ld =
368
  collect_model_ls info ls;
369 370 371 372 373
  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"
374
          (print_ident info) ls.ls_name
375
          (print_list comma (print_logic_binder info)) vl
376
          (print_type info) (Opt.get ls.ls_value)
377
          (print_term info) e
378
    | None ->
379
        fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
380
          (print_ident info) ls.ls_name
381 382 383
          (print_list comma (print_logic_binder info)) vl
          (print_fmla info) e
  end;
384
  List.iter (forget_var info) vl
385

386
let print_logic_decl info fmt (ls,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
387
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
388
    then () else (print_logic_decl info fmt ls ld; forget_tvs info)
389

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

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

410
let print_prop_decl vc_loc args info fmt k pr f =
411
  match k with
412 413
  | Paxiom ->
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
414
        (print_ident info) pr.pr_name (print_fmla info) f
415
  | Pgoal ->
416
      let model_list = print_info_model info in
417 418
      args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
				vc_term_loc = vc_loc;
419
				queried_terms = model_list;
420
                                list_projections = info.list_projs;
421
                                list_records = Mstr.empty};
422
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
423
        (print_ident info) pr.pr_name (print_fmla info) f
424
  | Plemma -> assert false
425

426
let print_prop_decl vc_loc args info fmt k pr f =
Andrei Paskevich's avatar
Andrei Paskevich committed
427
  if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
428
    then () else (print_prop_decl vc_loc args info fmt k pr f; forget_tvs info)
429

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

444 445 446 447 448 449 450 451
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

452 453 454
let check_options ((show,cast) as acc) = function
  | [Theory.MAstr "show_labels"] -> true, cast
  | [Theory.MAstr "no_type_cast"] -> show, false
455 456 457
  | [Theory.MAstr _] -> acc
  | _ -> assert false

458
let print_task args ?old:_ fmt task =
459 460 461 462 463
  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
464 465 466
  let cntexample = Prepare_for_counterexmp.get_counterexmp task in
  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
467 468 469 470 471 472 473 474 475
  let info = {
    info_syn = Discriminate.get_syntax_map task;
    info_ac  = Task.on_tagged_ls meta_ac task;
    info_show_labels = show;
    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;
476 477 478
    info_printer = ident_printer ();
    info_model = S.empty;
    info_vc_term = vc_info;
479
    info_in_goal = false;
480
    list_projs = Sstr.empty;
MARCHE Claude's avatar
MARCHE Claude committed
481
    meta_model_projection = Task.on_tagged_ls Theory.meta_projection task;
482
    info_cntexample = cntexample;
483
  } in
484 485
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
486 487 488 489 490
  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 ->
491
            begin try print_decl vc_loc args info fmt d
492 493 494 495
            with Unsupported s -> raise (UnsupportedDecl (d,s)) end
        | _ -> () end
    | None -> () in
  print_decls task;
496
  pp_print_flush fmt ()
497 498

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