diff options
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 84 |
1 files changed, 42 insertions, 42 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 7c515735..a35d1d88 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -3,10 +3,10 @@ open Declarations open Term open Environ open Conv_oracle -open Reduction +open Reduction open Closure open Vm -open Csymtable +open Csymtable open Univ let val_of_constr env c = @@ -27,7 +27,7 @@ let rec compare_stack stk1 stk2 = | z1::stk1, z2::stk2 -> if compare_zipper z1 z2 then compare_stack stk1 stk2 else false - | _, _ -> false + | _, _ -> false (* Conversion *) let conv_vect fconv vect1 vect2 cu = @@ -42,13 +42,13 @@ let conv_vect fconv vect1 vect2 cu = let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) -let rec conv_val pb k v1 v2 cu = - if v1 == v2 then cu +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 = + +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 -> sort_cmp pb s1 s2 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 @@ -58,11 +58,11 @@ and conv_whd pb k whd1 whd2 cu = if nargs args1 <> nargs args2 then raise NotConvertible else conv_arguments k args1 args2 (conv_fix k f1 f2 cu) | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu - | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) -> + | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) -> if nargs args1 <> nargs args2 then raise NotConvertible else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) - | Vconstr_const i1, Vconstr_const i2 -> - if i1 = i2 then cu else raise NotConvertible + | Vconstr_const i1, Vconstr_const i2 -> + if i1 = i2 then cu else raise NotConvertible | Vconstr_block b1, Vconstr_block b2 -> let sz = bsize b1 in if btag b1 = btag b2 && sz = bsize b2 then @@ -72,33 +72,33 @@ and conv_whd pb k whd1 whd2 cu = done; !rcu else raise NotConvertible - | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> + | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom pb k a1 stk1 a2 stk2 cu - | _, Vatom_stk(Aiddef(_,v),stk) -> + | _, Vatom_stk(Aiddef(_,v),stk) -> conv_whd pb k whd1 (force_whd v stk) cu - | Vatom_stk(Aiddef(_,v),stk), _ -> + | Vatom_stk(Aiddef(_,v),stk), _ -> conv_whd pb k (force_whd v stk) whd2 cu | _, _ -> raise NotConvertible and conv_atom pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind (kn1,i1), Aind(kn2,i2) -> - if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 then conv_stack k stk1 stk2 cu else raise NotConvertible - | Aid ik1, Aid ik2 -> - if ik1 = ik2 && compare_stack stk1 stk2 then - conv_stack k stk1 stk2 cu + | Aid ik1, Aid ik2 -> + if ik1 = ik2 && compare_stack stk1 stk2 then + conv_stack k stk1 stk2 cu else raise NotConvertible | Aiddef(ik1,v1), Aiddef(ik2,v2) -> begin try - if ik1 = ik2 && compare_stack stk1 stk2 then - conv_stack k stk1 stk2 cu + if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then + conv_stack k stk1 stk2 cu else raise NotConvertible with NotConvertible -> - if oracle_order ik1 ik2 then + if oracle_order ik1 ik2 then conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu end @@ -106,15 +106,15 @@ and conv_atom pb k a1 stk1 a2 stk2 cu = conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu | _, Aiddef(ik2,v2) -> conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu - | _, _ -> raise NotConvertible - + | _, _ -> raise NotConvertible + and conv_stack k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) + conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> - conv_stack k stk1 stk2 + conv_stack k stk1 stk2 (conv_arguments k args1 args2 (conv_fix k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then @@ -122,7 +122,7 @@ and conv_stack k stk1 stk2 cu = let rcu = ref (conv_val 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 := + rcu := conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu done; conv_stack k stk1 stk2 !rcu @@ -136,7 +136,7 @@ and conv_fun pb k f1 f2 cu = conv_val pb (k+arity) b1 b2 cu and conv_fix k f1 f2 cu = - if f1 == f2 then cu + if f1 == f2 then cu else if check_fix f1 f2 then let bf1, tf1 = reduce_fix k f1 in @@ -168,34 +168,34 @@ and conv_arguments k args1 args2 cu = else raise NotConvertible let rec conv_eq pb t1 t2 cu = - if t1 == t2 then cu + if t1 == t2 then cu else match kind_of_term t1, kind_of_term t2 with - | Rel n1, Rel n2 -> + | Rel n1, Rel n2 -> if n1 = n2 then cu else raise NotConvertible | Meta m1, Meta m2 -> if m1 = m2 then cu else raise NotConvertible - | Var id1, Var id2 -> + | Var id1, Var id2 -> if id1 = id2 then cu else raise NotConvertible | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu - | Prod (_,t1,c1), Prod (_,t2,c2) -> + | Prod (_,t1,c1), Prod (_,t2,c2) -> conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu) | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> conv_eq pb c1 c2 (conv_eq CONV b1 b2 cu) | App (c1,l1), App (c2,l2) -> conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu) | Evar (e1,l1), Evar (e2,l2) -> if e1 = e2 then conv_eq_vect l1 l2 cu else raise NotConvertible - | Const c1, Const c2 -> - if c1 = c2 then cu else raise NotConvertible - | Ind c1, Ind c2 -> - if c1 = c2 then cu else raise NotConvertible - | Construct c1, Construct c2 -> - if c1 = c2 then cu else raise NotConvertible + | Const c1, Const c2 -> + if eq_constant c1 c2 then cu else raise NotConvertible + | Ind c1, Ind c2 -> + if eq_ind c1 c2 then cu else raise NotConvertible + | Construct c1, Construct c2 -> + if eq_constructor c1 c2 then cu else raise NotConvertible | 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 @@ -203,7 +203,7 @@ let rec conv_eq pb t1 t2 cu = | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu) else raise NotConvertible - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu) else raise NotConvertible | _ -> raise NotConvertible @@ -216,7 +216,7 @@ and conv_eq_vect vt1 vt2 cu = rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu done; !rcu else raise NotConvertible - + let vconv pb env t1 t2 = let cu = try conv_eq pb t1 t2 Constraint.empty @@ -227,7 +227,7 @@ let vconv pb env t1 t2 = let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in cu in cu - + let _ = Reduction.set_vm_conv vconv let use_vm = ref false @@ -236,7 +236,7 @@ let set_use_vm b = use_vm := b; if b then Reduction.set_default_conv vconv else Reduction.set_default_conv Reduction.conv_cmp - + let use_vm _ = !use_vm |