module PSMap = Map.Make(OrderedPathStringElement);;
-(* module PSTrie = Trie.Make(PathStringElementMap);; *)
-
module OrderedPosEquality = struct
type t = Utils.pos * Inference.equality
module PosEqSet = Set.Make(OrderedPosEquality);;
+
+module PSTrie = Trie.Make(PSMap);;
+
+(*
(*
* Trie: maps over lists.
* Copyright (C) 2000 Jean-Christophe FILLIATRE
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 =
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 =
;;
+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
;;
+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) ->