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
|
open Util
open Names
open Environ
open Reduction
open Vm
open Vmvalues
open Csymtable
let val_of_constr env c =
val_of_constr (pre_env env) c
(* Test la structure des piles *)
let compare_zipper z1 z2 =
match z1, z2 with
| Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
| Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2)
| Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
| Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
let rec compare_stack stk1 stk2 =
match stk1, stk2 with
| [], [] -> true
| z1::stk1, z2::stk2 ->
if compare_zipper z1 z2 then compare_stack stk1 stk2
else false
| _, _ -> false
(* Conversion *)
let conv_vect fconv vect1 vect2 cu =
let n = Array.length vect1 in
if Int.equal n (Array.length vect2) then
let rcu = ref cu in
for i = 0 to n - 1 do
rcu := fconv vect1.(i) vect2.(i) !rcu
done;
!rcu
else raise NotConvertible
let rec conv_val env pb k v1 v2 cu =
if v1 == v2 then cu
else conv_whd env pb k (whd_val v1) (whd_val v2) cu
and conv_whd env pb k whd1 whd2 cu =
(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
match whd1, whd2 with
| Vuniv_level _ , _
| _ , Vuniv_level _ ->
(** Both of these are invalid since universes are handled via
** special cases in the code.
**)
assert false
| Vprod p1, Vprod p2 ->
let cu = conv_val env CONV k (dom p1) (dom p2) cu in
conv_fun env pb k (codom p1) (codom p2) cu
| Vfun f1, Vfun f2 -> conv_fun env CONV k f1 f2 cu
| Vfix (f1,None), Vfix (f2,None) -> conv_fix env k f1 f2 cu
| Vfix (f1,Some args1), Vfix(f2,Some args2) ->
if nargs args1 <> nargs args2 then raise NotConvertible
else conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)
| Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix env k cf1 cf2 cu
| Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->
if nargs args1 <> nargs args2 then raise NotConvertible
else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu)
| Vconstr_const i1, Vconstr_const i2 ->
if Int.equal i1 i2 then cu else raise NotConvertible
| Vconstr_block b1, Vconstr_block b2 ->
let tag1 = btag b1 and tag2 = btag b2 in
let sz = bsize b1 in
if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
let rcu = ref cu in
for i = 0 to sz - 1 do
rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
done;
!rcu
else raise NotConvertible
| Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
conv_atom env pb k a1 stk1 a2 stk2 cu
| Vfun _, _ | _, Vfun _ ->
(* on the fly eta expansion *)
conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
| Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
| Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
and conv_atom env pb k a1 stk1 a2 stk2 cu =
(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
match a1, a2 with
| Aind ((mi,i) as ind1) , Aind ind2 ->
if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
if Environ.polymorphic_ind ind1 env then
let mib = Environ.lookup_mind mi env in
let ulen =
match mib.Declarations.mind_universes with
| Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
| Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
| Declarations.Cumulative_ind cumi ->
Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
in
match stk1 , stk2 with
| [], [] -> assert (Int.equal ulen 0); cu
| Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
assert (ulen <= nargs args1);
assert (ulen <= nargs args2);
let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
let u1 = Univ.Instance.of_array u1 in
let u2 = Univ.Instance.of_array u2 in
let cu = convert_instances ~flex:false u1 u2 cu in
conv_arguments env ~from:ulen k args1 args2
(conv_stack env k stk1' stk2' cu)
| _, _ -> assert false (* Should not happen if problem is well typed *)
else
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Asort s1, Asort s2 ->
sort_cmp_universes env pb s1 s2 cu
| Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible
and conv_stack env k stk1 stk2 cu =
match stk1, stk2 with
| [], [] -> cu
| Zapp args1 :: stk1, Zapp args2 :: stk2 ->
conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
| Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
conv_stack env k stk1 stk2
(conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
| Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
if check_switch sw1 sw2 then
let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
let rcu = ref (conv_val env CONV k vt1 vt2 cu) in
let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
for i = 0 to Array.length b1 - 1 do
rcu :=
conv_val env CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
done;
conv_stack env k stk1 stk2 !rcu
else raise NotConvertible
| Zproj p1 :: stk1, Zproj p2 :: stk2 ->
if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
else raise NotConvertible
| [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
| Zproj _ :: _, _ -> raise NotConvertible
and conv_fun env pb k f1 f2 cu =
if f1 == f2 then cu
else
let arity,b1,b2 = decompose_vfun2 k f1 f2 in
conv_val env pb (k+arity) b1 b2 cu
and conv_fix env k f1 f2 cu =
if f1 == f2 then cu
else
if check_fix f1 f2 then
let bf1, tf1 = reduce_fix k f1 in
let bf2, tf2 = reduce_fix k f2 in
let cu = conv_vect (conv_val env CONV k) tf1 tf2 cu in
conv_vect (conv_fun env CONV (k + Array.length tf1)) bf1 bf2 cu
else raise NotConvertible
and conv_cofix env k cf1 cf2 cu =
if cf1 == cf2 then cu
else
if check_cofix cf1 cf2 then
let bcf1, tcf1 = reduce_cofix k cf1 in
let bcf2, tcf2 = reduce_cofix k cf2 in
let cu = conv_vect (conv_val env CONV k) tcf1 tcf2 cu in
conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
else raise NotConvertible
and conv_arguments env ?from:(from=0) k args1 args2 cu =
if args1 == args2 then cu
else
let n = nargs args1 in
if Int.equal n (nargs args2) then
let rcu = ref cu in
for i = from to n - 1 do
rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
done;
!rcu
else raise NotConvertible
let vm_conv_gen cv_pb env univs t1 t2 =
try
let v1 = val_of_constr env t1 in
let v2 = val_of_constr env t2 in
fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
with Not_found | Invalid_argument _ ->
warn_bytecode_compiler_failed ();
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
full_transparent_state env univs t1 t2
let vm_conv cv_pb env t1 t2 =
let univs = Environ.universes env in
let b =
if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
else Constr.eq_constr_univs univs t1 t2
in
if not b then
let univs = (univs, checked_universes) in
let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv
|
