From 17cc9a1c6353a5a57562434e9938fb54ca78b9c6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Jun 2005 15:04:49 +0000 Subject: [PATCH] CicSubstitution.delift ==> CicMetaSubst.delift_rels (since it will need to restrict metavariables in case of Rel capture) --- .../cic_proof_checking/cicSubstitution.ml | 76 ------------------ .../cic_proof_checking/cicSubstitution.mli | 8 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 77 +++++++++++++++++++ helm/ocaml/cic_unification/cicMetaSubst.mli | 7 ++ helm/ocaml/cic_unification/cicRefine.ml | 8 +- 5 files changed, 90 insertions(+), 86 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 229da24f0..2abce6a0e 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -29,7 +29,6 @@ exception ReferenceToVariable;; exception ReferenceToConstant;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; -exception DeliftingWouldCaptureAFreeVariable;; let debug_print = fun _ -> () @@ -107,81 +106,6 @@ let lift n t = lift_from 1 n t ;; -(* delifts a term t of n levels strating from k, that is changes (Rel m) - * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails - *) -let delift_from k n = - let rec liftaux k = - let module C = Cic in - function - C.Rel m -> - if m < k then - C.Rel m - else if m < k + n then - raise DeliftingWouldCaptureAFreeVariable - else - C.Rel (m - n) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i,l) -> - let l' = - List.map - (function - None -> None - | Some t -> Some (liftaux k t) - ) l - in - C.Meta(i,l') - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (liftaux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst - in - C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst - in - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, liftaux k outty, liftaux k t, - List.map (liftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - liftaux k - -let delift n t = - delift_from 1 n t - let subst arg = let rec substaux k = let module C = Cic in diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli index 5c8fa7ca5..21a1f5d0e 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -28,17 +28,13 @@ exception RelToHiddenHypothesis;; exception ReferenceToVariable;; exception ReferenceToConstant;; exception ReferenceToInductiveDefinition;; -exception DeliftingWouldCaptureAFreeVariable;; (* lift n t *) (* lifts [t] of [n] *) +(* NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *) +(* since it needs to restrict the metavariables in case of failure *) val lift : int -> Cic.term -> Cic.term -(** delifts t of n - * @raise Failure s - *) -val delift : int -> Cic.term -> Cic.term - (* lift from n t *) (* as lift but lifts only indexes >= from *) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index eaa094fdc..021e87ea5 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -71,6 +71,7 @@ context length: %d (avg = %.2f) exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string +exception DeliftingARelWouldCaptureAFreeVariable;; let debug_print = fun _ -> () @@ -757,6 +758,82 @@ debug_print(sprintf res, metasenv, subst ;; +(* delifts a term t of n levels strating from k, that is changes (Rel m) + * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails + *) +let delift_rels_from k n = + let rec liftaux k = + let module C = Cic in + function + C.Rel m -> + if m < k then + C.Rel m + else if m < k + n then + raise DeliftingARelWouldCaptureAFreeVariable + else + C.Rel (m - n) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (liftaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (liftaux k) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, liftaux k outty, liftaux k t, + List.map (liftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + liftaux k + +let delift_rels n t = + delift_rels_from 1 n t + + (**** END OF DELIFT ****) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 9a0bee6ae..04e493ec2 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -26,6 +26,7 @@ exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string +exception DeliftingARelWouldCaptureAFreeVariable;; (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) @@ -50,6 +51,12 @@ val delift : val restrict : Cic.substitution -> (int * int) list -> Cic.metasenv -> Cic.metasenv * Cic.substitution + +(** delifts the Rels in t of n + * @raise DeliftingARelWouldCaptureAFreeVariable + *) +val delift_rels : int -> Cic.term -> Cic.term + (** {2 Pretty printers} *) val ppsubst_unfolded: Cic.substitution -> string diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 57e4c5e9d..e64499b3b 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -507,7 +507,7 @@ and type_of_aux' metasenv context t ugraph = | (constructor_args_no,_,instance,_)::tl -> try let instance' = - CicSubstitution.delift constructor_args_no + CicMetaSubst.delift_rels constructor_args_no (CicMetaSubst.apply_subst subst instance) in let candidate,ugraph,metasenv,subst = @@ -519,7 +519,7 @@ and type_of_aux' metasenv context t ugraph = | Some ty -> try let instance' = - CicSubstitution.delift + CicMetaSubst.delift_rels constructor_args_no (CicMetaSubst.apply_subst subst instance) in @@ -529,7 +529,7 @@ and type_of_aux' metasenv context t ugraph = in candidate_oty,ugraph,metasenv,subst with - CicSubstitution.DeliftingWouldCaptureAFreeVariable + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> None,ugraph,metasenv,subst @@ -549,7 +549,7 @@ and type_of_aux' metasenv context t ugraph = Some (add_lambdas 0 t arity_instantiated_with_left_args), ugraph,metasenv,subst - with CicSubstitution.DeliftingWouldCaptureAFreeVariable -> + with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> None,ugraph4,metasenv,subst in match candidate with -- 2.39.2