some optimizations...

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 84559b22247fdde62f74f2485562eb34fef34cbb..5607ca3db7b85e2ef3c80cf434445c2ff36f6584 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -1,61 +1,41 @@
 
-let head_of_term = function
-  | Cic.Appl (hd::tl) -> hd
-  | t -> t
-;;
+type retrieval_mode = Matching | Unification;;
 
 
-(*
 let empty_table () =
-  Hashtbl.create 10
+  Path_indexing.PSTrie.empty
 ;;
 
-
-let index table eq =
-  let _, (_, l, r, ordering), _, _ = eq in
-  let hl = head_of_term l in
-  let hr = head_of_term r in
-  let index x pos = 
-    let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    Hashtbl.replace table x ((pos, eq)::x_entry)
-  in
-  let _ = 
-    match ordering with
-    | Utils.Gt ->
-        index hl Utils.Left
-    | Utils.Lt ->
-        index hr Utils.Right
-    | _ -> index hl Utils.Left; index hr Utils.Right
+let index = Path_indexing.index
+and remove_index = Path_indexing.remove_index
+and in_index = Path_indexing.in_index;;
+  
+let get_candidates mode trie term =
+  let s = 
+    match mode with
+    | Matching -> Path_indexing.retrieve_generalizations trie term
+    | Unification -> Path_indexing.retrieve_unifiables trie term
   in
-(*   index hl Utils.Left; *)
-(*   index hr Utils.Right; *)
-  table
+  Path_indexing.PosEqSet.elements s
 ;;
 
 
-let remove_index table eq =
-  let _, (_, l, r, ordering), _, _ = eq in
-  let hl = head_of_term l
-  and hr = head_of_term r in
-  let remove_index x pos =
-    let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in
-    Hashtbl.replace table x newentry
-  in
-  remove_index hl Utils.Left;
-  remove_index hr Utils.Right;
-  table
+(*
+let empty_table () =
+  Discrimination_tree.DiscriminationTree.empty
 ;;
-*)
 
+let index = Discrimination_tree.index
+and remove_index = Discrimination_tree.remove_index
+and in_index = Discrimination_tree.in_index;;
 
-let empty_table () =
-  Path_indexing.PSTrie.empty
+let get_candidates mode tree term =
+  match mode with
+  | Matching -> Discrimination_tree.retrieve_generalizations tree term
+  | Unification -> Discrimination_tree.retrieve_unifiables tree term
 ;;
+*)
 
-let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index;;
-  
 
 let rec find_matches metasenv context ugraph lift_amount term =
   let module C = Cic in
@@ -157,27 +137,6 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
 ;;
 
 
-type retrieval_mode = Matching | Unification;;
-
-(*
-let get_candidates mode table term =
-  try Hashtbl.find table (head_of_term term) with Not_found -> []
-;;
-*)
-
-
-let get_candidates mode trie term =
-  let s = 
-    match mode with
-    | Matching ->
-        Path_indexing.retrieve_generalizations trie term
-    | Unification ->
-        Path_indexing.retrieve_unifiables trie term
-  in
-  Path_indexing.PosEqSet.elements s
-;;
-
-
 let subsumption env table target =
   let _, (ty, tl, tr, _), tmetas, _ = target in
   let metasenv, context, ugraph = env in