`Fix.Make`

`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 M : sig ... end`

`module P : sig ... end`

`type variable = M.key`

The type of variables.

`type property = P.property`

The type of properties.

A right-hand side, when supplied with a valuation that gives meaning to its free variables, evaluates to a property. More precisely, a right-hand side is a monotone function of valuations to properties.

A system of equations is a mapping of variables to right-hand sides.

`lfp eqs`

produces the least solution of the system of monotone equations `eqs`

.

It is guaranteed that, for each variable `v`

, the application `eqs v`

is performed at most once (whereas the right-hand side produced by this application is, in general, evaluated multiple times). This guarantee can be used to perform costly pre-computation, or memory allocation, when `eqs`

is applied to its first argument.

When `lfp`

is applied to a system of equations `eqs`

, it performs no actual computation. It produces a valuation, `get`

, which represents the least solution of the system of equations. The actual fixed point computation takes place, on demand, when `get`

is applied.