From: Enrico Tassi Date: Mon, 31 Jan 2005 17:18:55 +0000 (+0000) Subject: added delift X-Git-Tag: V_0_1_0~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c9c376401844c389d682ba835845443105e4b1a;p=helm.git added delift --- diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 431fa4b50..cd9773160 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -104,6 +104,81 @@ 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 + (failwith "delifting this term whould capture free variables") + 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 9083212ae..1f0705881 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli @@ -33,6 +33,12 @@ exception ReferenceToInductiveDefinition;; (* lifts [t] of [n] *) 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 *) val lift_from: int -> int -> Cic.term -> Cic.term