source: Deliverables/D2.2/8051/src/common/atom.ml @ 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(* 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
7type universe = {
8    mutable next: int;
9    name: string
10  }
11
12let 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
20type t =
21   universe * int
22
23let fresh u =
24   let id = u.next in
25   u.next <- id + 1;
26   u, id
27
28let equal (u1, id1) (u2, id2) =
29  assert (u1 == u2);
30  ((id1 : int) = (id2 : int))
31
32let compare (u1, id1) (u2, id2) =
33  assert (u1 == u2);
34  compare (id1 : int) (id2 : int)
35
36let 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
40let flex_equal l1 l2 = flex_compare l1 l2 = 0
41
42let universe_of (u, _) = u
43
44let same_universe (u1, _) (u2, _) = u1 = u2
45
46let 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
53let 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
59type label_t = t
60
61module OrderedLabel = struct
62  type t = label_t
63  let compare = flex_compare
64end
65
66module FlexSet = Set.Make (OrderedLabel)
67
68module FlexMap = Map.Make (OrderedLabel)
69
70
71module OrderedInt = struct
72  type t = int
73  let compare x1 x2 = x1 - x2
74end
75
76(* We internally rely upon Objective Caml's integer sets and maps. *)
77
78module ISet = Set.Make (OrderedInt)
79module IMap = Map.Make (OrderedInt)
80
81(* Sets. *)
82
83module 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
233end
234
235(* Maps. *)
236
237module 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
356end
357
358(* An imperative interface to maps. *)
359
360module 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
383end
384
385(* Maps of atoms to sets of atoms. *)
386
387module SetMap = SetMap.MakeHomo(Set)(Map)
Note: See TracBrowser for help on using the repository browser.