(* This module defines a couple of signatures that specify the
interaction between [alphaLib] and user programs. *)
(*i ----------------------------------------------------------------------- i*)
(* \ocwmoduletype{Identifier} *)
(* This signature defines the operations that an implementation of
identifiers must provide in order to appear in an \kw{identifier
module} declaration.
Identifiers are usually human-readable. In fact, the default
implementation of identifiers, which is automatically supplied by
\ac when no \kw{identifier module} declaration is made, equates
identifiers with strings.
An implementation of atoms can be built on top of any implementation
of identifiers via the internal functor [AlphaLib.Atom.Make].
This functor application is automatically performed by \ac in
order to produce each of the ``atom'' modules (one per sort).
In order to implement this signature, one must isolate a strict
subset of identifiers, which we refer to as ``base'' identifiers.
There must exist a function, referred to as [basename], that maps
arbitrary identifiers to base identifiers. This function does not
have to (and usually cannot) be injective. (A function is injective
when it maps distinct inputs to distinct outputs.) Nevertheless,
the more information it preserves, the better. Conversely, there
must exist an injective function, referred to as [combine], that
maps a pair of a base identifier and an integer value to an
identifier.
Internally, every atom records the image through [basename] of the
identifier that it originally stood for. This base identifier plays
no role in determining the identity of the atom: that is, it is not
used when comparing two atoms. It is kept around for use when the
atom is converted back to an identifier. At this point, it is
combined, via [combine], with a unique integer, in order to obtain
suitably fresh identifier.
If [basename] and [combine] are properly chosen, then the final
identifier that is printed ``resembles'' the one that was
originally found. More precisely, it is desirable that the
next two laws be satisfied:
\begin{center}
[basename (combine identifier i) = identifier] \\
[combine identifier 0 = identifier]
\end{center}
The first law states that the information added by combining an
identifier with an integer [i] is exactly the information that
is lost when applying [basename]. The second law states that
combining the integer 0 with an identifier should have no effect.
This is exploited to avoid needless renamings.
The default implementation of identifiers as strings defines base
identifiers as strings that do not end with two underscore
characters and a number. A base identifier and an integer value are
combined simply by appending [__], followed with a decimal
representation of the latter, to the former. In practice, this
means that the identifier [x] will be successively renamed into
[x], [x__1], [x__2], [x__3], and so on. *)
module type Identifier = sig
(* [t] is the type of identifiers. *)
type t
(* Identifiers must be comparable. As usual in Objective Caml,
[compare id1 id2] must return a negative integer if [id1] is less
than [id2], a positive integer if [id2] is less than [id1], and
zero otherwise. *)
val compare: t -> t -> int
(* [basename] and [combine] are described above. *)
val basename: t -> t
val combine: t -> int -> t
(* The sub-module [Map] provides maps whose keys are identifiers.
It is usually produced by applying the standard library functor
[Map.Make] to the type [t] and the function [compare] above.
This sub-module is used by the functions that convert back and
forth between raw and internal forms, that is, between atoms
and identifiers. *)
module Map : Map.S with type key = t
end
(*i ----------------------------------------------------------------------- i*)
(* \ocwmoduletype{Atom} *)
(* This signature specifies the operations that every ``atom'' module
provides. These operations are grouped into several sub-modules
that provide:
\begin{itemize}
\item basic operations on atoms;
\item sets of atoms;
\item maps of atoms to arbitrary data;
\item maps of atoms to identifiers;
\item substitutions of atoms for atoms.
\end{itemize}
*)
(*i ----------------------------------------------------------------------- i*)
(* \ocwbar *)
module type Atom = sig
(* The type [identifier] is the type of the identifiers on top of
which this implementation of atoms is built. *)
type identifier
(* This exception is raised by the (automatically generated) functions
that convert raw forms into internal forms when an unbound identifier
is encountered. *)
exception UnboundIdentifier of identifier
(* This is a version of [Identifier.Map.find] that raises
[UnboundIdentifier] when it fails. *)
type 'a identifier_map
val find: identifier -> 'a identifier_map -> 'a
(* The sub-module [Atom] offers an abstract type of atoms. Atoms are
abstract entities that support two (classes of) operations,
namely creation of fresh atoms and comparison of two atoms.
Every atom carries a unique integer, which can be viewed as its
identity. This integer is used in comparisons. A global integer
counter is maintained and incremented when fresh atoms are
created.
Every atom also carries a base name, that is, an identifier. This
identifier is not in general unique, and is not part of the
atom's identity. It is used when converting atoms back to
identifiers: see, for instance, [AtomIdMap.add].
When a fresh atom is created, its base name is taken either from
an existing identifier or from an existing atom. Two functions,
[freshb] and [fresha], are provided for this purpose. *)
module Atom : sig
(* [t] is the type of atoms. *)
type t
(* The call [freshb identifier] produces a fresh atom whose base
name is that of [identifier]. *)
val freshb: identifier -> t
(* [mfreshb] is undocumented. *)
val mfreshb: unit identifier_map -> t identifier_map -> t identifier_map
(* The call [fresha a] produces a fresh atom whose base name is
that of [a]. *)
val fresha: t -> t
(* Atoms can be tested for equality, for ordering, and hashed.
The user is warned against careless use of [compare] and
[hash]. Atoms are renamed during \acon, which affects their
relative ordering and their hash code. It is fine to use
these operations as long as one guarantees that no renaming
takes place. *)
val equal: t -> t -> bool
val compare: t -> t -> int
val hash: t -> int
(* It is possible to retrieve an atom's identity and base name.
There is in general no good reason of doing so, except for
debugging purposes. *)
val identity: t -> int
val basename: t -> identifier
(* The exception [Unknown] is raised by [AtomIdMap.lookup]. *)
exception Unknown of t
end
(* The sub-module [AtomSet] offers a representation of finite sets
of atoms. *)
module AtomSet : sig
(* [t] is the type of sets of atoms. *)
type t
type element = Atom.t
(* [empty] is the empty set. *)
val empty: t
(* [singleton a] is the singleton set [{a}]. *)
val singleton: element -> t
(* [add x s] is ([{x}]\tcup[s]). *)
val add: element -> t -> t
(* [remove x s] is ([s]\tminus[{x}]). *)
val remove: element -> t -> t
(* [union s1 s2] is ([s1]\tcup[s2]). *)
val union: t -> t -> t
(* [inter s1 s2] is ([s1]\tcap[s2]). *)
val inter: t -> t -> t
(* [diff s1 s2] is ([s1]\tminus[s2]). *)
val diff: t -> t -> t
(* [mem a s] is [true] if and only if [a] is a member of [s]. *)
val mem: element -> t -> bool
(* [is_empty s] is [true] if and only if [s] is the empty set. *)
val is_empty: t -> bool
(* [disjoint s1 s2] is [true] if and only if the sets [s1] and
[s2] are disjoint, that is, if and only if their intersection
is empty. *)
val disjoint: t -> t -> 
