1 | (* Pasted from Pottier's PP compiler *) |
---|
2 | |
---|
3 | (** This signature describes atoms, that is, abstract entities |
---|
4 | equipped with a fresh element generation operation. *) |
---|
5 | |
---|
6 | module type S = sig |
---|
7 | |
---|
8 | (* ------------------------------------------------------------------------- *) |
---|
9 | (* This is the type of atoms. *) |
---|
10 | |
---|
11 | type t |
---|
12 | |
---|
13 | (* Atoms do not exist in the ether -- they are taken from universes. |
---|
14 | Creating a fresh atom requires specifying which universe it |
---|
15 | should be taken from. Atoms that belong to distinct universes |
---|
16 | cannot be mixed. *) |
---|
17 | |
---|
18 | type universe |
---|
19 | |
---|
20 | (* One can create as many universes as desired. A universe initially |
---|
21 | contains no atoms. A universe carries a name (a string) that is |
---|
22 | used when converting atoms to strings. *) |
---|
23 | |
---|
24 | val new_universe: string -> universe |
---|
25 | |
---|
26 | (* A universe is populated by creating fresh atoms. The atom produced |
---|
27 | by [fresh u] is guaranteed to be distinct from all existing atoms |
---|
28 | in the universe [u]. *) |
---|
29 | |
---|
30 | val fresh: universe -> t |
---|
31 | |
---|
32 | (* Comparison of atoms. Only atoms that belong to a common universe |
---|
33 | can be compared. *) |
---|
34 | |
---|
35 | val equal: t -> t -> bool |
---|
36 | val compare: t -> t -> int |
---|
37 | |
---|
38 | (* Added by Nicolas Ayache: flexible comparison. Atoms from |
---|
39 | different universes can be compared. *) |
---|
40 | val flex_compare: t -> t -> int |
---|
41 | val flex_equal: t -> t -> bool |
---|
42 | |
---|
43 | (* Added by Nicolas Ayache. *) |
---|
44 | val universe_of: t -> universe |
---|
45 | val same_universe: t -> t -> bool |
---|
46 | |
---|
47 | (* [print a] converts the atom [a] to a string. The string |
---|
48 | representation is unique within the universe that [a] belongs |
---|
49 | to. It is globally unique if universe names are unique. *) |
---|
50 | |
---|
51 | val print: t -> string |
---|
52 | |
---|
53 | (* ------------------------------------------------------------------------- *) |
---|
54 | |
---|
55 | |
---|
56 | (* Added by Nicolas Ayache: more flexible maps and sets where atoms |
---|
57 | from different universes can coexist. *) |
---|
58 | |
---|
59 | module FlexSet : Set.S with type elt = t |
---|
60 | |
---|
61 | module FlexMap : Map.S with type key = t |
---|
62 | |
---|
63 | |
---|
64 | (* Sets of atoms. *) |
---|
65 | |
---|
66 | module Set : sig |
---|
67 | |
---|
68 | type elt = t |
---|
69 | |
---|
70 | (* This is the type of sets of atoms. Every set of atoms is |
---|
71 | implicitly and permanently associated with a universe, which |
---|
72 | all members of the set inhabit. *) |
---|
73 | |
---|
74 | type t |
---|
75 | |
---|
76 | (* Operations over sets include those defined in Objective Caml's |
---|
77 | standard [Set] module, with the restriction that operations |
---|
78 | should never mix atoms, or sets of atoms, that inhabit distinct |
---|
79 | universes. Consult [Set.S] in Objective Caml's |
---|
80 | documentation. *) |
---|
81 | |
---|
82 | val empty: t |
---|
83 | val is_empty: t -> bool |
---|
84 | val mem: elt -> t -> bool |
---|
85 | val add: elt -> t -> t |
---|
86 | val remove: elt -> t -> t |
---|
87 | val singleton: elt -> t |
---|
88 | val union: t -> t -> t |
---|
89 | val inter: t -> t -> t |
---|
90 | val diff: t -> t -> t |
---|
91 | val iter: (elt -> unit) -> t -> unit |
---|
92 | val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a |
---|
93 | val choose: t -> elt |
---|
94 | val equal: t -> t -> bool |
---|
95 | val cardinal: t -> int |
---|
96 | val elements: t -> elt list |
---|
97 | val filter: (elt -> bool) -> t -> t |
---|
98 | |
---|
99 | (* [disjoint s1 s2] tells whether the intersection of [s1] |
---|
100 | and [s2] is empty. *) |
---|
101 | |
---|
102 | val disjoint: t -> t -> bool |
---|
103 | |
---|
104 | (* [couple x1 x2] is the set that contains [x1] and [x2]. It |
---|
105 | can be a singleton set if [x1] and [x2] are equal. *) |
---|
106 | |
---|
107 | val couple: elt -> elt -> t |
---|
108 | |
---|
109 | (* [of_list xs] is the set whose members are the elements |
---|
110 | of the list [xs]. *) |
---|
111 | |
---|
112 | val of_list: elt list -> t |
---|
113 | |
---|
114 | (* [pick s] returns a pair of an element [x] of [s] and of the |
---|
115 | set [remove x s]. It raises [Not_found] if [s] is empty. *) |
---|
116 | |
---|
117 | val pick: t -> elt * t |
---|
118 | |
---|
119 | (* [exhaust s accu f] takes an element [x] off the set [s], and |
---|
120 | applies [f] to [x] and [accu]. This yields a number of new |
---|
121 | elements, which are added to [s], and a new accumulator [accu]. |
---|
122 | This is repeated until [s] becomes empty, at which point the |
---|
123 | final value of the accumulator is returned. In short, this is a |
---|
124 | version of [fold] where the function [f] is allowed to produce |
---|
125 | new set elements. *) |
---|
126 | |
---|
127 | val exhaust: t -> 'a -> (elt -> 'a -> t * 'a) -> 'a |
---|
128 | |
---|
129 | (* [print s] converts the set [s] to a string. *) |
---|
130 | |
---|
131 | val print: t -> string |
---|
132 | |
---|
133 | end |
---|
134 | |
---|
135 | (* ------------------------------------------------------------------------- *) |
---|
136 | (* Maps over atoms. *) |
---|
137 | |
---|
138 | module Map : sig |
---|
139 | |
---|
140 | type key = t |
---|
141 | |
---|
142 | (* This is the type of maps over atoms. Every map over atoms is |
---|
143 | implicitly and permanently associated with a universe, which |
---|
144 | all keys inhabit. *) |
---|
145 | |
---|
146 | type +'a t |
---|
147 | |
---|
148 | (* Operations over maps include those defined in Objective Caml's |
---|
149 | standard [Map] module, with the restriction that operations |
---|
150 | should never mix atoms, or maps over atoms, that inhabit |
---|
151 | distinct universes. Consult [Map.S] in Objective Caml's |
---|
152 | documentation.*) |
---|
153 | |
---|
154 | val empty: 'a t |
---|
155 | val is_empty: 'a t -> bool |
---|
156 | val mem: key -> 'a t -> bool |
---|
157 | val add: key -> 'a -> 'a t -> 'a t |
---|
158 | val remove: key -> 'a t -> 'a t |
---|
159 | val find: key -> 'a t -> 'a |
---|
160 | val iter: (key -> 'a -> unit) -> 'a t -> unit |
---|
161 | val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b |
---|
162 | val map: ('a -> 'b) -> 'a t -> 'b t |
---|
163 | val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t |
---|
164 | |
---|
165 | (* [singleton x d] is the map that maps [x] to [d]. *) |
---|
166 | |
---|
167 | val singleton: key -> 'a -> 'a t |
---|
168 | |
---|
169 | (* [addm m1 m2] adds the bindings in the map [m1] to the map [m2], |
---|
170 | overriding any previous binding if [m1] and [m2] have common |
---|
171 | keys. *) |
---|
172 | |
---|
173 | val addm: 'a t -> 'a t -> 'a t |
---|
174 | |
---|
175 | (* [domain m] is the domain of the map [m]. *) |
---|
176 | |
---|
177 | val domain: 'a t -> Set.t |
---|
178 | |
---|
179 | (* [lift f s] lifts the set [s] into a map that maps every |
---|
180 | member [x] of [s] to [f x]. *) |
---|
181 | |
---|
182 | val lift: (key -> 'a) -> Set.t -> 'a t |
---|
183 | |
---|
184 | (* [restrict p m] restricts the domain of the map [m] to those |
---|
185 | keys that satisfy the predicate [p]. *) |
---|
186 | |
---|
187 | val restrict: (key -> bool) -> 'a t -> 'a t |
---|
188 | |
---|
189 | (* [generator u] creates a fresh reference [m] that holds an |
---|
190 | initially empty map; defines a function [generate] such that |
---|
191 | [generate d] generates a fresh atom [a], adds a mapping of [m] |
---|
192 | to [d] to [m], and returns [a]; and returns a pair of [m] and |
---|
193 | [generate]. *) |
---|
194 | |
---|
195 | val generator: universe -> 'a t ref * ('a -> key) |
---|
196 | |
---|
197 | end |
---|
198 | |
---|
199 | (* ------------------------------------------------------------------------- *) |
---|
200 | (* An imperative interface to maps. *) |
---|
201 | |
---|
202 | module ImperativeMap : sig |
---|
203 | type key = Map.key |
---|
204 | type 'data t |
---|
205 | val create: unit -> 'data t |
---|
206 | val clear: 'data t -> unit |
---|
207 | val add: key -> 'data -> 'data t -> unit |
---|
208 | val find: key -> 'data t -> 'data |
---|
209 | val iter: (key -> 'data -> unit) -> 'data t -> unit |
---|
210 | end |
---|
211 | |
---|
212 | (* ------------------------------------------------------------------------- *) |
---|
213 | (* Maps of atoms to sets of atoms. Consult the definition of |
---|
214 | [SetMap.Homogeneous] for a list of operations. *) |
---|
215 | |
---|
216 | module SetMap : SetMap.Homogeneous with type key = t |
---|
217 | and type item = t |
---|
218 | and type itemset = Set.t |
---|
219 | and type t = Set.t Map.t |
---|
220 | |
---|
221 | end |
---|