FixSourceA type alone.
An ordered type. A hashed type. These are standard notions.
A type whose elements can be enumerated.
Association 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.
Imperative 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.
An 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.
The 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.
The signature MINIMAL_SEMI_LATTICE is used by Fix.DataFlow.
The type of a fixed point combinator that constructs a value of type 'a.
Memoizers -- higher-order functions that construct memoizing functions.
Tabulators: 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.
Solvers: higher-order functions that compute the least solution of a monotone system of equations.
The signature SOLUTION is used to describe the result of Fix.DataFlow.
Directed, rooted graphs.
The 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.
Numberings.
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.
A 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).
A 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.
Injections.
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.
Glue contains glue code that helps build various implementations of association maps.
Memoize 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.
Numbering 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.
GraphNumbering offers a facility for discovering and numbering the reachable vertices in a finite directed graph.
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.
Tabulate 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.
Gensym offers a simple facility for generating fresh integer identifiers.
HashCons offers support for setting up a hash-consed data type, that is, a data type whose values carry unique integer identifiers.
DataFlow performs a forward data flow analysis over a directed graph.
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.
Prop offers a number of ready-made implementations of the signature PROPERTY.
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.