include Fix__.Sigs

module type TYPE = sig ... end

module type OrderedType = Stdlib.Map.OrderedType

module type HashedType = Stdlib.Hashtbl.HashedType

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.

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.

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.

type 'a fix

` = `('a -> 'a ) -> 'a

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 SOLVER = sig ... end

module type GRAPH = sig ... end

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.

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.

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.

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`

.