1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
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
222
223
224
225
226
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2015 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Smtlib2_ast
open SmtAtom
open SmtForm
open SmtMisc
open CoqTerms
(* For debugging *)
let pp_symbol s =
let pp_position p = "{pos_fname = "^p.Lexing.pos_fname^"; pos_lnum = "^(string_of_int p.Lexing.pos_lnum)^"; pos_bol = "^(string_of_int p.Lexing.pos_bol)^"; pos_cnum = "^(string_of_int p.Lexing.pos_cnum)^"}" in
let pp_loc (p1,p2) = "("^(pp_position p1)^", "^(pp_position p2)^")" in
match s with
| Symbol (l,s) -> "Symbol ("^(pp_loc l)^", "^s^")"
| SymbolWithOr (l,s) -> "SymbolWithOr ("^(pp_loc l)^", "^s^")"
(* Main functions *)
let string_of_symbol = function | Symbol (_,s) | SymbolWithOr (_,s) -> s
let identifier_of_qualidentifier = function
| QualIdentifierId (_,id) | QualIdentifierAs (_,id,_) -> id
let string_type s = match s with
| "Bool" -> Tbool
| "Int" -> TZ
| _ -> VeritSyntax.get_btype s
let sort_of_string s = (string_type s, [])
let sort_of_symbol s = sort_of_string (string_of_symbol s)
let string_of_identifier = function
| IdSymbol (_,s) -> (string_of_symbol s)
| IdUnderscoreSymNum (_,s,(_,l)) ->
List.fold_left (fun c c' -> c^"_"^c') (string_of_symbol s) l
let string_of_qualidentifier id = string_of_identifier (identifier_of_qualidentifier id)
let rec sort_of_sort = function
| SortIdentifier (_,id) -> sort_of_string (string_of_identifier id)
| SortIdSortMulti (_,id,(_,l)) ->
(string_type (string_of_identifier id), List.map sort_of_sort l)
let declare_sort rt sym =
let s = string_of_symbol sym in
let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in
let eq_t = declare_new_variable (Names.id_of_string ("eq_"^s)) (Term.mkArrow cons_t (Term.mkArrow cons_t (Lazy.force cbool))) in
let x = mkName "x" in
let y = mkName "y" in
let rx = Term.mkRel 2 in
let ry = Term.mkRel 1 in
let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in
let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in
let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in
let res = Btype.declare rt cons_t ce in
VeritSyntax.add_btype s res;
res
let declare_fun rt ro sym arg cod =
let s = string_of_symbol sym in
let tyl = List.map sort_of_sort arg in
let ty = sort_of_sort cod in
let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in
let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in
let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in
VeritSyntax.add_fun s op;
op
let make_root_specconstant ra = function
| SpecConstsDec _ -> failwith "Smtlib2_genConstr.make_root_specconstant: decimals not implemented yet"
| SpecConstNum (_,s) ->
(try
let i = int_of_string s in
Atom.hatom_Z_of_int ra i
with
| Failure _ ->
let i = Big_int.big_int_of_string s in
Atom.hatom_Z_of_bigint ra i)
| SpecConstString _ -> failwith "Smtlib2_genConstr.make_root_specconstant: strings not implemented yet"
| SpecConstsHex _ -> failwith "Smtlib2_genConstr.make_root_specconstant: hexadecimals not implemented yet"
| SpecConstsBinary _ -> failwith "Smtlib2_genConstr.make_root_specconstant: binaries not implemented yet"
type atom_form = | Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
let make_root ra rf t =
let hlets = Hashtbl.create 17 in
let rec make_root_term = function
| TermSpecConst (_,c) -> Atom (make_root_specconstant ra c)
| TermQualIdentifier (_,id) ->
let v = string_of_qualidentifier id in
(try Hashtbl.find hlets v with
| Not_found ->
make_root_app v [])
| TermQualIdTerm (_,id,(_,l)) ->
let v = string_of_qualidentifier id in
make_root_app v l
| TermLetTerm (_,(_,l),t) ->
List.iter (fun (VarBindingSymTerm (_, sym, u)) ->
let u' = make_root_term u in
let s' = string_of_symbol sym in
Hashtbl.add hlets s' u') l;
make_root_term t
| TermForAllTerm _ -> failwith "Smtlib2_genConstr.make_root_term: ForAll not implemented yet"
| TermExistsTerm _ -> failwith "Smtlib2_genConstr.make_root_term: Exists not implemented yet"
| TermExclimationPt (_,t,_) -> make_root_term t
and make_root_app v l =
match (v,l) with
| "=", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' ->
(match Atom.type_of a' with
| Tbool -> Form (Form.get rf (Fapp (Fiff, [|Form.get rf (Fatom a'); Form.get rf (Fatom b')|])))
| ty -> Atom (Atom.mk_eq ra ty a' b'))
| _, _ -> assert false)
| "<", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_lt ra a' b')
| _, _ -> assert false)
| "<=", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_le ra a' b')
| _, _ -> assert false)
| ">", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_gt ra a' b')
| _, _ -> assert false)
| ">=", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_ge ra a' b')
| _, _ -> assert false)
| "+", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_plus ra a' b')
| _, _ -> assert false)
| "-", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_minus ra a' b')
| _, _ -> assert false)
| "*", [a;b] ->
(match make_root_term a, make_root_term b with
| Atom a', Atom b' -> Atom (Atom.mk_mult ra a' b')
| _, _ -> assert false)
| "-", [a] ->
(match make_root_term a with
| Atom a' -> Atom (Atom.mk_opp ra a')
| _ -> assert false)
| "distinct", _ ->
let make_h h =
match make_root_term h with
| Atom h' -> h'
| _ -> assert false in
let a = Array.make (List.length l) (make_h (List.hd l)) in
let i = ref (-1) in
List.iter (fun h ->
incr i;
a.(!i) <- make_h h) l;
Atom (Atom.mk_distinct ra (Atom.type_of a.(0)) a)
| "true", _ -> Form (Form.get rf Form.pform_true)
| "false", _ -> Form (Form.get rf Form.pform_false)
| "and", _ ->
Form (Form.get rf (Fapp (Fand, Array.of_list (List.map make_root l))))
| "or", _ ->
Form (Form.get rf (Fapp (For, Array.of_list (List.map make_root l))))
| "xor", _ ->
Form (Form.get rf (Fapp (Fxor, Array.of_list (List.map make_root l))))
| "=>", _ ->
Form (Form.get rf (Fapp (Fimp, Array.of_list (List.map make_root l))))
| "ite", _ ->
Form (Form.get rf (Fapp (Fite, Array.of_list (List.map make_root l))))
| "not", [a] -> Form (Form.neg (make_root a))
| _, _ ->
let op = VeritSyntax.get_fun v in
let l' = List.map (fun t -> match make_root_term t with
| Atom h -> h | Form _ -> assert false) l in
Atom (Atom.get ra (Aapp (op, Array.of_list l')))
and make_root t =
match make_root_term t with
| Atom h -> Form.get rf (Fatom h)
| Form f -> f in
make_root t
let declare_commands rt ro ra rf acc = function
| CDeclareSort (_,sym,_) -> let _ = declare_sort rt sym in acc
| CDeclareFun (_,sym, (_, arg), cod) ->
let _ = declare_fun rt ro sym arg cod in acc
| CAssert (_, t) -> (make_root ra rf t)::acc
| _ -> acc
|
