reverted to previous version, as it worked better...

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

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index ddec5f9d42dcb1ac99958c92569e96dd14580d7f..bbd3c484446d4d727fd2a928cad8c1c336b6fd65 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -3,28 +3,24 @@ 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 _ =
+    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
 ;;
@@ -34,20 +30,16 @@ and remove_index = Path_indexing.remove_index
 and in_index = Path_indexing.in_index;;
   
 let get_candidates mode 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
+  let s = 
+    match mode with
+    | Matching -> Path_indexing.retrieve_generalizations trie term
+    | Unification -> Path_indexing.retrieve_unifiables trie term
   in
-  print_candidates mode term res;
-  res
+  Path_indexing.PosEqSet.elements s
 ;;
-*)
 
 
+(*
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -68,6 +60,7 @@ let get_candidates mode tree term =
 (*   print_candidates mode term res; *)
   res
 ;;
+*)
 
 
 let rec find_matches metasenv context ugraph lift_amount term =
@@ -228,10 +221,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
@@ -361,6 +354,7 @@ 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) ->
@@ -447,7 +441,6 @@ 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