diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:45:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 12:51:52 +0100 |
| commit | d041f19a7274b6065ca3ef565f0d8b8be08ef0d7 (patch) | |
| tree | 283194e5249935fb30580e7353e82072ea9caffd /kernel/nativeconv.ml | |
| parent | 76579aff8f8534cbc990b5ea2652b33655512213 (diff) | |
[native_compute] Fix handling of evars in conversion
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 6c755290d..bfa982136 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -60,7 +60,12 @@ and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu else match a1, a2 with - | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false + | Ameta (m1,_), Ameta (m2,_) -> + if Int.equal m1 m2 then cu else raise NotConvertible + | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + if Evar.equal ev1 ev2 then + Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu + else raise NotConvertible | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> @@ -112,7 +117,7 @@ and conv_atom env pb lvl a1 a2 cu = else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ - | Aproj _, _ -> raise NotConvertible + | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) and conv_fix env lvl t1 f1 t2 f2 cu = |