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.