]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/common/atom.ml
Package description and copyright added.
[pkg-cerco/acc.git] / src / common / atom.ml
1 (* Adapted from Pottier's PP compiler *)
2
3 (* A universe is a record, whose address defines the identity of the
4    universe. The integer counter [next] holds the number of the next
5    fresh atom. The [name] field holds the name of the universe. *)
6
7 type universe = {
8     mutable next: int;
9     name: string
10   }
11
12 let new_universe name = {
13   next = 0;
14   name = name
15 }
16
17 (* An atom is a pair of a universe and an integer. The latter defines
18    the atom's identity within its universe. *)
19
20 type t =
21    universe * int
22
23 let fresh u =
24    let id = u.next in
25    u.next <- id + 1;
26    u, id
27
28 let equal (u1, id1) (u2, id2) =
29   assert (u1 == u2);
30   ((id1 : int) = (id2 : int))
31
32 let compare (u1, id1) (u2, id2) =
33   assert (u1 == u2);
34   compare (id1 : int) (id2 : int)
35
36 let flex_compare (u1, id1) (u2, id2) =
37   if String.compare u1.name u2.name = 0 then Pervasives.compare id1 id2
38   else String.compare u1.name u2.name
39
40 let flex_equal l1 l2 = flex_compare l1 l2 = 0
41
42 let universe_of (u, _) = u
43
44 let same_universe (u1, _) (u2, _) = u1 = u2
45
46 let ends_with_a_digit s =
47   let n = String.length s in
48   n > 0 && s.[n-1] >= '0' && s.[n-1] <= '9'
49
50 (* This function is injective, that is, [u] and [id] can be recovered
51    out of [print (u, id)]. *)
52
53 let print (u, id) =
54   Printf.sprintf "%s%s%d" u.name (if ends_with_a_digit u.name then "_" else "") id
55
56 (* Added by Nicolas Ayache: more flexible maps and sets where atoms
57    from different universes can coexist. *)
58
59 type label_t = t
60
61 module OrderedLabel = struct
62   type t = label_t
63   let compare = flex_compare
64 end
65
66 module FlexSet = Set.Make (OrderedLabel)
67
68 module FlexMap = Map.Make (OrderedLabel)
69
70
71 module OrderedInt = struct
72   type t = int
73   let compare x1 x2 = x1 - x2
74 end
75
76 (* We internally rely upon Objective Caml's integer sets and maps. *)
77
78 module ISet = Set.Make (OrderedInt)
79 module IMap = Map.Make (OrderedInt)
80
81 (* Sets. *)
82
83 module Set = struct
84
85   (* A set is either empty or a pair of a universe and a (possibly
86      empty) internal set. The fact that we do not require the empty
87      set to be explicitly associated with a universe means that
88      [empty] can be a constant, as opposed to an operation that
89      expects a universe as a parameter. *)
90
91   type elt =
92       t
93
94   type t =
95     | E
96     | U of universe * ISet.t
97
98   let empty =
99     E
100
101   let is_empty = function
102     | E ->
103         true
104     | U (_, s) ->
105         ISet.is_empty s
106
107   let mem (u1, x) = function
108     | E ->
109         false
110     | U (u2, s) ->
111         assert (u1 == u2);
112         (u1 = u2) && (ISet.mem x s)
113
114   let add (u1, x) = function
115     | E ->
116         U (u1, ISet.singleton x)
117     | U (u2, s) ->
118         assert (u1 == u2);
119         U (u1, ISet.add x s)
120
121   let remove (u1, x) = function
122     | E ->
123         E
124     | U (u2, s) ->
125         assert (u1 == u2);
126         (* set can become empty but retains its universe *)
127         U (u1, ISet.remove x s)
128
129   let singleton x =
130     add x empty
131
132   let couple x1 x2 =
133     add x1 (singleton x2)
134
135   let of_list xs =
136     List.fold_right add xs empty
137
138   let union s1 s2 =
139     match s1, s2 with
140     | E, s
141     | s, E ->
142         s
143     | U (u1, s1), U (u2, s2) ->
144         assert (u1 == u2);
145         U (u1, ISet.union s1 s2)
146
147   let inter s1 s2 =
148     match s1, s2 with
149     | E, s
150     | s, E ->
151         E
152     | U (u1, s1), U (u2, s2) ->
153         assert (u1 == u2);
154         U (u1, ISet.inter s1 s2)
155
156   let disjoint s1 s2 =
157     is_empty (inter s1 s2)
158
159   let diff s1 s2 =
160     match s1, s2 with
161     | E, _ ->
162         E
163     | s, E ->
164         s
165     | U (u1, s1), U (u2, s2) ->
166         assert (u1 == u2);
167         U (u1, ISet.diff s1 s2)
168
169   let iter f = function
170     | E ->
171         ()
172     | U (u, s) ->
173         ISet.iter (fun x -> f (u, x)) s
174
175   let fold f s accu =
176     match s with
177     | E ->
178         accu
179     | U (u, s) ->
180         ISet.fold (fun x accu -> f (u, x) accu) s accu
181
182   let choose = function
183     | E ->
184         raise Not_found
185     | U (u, s) ->
186         u, ISet.choose s
187
188   let equal s1 s2 =
189     match s1, s2 with
190     | E, s
191     | s, E ->
192         is_empty s
193     | U (u1, s1), U (u2, s2) ->
194         assert (u1 == u2);
195         ISet.equal s1 s2
196
197   let cardinal = function
198     | E ->
199         0
200     | U (_, s) ->
201         ISet.cardinal s
202
203   let elements = function
204     | E ->
205         []
206     | U (u, s) ->
207         List.map (fun x -> (u, x)) (ISet.elements s)
208
209   let filter p = function
210     | E ->
211         E
212     | U (u, s) ->
213         U (u, ISet.filter (fun x -> p (u, x)) s)
214
215   let pick s =
216     let x = choose s in
217     let s = remove x s in
218     x, s
219
220   let rec exhaust s accu f =
221     if is_empty s then
222       accu
223     else
224       let x, s = pick s in
225       let s', accu = f x accu in
226       exhaust (union s s') accu f
227
228   open Print
229
230   let print s =
231     seplist comma (fun () x -> print x) () (elements s)
232
233 end
234
235 (* Maps. *)
236
237 module Map = struct
238
239   (* A map is either empty or a pair of a universe and a (possibly
240      empty) internal map. The fact that we do not require the empty
241      map to be explicitly associated with a universe means that
242      [empty] can be a constant, as opposed to an operation that
243      expects a universe as a parameter. *)
244
245   type key =
246       t
247
248   type 'a t =
249     | E
250     | U of universe * 'a IMap.t
251
252   let empty =
253     E
254
255   let is_empty = function
256     | E ->
257         true
258     | U (_, m) ->
259         IMap.is_empty m
260
261   let mem (u1, x) = function
262     | E ->
263         false
264     | U (u2, m) ->
265         assert (u1 == u2);
266         IMap.mem x m
267
268   let add (u1, x) d = function
269     | E ->
270         U (u1, IMap.add x d IMap.empty)
271     | U (u2, m) ->
272         assert (u1 == u2);
273         U (u1, IMap.add x d m)
274
275   let remove (u1, x) = function
276     | E ->
277         E
278     | U (u2, m) ->
279         assert (u1 == u2);
280         U (u1, IMap.remove x m)
281
282   let singleton x d =
283     add x d empty
284
285   let find (u1, x) = function
286     | E ->
287         raise Not_found
288     | U (u2, m) ->
289         assert (u1 == u2);
290         IMap.find x m
291
292   let iter f = function
293     | E ->
294         ()
295     | U (u, m) ->
296         IMap.iter (fun x d -> f (u, x) d) m
297
298   let fold f m accu =
299     match m with
300     | E ->
301         accu
302     | U (u, m) ->
303         IMap.fold (fun x d accu -> f (u, x) d accu) m accu
304
305   let map f = function
306     | E ->
307         E
308     | U (u, m) ->
309         U (u, IMap.map f m)
310
311   let mapi f = function
312     | E ->
313         E
314     | U (u, m) ->
315         U (u, IMap.mapi (fun x d -> f (u, x) d) m)
316
317   let domain = function
318     | E ->
319         Set.E
320     | U (u, m) ->
321         Set.U (u, IMap.fold (fun x _ s ->
322                     ISet.add x s
323                   ) m ISet.empty
324               )
325
326   let lift f = function
327     | Set.E ->
328         E
329     | Set.U (u, s) ->
330         U (u, ISet.fold (fun x m ->
331                 IMap.add x (f (u, x)) m
332               ) s IMap.empty
333           )
334
335
336   let generator u =
337     let m = ref empty in
338     let generate d =
339       let label = fresh u in
340       m := add label d !m;
341       label
342     in
343     m, generate
344
345   let addm m1 m2 =
346     fold add m1 m2
347
348   let restrict p m =
349     fold (fun x d m ->
350       if p x then
351         add x d m
352       else
353         m
354     ) m empty
355
356 end
357
358 (* An imperative interface to maps. *)
359
360 module ImperativeMap = struct
361
362   type key =
363       Map.key
364   
365   type 'data t =
366       'data Map.t ref
367       
368   let create () =
369     ref Map.empty
370
371   let clear t =
372     t := Map.empty
373     
374   let add k d t =
375     t := Map.add k d !t
376
377   let find k t =
378     Map.find k !t
379
380   let iter f t =
381     Map.iter f !t
382
383 end
384
385 (* Maps of atoms to sets of atoms. *)
386
387 module SetMap = SetMap.MakeHomo(Set)(Map)