goals after a superposition step are relocated

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index e7ef6fa7c2b9def7764a18273fef1981eaf91baa..26db9567c9593955e7174c2c3348814e0aec3f7d 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -913,8 +913,8 @@ let pp_goal_set msg goals names =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
   let names = names_of_context ctx in
+(*
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
 *)
   match ty with
@@ -928,8 +928,10 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
        match Indexing.unification env table goal_equation with 
         | Some (subst, equality, swapped ) ->
             prerr_endline 
-              ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
-            prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+              ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+            prerr_endline 
+              ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+            prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
@@ -1028,8 +1030,11 @@ let infer_goal_set env active goals =
             let new_passive_goals =
               if Utils.metas_of_term t1 = [] then passive_goals
               else 
-                let new' = 
-                   Indexing.superposition_left env (snd active) selected in
+                let newmaxmeta,new' = 
+                   Indexing.superposition_left env (snd active) selected
+                   !maxmeta 
+                in
+                maxmeta := newmaxmeta;
                 passive_goals @ new'
             in
             selected::active_goals, new_passive_goals
@@ -1073,7 +1078,8 @@ let infer_goal_set_with_current env current goals =
   active_goals, 
   List.fold_left 
     (fun acc g ->
-      let new' = Indexing.superposition_left env table g in
+      let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+      maxmeta := newmaxmeta;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1580,7 +1586,6 @@ let saturate
       prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
       let side_effects = 
@@ -1593,6 +1598,7 @@ let saturate
         Equality.build_goal_proof 
           eq_uri goalproof initial type_of_goal side_effects
       in
+      prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
@@ -1975,6 +1981,12 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
       let t = Equality.term_of_equality eq_uri e in
       prerr_endline (CicPp.pp t names)) 
   eql;
+  prerr_endline ("\n result proofs: ");
+  List.iter (fun e -> 
+    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+    let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+    Subst.ppsubst s ^ "\n" ^ 
+    CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
       let demod =