-
-
-(*
-(* NO INDEXING *)
-let init_index () = ()
-
-let empty_table () = []
-
-let index table equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- match ordering with
- | Utils.Gt -> (Utils.Left, equality)::table
- | Utils.Lt -> (Utils.Right, equality)::table
- | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
-;;
-
-let remove_index table equality =
- List.filter (fun (p, e) -> e != equality) table
-;;
-
-let in_index table equality =
- List.exists (fun (p, e) -> e == equality) table
-;;
-
-let get_candidates mode table term = table
-*)
-
-
-(*
-(* PATH INDEXING *)
-let init_index () = ()
-
-let empty_table () =
- Path_indexing.PSTrie.empty
-;;
-
-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 t1 = Unix.gettimeofday () in
- let res =
- let s =
- match mode with
- | Matching -> Path_indexing.retrieve_generalizations trie term
- | Unification -> Path_indexing.retrieve_unifiables trie term
-(* Path_indexing.retrieve_all trie term *)
- in
- Path_indexing.PosEqSet.elements s
- in
-(* print_candidates mode term res; *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- res
-;;
+let index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty
+let init_index = Index.init_index
+
+(* returns a list of all the equalities in the tree that are in relation
+ "mode" with the given term, where mode can be either Matching or
+ Unification.
+
+ Format of the return value: list of tuples in the form:
+ (position - Left or Right - of the term that matched the given one in this
+ equality,
+ equality found)
+
+ Note that if equality is "left = right", if the ordering is left > right,
+ the position will always be Left, and if the ordering is left < right,
+ position will be Right.