goals after a superposition step are relocated

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

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index e7166324de60d735480374a21595b3c9b1af8318..7b545dd47c5b72a1cec282bc92f40c25b57c60b7 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -27,8 +27,6 @@ let _profiler = <:profiler<_profiler>>;;
 
 (* $Id$ *)
 
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
 (*
 module Index = Equality_indexing.DT (* path tree based indexing *)
@@ -1048,30 +1046,48 @@ let build_newgoal context goal posu rule expansion =
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
-let superposition_left (metasenv, context, ugraph) table goal = 
+let superposition_left (metasenv, context, ugraph) table goal maxmeta = 
+  let names = Utils.names_of_context context in
   let proof,menv,eq,ty,l,r = open_goal goal in
   let c = !Utils.compare_terms l r in
-  if c = Utils.Incomparable then
-    begin
-    let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
-    let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
-    (* prerr_endline "incomparable"; 
-    prerr_endline (string_of_int (List.length expansionsl));
-    prerr_endline (string_of_int (List.length expansionsr));
-    *)
-    List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
-    @
-    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
-    end
-  else
-    let big,small,possmall = 
-      match c with 
-        Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right 
-      | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left
-      | _ -> assert false
-    in
-    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+  let newgoals = 
+    if c = Utils.Incomparable then
+      begin
+      let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+      let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+      (* prerr_endline "incomparable"; 
+      prerr_endline (string_of_int (List.length expansionsl));
+      prerr_endline (string_of_int (List.length expansionsr));
+      *)
+      List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+      @
+      List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+      end
+    else
+        match c with 
+        | Utils.Gt -> (* prerr_endline "GT"; *) 
+            let big,small,possmall = l,r,Utils.Right in
+            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+            List.map 
+              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              expansions
+        | Utils.Lt -> (* prerr_endline "LT"; *) 
+            let big,small,possmall = r,l,Utils.Left in
+            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+            List.map 
+              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              expansions
+        | Utils.Eq -> []
+        | _ ->
+            prerr_endline 
+              ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+            assert false
+  in
+  (* rinfresco le meta *)
+  List.fold_right
+    (fun g (max,acc) -> 
+       let max,g = Equality.fix_metas_goal max g in max,g::acc) 
+    newgoals (maxmeta,[])
 ;;
 
 (** demodulation, when the target is a goal *)