]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/extlib/discrimination_tree.ml
fixed makefile
[helm.git] / helm / software / 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     end
74
75 module Make (I:Indexable) (A:Set.S) : DiscriminationTree 
76 with type constant_name = I.constant_name and type input = I.input
77 and type data = A.elt and type dataset = A.t =
78
79     struct
80
81       module OrderedPathStringElement = struct
82         type t = I.constant_name path_string_elem
83         let compare = I.compare
84       end
85
86       type constant_name = I.constant_name
87       type data = A.elt
88       type dataset = A.t
89       type input = I.input
90
91       module PSMap = Map.Make(OrderedPathStringElement);;
92
93       type key = PSMap.key
94
95       module DiscriminationTree = Trie.Make(PSMap);;
96
97       type t = A.t DiscriminationTree.t
98
99       let empty = DiscriminationTree.empty;;
100
101       let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;;
102
103       let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;;
104
105       let index tree term info =
106         let ps = I.path_string_of term in
107         let ps_set =
108           try DiscriminationTree.find ps tree with Not_found -> A.empty 
109         in
110         DiscriminationTree.add ps (A.add info ps_set) tree
111       ;;
112
113       let remove_index tree term info =
114         let ps = I.path_string_of term in
115         try
116           let ps_set = A.remove info (DiscriminationTree.find ps tree) in
117           if A.is_empty ps_set then DiscriminationTree.remove ps tree
118           else DiscriminationTree.add ps ps_set tree
119         with Not_found -> tree
120       ;;
121
122       let in_index tree term test =
123         let ps = I.path_string_of term in
124         try
125           let ps_set = DiscriminationTree.find ps tree in
126           A.exists test ps_set
127         with Not_found -> false
128       ;;
129
130       (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is 
131          (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to
132          skip all its progeny, thus you want to reach t.
133       
134          You need to skip as many elements as the sum of all arieties contained
135           in the progeny of f.
136       
137          The input ariety is the one of f while the path is x.g....t  
138          Should be the equivalent of after_t in the literature (handbook A.R.)
139        *)
140       let rec skip arity path =
141         if arity = 0 then path else match path with 
142         | [] -> assert false 
143         | m::tl -> skip (arity-1+arity_of m) tl
144       ;;
145
146       (* the equivalent of skip, but on the index, thus the list of trees
147          that are rooted just after the term represented by the tree root
148          are returned (we are skipping the root) *)
149       let skip_root = function DiscriminationTree.Node (value, map) ->
150         let rec get n = function DiscriminationTree.Node (v, m) as tree ->
151            if n = 0 then [tree] else 
152            PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m []
153         in
154           PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map []
155       ;;
156
157       let retrieve unif tree term =
158         let path = I.path_string_of term in
159         let rec retrieve path tree =
160           match tree, path with
161           | DiscriminationTree.Node (Some s, _), [] -> s
162           | DiscriminationTree.Node (None, _), [] -> A.empty 
163           | DiscriminationTree.Node (_, map), Variable::path when unif ->
164               List.fold_left A.union A.empty
165                 (List.map (retrieve path) (skip_root tree))
166           | DiscriminationTree.Node (_, map), node::path ->
167               A.union
168                  (if not unif && node = Variable then A.empty else
169                   try retrieve path (PSMap.find node map)
170                   with Not_found -> A.empty)
171                  (try
172                     match PSMap.find Variable map,skip (arity_of node) path with
173                     | DiscriminationTree.Node (Some s, _), [] -> s
174                     | n, path -> retrieve path n
175                   with Not_found -> A.empty)
176        in
177         retrieve path tree
178       ;;
179
180       let retrieve_generalizations tree term = retrieve false tree term;;
181       let retrieve_unifiables tree term = retrieve true tree term;;
182   end
183 ;;
184