From 9135f92fe15418abd2c2ae81ab155a2517bc72ea Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 1 Jun 2006 07:31:25 +0000 Subject: [PATCH] Subsumption_subst must be applied to the initial proof before passing it to build_proof_goal. --- .../components/tactics/paramodulation/equality.ml | 15 ++++++++++++--- .../tactics/paramodulation/equality.mli | 1 + .../tactics/paramodulation/inference.ml | 4 ++-- .../tactics/paramodulation/saturation.ml | 7 ++++--- 4 files changed, 19 insertions(+), 8 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 2561ea56f..3979c0529 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -422,7 +422,14 @@ let contextualize_rewrites t ty = let eq,ty,l,r = open_eq ty in contextualize eq ty l r t ;; - + +let add_subst subst = + function + | Exact t -> Exact (Subst.apply_subst subst t) + | Step (s,(rule, id1, (pos,id2), pred)) -> + Step (Subst.concat subst s,(rule, id1, (pos,id2), pred)) +;; + let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred = let p1 = Subst.apply_subst_lift lift subst p1 in let p2 = Subst.apply_subst_lift lift subst p2 in @@ -722,8 +729,9 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), - se + (proof,se) + (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), + se *) ;; let refl_proof ty term = @@ -756,6 +764,7 @@ let relocate newmeta menv to_be_relocated = let fix_metas newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in let to_be_relocated = +(* List.map (fun i ,_,_ -> i) menv *) HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term left @ Utils.metas_of_term right)) diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 8c55516a9..cd60c5408 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -70,6 +70,7 @@ val refl_proof: Cic.term -> Cic.term -> Cic.term val fix_metas: int -> equality -> int * equality val metas_of_proof: proof -> int list +val add_subst : Subst.substitution -> proof -> proof exception TermIsNotAnEquality;; (** diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index 36e9f99a6..6a21bb173 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -140,8 +140,8 @@ let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = let metasenv = - HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) - (*metasenv1 @ metasenv2*) + HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) + (* metasenv1 @ metasenv2 *) in let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index b3a53d929..2b3bcc069 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1223,7 +1223,7 @@ let simplify_goal_set env goals passive active = (fun acc goal -> match simplify_goal env goal ~passive active with | _, g -> if find g acc then acc else g::acc) - [] active_goals + active_goals active_goals in if List.length active_goals <> List.length simplified then prerr_endline "SEMPLIFICANDO HO SCARTATO..."; @@ -1723,11 +1723,12 @@ let saturate ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in let goal_proof, side_effects_t = - let initial = newproof in + let initial = Equality.add_subst subsumption_subst newproof in Equality.build_goal_proof goalproof initial type_of_goal side_effects in (*prerr_endline (CicPp.pp goal_proof names);*) - let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + (* ?? *) + let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in let side_effects_t = List.map (Subst.apply_subst subsumption_subst) side_effects_t in -- 2.39.2