subsumption fixed and called in given_clause_fullred.

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index f612023960104c17c472e1f4e10e8ac07c9252c3..e6a2463c099a8a084e4ac83e42497eac382e3653 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -411,21 +411,24 @@ let subsumption env table target =
   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
@@ -440,7 +443,7 @@ let subsumption env table target =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching menv m context what other ugraph
+                Inference.matching metasenv menv context what other ugraph
               in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
@@ -450,10 +453,9 @@ 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 -> true, s)
         with Inference.MatchingFailure ->
           ok what tl
   in
@@ -464,7 +466,7 @@ let subsumption env table target =
     else
       let rightr =
         match right with
-          | Cic.Meta _ -> []
+          | Cic.Meta _ -> [] 
           | _ ->
               let rightc = get_candidates Matching table right in
                 find_all_matches ~unif_fun:Inference.matching