From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Nov 2005 15:38:06 +0000 (+0000)
Subject: Yet another semantics for simplify.
X-Git-Tag: V_0_7_2_3~102
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;p=helm.git

Yet another semantics for simplify.
---

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index fc3bfd3b8..62c2adab5 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -583,21 +583,20 @@ 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*)
 (*     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   *)
+(*     is applied again to the new redex; Step 3.1) is applied to the result *)
 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
 (*     reduced, than the delta-reductions fails and the delta-redex is       *)
 (*     not reduced. Otherwise, if the delta-residual is not the              *)
-(*     lambda-abstraction of a Fix, then it is reduced and the result is     *)
-(*     directly returned, without performing step 3).                        *) 
-(*  3) Folds the application of the constant to the arguments that did not   *)
+(*     lambda-abstraction of a Fix, then it performs step 3.2).              *)
+(* 3.1) Folds the application of the constant to the arguments that did not  *)
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
+(* 3.2) Computes the head beta-zeta normal form of the term. Then it tries   *)
+(*     reductions. If the reduction cannot be performed, it returns the      *)
+(*     original term (not the head beta-zeta normal form of the definiendum) *)
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
@@ -621,13 +620,7 @@ 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,_)) ->
-             let lifted_bo = S.lift n bo in
-             let applied_lifted_bo = mk_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
+             try_delta_expansion context l t (S.lift n bo)
 	  | None -> raise RelToHiddenHypothesis
         with
          Failure _ -> assert false)
@@ -868,7 +861,7 @@ let simpl context =
      in
       aux [] l body
     in
-     (**** Step 3 ****)
+     (**** Step 3.1 ****)
      let term_to_fold, delta_expanded_term_to_fold =
       match constant_args with
          [] -> term,body
@@ -880,9 +873,28 @@ let simpl context =
        replace (=) [simplified_term_to_fold] [term_to_fold] res
    with
       WrongShape ->
-       (* The constant does not unfold to a Fix lambda-abstracted  *)
-       (* w.r.t. zero or more variables. We just perform reduction.*)
-       reduceaux context l body
+       (**** Step 3.2 ****)
+       let rec aux l =
+        function
+           C.Lambda (name,s,t) ->
+             (match l with
+                [] -> raise AlreadySimplified
+              | he::tl ->
+                 (* when name is Anonimous the substitution should *)
+                 (* be superfluous                                 *)
+                 aux tl (S.subst he t))
+         | 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
+       in
+        (try aux l body
+         with
+          AlreadySimplified ->
+           if l = [] then term else C.Appl (term::l))
     | AlreadySimplified ->
        (* If we performed delta-reduction, we would find a Fix   *)
        (* not applied to a constructor. So, we refuse to perform *)