]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/extlib/discrimination_tree.mli
short names
[helm.git] / helm / software / components / extlib / discrimination_tree.mli
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
27 type 'a path_string_elem = 
28   | Constant of 'a * int (* name, arity *)
29   | Bound of int * int (* rel, arity *)
30   | Variable (* arity is 0 *)
31   | Proposition (* arity is 0 *) 
32   | Datatype (* arity is 0 *) 
33   | Dead (* arity is 0 *) 
34 ;;  
35
36 type 'a path = ('a path_string_elem) list;;
37
38 module type Indexable = sig
39   type input
40   type constant_name
41   val compare: 
42     constant_name path_string_elem -> 
43     constant_name path_string_elem -> int
44   val string_of_path : constant_name path -> string
45   val path_string_of : input -> constant_name path
46 end
47
48 module type DiscriminationTree  =
49     sig
50
51       type input 
52       type data
53       type dataset
54       type constant_name
55       type t
56
57       val iter : t -> (constant_name path -> dataset -> unit) -> unit
58       val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b
59
60       val empty : t
61       val index : t -> input -> data -> t
62       val remove_index : t -> input -> data -> t
63       val in_index : t -> input -> (data -> bool) -> bool
64       val retrieve_generalizations : t -> input -> dataset
65       val retrieve_unifiables : t -> input -> dataset
66     end
67
68
69 module Make (I : Indexable) (A : Set.S) : DiscriminationTree 
70 with type constant_name = I.constant_name and type input = I.input
71 and type data = A.elt and type dataset = A.t
72