From: Alberto Griggio <griggio@fbk.eu>
Date: Mon, 20 Jun 2005 18:02:42 +0000 (+0000)
Subject: *** empty log message ***
X-Git-Tag: INDEXING_NO_PROOFS~110
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c92657055fda5e7ddd7d00db502406c8f91bb1e3;p=helm.git

*** empty log message ***
---

diff --git a/helm/ocaml/paramodulation/test_path_indexing.ml b/helm/ocaml/paramodulation/test_path_indexing.ml
deleted file mode 100644
index 0514f9ab9..000000000
--- a/helm/ocaml/paramodulation/test_path_indexing.ml
+++ /dev/null
@@ -1,56 +0,0 @@
-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 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" (print_results unifications)
-;;
-
-
-main_test ();;