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

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 5607ca3db7b85e2ef3c80cf434445c2ff36f6584..ddec5f9d42dcb1ac99958c92569e96dd14580d7f 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -2,6 +2,29 @@
 type retrieval_mode = Matching | Unification;;
 
 
+let print_candidates mode term res =
+(*   match res with *)
+(*   | [] -> () *)
+(*   | _ -> *)
+      let _ =
+        match mode with
+        | Matching ->
+            Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
+        | Unification ->
+            Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
+      in
+      print_endline
+        (String.concat "\n"
+           (List.map
+              (fun (p, e) ->
+                 Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+                   (Inference.string_of_equality e))
+              res));
+      print_endline "|";
+;;  
+
+
+(*
 let empty_table () =
   Path_indexing.PSTrie.empty
 ;;
@@ -11,16 +34,20 @@ and remove_index = Path_indexing.remove_index
 and in_index = Path_indexing.in_index;;
   
 let get_candidates mode trie term =
-  let s = 
-    match mode with
-    | Matching -> Path_indexing.retrieve_generalizations trie term
-    | Unification -> Path_indexing.retrieve_unifiables trie term
+  let res = 
+    let s = 
+      match mode with
+      | Matching -> Path_indexing.retrieve_generalizations trie term
+      | Unification -> Path_indexing.retrieve_unifiables trie term
+    in
+    Path_indexing.PosEqSet.elements s
   in
-  Path_indexing.PosEqSet.elements s
+  print_candidates mode term res;
+  res
 ;;
+*)
 
 
-(*
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -30,11 +57,17 @@ and remove_index = Discrimination_tree.remove_index
 and in_index = Discrimination_tree.in_index;;
 
 let get_candidates mode tree term =
-  match mode with
-  | Matching -> Discrimination_tree.retrieve_generalizations tree term
-  | Unification -> Discrimination_tree.retrieve_unifiables tree term
+  let res =
+    let s = 
+      match mode with
+      | Matching -> Discrimination_tree.retrieve_generalizations tree term
+      | Unification -> Discrimination_tree.retrieve_unifiables tree term
+    in
+    Discrimination_tree.PosEqSet.elements s
+  in
+(*   print_candidates mode term res; *)
+  res
 ;;
-*)
 
 
 let rec find_matches metasenv context ugraph lift_amount term =
@@ -195,10 +228,10 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let candidates = get_candidates Matching table term in
   match term with
   | C.Meta _ -> None
   | term ->
+      let candidates = get_candidates Matching table term in
       let res =
         find_matches metasenv context ugraph lift_amount term candidates
       in
@@ -328,7 +361,6 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let candidates = get_candidates Unification table term in
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->
@@ -415,6 +447,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   match term with
   | C.Meta _ -> res, lifted_term
   | term ->
+      let candidates = get_candidates Unification table term in
       let r = 
         find_all_matches metasenv context ugraph lift_amount term candidates
       in