New functions [domain] and [codomain].

src/Atom.ml

@@ -139,6 +139,11 @@ module Set = struct
 
   include Set.Make(Order)
 
+  (* A disjointness test. *)
+
+  let disjoint xs ys =
+    is_empty (inter xs ys)
+
   (* Disjoint union. *)
 
   exception NonDisjointUnion of atom
@@ -194,5 +199,16 @@ module Set = struct
 
 end
 
-module Map =
-  Map.Make(Order)
+module Map = struct
+
+  include Map.Make(Order)
+
+  (* This is O(nlog n), whereas in principle O(n) is possible.
+     The abstraction barrier in OCaml's [Set] module hinders us. *)
+  let domain m =
+    fold (fun a _ accu -> Set.add a accu) m Set.empty
+
+  let codomain f m =
+    fold (fun _ v accu -> Set.union (f v) accu) m Set.empty
+
+end

src/Atom.mli

@@ -28,6 +28,8 @@ val hash: atom -> int
 module Set : sig
   include Set.S with type elt = atom
 
+  val disjoint: t -> t -> bool
+
   (* Disjoint union. *)
 
   exception NonDisjointUnion of atom
@@ -55,4 +57,11 @@ end
 
 (* Maps. *)
 
-module Map : Map.S with type key = atom
+module Map : sig
+
+  include Map.S with type key = atom
+
+  val domain: 'a t -> Set.t
+  val codomain: ('a -> Set.t) -> 'a t -> Set.t
+
+end