some experiments

[helm.git] / components / tactics / proofEngineReduction.ml

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index 0dc4ce4ee3e617a1b1cb6a98efa6dc68db8e922b..1db075c70d96455a80c15ab49865eb3a02cde7be 100644 (file)
--- a/components/tactics/proofEngineReduction.ml
+++ b/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' =
@@ -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