(* This signature describes atoms, that is, abstract entities equipped with a fresh element generation operation. *) module type S = sig (* ------------------------------------------------------------------------- *) (* This is the type of atoms. *) type t (* Atoms do not exist in the ether -- they are taken from universes. Creating a fresh atom requires specifying which universe it should be taken from. Atoms that belong to distinct universes cannot be mixed. *) type universe (* One can create as many universes as desired. A universe initially contains no atoms. A universe carries a name (a string) that is used when converting atoms to strings. *) val new_universe: string -> universe (* A universe is populated by creating fresh atoms. The atom produced by [fresh u] is guaranteed to be distinct from all existing atoms in the universe [u]. *) val fresh: universe -> t (* Comparison of atoms. Only atoms that belong to a common universe can be compared. *) val equal: t -> t -> bool val compare: t -> t -> int (* [print a] converts the atom [a] to a string. The string representation is unique within the universe that [a] belongs to. It is globally unique if universe names are unique. *) val print: t -> string (* ------------------------------------------------------------------------- *) (* Sets of atoms. *) module Set : sig type elt = t (* This is the type of sets of atoms. Every set of atoms is implicitly and permanently associated with a universe, which all members of the set inhabit. *) type t (* Operations over sets include those defined in Objective Caml's standard [Set] module, with the restriction that operations should never mix atoms, or sets of atoms, that inhabit distinct universes. Consult [Set.S] in Objective Caml's documentation. *) val empty: t val is_empty: t -> bool val mem: elt -> t -> bool val add: elt -> t -> t val remove: elt -> t -> t val singleton: elt -> t val union: t -> t -> t val inter: t -> t -> t val diff: t -> t -> t val iter: (elt -> unit) -> t -> unit val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a val choose: t -> elt val equal: t -> t -> bool val cardinal: t -> int val elements: t -> elt list val filter: (elt -> bool) -> t -> t (* [disjoint s1 s2] tells whether the intersection of [s1] and [s2] is empty. *) val disjoint: t -> t -> bool (* [couple x1 x2] is the set that contains [x1] and [x2]. It can be a singleton set if [x1] and [x2] are equal. *) val couple: elt -> elt -> t (* [of_list xs] is the set whose members are the elements of the list [xs]. *) val of_list: elt list -> t (* [pick s] returns a pair of an element [x] of [s] and of the set [remove x s]. It raises [Not_found] if [s] is empty. *) val pick: t -> elt * t (* [exhaust s accu f] takes an element [x] off the set [s], and applies [f] to [x] and [accu]. This yields a number of new elements, which are added to [s], and a new accumulator [accu]. This is repeated until [s] becomes empty, at which point the final value of the accumulator is returned. In short, this is a version of [fold] where the function [f] is allowed to produce new set elements. *) val exhaust: t -> 'a -> (elt -> 'a -> t * 'a) -> 'a (* [print s] converts the set [s] to a string. *) val print: t -> string end (* ------------------------------------------------------------------------- *) (* Maps over atoms. *) module Map : sig type key = t (* This is the type of maps over atoms. Every map over atoms is implicitly and permanently associated with a universe, which all keys inhabit. *) type +'a t (* Operations over maps include those defined in Objective Caml's standard [Map] module, with the restriction that operations should never mix atoms, or maps over atoms, that inhabit distinct universes. Consult [Map.S] in Objective Caml's documentation.*) val empty: 'a t val is_empty: 'a t -> bool val mem: key -> 'a t -> bool val add: key -> 'a -> 'a t -> 'a t val remove: key -> 'a t -> 'a t val find: key -> 'a t -> 'a val iter: (key -> 'a -> unit) -> 'a t -> unit val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val map: ('a -> 'b) -> 'a t -> 'b t val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t (* [singleton x d] is the map that maps [x] to [d]. *) val singleton: key -> 'a -> 'a t (* [addm m1 m2] adds the bindings in the map [m1] to the map [m2], overriding any previous binding if [m1] and [m2] have common keys. *) val addm: 'a t -> 'a t -> 'a t (* [domain m] is the domain of the map [m]. *) val domain: 'a t -> Set.t (* [lift f s] lifts the set [s] into a map that maps every member [x] of [s] to [f x]. *) val lift: (key -> 'a) -> Set.t -> 'a t (* [restrict p m] restricts the domain of the map [m] to those keys that satisfy the predicate [p]. *) val restrict: (key -> bool) -> 'a t -> 'a t (* [generator u] creates a fresh reference [m] that holds an initially empty map; defines a function [generate] such that [generate d] generates a fresh atom [a], adds a mapping of [m] to [d] to [m], and returns [a]; and returns a pair of [m] and [generate]. *) val generator: universe -> 'a t ref * ('a -> key) end (* ------------------------------------------------------------------------- *) (* An imperative interface to maps. *) module ImperativeMap : sig type key = Map.key type 'data t val create: unit -> 'data t val clear: 'data t -> unit val add: key -> 'data -> 'data t -> unit val find: key -> 'data t -> 'data val iter: (key -> 'data -> unit) -> 'data t -> unit end (* ------------------------------------------------------------------------- *) (* Maps of atoms to sets of atoms. Consult the definition of [SetMap.Homogeneous] for a list of operations. *) module SetMap : SetMap.Homogeneous with type key = t and type item = t and type itemset = Set.t and type t = Set.t Map.t end