X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineReduction.ml;h=6d198d4d133e721539c30e77d86196787ff6c1b5;hb=9fa0f092e8c7500a3890a73893483b44c56db171;hp=0dc4ce4ee3e617a1b1cb6a98efa6dc68db8e922b;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 0dc4ce4ee..6d198d4d1 100644
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -595,12 +595,24 @@ 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 =
+  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 +665,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 +717,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) =
@@ -814,7 +830,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 +859,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 ****)
@@ -859,10 +875,11 @@ let simpl context =
          | C.LetIn (_,s,t) -> aux l (S.subst s t)
          | t ->
             let simplified = reduceaux context l t in
-            if t = simplified then
-             raise AlreadySimplified
-            else
-             simplified
+            let t' = if l = [] then t else C.Appl (t::l) in
+             if t' = simplified then
+              raise AlreadySimplified
+             else
+              simplified
        in
         (try aux l body
          with