From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 14:27:39 +0000 (+0000)
Subject: New strategy for let-in unfolding (aka zeta reduction): a reference to a
X-Git-Tag: V_0_1_2_1~104
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13f7f0dcaa42805d33003850a0eb94d1c277fddd;p=helm.git

New strategy for let-in unfolding (aka zeta reduction): a reference to a
let-bound variable is expanded if and only if the simplified form of its definiendum (applied to the actual arguments) is different from the
non-simplified form.
---

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index d04acd181..087d32775 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -583,8 +583,11 @@ exception AlreadySimplified;;
 
 (* Takes a well-typed term and                                               *)
 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
+(*     Zeta-reduction is performed if and only if the simplified form of its *)
+(*     definiendum (applied to the actual arguments) is different from the   *)
+(*      non-simplified form.                                                 *)
 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
-(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it  *)
+(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it*)
 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
@@ -610,7 +613,14 @@ let simpl context =
          match List.nth context (n-1) with
             Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
           | Some (_,C.Def (bo,_)) ->
-             try_delta_expansion context l t (S.lift n bo)
+             let lifted_bo = S.lift n bo in
+             let applied_lifted_bo =
+              if l = [] then lifted_bo else C.Appl (lifted_bo::l) in
+             let simplified = try_delta_expansion context l t lifted_bo in
+              if simplified = applied_lifted_bo then
+               if l = [] then t else C.Appl (t::l)
+              else
+               simplified
 	  | None -> raise RelToHiddenHypothesis
         with
          Failure _ -> assert false)
@@ -714,7 +724,7 @@ let simpl context =
                 reduceaux context tl body'
          | t -> t
        in
-        (match decofix (reduceaux context [] term) with
+        (match decofix (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) =