X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineReduction.ml;h=f72ec4679842b9888bed5b07b9e92bc48fd50b28;hb=c465c17581bf606e0330cbd89b238279c184ad35;hp=c359313dd1e87e1ec88d1ef8684c46d6e48e3098;hpb=8ae990161006978a019f0afda4ff8d56a78d1fd0;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index c359313dd..f72ec4679 100644
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/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 =
@@ -370,8 +383,9 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
   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 
@@ -379,7 +393,7 @@ let subst_inv ~equality ~what =
    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) ->
@@ -573,8 +587,12 @@ let reduce context =
              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' =
@@ -611,8 +629,12 @@ let reduce context =
              | 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' =
@@ -805,8 +827,12 @@ let simpl context =
              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' =
@@ -843,8 +869,12 @@ let simpl context =
              | 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' =