From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 12:22:34 +0000 (+0000) Subject: added to CicMetaSubst subst wrapper for CicReduction.are_convertible X-Git-Tag: V_0_5_1_4~20 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6696898978f86977863429cc3a8690d2546a918b;p=helm.git added to CicMetaSubst subst wrapper for CicReduction.are_convertible --- diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 04cf03c67..f8a73f2f5 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -483,6 +483,11 @@ let whd subst context term = raise (MetaSubstFailure ("Weak head reduction failure: " ^ Printexc.to_string e)) +let are_convertible subst context t1 t2 = + let context = apply_subst_context subst context in + let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in + CicReduction.are_convertible context t1 t2 + let type_of_aux' metasenv subst context term = let term = apply_subst subst term in let context = apply_subst_context subst context in diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 3d1032aa8..635825c7f 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -69,6 +69,10 @@ val ppsubst: substitution -> string * the calculus *) val whd: substitution -> Cic.context -> Cic.term -> Cic.term +val are_convertible: + substitution -> Cic.context -> Cic.term -> Cic.term -> + bool val type_of_aux': - Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term + Cic.metasenv -> substitution -> Cic.context -> Cic.term -> + Cic.term diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 50387922d..e0ec5cb44 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -51,7 +51,7 @@ let type_of_aux' metasenv subst context term = let rec fo_unif_subst subst context metasenv t1 t2 = let module C = Cic in - let module R = CicReduction in + let module R = CicMetaSubst in let module S = CicSubstitution in match (t1, t2) with (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> @@ -66,7 +66,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = (* First possibility: restriction *) (* Second possibility: unification *) (* Third possibility: convertibility *) - R.are_convertible context t1' t2' + R.are_convertible subst context t1' t2' ) true ln lm in if ok then @@ -165,14 +165,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 = | (C.MutConstruct _, _) | (_, C.MutConstruct _) | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) | (_, C.CoFix _) -> - if R.are_convertible context t1 t2 then + if R.are_convertible subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf "Can't unify %s with %s because they are not convertible" (CicPp.ppterm t1) (CicPp.ppterm t2))) | (_,_) -> - if R.are_convertible context t1 t2 then + if R.are_convertible subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf