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

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 1502b600f..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,12 +674,22 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
+ (* a simplified term is active if it can create a redex when used as an *)
+ (* actual parameter                                                     *)
+ let rec is_active =
+  function
+     C.Lambda _
+   | C.MutConstruct _
+   | C.Appl (C.MutConstruct _::_)
+   | C.CoFix _ -> true
+   | C.Cast (bo,_) -> is_active bo
+   | C.LetIn _ -> assert false
+   | _ -> false
+ in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (* we never perform delta expansion automatically *)
@@ -653,9 +742,13 @@ let simpl context =
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
            C.Constant (_,Some body,_,_,_) ->
-            try_delta_expansion context l
-             (C.Const (uri,exp_named_subst'))
-             (CicSubstitution.subst_vars exp_named_subst' body)
+            if List.exists is_active l then
+             try_delta_expansion context l
+              (C.Const (uri,exp_named_subst'))
+              (CicSubstitution.subst_vars exp_named_subst' body)
+            else
+             let t' = C.Const (uri,exp_named_subst') in
+              if l = [] then t' else C.Appl (t'::l)
          | C.Constant (_,None,_,_,_) ->
             let t' = C.Const (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
@@ -701,7 +794,7 @@ let simpl context =
                reduceaux context tl' body'
          | t -> t
        in
-        (match decofix (CicReduction.whd context term) with
+        (match decofix (reduceaux context [] term) (*(CicReduction.whd context term)*) with
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
@@ -734,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' =
@@ -772,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' =
@@ -789,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 =
@@ -814,7 +913,7 @@ let simpl context =
              with
               _ -> raise AlreadySimplified
             in
-             (match CicReduction.whd context recparam with
+             (match reduceaux context [] recparam (*CicReduction.whd context recparam*) with
                  C.MutConstruct _
                | C.Appl ((C.MutConstruct _)::_) ->
                   let body' =
@@ -843,7 +942,7 @@ let simpl context =
       let simplified_term_to_fold =
        reduceaux context [] delta_expanded_term_to_fold
       in
-       replace (=) [simplified_term_to_fold] [term_to_fold] res
+       replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res
    with
       WrongShape ->
        (**** Step 3.2 ****)