From 5538a4548601ba1c1647ec9dc0fbbd875e5a93fd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Nov 2005 15:38:06 +0000 Subject: [PATCH] Yet another semantics for simplify. --- helm/ocaml/tactics/proofEngineReduction.ml | 48 ++++++++++++++-------- 1 file changed, 30 insertions(+), 18 deletions(-) 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 *) -- 2.39.2