From c92657055fda5e7ddd7d00db502406c8f91bb1e3 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 20 Jun 2005 18:02:42 +0000 Subject: [PATCH] *** empty log message *** --- .../paramodulation/test_path_indexing.ml | 56 ------------------- 1 file changed, 56 deletions(-) delete mode 100644 helm/ocaml/paramodulation/test_path_indexing.ml 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 ();; -- 2.39.2