exception WhatAndWithWhatDoNotHaveTheSameLength;;
-(* "textual" replacement of several subterms with other ones *)
+(* Replaces "textually" in "where" every term in "what" with the corresponding
+ term in "with_what". The terms in "what" ARE NOT lifted when binders are
+ crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
+ Every free variable in "where" IS NOT lifted by nnn.
+*)
let replace ~equality ~what ~with_what ~where =
let find_image t =
let rec find_image_aux =
aux where
;;
-(* replaces in a term a term with another one. *)
-(* Lifting are performed as usual. *)
+(* Replaces in "where" every term in "what" with the corresponding
+ term in "with_what". The terms in "what" ARE lifted when binders are
+ crossed. The terms in "with_what" ARE lifted when binders are crossed.
+ Every free variable in "where" IS NOT lifted by nnn.
+ Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
+ inverse of subst up to the fact that free variables in "where" are NOT
+ lifted. *)
let replace_lifting ~equality ~what ~with_what ~where =
let find_image what t =
let rec find_image_aux =
substaux 1 what where
;;
-(* replaces in a term a list of terms with other ones. *)
-(* Lifting are performed as usual. *)
+(* Replaces in "where" every term in "what" with the corresponding
+ term in "with_what". The terms in "what" ARE NOT lifted when binders are
+ crossed. The terms in "with_what" ARE lifted when binders are crossed.
+ Every free variable in "where" IS lifted by nnn.
+ Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
+ inverse of subst up to the fact that "what" terms are NOT lifted. *)
let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
let find_image t =
let rec find_image_aux =
substaux 1 where
;;
-(* This is the inverse of the subst function. *)
-let subst_inv ~equality ~what =
+(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
+ up to the fact that the index to start from can be specified *)
+let replace_with_rel_1_from ~equality ~what =
let rec find_image t = function
| [] -> false
| hd :: tl -> equality t hd || find_image t tl
let rec subst_term k t =
if find_image t what then C.Rel k else inspect_term k t
and inspect_term k = function
- | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n)
+ | C.Rel i -> if i < k then C.Rel i else C.Rel (succ i)
| C.Sort _ as t -> t
| C.Implicit _ as t -> t
| C.Var (uri, enss) ->
if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let tys =
- List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' () =
let fl' =
| None -> if l = [] then t' () else C.Appl ((t' ())::l)
)
| C.CoFix (i,fl) ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' =
let fl' =
if l = [] then res else C.Appl (res::l)
)
| C.Fix (i,fl) ->
- let tys =
- List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' () =
let fl' =
| None -> if l = [] then t' () else C.Appl ((t' ())::l)
)
| C.CoFix (i,fl) ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+ let tys,_ =
+ List.fold_left
+ (fun (types,len) (n,ty,_) ->
+ (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ) ([],0) fl
in
let t' =
let fl' =