(* Pasted from Pottier's PP compiler *)

(** 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

  (* Added by Nicolas Ayache: flexible comparison. Atoms from
     different universes can be compared. *)
  val flex_compare: t -> t -> int
  val flex_equal: t -> t -> bool

  (* Added by Nicolas Ayache. *)
  val universe_of: t -> universe
  val same_universe: t -> t -> bool

  (* [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

  (* ------------------------------------------------------------------------- *)


  (* Added by Nicolas Ayache: more flexible maps and sets where atoms
     from different universes can coexist. *)

  module FlexSet : Set.S with type elt = t

  module FlexMap : Map.S with type key = t


  (* 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