From 9135f92fe15418abd2c2ae81ab155a2517bc72ea Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
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