]> matita.cs.unibo.it Git - helm.git/blob - matita/components/extlib/discrimination_tree.ml
1a8147f7db8d62cb4eaf51111daa4a77e5587607
[helm.git] / matita / components / extlib / discrimination_tree.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
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 *) 
35 ;;  
36
37 type 'a path = ('a path_string_elem) list;;
38
39 module type Indexable = sig
40   type input
41   type constant_name
42   val compare: 
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
47 end
48
49 let arity_of = function
50   | Constant (_,a) 
51   | Bound (_,a) -> a
52   | _ -> 0 
53 ;;
54
55 module type DiscriminationTree =
56     sig
57
58       type input 
59       type data
60       type dataset
61       type constant_name
62       type t
63
64       val iter : t -> (constant_name path -> dataset -> unit) -> unit
65       val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
66
67       val empty : t
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
74       module type Collector = sig
75         type t
76         val empty : t
77         val union : t -> t -> t
78         val inter : t -> t -> data list
79         val to_list : t -> data list
80       end
81       module Collector : Collector
82       val retrieve_generalizations_sorted : t -> input -> Collector.t
83       val retrieve_unifiables_sorted : t -> input -> Collector.t
84     end
85
86 module Make (I:Indexable) (A:Set.S) : DiscriminationTree 
87 with type constant_name = I.constant_name and type input = I.input
88 and type data = A.elt and type dataset = A.t =
89
90     struct
91
92       module OrderedPathStringElement = struct
93         type t = I.constant_name path_string_elem
94         let compare = I.compare
95       end
96
97       type constant_name = I.constant_name
98       type data = A.elt
99       type dataset = A.t
100       type input = I.input
101
102       module PSMap = Map.Make(OrderedPathStringElement);;
103
104       type key = PSMap.key
105
106       module DiscriminationTree = Trie.Make(PSMap);;
107
108       type t = A.t DiscriminationTree.t
109
110       let empty = DiscriminationTree.empty;;
111
112       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
113
114       let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
115
116       let index tree term info =
117         let ps = I.path_string_of term in
118         let ps_set =
119           try DiscriminationTree.find ps tree with Not_found -> A.empty 
120         in
121         DiscriminationTree.add ps (A.add info ps_set) tree
122       ;;
123
124       let remove_index tree term info =
125         let ps = I.path_string_of term in
126         try
127           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
128           if A.is_empty ps_set then DiscriminationTree.remove ps tree
129           else DiscriminationTree.add ps ps_set tree
130         with Not_found -> tree
131       ;;
132
133       let in_index tree term test =
134         let ps = I.path_string_of term in
135         try
136           let ps_set = DiscriminationTree.find ps tree in
137           A.exists test ps_set
138         with Not_found -> false
139       ;;
140
141       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is 
142          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
143          skip all its progeny, thus you want to reach t.
144       
145          You need to skip as many elements as the sum of all arieties contained
146           in the progeny of f.
147       
148          The input ariety is the one of f while the path is x.g....t  
149          Should be the equivalent of after_t in the literature (handbook A.R.)
150        *)
151       let rec skip arity path =
152         if arity = 0 then path else match path with 
153         | [] -> assert false 
154         | m::tl -> skip (arity-1+arity_of m) tl
155       ;;
156
157       (* the equivalent of skip, but on the index, thus the list of trees
158          that are rooted just after the term represented by the tree root
159          are returned (we are skipping the root) *)
160       let skip_root = function DiscriminationTree.Node (_value, map) ->
161         let rec get n = function DiscriminationTree.Node (_v, m) as tree ->
162            if n = 0 then [tree] else 
163            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
164         in
165           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
166       ;;
167
168       let retrieve unif tree term =
169         let path = I.path_string_of term in
170         let rec retrieve path tree =
171           match tree, path with
172           | DiscriminationTree.Node (Some s, _), [] -> s
173           | DiscriminationTree.Node (None, _), [] -> A.empty 
174           | DiscriminationTree.Node (_, _map), Variable::path when unif ->
175               List.fold_left A.union A.empty
176                 (List.map (retrieve path) (skip_root tree))
177           | DiscriminationTree.Node (_, map), node::path ->
178               A.union
179                  (if not unif && node = Variable then A.empty else
180                   try retrieve path (PSMap.find node map)
181                   with Not_found -> A.empty)
182                  (try
183                     match PSMap.find Variable map,skip (arity_of node) path with
184                     | DiscriminationTree.Node (Some s, _), [] -> s
185                     | n, path -> retrieve path n
186                   with Not_found -> A.empty)
187        in
188         retrieve path tree
189       ;;
190
191       let retrieve_generalizations tree term = retrieve false tree term;;
192       let retrieve_unifiables tree term = retrieve true tree term;;
193
194       module O = struct
195         type t = A.t * int
196         let compare (sa,wa) (sb,wb) = 
197           let c = compare wb wa in
198           if c <> 0 then c else A.compare sb sa
199       end
200       module S = Set.Make(O)
201
202       (* TASSI: here we should think of a smarted data structure *)
203       module type Collector = sig
204         type t
205         val empty : t
206         val union : t -> t -> t
207         val inter : t -> t -> data list
208         val to_list : t -> data list
209       end
210       module Collector : Collector with type t = S.t = struct
211         type t = S.t
212         let union = S.union
213         let empty = S.empty
214
215         let merge l = 
216           let rec aux s w = function
217             | [] -> [s,w]
218             | (t, wt)::tl when w = wt -> aux (A.union s t) w tl
219             | (t, wt)::tl -> (s, w) :: aux t wt tl
220           in
221           match l with
222           | [] -> []
223           | (s, w) :: l -> aux s w l
224           
225         let rec undup ~eq = function
226           | [] -> []
227           | x :: tl -> x :: undup ~eq (List.filter (fun y -> not(eq x y)) tl)
228
229         let to_list t =
230           undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y)) 
231             (List.flatten (List.map 
232               (fun x,_ -> A.elements x) (merge (S.elements t))))
233
234         let inter t1 t2 =
235           let l1 = merge (S.elements t1) in
236           let l2 = merge (S.elements t2) in
237           let res = 
238            List.flatten
239             (List.map
240               (fun s, w ->
241                  HExtlib.filter_map (fun x ->
242                    try Some (x, w + snd (List.find (fun (s,_w) -> A.mem x s) l2))
243                    with Not_found -> None)
244                    (A.elements s))
245               l1)
246           in
247           undup ~eq:(fun x y -> A.equal (A.singleton x) (A.singleton y)) 
248             (List.map fst (List.sort (fun (_,x) (_,y) -> y - x) res))
249       end
250
251       let retrieve_sorted unif tree term =
252         let path = I.path_string_of term in
253         let rec retrieve n path tree =
254           match tree, path with
255           | DiscriminationTree.Node (Some s, _), [] -> S.singleton (s, n)
256           | DiscriminationTree.Node (None, _), [] -> S.empty
257           | DiscriminationTree.Node (_, _map), Variable::path when unif ->
258               List.fold_left S.union S.empty
259                 (List.map (retrieve n path) (skip_root tree))
260           | DiscriminationTree.Node (_, map), node::path ->
261               S.union
262                  (if not unif && node = Variable then S.empty else
263                   try retrieve (n+1) path (PSMap.find node map)
264                   with Not_found -> S.empty)
265                  (try
266                     match PSMap.find Variable map,skip (arity_of node) path with
267                     | DiscriminationTree.Node (Some s, _), [] -> 
268                        S.singleton (s, n)
269                     | no, path -> retrieve n path no
270                   with Not_found -> S.empty)
271        in
272         retrieve 0 path tree
273       ;;
274
275       let retrieve_generalizations_sorted tree term = 
276         retrieve_sorted false tree term;;
277       let retrieve_unifiables_sorted tree term = 
278         retrieve_sorted true tree term;;
279   end
280 ;;
281