Subsumption_subst must be applied to the initial proof before passing

it to build_proof_goal.

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2561ea56f5a587549fdc89f6fb55fc56ecc8aece..3979c052985f76f542a68ad1c409ef8cf4274a44 100644 (file)
--- 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 8c55516a9db82167e95189458ebe3608649b033a..cd60c5408e649456735932a9cc55c5a69a0ed9ef 100644 (file)
--- 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 36e9f99a64a710785976c200979d0764620bc849..6a21bb173d1f76f8cc380b56b4bd34160beed287 100644 (file)
--- 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 b3a53d92953f61e2f86dad7baf146deab69dec79..2b3bcc0692d5d44d007d6e063747cc0bfbdb5fb2 100644 (file)
--- 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