From 1f1e441c320c1ed94e648f5e126cf2298a1eda00 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Mar 2007 16:17:42 +0000 Subject: [PATCH] Role of - replace - replace_lifting - replace_lifting_csc clarified with comments. None of this function is the inverse of subst :-) --- components/tactics/proofEngineReduction.ml | 23 ++++++++++++++++----- components/tactics/proofEngineReduction.mli | 21 +++++++++++++++++++ 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml index c359313dd..dbc98f722 100644 --- a/components/tactics/proofEngineReduction.ml +++ b/components/tactics/proofEngineReduction.ml @@ -122,7 +122,11 @@ let alpha_equivalence = 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 = @@ -182,8 +186,13 @@ let replace ~equality ~what ~with_what ~where = 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 = @@ -278,8 +287,12 @@ let replace_lifting ~equality ~what ~with_what ~where = 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 = diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli index c0318bdfe..39beb84aa 100644 --- a/components/tactics/proofEngineReduction.mli +++ b/components/tactics/proofEngineReduction.mli @@ -35,15 +35,36 @@ exception AlreadySimplified exception WhatAndWithWhatDoNotHaveTheSameLength;; val alpha_equivalence: Cic.term -> Cic.term -> bool + +(* 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. *) val replace : equality:('a -> Cic.term -> bool) -> what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term + +(* 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. *) val replace_lifting : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term + +(* 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. *) val replace_lifting_csc : int -> equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term + val subst_inv : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> int -> Cic.term -> Cic.term -- 2.39.2