testing...

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
new file mode 100644 (file)
index 0000000..a54e0ae
--- /dev/null
+++ b/helm/ocaml/paramodulation/test_indexing.ml
@@ -0,0 +1,95 @@
+open Path_indexing
+
+
+let build_equality term =
+  let module C = Cic in
+  C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
+;;
+
+
+(*
+  f = Rel 1
+  g = Rel 2
+  a = Rel 3
+  b = Rel 4
+  c = Rel 5
+*)
+let main_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 1; C.Meta (1, []); C.Meta (1, [])]
+  ] in
+  let path_strings = List.map (path_strings_of_term 0) terms in
+  let table =
+    List.fold_left index PSTrie.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 matches = retrieve_generalizations table query in
+  let unifications = 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 = in_index table eq1
+  and res2 = in_index table eq2 in
+  let print_results res =
+    String.concat "\n"
+      (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
+          (fun l ->
+             "{" ^ (String.concat "; " (List.map string_of_path_string l)) ^ "}"
+          ) path_strings));
+  Printf.printf "table:\n%s\n\n" (string_of_pstrie 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);
+;;
+
+
+let differing () =
+  let module C = Cic in
+  let t1 =
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Meta (1, [])]; C.Rel 5]
+  and t2 = 
+    C.Appl [C.Rel 1; C.Appl [C.Rel 5; C.Rel 4; C.Meta (1, [])]; C.Rel 5]
+  in
+  let res = Inference.extract_differing_subterms t1 t2 in
+  match res with
+  | None -> print_endline "NO DIFFERING SUBTERMS???"
+  | Some (t1, t2) ->
+      Printf.printf "OK: %s, %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
+;;
+
+
+let next_after () =
+  let module C = Cic in
+  let t =
+    C.Appl [C.Rel 1; C.Appl [C.Rel 2; C.Rel 3; C.Rel 4]; C.Rel 5]
+  in
+  let pos1 = Discrimination_tree.next_t [1] t in
+  let pos2 = Discrimination_tree.after_t [1] t in
+  Printf.printf "next_t 1: %s\nafter_t 1: %s\n"
+    (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos1 t))
+    (CicPp.ppterm (Discrimination_tree.subterm_at_pos pos2 t));
+;;
+
+
+(* differing ();; *)
+(* main_test ();; *)
+next_after ();;
+