(** This module provides a generic algorithm to compute the least
solution of a system of monotonic equations. *)
(**************************************************************************)
(* *)
(* Fix *)
(* *)
(* Author: François Pottier, INRIA Paris-Rocquencourt *)
(* Version: 20091201 *)
(* *)
(* The copyright to this code is held by Institut National de Recherche *)
(* en Informatique et en Automatique (INRIA). All rights reserved. This *)
(* file is distributed under the license CeCILL-C (see file LICENSE). *)
(* *)
(**************************************************************************)
(* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)
(* -------------------------------------------------------------------------- *)
(* Maps. *)
(* We require imperative maps, that is, maps that can be updated in place.
An implementation of persistent maps, such as the one offered by ocaml's
standard library, can easily be turned into an implementation of imperative
maps, so this is a weak requirement. *)
module type IMPERATIVE_MAPS = sig
type key
type 'data t
val create: unit -> 'data t
val clear: 'data t -> unit
val add: key -> 'data -> 'data t -> unit
val find: key -> 'data t -> 'data
val iter: (key -> 'data -> unit) -> 'data t -> unit
end
(* -------------------------------------------------------------------------- *)
(* Properties. *)
(* Properties must form a partial order, equipped with a least element, and
must satisfy the ascending chain condition: every monotone sequence
eventually stabilizes. *)
(* [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 return [false]. If [is_maximal p]
returns [true], then [p] must have no upper bound other than itself. In
particular, if properties form a lattice, then [p] must be the top
element. This feature, not described in the paper, enables a couple of
minor optimizations. *)
module type PROPERTY = sig
type property
val bottom: property
val equal: property -> property -> bool
val is_maximal: property -> bool
end
(* -------------------------------------------------------------------------- *)
(* The code is parametric in an implementation of maps over variables and in
an implementation of properties. *)
module Make
(M : IMPERATIVE_MAPS)
(P : PROPERTY)
: sig
type variable = M.key
type property = P.property
(* A valuation is a mapping of variables to properties. *)
type valuation = variable -> property
(* 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. *)
type rhs = valuation -> property
(* A system of equations is a mapping of variables to right-hand
sides. *)
type equations = variable -> rhs
(* [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. *)
val lfp: equations -> valuation
end
(** val compute_fixpoint : Fixpoints.fixpoint_computer **)