alt_ergo.ml 8.9 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
19

20
21
22
23
24
open Format
open Pp
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
25
26
open Decl
open Task
27
28
open Printer

29
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
30

31
let ident_printer = 
32
33
34
35
36
  let bls = [
    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "else"; "exists";
    "false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
    "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "then"; "true"; "type"; "unit"; "void";
37
    "select"; "store";
38
39
  ] 
  in
40
  let san = sanitizer char_to_alpha char_to_alnumus in
41
  create_ident_printer bls ~sanitizer:san
42
43

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

Francois Bobot's avatar
Francois Bobot committed
46
47
48
49
let print_tvsymbols fmt tv =
  let sanitize n = "'" ^ n in
  let n = id_unique ident_printer ~sanitizer:sanitize tv.tv_name in
  fprintf fmt "%s" n
50

51
52
let forget_var v = forget_id ident_printer v.vs_name

53
54
55
56
57
58
59
type info = {
  info_syn : syntax_map;
  info_rem : Sid.t;
  info_ac  : Sid.t;
}

let rec print_type info fmt ty = match ty.ty_node with
60
  | Tyvar id -> 
61
      print_tvsymbols fmt id
62
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
63
64
      | Some s -> syntax_arguments s (print_type info) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
65
66
    end

67
and print_tyapp info fmt = function
68
  | [] -> ()
69
70
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
71

72
let rec print_term info fmt t = match t.t_node with
73
74
  | Tbvar _ -> 
      assert false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
76
  | Tconst c ->
      Pretty.print_const fmt c
77
  | Tvar { vs_name = id } ->
78
      print_ident fmt id
79
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
80
81
      | Some s -> syntax_arguments s (print_term info) fmt tl
      | None -> fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl
82
    end
83
  | Tlet _ -> unsupportedTerm t
84
      "alt-ergo : you must eliminate let in term"
85
  | Tif _ -> unsupportedTerm t 
86
      "alt-ergo : you must eliminate if_then_else"
87
  | Tcase _ -> unsupportedTerm t 
88
      "alt-ergo : you must eliminate match"
89
  | Teps _ -> unsupportedTerm t 
90
      "alt-ergo : you must eliminate epsilon"
91

92
and print_tapp info fmt = function
93
  | [] -> ()
94
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
95

96
let rec print_fmla info fmt f = match f.f_node with
97
98
  | Fapp ({ ls_name = id }, []) ->
      print_ident fmt id
99
  | Fapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
100
      | Some s -> syntax_arguments s (print_term info) fmt tl
101
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name 
102
                    (print_list comma (print_term info)) tl
103
    end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104
105
  | Fquant (q, fq) ->
      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
106
107
      let vl, tl, f = f_open_quant fq in
      let forall fmt v = 
108
	fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type info) v.vs_ty
109
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
111
        (print_triggers info) tl (print_fmla info) f;
112
      List.iter forget_var vl
113
  | Fbinop (Fand, f1, f2) ->
114
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
115
  | Fbinop (For, f1, f2) ->
116
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
117
  | Fbinop (Fimplies, f1, f2) ->
118
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
119
  | Fbinop (Fiff, f1, f2) ->
120
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
121
  | Fnot f ->
122
      fprintf fmt "(not %a)" (print_fmla info) f
123
124
125
126
127
128
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fif (f1, f2, f3) ->
      fprintf fmt "((%a and %a) or (not %a and %a))"
129
130
	(print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
        f1 (print_fmla info) f3
131
  | Flet _ -> unsupportedFmla f
132
      "alt-ergo : you must eliminate let in formula"
133
  | Fcase _ -> unsupportedFmla f 
134
135
      "alt-ergo : you must eliminate match"
  
136

137
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
138

139
and print_triggers info fmt tl =
140
  let filter = function 
141
142
    | Term _ -> true 
    | Fmla {f_node = Fapp (ps,_)} -> not (ls_equal ps ps_equ)
143
144
    | _ -> false in
  let tl = List.map (List.filter filter)
145
    tl in
146
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147
  if tl = [] then () else fprintf fmt "@ [%a]"
148
    (print_list alt (print_list comma (print_expr info))) tl
149

150
151
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
152

153
154
let print_type_decl fmt ts = match ts.ts_args with
  | [] -> fprintf fmt "type %a" print_ident ts.ts_name
155
  | [tv] -> fprintf fmt "type %a %a" print_tvsymbols tv print_ident ts.ts_name
156
157
158
  | tl -> fprintf fmt "type (%a) %a" 
      (print_list comma print_tvsymbols) tl print_ident ts.ts_name

159
160
let print_type_decl info fmt = function
  | ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
161
  | ts, Tabstract -> print_type_decl fmt ts; true
162
163
  | _, Talgebraic _ -> unsupported 
      "alt-ergo : algebraic datatype are not supported"
164

165
let ac_th = ["algebra";"AC"]
166

167
let print_logic_decl info fmt (ls,ld) =
168
169
  match ld with
    | None ->
170
        let sac = if Sid.mem ls.ls_name info.info_ac then "ac " else "" in
171
172
        fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
          sac print_ident ls.ls_name
173
          (print_list comma (print_type info)) ls.ls_args 
174
          (if ls.ls_args = [] then "" else " -> ")
175
          (print_option_or_default "prop" (print_type info)) ls.ls_value
176
177
178
179
180
181
182
    | Some ld ->
        let vl,e = open_ls_defn ld in
        begin match e with
          | Term t ->
              (* TODO AC? *)
              fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" 
                print_ident ls.ls_name
183
184
185
                (print_list comma (print_logic_binder info)) vl 
                (print_type info) (Util.of_option ls.ls_value) 
                (print_term info) t
186
187
188
          | Fmla f ->
              fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
                print_ident ls.ls_name 
189
190
                (print_list comma (print_logic_binder info)) vl 
                (print_fmla info) f
191
        end;
192
193
        List.iter forget_var vl

194
195
196
let print_logic_decl info fmt d =
  if Sid.mem (fst d).ls_name info.info_rem then
    false else (print_logic_decl info fmt d; true)
197

198
let print_decl info fmt d = match d.d_node with
199
  | Dtype dl ->
200
      print_list_opt newline (print_type_decl info) fmt dl
201
  | Dlogic dl ->
202
      print_list_opt newline (print_logic_decl info) fmt dl
203
  | Dind _ -> unsupportedDecl d 
204
      "alt-ergo : inductive definition are not supported"
205
  | Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
206
  | Dprop (Paxiom, pr, f) ->
207
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
208
        print_ident pr.pr_name (print_fmla info) f; true
209
  | Dprop (Pgoal, pr, f) ->
210
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
211
        print_ident pr.pr_name (print_fmla info) f; true
212
  | Dprop ((Plemma|Pskip), _, _) ->
213
214
      assert false

215
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
216

217
218
219
220
221
222
let print_task pr thpr syn fmt task =
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  let info = {
    info_syn = syn;
    info_rem = get_remove_set task;
223
    info_ac  = Task.find_tagged meta_ac (find_meta task meta_ac) Sid.empty }
224
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
225
  let decls = Task.task_decls task in
226
  ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
227

228
let () = register_printer "alt-ergo" 
229
  (fun pr thpr syn fmt task -> 
230
     forget_all ident_printer;
231
     print_task pr thpr syn fmt task)
232

233
234
235
236
237
(*
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
*)
238