Removed negative equations.

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

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index f612023960104c17c472e1f4e10e8ac07c9252c3..873cc5698cadab2be35ce92860a7cab7ad7c14ec 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -407,40 +407,51 @@ 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
-  let samesubst subst subst' =
-    let tbl = Hashtbl.create (List.length subst) in
-    List.iter (fun (m, x) -> Hashtbl.add tbl m x) subst;
-    List.for_all
-      (fun (m, x) ->
-         try
-           let x' = Hashtbl.find tbl m in
-           x = x'
-         with Not_found ->
-           true)
-      subst'
+  let merge_if_possible s1 s2 =
+    let already_in = Hashtbl.create 13 in
+    let rec aux acc = function
+      | ((i,x) as s)::tl ->
+          (try 
+            let x' = Hashtbl.find already_in i in
+            if x = x' then aux acc tl else None
+          with
+          | Not_found -> 
+              Hashtbl.add already_in i x;
+              aux (s::acc) tl)
+      | [] -> Some acc 
+    in  
+      aux [] (s1@s2)
   in
   let leftr =
     match left with
-    | Cic.Meta _ -> []
+    | Cic.Meta _ -> []   
     | _ ->
         let leftc = get_candidates Matching table left in
         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 menv m 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);
@@ -450,34 +461,30 @@ let subsumption env table target =
               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
               raise e
           in
-          if samesubst subst subst' then
-            true, subst
-          else
-            ok what tl
+          (match merge_if_possible subst subst' with
+          | None -> ok what tl
+          | 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 _ -> []
+          | Cic.Meta _ -> [] 
           | _ ->
               let rightc = get_candidates Matching table right in
                 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) 
@@ -707,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