1 (* Pasted from Pottier's PP compiler *)
3 (** This signature describes atoms, that is, abstract entities
4 equipped with a fresh element generation operation. *)
8 (* ------------------------------------------------------------------------- *)
9 (* This is the type of atoms. *)
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
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. *)
24 val new_universe: string -> universe
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]. *)
30 val fresh: universe -> t
32 (* Comparison of atoms. Only atoms that belong to a common universe
35 val equal: t -> t -> bool
36 val compare: t -> t -> int
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
43 (* Added by Nicolas Ayache. *)
44 val universe_of: t -> universe
45 val same_universe: t -> t -> bool
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. *)
51 val print: t -> string
53 (* ------------------------------------------------------------------------- *)
56 (* Added by Nicolas Ayache: more flexible maps and sets where atoms
57 from different universes can coexist. *)
59 module FlexSet : Set.S with type elt = t
61 module FlexMap : Map.S with type key = t
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. *)
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
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
91 val iter: (elt -> unit) -> t -> unit
92 val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
94 val equal: t -> t -> bool
95 val cardinal: t -> int
96 val elements: t -> elt list
97 val filter: (elt -> bool) -> t -> t
99 (* [disjoint s1 s2] tells whether the intersection of [s1]
100 and [s2] is empty. *)
102 val disjoint: t -> t -> bool
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. *)
107 val couple: elt -> elt -> t
109 (* [of_list xs] is the set whose members are the elements
112 val of_list: elt list -> t
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. *)
117 val pick: t -> elt * t
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
127 val exhaust: t -> 'a -> (elt -> 'a -> t * 'a) -> 'a
129 (* [print s] converts the set [s] to a string. *)
131 val print: t -> string
135 (* ------------------------------------------------------------------------- *)
136 (* Maps over atoms. *)
142 (* This is the type of maps over atoms. Every map over atoms is
143 implicitly and permanently associated with a universe, which
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
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
165 (* [singleton x d] is the map that maps [x] to [d]. *)
167 val singleton: key -> 'a -> 'a t
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
173 val addm: 'a t -> 'a t -> 'a t
175 (* [domain m] is the domain of the map [m]. *)
177 val domain: 'a t -> Set.t
179 (* [lift f s] lifts the set [s] into a map that maps every
180 member [x] of [s] to [f x]. *)
182 val lift: (key -> 'a) -> Set.t -> 'a t
184 (* [restrict p m] restricts the domain of the map [m] to those
185 keys that satisfy the predicate [p]. *)
187 val restrict: (key -> bool) -> 'a t -> 'a t
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
195 val generator: universe -> 'a t ref * ('a -> key)
199 (* ------------------------------------------------------------------------- *)
200 (* An imperative interface to maps. *)
202 module ImperativeMap : sig
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
212 (* ------------------------------------------------------------------------- *)
213 (* Maps of atoms to sets of atoms. Consult the definition of
214 [SetMap.Homogeneous] for a list of operations. *)
216 module SetMap : SetMap.Homogeneous with type key = t
218 and type itemset = Set.t
219 and type t = Set.t Map.t