Commit a24e358e authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Improved documentation comments.

parent 73245c1a
......@@ -10,17 +10,21 @@
(* *)
(******************************************************************************)
(**This module implements a mutable FIFO queue, like OCaml's [Queue] module.
In comparison with [Queue], it uses a more compact internal representation:
elements are stored contiguously in an array. This has a positive impact on
performance: both time and memory consumption are reduced.
The implementation is optimized for maximum throughput. The internal array
is never shrunk, so a queue that has contained many elements in the past
remains large. Furthermore, array slots are not overwritten when elements
are extracted; thus, an element that has appeared in the queue in the past
can remain reachable. These drawbacks are usually acceptable provided that
the queue is thrown away after use. *)
(**This module offers {b a minimalist mutable FIFO queue} that is
tuned for performance.
In comparison with OCaml's [Queue] module, it uses a more compact
internal representation: elements are stored contiguously in an
array. This has a positive impact on performance: both time and
memory consumption are reduced.
The implementation is optimized for maximum throughput. The
internal array is never shrunk, so a queue that has contained many
elements in the past remains large. Furthermore, array slots are
not overwritten when elements are extracted; thus, an element that
has appeared in the queue in the past can remain reachable. These
drawbacks are usually acceptable provided that the queue is thrown
away after use. *)
type 'a t
(**The type of a queue. *)
......
......@@ -10,20 +10,24 @@
(* *)
(******************************************************************************)
(**[Fix] offers support for computing the least solution of a set of monotone
equations, as described in the unpublished paper "Lazy Least Fixed Points
in ML". In other words, it allows defining a recursive function of type
[variable -> property], where cyclic dependencies between variables are
allowed, and properties must be equipped with a partial order. The function
thus obtained performs the fixed point computation on demand, in an
incremental manner, and is memoizing. *)
(**This module offers support for {b computing the least solution of a set
of monotone equations}, as described in the unpublished paper
{{:http://cambium.inria.fr/~fpottier/publis/fpottier-fix.pdf}Lazy Least
Fixed Points in ML}. In other words, it allows defining a recursive
function of type [variable -> property], where {b cyclic dependencies}
between variables are allowed, and properties must be equipped with a
partial order that has finite ascending chains. This function performs
the fixed point computation on demand, in an incremental manner, and is
memoizing. This is typically used to perform a {b backward data flow
analysis} over a directed graph. This algorithm performs {b dynamic
dependency discovery}, so there is no need for the user to explicitly
describe dependencies between variables. *)
open Sigs
(**[Make] constructs a solver for a type [key] that is equipped with
(**{!Make} constructs a solver for a type [key] that is equipped with
an implementation of imperative maps and a type [property] that is
equipped with [bottom], [equal], and [is_maximal] functions. *)
module Make
(M : IMPERATIVE_MAPS)
(P : PROPERTY)
......@@ -31,11 +35,10 @@ module Make
with type variable = M.key
and type property = P.property
(**[ForOrderedType] is a special case of [Make] where it
(**{!ForOrderedType} is a special case of {!Make} where it
suffices to pass an ordered type [T] as an argument.
A reference to a persistent map is used to hold the
memoization table. *)
module ForOrderedType
(T : OrderedType)
(P : PROPERTY)
......@@ -43,10 +46,9 @@ module ForOrderedType
with type variable = T.t
and type property = P.property
(**[ForHashedType] is a special case of [Make] where it
(**{!ForHashedType} is a special case of {!Make} where it
suffices to pass a hashed type [T] as an argument. A
hash table is used to hold the memoization table. *)
module ForHashedType
(T : HashedType)
(P : PROPERTY)
......@@ -54,11 +56,10 @@ module ForHashedType
with type variable = T.t
and type property = P.property
(**[ForType] is a special case of [Make] where it suffices
(**{!ForType} is a special case of {!Make} where it suffices
to pass an arbitrary type [T] as an argument. A hash table
is used to hold the memoization table. OCaml's built-in
generic equality and hash functions are used. *)
module ForType
(T : TYPE)
(P : PROPERTY)
......
......@@ -10,19 +10,24 @@
(* *)
(******************************************************************************)
(**[DataFlow] performs a forward data flow analysis over a directed graph. *)
(**This module performs a {b forward data flow analysis} over a (possibly
cyclic) directed graph. Like [Fix.Fix], it computes the least function of
type [variable -> property] that satisfies a fixed point equation. It is
less widely applicable than [Fix.Fix], but, when it is applicable, it can
be both easier to use and more efficient. It does not perform dynamic
dependency discovery. The submodule [Fix.DataFlow.ForCustomMaps] is
particularly {b tuned for performance}. *)
open Sigs
(**[Run] requires a type [variable] that is equipped with an implementation of
(**{!Run} requires a type [variable] that is equipped with an implementation of
imperative maps, a type [property] that is equipped with [leq] and [join]
functions, and a data flow graph whose edges describe the propagation of
properties. It performs a forward data flow analysis and returns its
result. *)
result.
(**The function [solution] has type [variable -> property option]. A reachable
The function [solution] has type [variable -> property option]. A reachable
variable is mapped to [Some _]; an unreachable one is mapped to [None]. *)
module Run
(M : MINIMAL_IMPERATIVE_MAPS)
(P : MINIMAL_SEMI_LATTICE)
......@@ -31,11 +36,10 @@ module Run
with type variable = G.variable
and type property = P.property option
(**[ForOrderedType] is a special case of [Run] where it
(**{!ForOrderedType} is a special case of {!Run} where it
suffices to pass an ordered type [T] as an argument.
A reference to a persistent map is used to hold the
memoization table. *)
module ForOrderedType
(T : OrderedType)
(P : MINIMAL_SEMI_LATTICE)
......@@ -44,10 +48,9 @@ module ForOrderedType
with type variable = G.variable
and type property = P.property option
(**[ForHashedType] is a special case of [Run] where it
(**{!ForHashedType} is a special case of {!Run} where it
suffices to pass a hashed type [T] as an argument. A
hash table is used to hold the memoization table. *)
module ForHashedType
(T : HashedType)
(P : MINIMAL_SEMI_LATTICE)
......@@ -56,11 +59,10 @@ module ForHashedType
with type variable = G.variable
and type property = P.property option
(**[ForType] is a special case of [Run] where it suffices
(**{!ForType} is a special case of {!Run} where it suffices
to pass an arbitrary type [T] as an argument. A hash table
is used to hold the memoization table. OCaml's built-in
generic equality and hash functions are used. *)
module ForType
(T : TYPE)
(P : MINIMAL_SEMI_LATTICE)
......@@ -69,9 +71,8 @@ module ForType
with type variable = G.variable
and type property = P.property option
(**[ForIntSegment] is a special case of [Run] where the type of variables
(**{!ForIntSegment} is a special case of {!Run} where the type of variables
is the integer segment [\[0..n)]. An array is used to hold the table. *)
module ForIntSegment
(K : sig val n: int end)
(P : MINIMAL_SEMI_LATTICE)
......@@ -80,11 +81,11 @@ module ForIntSegment
with type variable = G.variable
and type property = P.property option
(**[ForCustomMaps] is a forward data flow analysis that is tuned for greater
performance. It internally relies on [CompactQueue], instead of [Queue].
(**{!ForCustomMaps} is a forward data flow analysis that is tuned for greater
performance. It internally relies on {!CompactQueue}, instead of [Queue].
Furthermore, instead of relying on a full-fledged implementation of maps
as described by [MINIMAL_IMPERATIVE_MAPS], it expects the user to create
and initialize two maps [V] and [B] that satisfy the signature [ARRAY].
as described by {!MINIMAL_IMPERATIVE_MAPS}, it expects the user to create
and initialize two maps [V] and [B] that satisfy the signature {!ARRAY}.
This typically allows the user to choose an efficient, specialized data
representation.
......@@ -93,7 +94,6 @@ module ForIntSegment
The functor returns nothing: the map [V] is modified in place and can be
read by the user after the fixed point has been reached. *)
module ForCustomMaps
(P : MINIMAL_SEMI_LATTICE)
(G : DATA_FLOW_GRAPH with type property := P.property)
......
......@@ -34,21 +34,21 @@ module HashCons = HashCons
module DataFlow = DataFlow
module CompactQueue = CompactQueue
(**This module defines {b a few common partial orders}, each of which
satisfies the signature [PROPERTY]. These include Booleans,
options, and sets. *)
module Prop = struct
(**[Prop] offers a number of ready-made implementations of the
signature [PROPERTY]. *)
(**The lattice of Booleans. *)
module Boolean = Boolean
(* The following declarations are set up so that the user sees
[Prop.Option] and [Prop.Set] as functors. *)
(**The lattice of options. *)
(*The lattice of options. *)
include Option
(**The lattice of sets. *)
(*The lattice of sets. *)
include Set
end
......
......@@ -10,28 +10,26 @@
(* *)
(******************************************************************************)
(**[Gensym] offers a simple facility for generating fresh integer
identifiers. *)
(**This module offers a simple facility for {b generating fresh integer
identifiers}. *)
(**A gensym is a generator of unique integer identifiers. *)
type gensym =
unit -> int
(**[make()] produces a new gensym. *)
val make : unit -> gensym
(**A slightly more powerful abstraction is a generator whose current state
can be inspected (without modification). *)
(**A generator whose current state can be inspected (but not modified). *)
type generator
(**[generator()] creates a new generator. [fresh generator] causes the
generator to create and return a fresh integer identifier. [current
generator] returns the generator's current state, that is, the next
available integer identifier. *)
(**[generator()] creates a new generator. *)
val generator: unit -> generator
(**[fresh g] causes the generator [g] to create and return a fresh
integer identifier. *)
val fresh: generator -> int
(**[current g] returns the current state of the generator [g], that
is, the next available integer identifier. *)
val current: generator -> int
......@@ -10,40 +10,48 @@
(* *)
(******************************************************************************)
(**[Glue] contains glue code that helps build various implementations of
association maps. *)
(**This module contains glue code that helps use the functors provided by
other modules. In particular, it helps build various implementations of
{b association maps}. *)
open Sigs
(* -------------------------------------------------------------------------- *)
(**Some common types, packaged as modules of signature [TYPE]. *)
(** {1 Types} *)
(**The type [char], packaged as a module of signature {!TYPE}. *)
module CHAR : TYPE with type t = char
(**The type [int], packaged as a module of signature {!TYPE}. *)
module INT : TYPE with type t = int
(**The type [string], packaged as a module of signature {!TYPE}. *)
module STRING : TYPE with type t = string
(* -------------------------------------------------------------------------- *)
(**An arbitrary type can be equipped with an ordering function,
just by using OCaml's built-in generic comparison function. *)
(** {1 Ordered and Hashed Types} *)
(**{!TrivialOrderedType} equips an arbitrary type with an ordering function,
just by using OCaml's built-in generic comparison function. *)
module TrivialOrderedType
(T : TYPE)
: OrderedType with type t = T.t
(**An arbitrary type can be equipped with equality and hash functions,
just by using OCaml's built-in generic equality and hash functions. *)
(**{!TrivialHashedType} equips an arbitrary type with equality and hash
functions, just by using OCaml's built-in generic equality and hash
functions. *)
module TrivialHashedType
(T : TYPE)
: HashedType with type t = T.t
(* -------------------------------------------------------------------------- *)
(** {1 Exploiting Injections} *)
(**If there is an injection of [t] into [u], then an ordering on [u] gives
rise to an ordering on [t]. *)
module InjectOrderedType
(U : OrderedType)
(I : INJECTION with type u := U.t)
......@@ -51,7 +59,6 @@ module InjectOrderedType
(**If there is an injection of [t] into [u], then a hashed-type structure
on [u] can be transported to [t]. *)
module InjectHashedType
(U : HashedType)
(I : INJECTION with type u := U.t)
......@@ -59,7 +66,6 @@ module InjectHashedType
(**If there is an injection of [t] into [u], then an implementation of minimal
imperative maps for the type [u] can be transported to the type [t]. *)
module InjectMinimalImperativeMaps
(M : MINIMAL_IMPERATIVE_MAPS)
(I : INJECTION with type u := M.key)
......@@ -68,7 +74,6 @@ module InjectMinimalImperativeMaps
(**If there is an injection of [t] into [u], and if the inverse mapping can be
effectively computed, then an implementation of imperative maps for the
type [u] can be transported to the type [t]. *)
module InjectImperativeMaps
(M : IMPERATIVE_MAPS)
(I : INJECTION with type u := M.key)
......@@ -77,12 +82,11 @@ module InjectImperativeMaps
(* -------------------------------------------------------------------------- *)
(**Implementations of various map signatures. *)
(** {1 Maps} *)
(**An implementation of persistent maps can be made to satisfy the interface
of imperative maps. An imperative map is represented as a persistent map,
wrapped within a reference cell. *)
module PersistentMapsToImperativeMaps
(M : PERSISTENT_MAPS)
: IMPERATIVE_MAPS with type key = M.key
......@@ -90,14 +94,12 @@ module PersistentMapsToImperativeMaps
(**An implementation of imperative maps as arrays is possible if keys
are consecutive integers. *)
module ArraysAsImperativeMaps
(K : sig val n: int end)
: IMPERATIVE_MAPS with type key = int
and type 'data t = 'data option array
(**An implementation of imperative maps as a hash table. *)
module HashTablesAsImperativeMaps
(H : HashedType)
: IMPERATIVE_MAPS with type key = H.t
......@@ -106,7 +108,6 @@ module HashTablesAsImperativeMaps
(**An implementation of imperative maps as a weak hash table.
Use with caution: this table can forget some of its entries,
and can therefore be unsuitable for use in some applications. *)
module WeakHashTablesAsImperativeMaps
(H : HashedType)
: IMPERATIVE_MAPS with type key = H.t
......@@ -114,10 +115,11 @@ module WeakHashTablesAsImperativeMaps
(* -------------------------------------------------------------------------- *)
(**[MinimalSemiLattice] converts a semi-lattice to a minimal semi-lattice;
(** {1 Semi-Lattices} *)
(**{!MinimalSemiLattice} converts a semi-lattice to a minimal semi-lattice;
that is, it implements [leq_join] in terms of separate [leq] and [join]
operations. *)
module MinimalSemiLattice
(P : SEMI_LATTICE)
: MINIMAL_SEMI_LATTICE with type property = P.property
......@@ -10,8 +10,8 @@
(* *)
(******************************************************************************)
(**[GraphNumbering] offers a facility for discovering and numbering the
reachable vertices in a finite directed graph. *)
(**This module offers a facility for {b discovering and numbering the
reachable vertices} in a finite directed graph. *)
open Sigs
......@@ -19,32 +19,28 @@ open Sigs
the subset of the vertices of [G] that are reachable from the roots. The
type of the vertices must be equipped with an implementation of imperative
maps. *)
module Make
(M : IMPERATIVE_MAPS)
(G : GRAPH with type t = M.key)
: NUMBERING with type t = G.t
(**[ForOrderedType] is a special case of [Make] where it suffices for
(**{!ForOrderedType} is a special case of {!Make} where it suffices for
the vertices of [G] to be ordered. *)
module ForOrderedType
(T : OrderedType)
(G : GRAPH with type t = T.t)
: NUMBERING with type t = G.t
(**[ForHashedType] is a special case of [Make] where it suffices for
(**{!ForHashedType} is a special case of {!Make} where it suffices for
the vertices of [G] to be hashed. *)
module ForHashedType
(T : HashedType)
(G : GRAPH with type t = T.t)
: NUMBERING with type t = G.t
(**[ForType] is a special case of [Make] where the vertices of [G] can
(**{!ForType} is a special case of {!Make} where the vertices of [G] can
have arbitrary type. OCaml's built-in generic equality and hash
functions are used. *)
module ForType
(T : TYPE)
(G : GRAPH with type t = T.t)
......
......@@ -10,68 +10,72 @@
(* *)
(******************************************************************************)
(**[HashCons] offers support for setting up a hash-consed data type, that is,
a data type whose values carry unique integer identifiers. *)
(**This module offers support for {b setting up a hash-consed data type},
that is, a data type whose values carry unique integer identifiers. *)
open Sigs
(**The type ['data cell] describes a cell that carries a unique identifier
[id] as well as a payload [data]. *)
[id] as well as a payload [data].
(**This type is marked [private], which means that the user has no direct
way of allocating cells. Instead, the user must apply the functor [Make]
This type is marked [private], which means that the user has no direct
way of allocating cells. Instead, the user must apply the functor {!Make}
(below) to obtain a function [make] which either allocates a fresh cell
or returns an existing cell. The user is still allowed to read existing
cells. *)
type 'data cell = private
{ id: int; data: 'data }
(**Accessors. *)
(**[id cell] returns the integer identifier of the cell [cell]. *)
val id : 'data cell -> int
(**[data cell] returns the payload of the cell [cell]. *)
val data: 'data cell -> 'data
(**Cells come with an equality test, a comparison function, and and a hash
function. These functions exploit the cell's unique identifier only -- the
data is ignored. *)
(**Cells come with an equality test {!equal}, a comparison function
{!compare}, and and a hash function {!hash}. These functions exploit the
cell's unique identifier only: the data is ignored.
(**Wherever a module of signature [HashedType with type t = foo cell] is
expected, the module [HashCons] can be supplied. This holds regardless
of the type [foo]. *)
As a result, wherever a module of signature [HashedType with type t = foo
cell] is expected, the module {!HashCons} can be supplied. This holds
regardless of the type [foo]. *)
(**[equal] determines whether two cells are the same cell.
It is based on the cells' integer identifiers. *)
val equal: 'data cell -> 'data cell -> bool
(**[compare] implements a total order on cells,
It is based on the cells' integer identifiers. *)
val compare: 'data cell -> 'data cell -> int
(**[hash] is a hash function on cells.
It is based on the cells' integer identifiers. *)
val hash : 'data cell -> int
(**A hash-consing service allocates uniquely-numbered cells for data. The
smart constructor [make] either allocates a fresh cell or returns an
existing cell, as appropriate. *)
module type SERVICE = sig
type data
val make: data -> data cell
end
(**The functor [Make] expects a type [data] for which a memoizer exists, and
(**The functor {!Make} expects a type [data] for which a memoizer exists, and
produces a hash-consing service for it. *)
module Make
(M : MEMOIZER)
: SERVICE with type data = M.key
(**[ForHashedType] is a special case of [Make] where it
(**{!ForHashedType} is a special case of {!Make} where it
suffices to pass a hashed type [T] as an argument. A
hash table is used to hold the memoization table. *)
module ForHashedType
(T : HashedType)
: SERVICE with type data = T.t
(**[ForHashedTypeWeak] is a special case of [Make] where it
(**{!ForHashedTypeWeak} is a special case of {!Make} where it
suffices to pass a hashed type [T] as an argument. A weak
hash table is used to hold the memoization table. *)
module ForHashedTypeWeak
(T : HashedType)
: SERVICE with type data = T.t
......@@ -10,17 +10,20 @@
(* *)
(******************************************************************************)
(**This module provides support for constructing finite sets at the type level
and for encoding the inhabitants of these sets as runtime integers. These
runtime integers are statically branded with the name of the set that they
inhabit, so two inhabitants of two distinct sets cannot be inadvertently
confused. *)
(**This module offers {b a safe API for manipulating indices into fixed-size
arrays}.
It provides support for constructing finite sets at the type level and
for encoding the inhabitants of these sets as runtime integers. These
runtime integers are statically branded with the name of the set that
they inhabit, so two inhabitants of two distinct sets cannot be
inadvertently confused. *)
(**If [n] is a type-level name for a finite set, then a value of type
[n cardinal] is a runtime integer that represents the cardinal of
the set [n].
In the following, the functor [Gensym] allows creating open-ended
In the following, the functor {!Gensym} allows creating open-ended
sets, which can grow over time. If [n] is such a set, then a value
of type [n cardinal] can be thought of as the as-yet-undetermined
cardinal of the set. *)
......@@ -29,7 +32,7 @@ type 'n cardinal
(**If [n] is the cardinal of the set [n], then [cardinal n] returns the
cardinal of this set, as a concrete integer.
In the following, the functor [Gensym] allows creating open-ended sets,
In the following, the functor {!Gensym} allows creating open-ended sets,
which can grow over time. If [n] is such a set, then calling [cardinal n]
has the side-effect of freezing this set, thereby fixing its cardinal:
thereafter, calling [fresh] becomes forbidden, so no new elements can be
......@@ -47,7 +50,7 @@ val cardinal : 'n cardinal -> int
type 'n index =
private int
(**A new type-level set is created by an application of the functor {!Const},
(**A new type-level set is created by an application of the functors {!Const},
{!Gensym}, and {!Sum} below. Each functor application creates a fresh type
name [n]. More precisely, each functor application returns a module whose
signature is {!CARDINAL}: it contains both a fresh abstract type [n] and a
......@@ -62,15 +65,15 @@ end
set whose cardinal is [c]. [c] must be nonnegative. *)
module Const (X : sig val cardinal : int end) : CARDINAL
(**The function [const] is a value-level analogue of the functor {!Const}. *)
(**The function {!const} is a value-level analogue of the functor {!Const}. *)
val const : int -> (module CARDINAL)
(**[Empty] contains a type-level name for the empty set. *)
(**{!Empty} contains a type-level name for the empty set. *)
module Empty: CARDINAL
(**[Gensym()] creates an open-ended type-level set, whose cardinality is not
known a priori. As long as the cardinal of the set has not been observed by
invoking [cardinal], new elements can be added to the set by invoking
invoking {!val-cardinal}, new elements can be added to the set by invoking
[fresh]. *)
module Gensym () : sig
......@@ -91,7 +94,7 @@ type ('l, 'r) either =
| L of 'l
| R of 'r
(**The signature [SUM] extends [CARDINAL] with an explicit isomorphism between
(**The signature {!SUM} extends {!CARDINAL} with an explicit isomorphism between
the set [n] and the disjoint sum [l + r]. The functions [inj_l] and [inj_r]
convert an index into [l] or an index into [r] into an index into [n].
Conversely, the function [prj] converts an index into [r] into either an
......@@ -115,11 +118,11 @@ module Sum (L : CARDINAL)(R : CARDINAL) :
SUM with type l := L.n
and type r := R.n
(**The function [sum] is a value-level analogue of the functor {!Sum}. *)
(**The function {!sum} is a value-level analogue of the functor {!Sum}. *)
val sum : 'l cardinal -> 'r cardinal ->
(module SUM with type l = 'l and type r = 'r)
(**The submodule [Index] allows safely manipulating indices
(**The submodule {!Index} allows safely manipulating indices
into a finite set. *)
module Index : sig
......@@ -132,20 +135,20 @@ module Index : sig
fixes the cardinal [n]. *)
val of_int : 'n cardinal -> int -> 'n index
(**[to_int] casts an index [i] back to an ordinary integer value. *)
(**{!to_int} casts an index [i] back to an ordinary integer value. *)
val to_int : 'n index -> int
(**[iter n yield] calls [yield i] successively for every index in the range
[\[0, n)], in increasing order. *)
val iter : 'n cardinal -> ('n index -> unit) -> unit
(**This exception is raised by an iterator (created by [enumerate]) that is
(**This exception is raised by an iterator (created by {!enumerate}) that is
queried after it has been exhausted. *)
exception End_of_set
(**[enumerate n] returns an imperative iterator, which produces all indices
in the range [\[0, n)] in increasing order. Querying the iterator after