profiling experiments...

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index c45e19ab0de0862d05b2d9dab52b85ab13f24c50..0553146762231344dc9f158e55e6373d976396eb 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -1,6 +1,6 @@
-(* type naif_indexing =
-    (Cic.term * ((bool * Inference.equality) list)) list 
-;; *)
+(** settable by the command line (-i switch) *)
+let use_index = ref true;;
+
 
 type pos = Left | Right ;;
 
@@ -47,7 +47,7 @@ let remove_index table eq =
 ;;
 
 
-let rec find_matches unif_fun metasenv context ugraph lift_amount term =
+let rec find_matches metasenv context ugraph lift_amount term =
   let module C = Cic in
   let module U = Utils in
   let module S = CicSubstitution in
@@ -74,7 +74,7 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term =
           let subst', metasenv', ugraph' =
 (*             Inference.matching (metasenv @ metas) context term *)
 (*               (S.lift lift_amount c) ugraph *)
-            unif_fun (metasenv @ metas) context
+            Inference.matching (metasenv @ metas) context
               term (S.lift lift_amount c) ugraph
           in
 (*           let names = U.names_of_context context in *)
@@ -96,7 +96,7 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term =
             res
           with e ->
 (*             Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); *)
-            find_matches unif_fun metasenv context ugraph lift_amount term tl
+            find_matches metasenv context ugraph lift_amount term tl
         else
           let res = try do_match c other eq_URI with e -> None in
           match res with
@@ -112,10 +112,17 @@ let rec find_matches unif_fun metasenv context ugraph lift_amount term =
               if order = U.Gt then
                 res
               else
-                find_matches unif_fun metasenv context ugraph
-                  lift_amount term tl
+                find_matches metasenv context ugraph lift_amount term tl
           | None ->
-              find_matches unif_fun metasenv context ugraph lift_amount term tl
+              find_matches metasenv context ugraph lift_amount term tl
+;;
+
+
+let get_candidates table term =
+  if !use_index then
+    try Hashtbl.find table (head_of_term term) with Not_found -> []
+  else
+    Hashtbl.fold (fun k v l -> v @ l) table []
 ;;
 
 
@@ -124,14 +131,12 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let hd_term = head_of_term term in
-  let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
+  let candidates = get_candidates table term in
   match term with
   | C.Meta _ -> None
   | term ->
       let res =
-        find_matches Inference.matching metasenv context ugraph
-          lift_amount term candidates
+        find_matches metasenv context ugraph lift_amount term candidates
       in
       if res <> None then
         res
@@ -233,13 +238,8 @@ let rec demodulation newmeta env table target =
       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
         (Inference.meta_convertibility_eq target newtarget) then
           newmeta, newtarget
-      else (
-(*         Printf.printf "Going on 1:\ntarget: %s\nnewtarget: %s\n%s\n\n" *)
-(*           (Inference.string_of_equality ~env target) *)
-(*           (Inference.string_of_equality ~env newtarget) *)
-(*           (string_of_bool (target = newtarget)); *)
+      else 
         demodulation newmeta env table newtarget
-      )
   | None ->
       let res = demodulate_term metasenv' context ugraph table 0 right in
       match res with
@@ -248,12 +248,8 @@ let rec demodulation newmeta env table target =
           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
             (Inference.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
-          else (
-(*             Printf.printf "Going on 2:\ntarget: %s\nnewtarget: %s\n\n" *)
-(*               (Inference.string_of_equality ~env target) *)
-(*               (Inference.string_of_equality ~env newtarget); *)
+          else 
             demodulation newmeta env table newtarget
-          )
       | None ->
           newmeta, target
 ;;
@@ -313,8 +309,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let hd_term = head_of_term term in
-  let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
+  let candidates = get_candidates table term in
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->