1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 type 'a path_string_elem =
29 | Constant of 'a * int (* name, arity *)
30 | Bound of int * int (* rel, arity *)
31 | Variable (* arity is 0 *)
32 | Proposition (* arity is 0 *)
33 | Datatype (* arity is 0 *)
34 | Dead (* arity is 0 *)
37 type 'a path = ('a path_string_elem) list;;
39 module type Indexable = sig
43 constant_name path_string_elem ->
44 constant_name path_string_elem -> int
45 val string_of_path : constant_name path -> string
46 val path_string_of : input -> constant_name path
49 let arity_of = function
55 module type DiscriminationTree =
64 val iter : t -> (constant_name path -> dataset -> unit) -> unit
65 val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
68 val index : t -> input -> data -> t
69 val remove_index : t -> input -> data -> t
70 val in_index : t -> input -> (data -> bool) -> bool
71 val retrieve_generalizations : t -> input -> dataset
72 val retrieve_unifiables : t -> input -> dataset
73 val retrieve_generalizations_sorted : t -> input -> (data * int) list
74 val retrieve_unifiables_sorted : t -> input -> (data * int) list
77 module Make (I:Indexable) (A:Set.S) : DiscriminationTree
78 with type constant_name = I.constant_name and type input = I.input
79 and type data = A.elt and type dataset = A.t =
83 module OrderedPathStringElement = struct
84 type t = I.constant_name path_string_elem
85 let compare = I.compare
88 type constant_name = I.constant_name
93 module PSMap = Map.Make(OrderedPathStringElement);;
97 module DiscriminationTree = Trie.Make(PSMap);;
99 type t = A.t DiscriminationTree.t
101 let empty = DiscriminationTree.empty;;
103 let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
105 let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
107 let index tree term info =
108 let ps = I.path_string_of term in
110 try DiscriminationTree.find ps tree with Not_found -> A.empty
112 DiscriminationTree.add ps (A.add info ps_set) tree
115 let remove_index tree term info =
116 let ps = I.path_string_of term in
118 let ps_set = A.remove info (DiscriminationTree.find ps tree) in
119 if A.is_empty ps_set then DiscriminationTree.remove ps tree
120 else DiscriminationTree.add ps ps_set tree
121 with Not_found -> tree
124 let in_index tree term test =
125 let ps = I.path_string_of term in
127 let ps_set = DiscriminationTree.find ps tree in
129 with Not_found -> false
132 (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
133 (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
134 skip all its progeny, thus you want to reach t.
136 You need to skip as many elements as the sum of all arieties contained
139 The input ariety is the one of f while the path is x.g....t
140 Should be the equivalent of after_t in the literature (handbook A.R.)
142 let rec skip arity path =
143 if arity = 0 then path else match path with
145 | m::tl -> skip (arity-1+arity_of m) tl
148 (* the equivalent of skip, but on the index, thus the list of trees
149 that are rooted just after the term represented by the tree root
150 are returned (we are skipping the root) *)
151 let skip_root = function DiscriminationTree.Node (value, map) ->
152 let rec get n = function DiscriminationTree.Node (v, m) as tree ->
153 if n = 0 then [tree] else
154 PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
156 PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
159 let retrieve unif tree term =
160 let path = I.path_string_of term in
161 let rec retrieve path tree =
162 match tree, path with
163 | DiscriminationTree.Node (Some s, _), [] -> s
164 | DiscriminationTree.Node (None, _), [] -> A.empty
165 | DiscriminationTree.Node (_, map), Variable::path when unif ->
166 List.fold_left A.union A.empty
167 (List.map (retrieve path) (skip_root tree))
168 | DiscriminationTree.Node (_, map), node::path ->
170 (if not unif && node = Variable then A.empty else
171 try retrieve path (PSMap.find node map)
172 with Not_found -> A.empty)
174 match PSMap.find Variable map,skip (arity_of node) path with
175 | DiscriminationTree.Node (Some s, _), [] -> s
176 | n, path -> retrieve path n
177 with Not_found -> A.empty)
182 let retrieve_generalizations tree term = retrieve false tree term;;
183 let retrieve_unifiables tree term = retrieve true tree term;;
187 let compare (_,a) (_,b) = compare b a
189 module S = Set.Make(O)
191 let retrieve_sorted unif tree term =
192 let path = I.path_string_of term in
193 let rec retrieve n path tree =
194 match tree, path with
195 | DiscriminationTree.Node (Some s, _), [] -> S.singleton (s, n)
196 | DiscriminationTree.Node (None, _), [] -> S.empty
197 | DiscriminationTree.Node (_, map), Variable::path when unif ->
198 List.fold_left S.union S.empty
199 (List.map (retrieve n path) (skip_root tree))
200 | DiscriminationTree.Node (_, map), node::path ->
202 (if not unif && node = Variable then S.empty else
203 try retrieve (n+1) path (PSMap.find node map)
204 with Not_found -> S.empty)
206 match PSMap.find Variable map,skip (arity_of node) path with
207 | DiscriminationTree.Node (Some s, _), [] ->
209 | no, path -> retrieve n path no
210 with Not_found -> S.empty)
213 (List.map (fun x -> List.map (fun y -> y, snd x) (A.elements (fst x)))
214 (S.elements (retrieve 0 path tree)))
217 let retrieve_generalizations_sorted tree term =
218 retrieve_sorted false tree term;;
219 let retrieve_unifiables_sorted tree term =
220 retrieve_sorted true tree term;;