From 01b776465cd1d0779e635a551da0c6ca77d05b70 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Dec 2002 14:29:52 +0000 Subject: [PATCH] Simplification euristic improved. It is now able to simplify a Fix which expands to an expressions which simplifiable Fixes therein. --- helm/gTopLevel/proofEngineReduction.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 21f2cbebf..04bfe9ae5 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -42,6 +42,7 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; exception WrongUriToInductiveDefinition;; +exception WrongUriToConstant;; exception RelToHiddenHypothesis;; let alpha_equivalence = @@ -475,7 +476,7 @@ exception AlreadySimplified;; (*CSC: It does not perform simplification in a Case *) let simpl context = (* reduceaux is equal to the reduceaux locally defined inside *) - (*reduce, but for the const case. *) + (* reduce, but for the const case. *) (**** Step 1 ****) let rec reduceaux context l = let module C = Cic in @@ -584,12 +585,15 @@ let simpl context = in (**** Step 3 ****) let term_to_fold = - match constant_args with - [] -> C.Const (uri,exp_named_subst') - | _ -> C.Appl ((C.Const(uri,exp_named_subst'))::constant_args) + let body' = CicSubstitution.subst_vars exp_named_subst' body in + match constant_args with + [] -> body' + | _ -> C.Appl (body'::constant_args) in - let reduced_term_to_fold = reduce context term_to_fold in - replace (=) reduced_term_to_fold term_to_fold res + let simplified_term_to_fold = + reduceaux context [] term_to_fold + in + replace (=) simplified_term_to_fold term_to_fold res with WrongShape -> (* The constant does not unfold to a Fix lambda-abstracted *) -- 2.39.2