```(* A universe is a record, whose address defines the identity of the
universe. The integer counter [next] holds the number of the next
fresh atom. The [name] field holds the name of the universe. *)

type universe = {
mutable next: int;
name: string
}

let new_universe name = {
next = 0;
name = name
}

(* An atom is a pair of a universe and an integer. The latter defines
the atom's identity within its universe. *)

type t =
universe * int

let fresh u =
let id = u.next in
u.next <- id + 1;
u, id

let equal (u1, id1) (u2, id2) =
assert (u1 == u2);
(id1 : int) = (id2 : int)

let compare (u1, id1) (u2, id2) =
assert (u1 == u2);
compare (id1 : int) (id2 : int)

let ends_with_a_digit s =
let n = String.length s in
n > 0 && s.[n-1] >= '0' && s.[n-1] <= '9'

(* This function is injective, that is, [u] and [id] can be recovered
out of [print (u, id)]. *)

let print (u, id) =
Printf.sprintf "%s%s%d" u.name (if ends_with_a_digit u.name then "_" else "") id

module OrderedInt = struct
type t = int
let compare x1 x2 = x1 - x2
end

(* We internally rely upon Objective Caml's integer sets and maps. *)

module ISet = Set.Make (OrderedInt)
module IMap = Map.Make (OrderedInt)

(* Sets. *)

module Set = struct

(* A set is either empty or a pair of a universe and a (possibly
empty) internal set. The fact that we do not require the empty
set to be explicitly associated with a universe means that
[empty] can be a constant, as opposed to an operation that
expects a universe as a parameter. *)

type elt =
t

type t =
| E
| U of universe * ISet.t

let empty =
E

let is_empty = function
| E ->
true
| U (_, s) ->
ISet.is_empty s

let mem (u1, x) = function
| E ->
false
| U (u2, s) ->
assert (u1 == u2);
ISet.mem x s

let add (u1, x) = function
| E ->
U (u1, ISet.singleton x)
| U (u2, s) ->
assert (u1 == u2);

let remove (u1, x) = function
| E ->
E
| U (u2, s) ->
assert (u1 == u2);
(* set can become empty but retains its universe *)
U (u1, ISet.remove x s)

let singleton x =

let couple x1 x2 =

let of_list xs =

let union s1 s2 =
match s1, s2 with
| E, s
| s, E ->
s
| U (u1, s1), U (u2, s2) ->
assert (u1 == u2);
U (u1, ISet.union s1 s2)

let inter s1 s2 =
match s1, s2 with
| E, s
| s, E ->
E
| U (u1, s1), U (u2, s2) ->
assert (u1 == u2);
U (u1, ISet.inter s1 s2)

let disjoint s1 s2 =
is_empty (inter s1 s2)

let diff s1 s2 =
match s1, s2 with
| E, _ ->
E
| s, E ->
s
| U (u1, s1), U (u2, s2) ->
assert (u1 == u2);
U (u1, ISet.diff s1 s2)

let iter f = function
| E ->
()
| U (u, s) ->
ISet.iter (fun x -> f (u, x)) s

let fold f s accu =
match s with
| E ->
accu
| U (u, s) ->
ISet.fold (fun x accu -> f (u, x) accu) s accu

let choose = function
| E ->
raise Not_found
| U (u, s) ->
u, ISet.choose s

let equal s1 s2 =
match s1, s2 with
| E, s
| s, E ->
is_empty s
| U (u1, s1), U (u2, s2) ->
assert (u1 == u2);
ISet.equal s1 s2

let cardinal = function
| E ->
0
| U (_, s) ->
ISet.cardinal s

let elements = function
| E ->
[]
| U (u, s) ->
List.map (fun x -> (u, x)) (ISet.elements s)

let filter p = function
| E ->
E
| U (u, s) ->
U (u, ISet.filter (fun x -> p (u, x)) s)

let pick s =
let x = choose s in
let s = remove x s in
x, s

let rec exhaust s accu f =
if is_empty s then
accu
else
let x, s = pick s in
let s', accu = f x accu in
exhaust (union s s') accu f

open Print

let print s =
seplist comma (fun () x -> print x) () (elements s)

end

(* Maps. *)

module Map = struct

(* A map is either empty or a pair of a universe and a (possibly
empty) internal map. The fact that we do not require the empty
map to be explicitly associated with a universe means that
[empty] can be a constant, as opposed to an operation that
expects a universe as a parameter. *)

type key =
t

type 'a t =
| E
| U of universe * 'a IMap.t

let empty =
E

let is_empty = function
| E ->
true
| U (_, m) ->
IMap.is_empty m

let mem (u1, x) = function
| E ->
false
| U (u2, m) ->
assert (u1 == u2);
IMap.mem x m

let add (u1, x) d = function
| E ->
U (u1, IMap.add x d IMap.empty)
| U (u2, m) ->
assert (u1 == u2);
U (u1, IMap.add x d m)

let remove (u1, x) = function
| E ->
E
| U (u2, m) ->
assert (u1 == u2);
U (u1, IMap.remove x m)

let singleton x d =

let find (u1, x) = function
| E ->
raise Not_found
| U (u2, m) ->
assert (u1 == u2);
IMap.find x m

let iter f = function
| E ->
()
| U (u, m) ->
IMap.iter (fun x d -> f (u, x) d) m

let fold f m accu =
match m with
| E ->
accu
| U (u, m) ->
IMap.fold (fun x d accu -> f (u, x) d accu) m accu

let map f = function
| E ->
E
| U (u, m) ->
U (u, IMap.map f m)

let mapi f = function
| E ->
E
| U (u, m) ->
U (u, IMap.mapi (fun x d -> f (u, x) d) m)

let domain = function
| E ->
Set.E
| U (u, m) ->
Set.U (u, IMap.fold (fun x _ s ->
) m ISet.empty
)

let lift f = function
| Set.E ->
E
| Set.U (u, s) ->
U (u, ISet.fold (fun x m ->
IMap.add x (f (u, x)) m
) s IMap.empty
)

let generator u =
let m = ref empty in
let generate d =
let label = fresh u in
m := add label d !m;
label
in
m, generate

let restrict p m =
fold (fun x d m ->
if p x then
else
m
) m empty

end

(* An imperative interface to maps. *)

module ImperativeMap = struct

type key =
Map.key

type 'data t =
'data Map.t ref

let create () =
ref Map.empty

let clear t =
t := Map.empty

let add k d t =
t := Map.add k d !t

let find k t =
Map.find k !t

let iter f t =
Map.iter f !t

end

(* Maps of atoms to sets of atoms. *)

module SetMap = SetMap.MakeHomo(Set)(Map)

```