alt_ergo.ml 14.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
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 16 17 18
open Format
open Pp
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
19
open Decl
20 21
open Printer

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

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

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

33 34 35 36
type info = {
  info_syn : syntax_map;
  info_ac  : Sls.t;
  info_show_labels : bool;
37
  info_type_casts : bool;
38 39 40
  info_csm : lsymbol list Mls.t;
  info_pjs : Sls.t;
  info_axs : Spr.t;
41
  info_inv_trig : Sls.t;
42
}
43

44
let ident_printer =
45
  let bls = [
46 47 48 49 50 51 52
    "ac"; "and"; "array"; "as"; "axiom"; "bitv"; "bool";
    "check"; "cut"; "distinct"; "else"; "exists";
    "false"; "forall"; "function"; "goal";
    "if"; "in"; "include"; "int"; "inversion";
    "let"; "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "rewriting"; "select"; "store";
    "then"; "true"; "type"; "unit"; "void"; "with";
53
  ]
54
  in
55
  let san = sanitizer char_to_alpha char_to_alnumus in
56
  create_ident_printer bls ~sanitizer:san
57 58

let print_ident fmt id =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
  fprintf fmt "%s" (id_unique ident_printer id)
60

61 62 63
let print_label fmt l =
  fprintf fmt "\"%s\"" l.lab_string

64 65
let print_ident_label info fmt id =
  if info.info_show_labels then
66 67 68 69 70 71
    fprintf fmt "%s %a"
      (id_unique ident_printer id)
      (print_list space print_label) (Slab.elements id.id_label)
  else
    print_ident fmt id

72 73
let forget_var v = forget_id ident_printer v.vs_name

74
(*
75 76 77 78 79
let tv_printer =
  let san = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:san

let print_tvsymbol fmt tv =
80
  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)
81 82

let forget_tvs () = forget_all tv_printer
83 84 85 86 87 88 89 90 91 92 93
*)

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

95
let rec print_type info fmt ty = match ty.ty_node with
96
  | Tyvar id ->
97
      print_tvsymbol fmt id
98
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
99 100
      | Some s -> syntax_arguments s (print_type info) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
101 102
    end

103
and print_tyapp info fmt = function
104
  | [] -> ()
105 106
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
107

108 109 110 111 112 113 114 115 116 117 118 119 120
(* 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)

121
let rec print_term info fmt t = match t.t_node with
122
  | Tconst c ->
123
      let number_format = {
124
          Number.long_int_support = true;
125
          Number.extra_leading_zeros_support = true;
126 127 128 129 130 131 132 133 134
          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;
          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;
135
        } in
136
      Number.print number_format fmt c
137
  | Tvar { vs_name = id } ->
138
      print_ident fmt id
139
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
140
      | Some s -> syntax_arguments s (print_term info) fmt tl
Andrei Paskevich's avatar
Andrei Paskevich committed
141 142 143 144 145 146 147
      | None when Mls.mem ls info.info_csm ->
          let print_field fmt ({ls_name = id},t) =
            fprintf fmt "%a =@ %a" print_ident id (print_term info) t in
          fprintf fmt "{@ %a@ }" (print_list semi print_field)
            (List.combine (Mls.find ls info.info_csm) tl)
      | None when Sls.mem ls info.info_pjs ->
          fprintf fmt "%a.%a" (print_tapp info) tl print_ident ls.ls_name
148
      | None when unambig_fs ls || not info.info_type_casts ->
Andrei Paskevich's avatar
Andrei Paskevich committed
149
          fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl
150 151 152
      | None ->
          fprintf fmt "(%a%a : %a)" print_ident ls.ls_name (print_tapp info) tl
             (print_type info) (t_type t)
153
    end
154
  | Tlet _ -> unsupportedTerm t
155
      "alt-ergo : you must eliminate let in term"
156
  | Tif _ -> unsupportedTerm t
157
      "alt-ergo : you must eliminate if_then_else"
158
  | Tcase _ -> unsupportedTerm t
159
      "alt-ergo : you must eliminate match"
160
  | Teps _ -> unsupportedTerm t
161
      "alt-ergo : you must eliminate epsilon"
162
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
163

164
and print_tapp info fmt = function
165
  | [] -> ()
166
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
167

168
let rec print_fmla info fmt f =
169
  if info.info_show_labels then
170 171 172 173 174 175 176 177 178 179
    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

and print_fmla_node info fmt f = match f.t_node with
180
  | Tapp ({ ls_name = id }, []) ->
181
      print_ident fmt id
182
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
183
      | Some s -> syntax_arguments s (print_term info) fmt tl
184
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name
185
                    (print_list comma (print_term info)) tl
186
    end
187 188
  | Tquant (q, fq) ->
      let vl, tl, f = t_open_quant fq in
189 190
      let q, tl = match q with
        | Tforall -> "forall", tl
191
        | Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
192
      in
193
      let forall fmt v =
194 195
        fprintf fmt "%s %a:%a" q (print_ident_label info) v.vs_name
          (print_type info) v.vs_ty
196
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
198
        (print_triggers info) tl (print_fmla info) f;
199
      List.iter forget_var vl
200
  | Tbinop (Tand, f1, f2) ->
201
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
202
  | Tbinop (Tor, f1, f2) ->
203
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
204
  | Tbinop (Timplies, f1, f2) ->
205
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
206
  | Tbinop (Tiff, f1, f2) ->
207
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
208
  | Tnot f ->
209
      fprintf fmt "(not %a)" (print_fmla info) f
210
  | Ttrue ->
211
      fprintf fmt "true"
212
  | Tfalse ->
213
      fprintf fmt "false"
214
  | Tif (f1, f2, f3) ->
215
      fprintf fmt "((%a and@ %a)@ or@ (not@ %a and@ %a))"
216
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
217
        f1 (print_fmla info) f3
218
  | Tlet _ -> unsupportedTerm f
219
      "alt-ergo: you must eliminate let in formula"
220
  | Tcase _ -> unsupportedTerm f
221
      "alt-ergo: you must eliminate match"
222
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
223

224 225
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
226

227
and print_triggers info fmt tl =
228
  let filter = function
Andrei Paskevich's avatar
Andrei Paskevich committed
229
    | { t_ty = Some _ } -> true
230
    | { t_node = Tapp (ps,_) } -> not (Sls.mem ps info.info_inv_trig)
231
    | _ -> false in
232
  let tl = List.map (List.filter filter) tl in
233
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234
  if tl = [] then () else fprintf fmt "@ [%a]"
235
    (print_list alt (print_list comma (print_expr info))) tl
236

237 238
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
239

240
let print_type_decl fmt ts = match ts.ts_args with
Andrei Paskevich's avatar
Andrei Paskevich committed
241
  | [] -> fprintf fmt "type %a"
242
      print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
243
  | [tv] -> fprintf fmt "type %a %a"
244
      print_tvsymbol tv print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
245
  | tl -> fprintf fmt "type (%a) %a"
246
      (print_list comma print_tvsymbol) tl print_ident ts.ts_name
247

248 249
let print_enum_decl fmt ts csl =
  let print_cs fmt (ls,_) = print_ident fmt ls.ls_name in
250 251
  fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" print_ident ts.ts_name
    (print_list alt2 print_cs) csl
252

253 254 255 256 257 258
let print_ty_decl info fmt ts =
  if Mid.mem ts.ts_name info.info_syn then () else
  (fprintf fmt "%a@\n@\n" print_type_decl ts; forget_tvs ())

let print_data_decl info fmt = function
  | ts, csl (* monomorphic enumeration *)
259 260
    when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
      print_enum_decl fmt ts csl
261
  | ts, [cs,_] (* non-recursive records *)
Andrei Paskevich's avatar
Andrei Paskevich committed
262 263 264 265
    when Mls.mem cs info.info_csm ->
      let pjl = Mls.find cs info.info_csm in
      let print_field fmt ls =
        fprintf fmt "%a@ :@ %a" print_ident ls.ls_name
266
          (print_type info) (Opt.get ls.ls_value) in
Andrei Paskevich's avatar
Andrei Paskevich committed
267 268
      fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" print_type_decl ts
        (print_list semi print_field) pjl
269
  | _, _ -> unsupported
270
      "alt-ergo : algebraic datatype are not supported"
271

MARCHE Claude's avatar
MARCHE Claude committed
272
let print_data_decl info fmt ((ts, _csl) as p) =
273 274 275
  if Mid.mem ts.ts_name info.info_syn then () else
  print_data_decl info fmt p

276 277 278 279 280 281 282 283
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"
    sac print_ident ls.ls_name
    (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
284 285 286 287
let print_param_decl info fmt ls =
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
    then () else (print_param_decl info fmt ls; forget_tvs ())

288 289 290 291 292 293 294 295
let print_logic_decl info fmt ls ld =
  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"
          print_ident ls.ls_name
          (print_list comma (print_logic_binder info)) vl
296
          (print_type info) (Opt.get ls.ls_value)
297
          (print_term info) e
298
    | None ->
299 300 301 302 303 304
        fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
          print_ident ls.ls_name
          (print_list comma (print_logic_binder info)) vl
          (print_fmla info) e
  end;
  List.iter forget_var vl
305

306
let print_logic_decl info fmt (ls,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
307 308
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
    then () else (print_logic_decl info fmt ls ld; forget_tvs ())
309 310 311 312 313 314 315 316 317 318 319

let print_prop_decl info fmt k pr f = match k with
  | Paxiom ->
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
        print_ident pr.pr_name (print_fmla info) f
  | Pgoal ->
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
        print_ident pr.pr_name (print_fmla info) f
  | Plemma| Pskip -> assert false

let print_prop_decl info fmt k pr f =
Andrei Paskevich's avatar
Andrei Paskevich committed
320 321
  if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
    then () else (print_prop_decl info fmt k pr f; forget_tvs ())
322

323
let print_decl info fmt d = match d.d_node with
324 325 326 327 328 329
  | Dtype ts ->
      print_ty_decl info fmt ts
  | Ddata dl ->
      print_list nothing (print_data_decl info) fmt dl
  | Dparam ls ->
      print_param_decl info fmt ls
330
  | Dlogic dl ->
331
      print_list nothing (print_logic_decl info) fmt dl
332
  | Dind _ -> unsupportedDecl d
333
      "alt-ergo: inductive definitions are not supported"
334
  | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
335

336
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
337

338 339 340 341 342 343 344 345
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

346 347 348 349 350 351 352 353 354
let check_showlabels acc = function
  | [Theory.MAstr "show_labels"] -> true
  | [Theory.MAstr _] -> acc
  | _ -> assert false

let check_typecasts acc = function
  | [Theory.MAstr "no_type_cast"] -> false
  | [Theory.MAstr _] -> acc
  | _ -> assert false
355 356

(*
357
let print_task_old pr thpr fmt task =
358 359
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
360 361
  let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
    add_projection (Mls.empty,Sls.empty,Spr.empty) task in
362
  let info = {
363
    info_syn = get_syntax_map task;
Andrei Paskevich's avatar
Andrei Paskevich committed
364
    info_ac  = Task.on_tagged_ls meta_ac task;
365 366
    info_show_labels =
      Task.on_meta meta_printer_option check_showlabels false task;
367 368 369
    info_csm = Mls.map Array.to_list csm;
    info_pjs = pjs;
    info_axs = axs;
Andrei Paskevich's avatar
Andrei Paskevich committed
370
  } in
Andrei Paskevich's avatar
Andrei Paskevich committed
371
  let decls = Task.task_decls task in
372
  fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
373

374
let () = register_printer "alt-ergo-old"
375
  (fun _env pr thpr ?old:_ fmt task ->
376
     forget_all ident_printer;
377
     print_task_old pr thpr fmt task)
378
*)
379 380

let print_decls =
381
  let print inv_trig ac sl tc csm pjs axs sm fmt d =
382 383
    let info = {
      info_syn = sm;
Andrei Paskevich's avatar
Andrei Paskevich committed
384
      info_ac  = ac;
385
      info_show_labels = sl;
386
      info_type_casts = tc;
387
      info_csm = Mls.map Array.to_list csm;
Andrei Paskevich's avatar
Andrei Paskevich committed
388 389
      info_pjs = pjs;
      info_axs = axs;
390
      info_inv_trig = Sls.add ps_equ inv_trig;
Andrei Paskevich's avatar
Andrei Paskevich committed
391
    } in
392
    print_decl info fmt d in
393
  Trans.on_tagged_ls meta_invalid_trigger (fun inv_trig ->
394
  Trans.on_tagged_ls meta_ac (fun ac ->
395 396
  Trans.on_meta meta_printer_option (fun args ->
    let sl = List.fold_left check_showlabels false args in
397
    let tc = List.fold_left check_typecasts  true  args in
Andrei Paskevich's avatar
Andrei Paskevich committed
398
  Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
399 400
    let csm,pjs,axs = List.fold_left
      add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
401
    Printer.sprint_decls (print inv_trig ac sl tc csm pjs axs)))))
402

403
let print_task _env pr thpr _blacklist ?old:_ fmt task =
404 405 406 407 408 409 410 411
  (* In trans-based p-printing [forget_all] is a no-no *)
  (* forget_all ident_printer; *)
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  fprintf fmt "%a@." (print_list nothing string)
    (List.rev (Trans.apply print_decls task))

let () = register_printer "alt-ergo" print_task
Andrei Paskevich's avatar
Andrei Paskevich committed
412
  ~desc:"Printer for the Alt-Ergo theorem prover."
413 414 415 416 417
(*
let print_goal info fmt (id, f, task) =
  print_task info fmt task;
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla info) f
*)
418