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
67 val index : t -> input -> data -> t
68 val remove_index : t -> input -> data -> t
69 val in_index : t -> input -> (data -> bool) -> bool
70 val retrieve_generalizations : t -> input -> dataset
71 val retrieve_unifiables : t -> input -> dataset
74 module Make (I:Indexable) (A:Set.S) : DiscriminationTree
75 with type constant_name = I.constant_name and type input = I.input
76 and type data = A.elt and type dataset = A.t =
80 module OrderedPathStringElement = struct
81 type t = I.constant_name path_string_elem
82 let compare = I.compare
85 type constant_name = I.constant_name
90 module PSMap = Map.Make(OrderedPathStringElement);;
94 module DiscriminationTree = Trie.Make(PSMap);;
96 type t = A.t DiscriminationTree.t
98 let empty = DiscriminationTree.empty;;
100 let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
102 let index tree term info =
103 let ps = I.path_string_of term in
105 try DiscriminationTree.find ps tree with Not_found -> A.empty
107 DiscriminationTree.add ps (A.add info ps_set) tree
110 let remove_index tree term info =
111 let ps = I.path_string_of term in
113 let ps_set = A.remove info (DiscriminationTree.find ps tree) in
114 if A.is_empty ps_set then DiscriminationTree.remove ps tree
115 else DiscriminationTree.add ps ps_set tree
116 with Not_found -> tree
119 let in_index tree term test =
120 let ps = I.path_string_of term in
122 let ps_set = DiscriminationTree.find ps tree in
124 with Not_found -> false
127 (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is
128 (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
129 skip all its progeny, thus you want to reach t.
131 You need to skip as many elements as the sum of all arieties contained
134 The input ariety is the one of f while the path is x.g....t
135 Should be the equivalent of after_t in the literature (handbook A.R.)
137 let rec skip arity path =
138 if arity = 0 then path else match path with
140 | m::tl -> skip (arity-1+arity_of m) tl
143 (* the equivalent of skip, but on the index, thus the list of trees
144 that are rooted just after the term represented by the tree root
145 are returned (we are skipping the root) *)
146 let skip_root = function DiscriminationTree.Node (value, map) ->
147 let rec get n = function DiscriminationTree.Node (v, m) as tree ->
148 if n = 0 then [tree] else
149 PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
151 PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
154 let retrieve unif tree term =
155 let path = I.path_string_of term in
156 let rec retrieve path tree =
157 match tree, path with
158 | DiscriminationTree.Node (Some s, _), [] -> s
159 | DiscriminationTree.Node (None, _), [] -> A.empty
160 | DiscriminationTree.Node (_, map), Variable::path when unif ->
161 List.fold_left A.union A.empty
162 (List.map (retrieve path) (skip_root tree))
163 | DiscriminationTree.Node (_, map), node::path ->
165 (if not unif && node = Variable then A.empty else
166 try retrieve path (PSMap.find node map)
167 with Not_found -> A.empty)
169 match PSMap.find Variable map,skip (arity_of node) path with
170 | DiscriminationTree.Node (Some s, _), [] -> s
171 | n, path -> retrieve path n
172 with Not_found -> A.empty)
177 let retrieve_generalizations tree term = retrieve false tree term;;
178 let retrieve_unifiables tree term = retrieve true tree term;;