diff options
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 484ee2a50..62ddeb182 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -42,13 +42,15 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) +let eq_table_key = Names.eq_table_key eq_constant + let rec conv_val pb k v1 v2 cu = if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu and conv_whd pb k whd1 whd2 cu = match whd1, whd2 with - | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu + | Vsort s1, Vsort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu | Vprod p1, Vprod p2 -> let cu = conv_val CONV k (dom p1) (dom p2) cu in conv_fun pb k (codom p1) (codom p2) cu @@ -169,6 +171,13 @@ and conv_arguments k args1 args2 cu = !rcu else raise NotConvertible +let rec eq_puniverses f (x,l1) (y,l2) cu = + if f x y then conv_universes l1 l2 cu + else raise NotConvertible + +and conv_universes l1 l2 cu = + if Univ.Instance.eq l1 l2 then cu else raise NotConvertible + let rec conv_eq pb t1 t2 cu = if t1 == t2 then cu else @@ -179,7 +188,7 @@ let rec conv_eq pb t1 t2 cu = if Int.equal m1 m2 then cu else raise NotConvertible | Var id1, Var id2 -> if Id.equal id1 id2 then cu else raise NotConvertible - | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu + | Sort s1, Sort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu | Prod (_,t1,c1), Prod (_,t2,c2) -> @@ -192,12 +201,13 @@ let rec conv_eq pb t1 t2 cu = | Evar (e1,l1), Evar (e2,l2) -> if Evar.equal e1 e2 then conv_eq_vect l1 l2 cu else raise NotConvertible - | Const c1, Const c2 -> - if eq_constant c1 c2 then cu else raise NotConvertible + | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu + | Proj (p1,c1), Proj (p2,c2) -> + if eq_constant p1 p2 then conv_eq pb c1 c2 cu else raise NotConvertible | Ind c1, Ind c2 -> - if eq_ind c1 c2 then cu else raise NotConvertible + eq_puniverses eq_ind c1 c2 cu | Construct c1, Construct c2 -> - if eq_constructor c1 c2 then cu else raise NotConvertible + eq_puniverses eq_constructor c1 c2 cu | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> let pcu = conv_eq CONV p1 p2 cu in let ccu = conv_eq CONV c1 c2 pcu in @@ -221,14 +231,14 @@ and conv_eq_vect vt1 vt2 cu = let vconv pb env t1 t2 = infos := create_clos_infos betaiotazeta env; - let cu = - try conv_eq pb t1 t2 empty_constraint + let _cu = + try conv_eq pb t1 t2 (universes env) with NotConvertible -> let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in - let cu = conv_val pb (nb_rel env) v1 v2 empty_constraint in + let cu = conv_val pb (nb_rel env) v1 v2 (universes env) in cu - in cu + in () let _ = Reduction.set_vm_conv vconv |