-module DiscriminationTreeIndexing =
- functor (A:Set.S) ->
- struct
-
- module OrderedPathStringElement = struct
- type t = path_string_elem
- let compare = compare_elem
- end
-
- module PSMap = Map.Make(OrderedPathStringElement);;
-
- type key = PSMap.key
-
- module DiscriminationTree = Trie.Make(PSMap);;
-
- type t = A.t DiscriminationTree.t
-
- let empty = DiscriminationTree.empty;;
-
- let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
-
- let index tree term info =
- let ps = path_string_of_term_with_jl term in
- let ps_set =
- try DiscriminationTree.find ps tree with Not_found -> A.empty
- in
- DiscriminationTree.add ps (A.add info ps_set) tree
- ;;
-
- let remove_index tree term info =
- let ps = path_string_of_term_with_jl term in
- try
- let ps_set = A.remove info (DiscriminationTree.find ps tree) in
- if A.is_empty ps_set then DiscriminationTree.remove ps tree
- else DiscriminationTree.add ps ps_set tree
- with Not_found -> tree
- ;;
-
- let in_index tree term test =
- let ps = path_string_of_term_with_jl term in
- try
- let ps_set = DiscriminationTree.find ps tree in
- A.exists test ps_set
- with Not_found -> false
- ;;
-
- (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
- (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
- skip all its progeny, thus you want to reach t.
-
- You need to skip as many elements as the sum of all arieties contained
- in the progeny of f.
-
- The input ariety is the one of f while the path is x.g....t
- Should be the equivalent of after_t in the literature (handbook A.R.)
- *)
- let rec skip arity path =
- if arity = 0 then path else match path with
- | [] -> assert false
- | m::tl -> skip (arity-1+arity_of m) tl
- ;;
-
- (* the equivalent of skip, but on the index, thus the list of trees
- that are rooted just after the term represented by the tree root
- are returned (we are skipping the root) *)
- let skip_root = function DiscriminationTree.Node (_, map) ->
- let rec get n = function DiscriminationTree.Node (_, m) as tree ->
- if n = 0 then [tree] else
- PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
- in
- PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
- ;;
-
- let retrieve unif tree term =
- let path = path_string_of_term_with_jl term in
- let rec retrieve path tree =
- match tree, path with
- | DiscriminationTree.Node (Some s, _), [] -> s
- | DiscriminationTree.Node (None, _), [] -> A.empty
- | DiscriminationTree.Node _, Variable::path when unif ->
- List.fold_left A.union A.empty
- (List.map (retrieve path) (skip_root tree))
- | DiscriminationTree.Node (_, map), node::path ->
- A.union
- (if not unif && node = Variable then A.empty else
- try retrieve path (PSMap.find node map)
- with Not_found -> A.empty)
- (try
- match PSMap.find Variable map,skip (arity_of node) path with
- | DiscriminationTree.Node (Some s, _), [] -> s
- | n, path -> retrieve path n
- with Not_found -> A.empty)
- in
- retrieve path tree
- ;;
-
- let retrieve_generalizations tree term = retrieve false tree term;;
- let retrieve_unifiables tree term = retrieve true tree term;;
- end
-;;