From 13f7f0dcaa42805d33003850a0eb94d1c277fddd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 14:27:39 +0000 Subject: [PATCH] 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. --- helm/ocaml/tactics/proofEngineReduction.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) 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) = -- 2.39.2