src/common/atomSig.mli

   1 (* Pasted from Pottier's PP compiler *)
   2
   3 (** This signature describes atoms, that is, abstract entities
   4     equipped with a fresh element generation operation. *)
   5
   6 module type S = sig
   7
   8   (* ------------------------------------------------------------------------- *)
   9   (* This is the type of atoms. *)
  10
  11   type t
  12
  13   (* Atoms do not exist in the ether -- they are taken from universes.
  14      Creating a fresh atom requires specifying which universe it
  15      should be taken from. Atoms that belong to distinct universes
  16      cannot be mixed. *)
  17
  18   type universe
  19
  20   (* One can create as many universes as desired. A universe initially
  21      contains no atoms. A universe carries a name (a string) that is
  22      used when converting atoms to strings. *)
  23
  24   val new_universe: string -> universe
  25
  26   (* A universe is populated by creating fresh atoms. The atom produced
  27      by [fresh u] is guaranteed to be distinct from all existing atoms
  28      in the universe [u]. *)
  29
  30   val fresh: universe -> t
  31
  32   (* Comparison of atoms. Only atoms that belong to a common universe
  33      can be compared. *)
  34
  35   val equal: t -> t -> bool
  36   val compare: t -> t -> int
  37
  38   (* Added by Nicolas Ayache: flexible comparison. Atoms from
  39      different universes can be compared. *)
  40   val flex_compare: t -> t -> int
  41   val flex_equal: t -> t -> bool
  42
  43   (* Added by Nicolas Ayache. *)
  44   val universe_of: t -> universe
  45   val same_universe: t -> t -> bool
  46
  47   (* [print a] converts the atom [a] to a string. The string
  48      representation is unique within the universe that [a] belongs
  49      to. It is globally unique if universe names are unique. *)
  50
  51   val print: t -> string
  52
  53   (* ------------------------------------------------------------------------- *)
  54
  55
  56   (* Added by Nicolas Ayache: more flexible maps and sets where atoms
  57      from different universes can coexist. *)
  58
  59   module FlexSet : Set.S with type elt = t
  60
  61   module FlexMap : Map.S with type key = t
  62
  63
  64   (* Sets of atoms. *)
  65
  66   module Set : sig
  67
  68     type elt = t
  69
  70     (* This is the type of sets of atoms. Every set of atoms is
  71        implicitly and permanently associated with a universe, which
  72        all members of the set inhabit. *)
  73
  74     type t
  75
  76     (* Operations over sets include those defined in Objective Caml's
  77        standard [Set] module, with the restriction that operations
  78        should never mix atoms, or sets of atoms, that inhabit distinct
  79        universes. Consult [Set.S] in Objective Caml's
  80        documentation. *)
  81
  82     val empty: t
  83     val is_empty: t -> bool
  84     val mem: elt -> t -> bool
  85     val add: elt -> t -> t
  86     val remove: elt -> t -> t
  87     val singleton: elt -> t
  88     val union: t -> t -> t
  89     val inter: t -> t -> t
  90     val diff: t -> t -> t
  91     val iter: (elt -> unit) -> t -> unit
  92     val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
  93     val choose: t -> elt
  94     val equal: t -> t -> bool
  95     val cardinal: t -> int
  96     val elements: t -> elt list
  97     val filter: (elt -> bool) -> t -> t
  98
  99     (* [disjoint s1 s2] tells whether the intersection of [s1]
 100        and [s2] is empty. *)
 101
 102     val disjoint: t -> t -> bool
 103
 104     (* [couple x1 x2] is the set that contains [x1] and [x2]. It
 105        can be a singleton set if [x1] and [x2] are equal. *)
 106
 107     val couple: elt -> elt -> t
 108
 109     (* [of_list xs] is the set whose members are the elements
 110        of the list [xs]. *)
 111
 112     val of_list: elt list -> t
 113
 114     (* [pick s] returns a pair of an element [x] of [s] and of the
 115        set [remove x s]. It raises [Not_found] if [s] is empty. *)
 116
 117     val pick: t -> elt * t
 118
 119     (* [exhaust s accu f] takes an element [x] off the set [s], and
 120        applies [f] to [x] and [accu]. This yields a number of new
 121        elements, which are added to [s], and a new accumulator [accu].
 122        This is repeated until [s] becomes empty, at which point the
 123        final value of the accumulator is returned. In short, this is a
 124        version of [fold] where the function [f] is allowed to produce
 125        new set elements. *)
 126
 127     val exhaust: t -> 'a -> (elt -> 'a -> t * 'a) -> 'a
 128
 129     (* [print s] converts the set [s] to a string. *)
 130
 131     val print: t -> string
 132
 133   end
 134
 135   (* ------------------------------------------------------------------------- *)
 136   (* Maps over atoms. *)
 137
 138   module Map : sig
 139
 140     type key = t
 141
 142     (* This is the type of maps over atoms. Every map over atoms is
 143        implicitly and permanently associated with a universe, which
 144        all keys inhabit. *)
 145
 146     type +'a t
 147
 148     (* Operations over maps include those defined in Objective Caml's
 149        standard [Map] module, with the restriction that operations
 150        should never mix atoms, or maps over atoms, that inhabit
 151        distinct universes. Consult [Map.S] in Objective Caml's
 152        documentation.*)
 153
 154     val empty: 'a t
 155     val is_empty: 'a t -> bool
 156     val mem: key -> 'a t -> bool
 157     val add: key -> 'a -> 'a t -> 'a t
 158     val remove: key -> 'a t -> 'a t
 159     val find: key -> 'a t -> 'a
 160     val iter: (key -> 'a -> unit) -> 'a t -> unit
 161     val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
 162     val map: ('a -> 'b) -> 'a t -> 'b t
 163     val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
 164
 165     (* [singleton x d] is the map that maps [x] to [d]. *)
 166
 167     val singleton: key -> 'a -> 'a t
 168
 169     (* [addm m1 m2] adds the bindings in the map [m1] to the map [m2],
 170        overriding any previous binding if [m1] and [m2] have common
 171        keys. *)
 172
 173     val addm: 'a t -> 'a t -> 'a t
 174
 175     (* [domain m] is the domain of the map [m]. *)
 176
 177     val domain: 'a t -> Set.t
 178
 179     (* [lift f s] lifts the set [s] into a map that maps every
 180        member [x] of [s] to [f x]. *)
 181
 182     val lift: (key -> 'a) -> Set.t -> 'a t
 183
 184     (* [restrict p m] restricts the domain of the map [m] to those
 185        keys that satisfy the predicate [p]. *)
 186
 187     val restrict: (key -> bool) -> 'a t -> 'a t
 188
 189     (* [generator u] creates a fresh reference [m] that holds an
 190        initially empty map; defines a function [generate] such that
 191        [generate d] generates a fresh atom [a], adds a mapping of [m]
 192        to [d] to [m], and returns [a]; and returns a pair of [m] and
 193        [generate]. *)
 194
 195     val generator: universe -> 'a t ref * ('a -> key)
 196
 197   end
 198
 199   (* ------------------------------------------------------------------------- *)
 200   (* An imperative interface to maps. *)
 201
 202   module ImperativeMap : sig
 203     type key = Map.key
 204     type 'data t
 205     val create: unit -> 'data t
 206     val clear: 'data t -> unit
 207     val add: key -> 'data -> 'data t -> unit
 208     val find: key -> 'data t -> 'data
 209     val iter: (key -> 'data -> unit) -> 'data t -> unit
 210   end
 211
 212   (* ------------------------------------------------------------------------- *)
 213   (* Maps of atoms to sets of atoms. Consult the definition of
 214      [SetMap.Homogeneous] for a list of operations. *)
 215
 216   module SetMap : SetMap.Homogeneous with type key = t
 217                                       and type item = t
 218                                       and type itemset = Set.t
 219                                       and type t = Set.t Map.t
 220
 221 end