module PosEqSet = Set.Make(OrderedPosEquality);;
+
module PSTrie = Trie.Make(PSMap);;
(*
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 _, _, (_, 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 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) ->