X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=7b545dd47c5b72a1cec282bc92f40c25b57c60b7;hb=cec2e3fc6d110cb0c2996c104ca277fbee33bb9e;hp=c74abe27d4605b8cf7b2638b826b8181d2bf77ca;hpb=c515304b306f38ae7387aff6fe44e36fa9e7bfa5;p=helm.git

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index c74abe27d..7b545dd47 100644
--- 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,41 +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
-      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
+  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 *)