diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 179 |
1 files changed, 10 insertions, 169 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 410f8aa08..eb798ee44 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -20,6 +20,7 @@ open Environ open Instantiate open Closure open Esubst +open Reduction exception Elimconst @@ -459,10 +460,6 @@ type conversion_function = type conversion_test = constraints -> constraints -exception NotConvertible - -(* Convertibility of sorts *) - type conv_pb = | CONV | CUMUL @@ -493,169 +490,12 @@ let base_sort_cmp pb s0 s1 = | (Type u1, Type u2) -> true | (_, _) -> false -(* Conversion between [lft1]term1 and [lft2]term2 *) -let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = - eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) cuniv - -(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *) -and eqappr cv_pb infos appr1 appr2 cuniv = - let (lft1,(n1,hd1,v1)) = appr1 - and (lft2,(n2,hd2,v2)) = appr2 in - let el1 = el_shft n1 lft1 - and el2 = el_shft n2 lft2 in - match (fterm_of hd1, fterm_of hd2) with - (* case of leaves *) - | (FAtom a1, FAtom a2) -> - (match kind_of_term a1, kind_of_term a2 with - | (Sort s1, Sort s2) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then sort_cmp cv_pb s1 s2 cuniv - else raise NotConvertible - | (Meta n, Meta m) -> - if n=m - then convert_stacks infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - | _ -> raise NotConvertible) - - (* 2 index known to be bound to no constant *) - | (FRel n, FRel m) -> - if reloc_rel n el1 = reloc_rel m el2 - then convert_stacks infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - - (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *) - | (FFlex fl1, FFlex fl2) -> - (try (* try first intensional equality *) - if fl1 = fl2 - then - convert_stacks infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - with NotConvertible -> - (* else expand the second occurrence (arbitrary heuristic) *) - match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb infos appr1 - (lft2, fhnf_apply infos n2 def2 v2) cuniv - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr cv_pb infos - (lft1, fhnf_apply infos n1 def1 v1) appr2 cuniv - | None -> raise NotConvertible)) - - (* only one constant, existential, defined var or defined rel *) - | (FFlex fl1, _) -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) - appr2 cuniv - | None -> raise NotConvertible) - | (_, FFlex fl2) -> - (match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb infos appr1 - (lft2, fhnf_apply infos n2 def2 v2) - cuniv - | None -> raise NotConvertible) - - (* other constructors *) - | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then - let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in - ccnv CONV infos - (el_lift el1) (el_lift el2) c2 c'2 u1 - else raise NotConvertible - - | (FLetIn _, _) | (_, FLetIn _) -> - anomaly "LetIn normally removed by fhnf" - - | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) -> - if stack_args_size v1 = 0 && stack_args_size v2 = 0 - then (* Luo's system *) - let u1 = ccnv CONV infos el1 el2 c1 c'1 cuniv in - ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 u1 - else raise NotConvertible - - (* Inductive types: Ind Construct Case Fix Cofix *) - - (* Les annotations du Case ne servent qu'à l'affichage *) - - | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) -> - let u1 = ccnv CONV infos el1 el2 p1 p2 cuniv in - let u2 = ccnv CONV infos el1 el2 c1 c2 u1 in - let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in - convert_stacks infos lft1 lft2 v1 v2 u3 - - | (FInd op1, FInd op2) -> - if op1 = op2 - then convert_stacks infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - - | (FConstruct op1, FConstruct op2) -> - if op1 = op2 - then convert_stacks infos lft1 lft2 v1 v2 cuniv - else raise NotConvertible - - | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) -> - if op1 = op2 - then - let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in - let n = Array.length cl1 in - let u2 = - convert_vect infos - (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in - convert_stacks infos lft1 lft2 v1 v2 u2 - else raise NotConvertible - - | (FCoFix (op1,(_,tys1,cl1),_,_), FCoFix(op2,(_,tys2,cl2),_,_)) -> - if op1 = op2 - then - let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in - let n = Array.length cl1 in - let u2 = - convert_vect infos - (el_liftn n el1) (el_liftn n el2) cl1 cl2 u1 in - convert_stacks infos lft1 lft2 v1 v2 u2 - else raise NotConvertible - - | _ -> raise NotConvertible - -and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = - match (decomp_stack stk1, decomp_stack stk2) with - (Some(a1,s1), Some(a2,s2)) -> - let u1 = ccnv CONV infos lft1 lft2 a1 a2 cuniv in - convert_stacks infos lft1 lft2 s1 s2 u1 - | (None, None) -> cuniv - | _ -> raise NotConvertible - -and convert_vect infos lft1 lft2 v1 v2 cuniv = - let lv1 = Array.length v1 in - let lv2 = Array.length v2 in - if lv1 = lv2 - then - let rec fold n univ = - if n >= lv1 then univ - else - let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in - fold (n+1) u1 in - fold 0 cuniv - else raise NotConvertible - - - -let fconv cv_pb env sigma t1 t2 = - if eq_constr t1 t2 then - Constraint.empty - else - let infos = create_clos_infos hnf_flags env in - ccnv cv_pb infos ELID ELID - (inject (nf_evar sigma t1)) - (inject (nf_evar sigma t2)) - Constraint.empty -let conv env = fconv CONV env -let conv_leq env = fconv CUMUL env +let conv env sigma t1 t2 = + Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2) +let conv_leq env sigma t1 t2 = + Reduction.conv env (nf_evar sigma t1) (nf_evar sigma t2) +let fconv = function CONV -> conv | CUMUL -> conv_leq (* let convleqkey = Profile.declare_profile "conv_leq";; @@ -680,10 +520,11 @@ let conv_forall2_i f env sigma v1 v2 = v1 v2 let test_conversion f env sigma x y = - try let _ = f env sigma x y in true with NotConvertible -> false + try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true + with NotConvertible -> false -let is_conv env sigma = test_conversion conv env sigma -let is_conv_leq env sigma = test_conversion conv_leq env sigma +let is_conv env sigma = test_conversion Reduction.conv env sigma +let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq (********************************************************************) |