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

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 6d198d4d1..f72ec4679 100644
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -46,8 +46,10 @@ exception WrongUriToInductiveDefinition;;
 exception WrongUriToConstant;;
 exception RelToHiddenHypothesis;;
 
+module C = Cic
+module S = CicSubstitution
+
 let alpha_equivalence =
- let module C = Cic in
   let rec aux t t' =
    if t = t' then true
    else
@@ -120,9 +122,12 @@ 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 module C = Cic in
   let find_image t =
    let rec find_image_aux =
     function
@@ -181,11 +186,14 @@ 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 module C = Cic in
- let module S = CicSubstitution in
   let find_image what t =
    let rec find_image_aux =
     function
@@ -279,11 +287,13 @@ 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 module C = Cic in
- let module S = CicSubstitution in
   let find_image t =
    let rec find_image_aux =
     function
@@ -373,12 +383,73 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
   substaux 1 where
 ;;
 
+(* 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 
+   in
+   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 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) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Var (uri, enss)
+      | C.Const (uri ,enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.Const (uri, enss)
+     | C.MutInd (uri, tyno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutInd (uri, tyno, enss)
+     | C.MutConstruct (uri, tyno, consno, enss) ->
+         let enss = List.map (subst_ens k) enss in
+         C.MutConstruct (uri, tyno, consno, enss)
+     | C.Meta (i, mss) -> 
+         let mss = List.map (subst_ms k) mss in
+         C.Meta(i, mss)
+     | C.Cast (t, v) -> C.Cast (subst_term k t, subst_term k v)
+     | C.Appl ts ->      
+         let ts = List.map (subst_term k) ts in
+         C.Appl ts
+     | C.MutCase (uri, tyno, outty, t, cases) ->
+         let cases = List.map (subst_term k) cases in
+	 C.MutCase (uri, tyno, subst_term k outty, subst_term k t, cases)
+     | C.Prod (n, v, t) ->
+        C.Prod (n, subst_term k v, subst_term (succ k) t)
+     | C.Lambda (n, v, t) ->
+        C.Lambda (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, t) ->
+        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.Fix (i, fixes) ->
+        let fixesno = List.length fixes in
+        let fixes = List.map (subst_fix fixesno k) fixes in
+        C.Fix (i, fixes)
+     | C.CoFix (i, cofixes) ->
+        let cofixesno = List.length cofixes in
+        let cofixes = List.map (subst_cofix cofixesno k) cofixes in
+         C.CoFix (i, cofixes)
+   and subst_ens k (uri, t) = uri, subst_term k t   
+   and subst_ms k = function
+      | None   -> None
+      | Some t -> Some (subst_term k t)
+   and subst_fix fixesno k (n, ind, ty, bo) =
+      n, ind, subst_term k ty, subst_term (k + fixesno) bo
+   and subst_cofix cofixesno k (n, ty, bo) =
+      n, subst_term k ty, subst_term (k + cofixesno) bo
+in
+subst_term
+   
+
+
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (match List.nth context (n-1) with
@@ -516,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' =
@@ -554,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' =
@@ -595,8 +674,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let module C = Cic in
- let module S = CicSubstitution in
  (* a simplified term is active if it can create a redex when used as an *)
  (* actual parameter                                                     *)
  let rec is_active =
@@ -750,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' =
@@ -788,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' =
@@ -805,8 +890,6 @@ let simpl context =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
  and try_delta_expansion context l term body =
-  let module C = Cic in
-  let module S = CicSubstitution in
    try
     let res,constant_args =
      let rec aux rev_constant_args l =