source: Deliverables/D2.2/8051/src/common/atomSig.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 6.8 KB
Line 
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
6module 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
221end
Note: See TracBrowser for help on using the repository browser.