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
227
228
229
230
231
232
233
234
235
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2019 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open SmtMisc
open CoqTerms
(** Syntaxified version of Coq type *)
type indexed_type = Term.constr gen_hashed
let dummy_indexed_type i = {index = i; hval = Term.mkProp}
let indexed_type_index i = i.index
let indexed_type_hval i = i.hval
type btype =
| TZ
| Tbool
| Tpositive
| TBV of int
| TFArray of btype * btype
| Tindex of indexed_type
let index_tbl = Hashtbl.create 17
let index_to_coq i =
try Hashtbl.find index_tbl i
with Not_found ->
let interp = mklApp cTindex [|mkInt i|] in
Hashtbl.add index_tbl i interp;
interp
let indexed_type_of_int i =
{index = i; hval = index_to_coq i }
let rec equal t1 t2 =
match t1,t2 with
| Tindex i, Tindex j -> i.index == j.index
| TBV i, TBV j -> i == j
| TFArray (ti, te), TFArray (ti', te') -> equal ti ti' && equal te te'
| _ -> t1 == t2
let rec to_coq = function
| TZ -> Lazy.force cTZ
| Tbool -> Lazy.force cTbool
| Tpositive -> Lazy.force cTpositive
| TBV n -> mklApp cTBV [|mkN n|]
| Tindex i -> index_to_coq i.index
| TFArray (ti, te) ->
mklApp cTFArray [|to_coq ti; to_coq te|]
let rec to_smt fmt = function
| TZ -> Format.fprintf fmt "Int"
| Tbool -> Format.fprintf fmt "Bool"
| Tpositive -> Format.fprintf fmt "Int"
| TBV i -> Format.fprintf fmt "(_ BitVec %i)" i
| Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
| TFArray (ti, te) ->
Format.fprintf fmt "(Array %a %a)" to_smt ti to_smt te
let rec logic = function
| TZ | Tpositive -> SL.singleton LLia
| Tbool -> SL.empty
| TBV _ -> SL.singleton LBitvectors
| Tindex _ -> SL.singleton LUF
| TFArray (ti, te) -> SL.add LArrays (SL.union (logic ti) (logic te))
(* reify table *)
type reify_tbl =
{ mutable count : int;
tbl : (Term.constr, btype) Hashtbl.t;
mutable cuts : (Structures.names_id * Term.types) list;
unsup_tbl : (btype, btype) Hashtbl.t;
}
let create () =
let htbl = Hashtbl.create 17 in
Hashtbl.add htbl (Lazy.force cZ) TZ;
Hashtbl.add htbl (Lazy.force cbool) Tbool;
(* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
{ count = 0;
tbl = htbl;
cuts = [];
unsup_tbl = Hashtbl.create 17;
}
(* Should we give a way to clear it? *)
let op_coq_types = Hashtbl.create 17
let get_coq_type_op = Hashtbl.find op_coq_types
(* let logic_of_coq reify t = logic (of_coq reify t) *)
let interp_tbl reify =
let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_compdec) in
let set _ = function
| Tindex it -> t.(it.index) <- it.hval
| _ -> () in
Hashtbl.iter set reify.tbl;
Structures.mkArray (Lazy.force ctyp_compdec, t)
let to_list reify =
let set _ t acc = match t with
| Tindex it -> (it.index,it)::acc
| _ -> acc in
Hashtbl.fold set reify.tbl []
let make_t_i rt = interp_tbl rt
(* let interp_t t_i t =
* mklApp cinterp_t [|t_i ; to_coq t|] *)
let dec_interp t_i t =
mklApp cdec_interp [|t_i ; to_coq t|]
let ord_interp t_i t =
mklApp cord_interp [|t_i ; to_coq t|]
let comp_interp t_i t =
mklApp ccomp_interp [|t_i ; to_coq t|]
let inh_interp t_i t =
mklApp cinh_interp [|t_i ; to_coq t|]
let rec interp t_i = function
| TZ -> Lazy.force cZ
| Tbool -> Lazy.force cbool
| Tpositive -> Lazy.force cpositive
| TBV n -> mklApp cbitvector [|mkN n|]
| Tindex c -> mklApp cte_carrier [|c.hval|]
(* | TFArray _ as t -> interp_t t_i t *)
| TFArray (ti,te) ->
mklApp cfarray [| interp t_i ti; interp t_i te;
ord_interp t_i ti; inh_interp t_i te |]
let interp_to_coq reify t = interp (make_t_i reify) t
let get_cuts reify = reify.cuts
let declare reify t typ_compdec =
(* TODO: allows to have only typ_compdec *)
assert (not (Hashtbl.mem reify.tbl t));
let res = Tindex {index = reify.count; hval = typ_compdec} in
Hashtbl.add reify.tbl t res;
reify.count <- reify.count + 1;
res
exception Unknown_type of btype
let check_known ty known_logic =
let l = logic ty in
if not (SL.subset l known_logic) then raise (Unknown_type ty)
else ty
let rec compdec_btype reify = function
| Tbool -> Lazy.force cbool_compdec
| TZ -> Lazy.force cZ_compdec
| Tpositive -> Lazy.force cPositive_compdec
| TBV s -> mklApp cBV_compdec [|mkN s|]
| TFArray (ti, te) ->
mklApp cFArray_compdec
[|interp_to_coq reify ti; interp_to_coq reify te;
compdec_btype reify ti; compdec_btype reify te|]
| Tindex i ->
let c, args = Term.decompose_app i.hval in
if Term.eq_constr c (Lazy.force cTyp_compdec) then
match args with
| [_; tic] -> tic
| _ -> assert false
else assert false
let declare_and_compdec reify t ty =
try Hashtbl.find reify.unsup_tbl ty
with Not_found ->
let res =
declare reify t (mklApp cTyp_compdec [|t; compdec_btype reify ty|])
in
Hashtbl.add reify.unsup_tbl ty res;
res
let rec of_coq reify known_logic t =
try
let c, args = Term.decompose_app t in
if Term.eq_constr c (Lazy.force cbool) ||
Term.eq_constr c (Lazy.force cTbool) then Tbool
else if Term.eq_constr c (Lazy.force cZ) ||
Term.eq_constr c (Lazy.force cTZ) then
check_known TZ known_logic
else if Term.eq_constr c (Lazy.force cpositive) ||
Term.eq_constr c (Lazy.force cTpositive) then
check_known Tpositive known_logic
else if Term.eq_constr c (Lazy.force cbitvector) ||
Term.eq_constr c (Lazy.force cTBV) then
match args with
| [s] -> check_known (TBV (mk_bvsize s)) known_logic
| _ -> assert false
else if Term.eq_constr c (Lazy.force cfarray) ||
Term.eq_constr c (Lazy.force cTFArray) then
match args with
| ti :: te :: _ ->
let ty = TFArray (of_coq reify known_logic ti,
of_coq reify known_logic te) in
check_known ty known_logic
| _ -> assert false
else
try Hashtbl.find reify.tbl t
with Not_found ->
let n = string_of_int (List.length reify.cuts) in
let compdec_name = Names.id_of_string ("CompDec"^n) in
let compdec_var = Term.mkVar compdec_name in
let compdec_type = mklApp cCompDec [| t |]in
reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
let ce = mklApp cTyp_compdec [|t; compdec_var|] in
let ty = declare reify t ce in
(match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false);
ty
with Unknown_type ty ->
try Hashtbl.find reify.tbl t
with Not_found -> declare_and_compdec reify t ty
|
