the tactic now returns as open goals the open metas in the proof

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

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index e6a2463c099a8a084e4ac83e42497eac382e3653..873cc5698cadab2be35ce92860a7cab7ad7c14ec 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -407,7 +407,13 @@ let find_all_matches
 (*
   returns true if target is subsumed by some equality in table
 *)
-let subsumption env table target =
+let subsumption env table target = 
+  (* 
+  let print_res l =
+    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+    ((pos,equation),_)) -> Inference.string_of_equality equation)l))
+  in
+  *)
   let _, _, (ty, left, right, _), tmetas = target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
@@ -434,16 +440,18 @@ let subsumption env table target =
         find_all_matches ~unif_fun:Inference.matching
           metasenv context ugraph 0 left ty leftc
   in
+(*  print_res leftr;*)
   let rec ok what = function
-    | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+    | [] -> None
+    | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+        let _, _, (_, l, r, o), m = equation in
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching metasenv menv context what other ugraph
+                Inference.matching metasenv m context what other ugraph
               in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
@@ -455,15 +463,13 @@ let subsumption env table target =
           in
           (match merge_if_possible subst subst' with
           | None -> ok what tl
-          | Some s -> true, s)
+          | Some s -> Some (s, equation))
         with Inference.MatchingFailure ->
           ok what tl
   in
-  let r, subst = ok right leftr in
-  let r, s =
-    if r then
-      true, subst
-    else
+  match ok right leftr with
+  | Some _ as res -> res
+  | None -> 
       let rightr =
         match right with
           | Cic.Meta _ -> [] 
@@ -472,14 +478,13 @@ let subsumption env table target =
                 find_all_matches ~unif_fun:Inference.matching
                   metasenv context ugraph 0 right ty rightc
       in
+(*        print_res rightr;*)
         ok left rightr
-  in
 (*     (if r then  *)
 (*        debug_print  *)
 (*          (lazy *)
 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
-    r, s
 ;;
 
 let rec demodulation_aux ?from ?(typecheck=false) 
@@ -709,6 +714,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
           prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+            newmenv));
           raise exc;
       else () 
     in