use of discrimination trees instead of path indexes, for a little

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

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index a54e0aef3a7bd2bf152f38d7f3e1dac2d228aae2..2ef07a17cd18a38e2a03cab982d90a71e37dc2ea 100644 (file)
--- a/helm/ocaml/paramodulation/test_indexing.ml
+++ b/helm/ocaml/paramodulation/test_indexing.ml
@@ -14,7 +14,7 @@ let build_equality term =
   b = Rel 4
   c = Rel 5
 *)
-let main_test () =
+let path_indexing_test () =
   let module C = Cic in
   let terms = [
     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
@@ -89,7 +89,59 @@ let next_after () =
 ;;
 
 
+let discrimination_tree_test () =
+  let module C = Cic in
+  let terms = [
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5];
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Meta (1, [])];
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5];
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 5]; C.Rel 4];
+    C.Appl [C.Rel 10; C.Meta (5, []); C.Rel 11]
+  ] in
+  let path_strings =
+    List.map Discrimination_tree.path_string_of_term terms in
+  let table =
+    List.fold_left
+      Discrimination_tree.index
+      Discrimination_tree.DiscriminationTree.empty
+      (List.map build_equality terms)
+  in
+(*   let query = *)
+(*     C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Meta (1, []); C.Rel 4]; C.Rel 5] in *)
+  let query = C.Appl [C.Rel 10; C.Meta (14, []); C.Meta (13, [])] in
+  let matches = Discrimination_tree.retrieve_generalizations table query in
+  let unifications = Discrimination_tree.retrieve_unifiables table query in
+  let eq1 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (1, [])])
+  and eq2 = build_equality (C.Appl [C.Rel 1; C.Meta (1, []); C.Meta (2, [])]) in
+  let res1 = Discrimination_tree.in_index table eq1
+  and res2 = Discrimination_tree.in_index table eq2 in
+  let print_results res =
+    String.concat "\n"
+      (Discrimination_tree.PosEqSet.fold
+         (fun (p, e) l ->
+            let s = 
+              "(" ^ (Utils.string_of_pos p) ^ ", " ^
+                (Inference.string_of_equality e) ^ ")"
+            in
+            s::l)
+         res [])
+  in
+  Printf.printf "path_strings:\n%s\n\n"
+    (String.concat "\n"
+       (List.map Discrimination_tree.string_of_path_string path_strings));
+  Printf.printf "table:\n%s\n\n"
+    (Discrimination_tree.string_of_discrimination_tree table);
+  Printf.printf "matches:\n%s\n\n" (print_results matches);
+  Printf.printf "unifications:\n%s\n\n" (print_results unifications);
+  Printf.printf "in_index %s: %s\n"
+    (Inference.string_of_equality eq1) (string_of_bool res1);
+  Printf.printf "in_index %s: %s\n"
+    (Inference.string_of_equality eq2) (string_of_bool res2);
+;;
+
+
 (* differing ();; *)
-(* main_test ();; *)
-next_after ();;
+(* next_after ();; *)
+discrimination_tree_test ();;
+(* path_indexing_test ();; *)