X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fpath_indexing.ml;h=72120c7f7cabbabc686c78ed1d0d704d82533c0a;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=87e917fff79b5c176401225a1cc757f20f64967c;hpb=b9599336a7e5b19b3cf37d73a9d14f9899e2b82f;p=helm.git

diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index 87e917fff..72120c7f7 100644
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -49,8 +49,6 @@ end
 
 module PSMap = Map.Make(OrderedPathStringElement);;
 
-(* module PSTrie = Trie.Make(PathStringElementMap);; *)
-
 module OrderedPosEquality = struct
   type t = Utils.pos * Inference.equality
 
@@ -59,6 +57,10 @@ end
 
 module PosEqSet = Set.Make(OrderedPosEquality);;
 
+
+module PSTrie = Trie.Make(PSMap);;
+
+(*
 (*
  * Trie: maps over lists.
  * Copyright (C) 2000 Jean-Christophe FILLIATRE
@@ -111,10 +113,11 @@ module PSTrie = struct
     traverse [] t acc
 
 end
+*)
 
 
 let index trie equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_strings_of_term 0 l
   and psr = path_strings_of_term 0 r in
   let index pos trie ps =
@@ -135,7 +138,7 @@ let index trie equality =
       
 
 let remove_index trie equality =
-  let _, (_, l, r, ordering), _, _ = equality in
+  let _, _, (_, l, r, ordering), _, _ = equality in
   let psl = path_strings_of_term 0 l
   and psr = path_strings_of_term 0 r in
   let remove_index pos trie ps =
@@ -160,6 +163,22 @@ let remove_index trie equality =
 ;;
 
 
+let in_index trie equality =
+  let _, _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_strings_of_term 0 l
+  and psr = path_strings_of_term 0 r in
+  let meta_convertibility = Inference.meta_convertibility_eq equality in
+  let ok ps =
+    try
+      let set = PSTrie.find ps trie in
+      PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
+    with Not_found ->
+      false
+  in
+  (List.exists ok psl) || (List.exists ok psr)
+;;
+
+
 let head_of_term = function
   | Cic.Appl (hd::tl) -> hd
   | term -> term
@@ -273,6 +292,12 @@ let rec retrieve_unifiables trie term =
 ;;
 
 
+let retrieve_all trie term =
+  PSTrie.fold
+    (fun k v s -> PosEqSet.union v s) trie PosEqSet.empty
+;;
+
+
 let string_of_pstrie trie =
   let rec to_string level = function
     | PSTrie.Node (v, map) ->