alt_ergo.ml 14.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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
headers    
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

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

39
let ident_printer =
40
  let bls = [
41
42
43
44
45
46
47
    "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";
48
  ]
49
  in
50
  let san = sanitizer char_to_alpha char_to_alnumus in
51
  create_ident_printer bls ~sanitizer:san
52
53

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

56
57
58
let print_label fmt l =
  fprintf fmt "\"%s\"" l.lab_string

59
60
let print_ident_label info fmt id =
  if info.info_show_labels then
61
62
63
64
65
66
    fprintf fmt "%s %a"
      (id_unique ident_printer id)
      (print_list space print_label) (Slab.elements id.id_label)
  else
    print_ident fmt id

67
68
let forget_var v = forget_id ident_printer v.vs_name

69
(*
70
71
72
73
74
let tv_printer =
  let san = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:san

let print_tvsymbol fmt tv =
75
  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)
76
77

let forget_tvs () = forget_all tv_printer
78
79
80
81
82
83
84
85
86
87
88
*)

(* 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)
89

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

98
and print_tyapp info fmt = function
99
  | [] -> ()
100
101
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
102

103
104
105
106
107
108
109
110
111
112
113
114
115
(* 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)

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

158
and print_tapp info fmt = function
159
  | [] -> ()
160
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
161

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

218
219
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
220

221
and print_triggers info fmt tl =
222
  let filter = function
Andrei Paskevich's avatar
Andrei Paskevich committed
223
224
    | { t_ty = Some _ } -> true
    | { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
225
    | _ -> false in
226
  let tl = List.map (List.filter filter) tl in
227
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
228
  if tl = [] then () else fprintf fmt "@ [%a]"
229
    (print_list alt (print_list comma (print_expr info))) tl
230

231
232
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
233

234
let print_type_decl fmt ts = match ts.ts_args with
Andrei Paskevich's avatar
Andrei Paskevich committed
235
  | [] -> fprintf fmt "type %a"
236
      print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
237
  | [tv] -> fprintf fmt "type %a %a"
238
      print_tvsymbol tv print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
239
  | tl -> fprintf fmt "type (%a) %a"
240
      (print_list comma print_tvsymbol) tl print_ident ts.ts_name
241

242
243
let print_enum_decl fmt ts csl =
  let print_cs fmt (ls,_) = print_ident fmt ls.ls_name in
244
245
  fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" print_ident ts.ts_name
    (print_list alt2 print_cs) csl
246

247
248
249
250
251
252
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 *)
253
254
    when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
      print_enum_decl fmt ts csl
255
  | ts, [cs,_] (* non-recursive records *)
Andrei Paskevich's avatar
Andrei Paskevich committed
256
257
258
259
    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
260
          (print_type info) (Opt.get ls.ls_value) in
Andrei Paskevich's avatar
Andrei Paskevich committed
261
262
      fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" print_type_decl ts
        (print_list semi print_field) pjl
263
  | _, _ -> unsupported
264
      "alt-ergo : algebraic datatype are not supported"
265

MARCHE Claude's avatar
MARCHE Claude committed
266
let print_data_decl info fmt ((ts, _csl) as p) =
267
268
269
  if Mid.mem ts.ts_name info.info_syn then () else
  print_data_decl info fmt p

270
271
272
273
274
275
276
277
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
278
279
280
281
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 ())

282
283
284
285
286
287
288
289
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
290
          (print_type info) (Opt.get ls.ls_value)
291
          (print_term info) e
292
    | None ->
293
294
295
296
297
298
        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
299

300
let print_logic_decl info fmt (ls,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
301
302
  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 ())
303
304
305
306
307
308
309
310
311
312
313

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
314
315
  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 ())
316

317
let print_decl info fmt d = match d.d_node with
318
319
320
321
322
323
  | 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
324
  | Dlogic dl ->
325
      print_list nothing (print_logic_decl info) fmt dl
326
  | Dind _ -> unsupportedDecl d
327
      "alt-ergo: inductive definitions are not supported"
328
  | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
329

330
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
331

332
333
334
335
336
337
338
339
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

340
341
342
343
344
345
346
347
348
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
349
350

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

368
let () = register_printer "alt-ergo-old"
369
  (fun _env pr thpr ?old:_ fmt task ->
370
     forget_all ident_printer;
371
     print_task_old pr thpr fmt task)
372
*)
373
374

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

395
let print_task _env pr thpr _blacklist ?old:_ fmt task =
396
397
398
399
400
401
402
403
  (* 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
404
  ~desc:"Printer for the Alt-Ergo theorem prover."
405
406
407
408
409
(*
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
*)
410