module type TYPE = sig ... endAn ordered type. A hashed type. These are standard notions.
module type OrderedType = Map.OrderedTypemodule type HashedType = Hashtbl.HashedTypeA type whose elements can be enumerated.
module type FINITE_TYPE = sig ... endAssociation maps.
Following the convention of the ocaml standard library, find raises the exception Not_found when the key is not in the domain of the map. In contrast, get returns an option.
Persistent maps. The empty map is a constant. Insertion creates a new map.
This is a fragment of the standard signature Map.S.
module type PERSISTENT_MAPS = sig ... endImperative maps. A fresh empty map is produced by create. Insertion updates a map in place. clear empties an existing map.
The order of the arguments to add and find is consistent with the order used in PERSISTENT_MAPS above. Thus, it departs from the convention used in OCaml's Hashtbl module.
module type MINIMAL_IMPERATIVE_MAPS = sig ... endmodule type IMPERATIVE_MAPS = sig ... endmodule type ARRAY = sig ... endAn instance of the signature ARRAY represents one mutable map. There is no type 'data t and no create operation; there exists just one map. Furthermore, the type value, which corresponds to 'data in the previous signatures, is fixed.
The signature PROPERTY is used by Fix.Make, the least fixed point computation algorithm.
The type property must form a partial order. It must be equipped with a least element bottom and with an equality test equal. (In the function call equal p q, it is permitted to assume that p <= q holds.) We do not require an ordering test leq. We do not require a join operation lub. We do require the ascending chain condition: every monotone sequence must eventually stabilize.
The function is_maximal determines whether a property p is maximal with respect to the partial order. Only a conservative check is required: in any event, it is permitted for is_maximal p to be false. If is_maximal p is true, then p must have no strict upper bound. In particular, in the case where properties form a lattice, this means that p must be the top element.
module type PROPERTY = sig ... endThe signature SEMI_LATTICE offers separate leq and join functions. The functor Glue.MinimalSemiLattice can be used, if necessary, to convert this signature to MINIMAL_SEMI_LATTICE.
module type SEMI_LATTICE = sig ... endThe signature MINIMAL_SEMI_LATTICE is used by Fix.DataFlow.
module type MINIMAL_SEMI_LATTICE = sig ... endThe type of a fixed point combinator that constructs a value of type 'a.
Memoizers -- higher-order functions that construct memoizing functions.
module type MEMOIZER = sig ... endTabulators: higher-order functions that construct tabulated functions.
Like memoization, tabulation guarantees that, for every key x, the image f x is computed at most once. Unlike memoization, where this computation takes place on demand, in the case of tabulation, the computation of every f x takes place immediately, when tabulate is invoked. The graph of the function f, a table, is constructed and held in memory.
module type TABULATOR = sig ... endSolvers: higher-order functions that compute the least solution of a monotone system of equations.
module type SOLVER = sig ... endThe signature SOLUTION is used to describe the result of Fix.DataFlow.
module type SOLUTION = sig ... endDirected, rooted graphs.
module type GRAPH = sig ... endThe signature DATA_FLOW_GRAPH is used to describe a data flow analysis problem. It is used to describe the input to Fix.DataFlow.
The function foreach_root describes the root nodes of the data flow graph as well as the properties associated with them. foreach_call contribute is expected to call contribute x p to indicate that x is a root and that p is a lower bound on the solution at x. It is permitted to call contribute x _ several times at a root x.
The function foreach_successor describes the edges of the data flow graph as well as the manner in which a property at the source of an edge is transformed into a property at the target. The property at the target must of course be a monotonic function of the property at the source.
module type DATA_FLOW_GRAPH = sig ... endNumberings.
An ongoing numbering of (a subset of) a type t offers a function encode which maps a value of type t to a unique integer code. If applied twice to the same value, encode returns the same code; if applied to a value that has never been encountered, it returns a fresh code. The function current returns the next available code, which is also the number of values that have been encoded so far. The function has_been_encoded tests whether a value has been encoded already.
module type ONGOING_NUMBERING = sig ... endA numbering of (a subset of) a type t is a triple of an integer n and two functions encode and decode which represent an isomorphism between this subset of t and the interval [0..n).
module type NUMBERING = sig ... endA combination of the above two signatures. According to this signature, a numbering process is organized in two phases. During the first phase, the numbering is ongoing; one can encode keys, but not decode. Applying the functor Done() ends the first phase. A fixed numbering then becomes available, which gives access to the total number n of encoded keys and to both encode and decode functions.
module type TWO_PHASE_NUMBERING = sig ... endInjections.
An injection of t into u is an injective function of type t -> u. Because encode is injective, encode x can be thought of as the identity of the object x.
module type INJECTION = sig ... endmodule Glue : sig ... endGlue contains glue code that helps build various implementations of association maps.
module Memoize : sig ... endMemoize offers a number of combinators that help construct possibly recursive memoizing functions, that is, functions that lazily record their input/output graph, so as to avoid repeated computation.
module Numbering : sig ... endNumbering offers a facility for assigning a unique number to each value in a certain finite set and translating (both ways) between values and their numbers.
module GraphNumbering : sig ... endGraphNumbering offers a facility for discovering and numbering the reachable vertices in a finite directed graph.
module Indexing : sig ... endThis 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.
module Tabulate : sig ... endTabulate offers facilities for tabulating a function, that is, eagerly evaluating this function at every point in its domain, so as to obtain an equivalent function that can be queried in constant time.
module Gensym : sig ... endGensym offers a simple facility for generating fresh integer identifiers.
module HashCons : sig ... endHashCons offers support for setting up a hash-consed data type, that is, a data type whose values carry unique integer identifiers.
module DataFlow : sig ... endDataFlow performs a forward data flow analysis over a directed graph.
module CompactQueue : sig ... endThis 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.
module Prop : sig ... endProp offers a number of ready-made implementations of the signature PROPERTY.
module Fix : sig ... endFix 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.