2 (** This module provides a generic algorithm to compute the least
3 solution of a system of monotonic equations. *)
5 (**************************************************************************)
9 (* Author: François Pottier, INRIA Paris-Rocquencourt *)
10 (* Version: 20091201 *)
12 (* The copyright to this code is held by Institut National de Recherche *)
13 (* en Informatique et en Automatique (INRIA). All rights reserved. This *)
14 (* file is distributed under the license CeCILL-C (see file LICENSE). *)
16 (**************************************************************************)
18 (* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)
20 (* -------------------------------------------------------------------------- *)
24 (* We require imperative maps, that is, maps that can be updated in place.
25 An implementation of persistent maps, such as the one offered by ocaml's
26 standard library, can easily be turned into an implementation of imperative
27 maps, so this is a weak requirement. *)
29 module type IMPERATIVE_MAPS = sig
32 val create: unit -> 'data t
33 val clear: 'data t -> unit
34 val add: key -> 'data -> 'data t -> unit
35 val find: key -> 'data t -> 'data
36 val iter: (key -> 'data -> unit) -> 'data t -> unit
39 (* -------------------------------------------------------------------------- *)
43 (* Properties must form a partial order, equipped with a least element, and
44 must satisfy the ascending chain condition: every monotone sequence
45 eventually stabilizes. *)
47 (* [is_maximal] determines whether a property [p] is maximal with respect to
48 the partial order. Only a conservative check is required: in any event, it
49 is permitted for [is_maximal p] to return [false]. If [is_maximal p]
50 returns [true], then [p] must have no upper bound other than itself. In
51 particular, if properties form a lattice, then [p] must be the top
52 element. This feature, not described in the paper, enables a couple of
53 minor optimizations. *)
55 module type PROPERTY = sig
58 val equal: property -> property -> bool
59 val is_maximal: property -> bool
62 (* -------------------------------------------------------------------------- *)
64 (* The code is parametric in an implementation of maps over variables and in
65 an implementation of properties. *)
72 type property = P.property
74 (* A valuation is a mapping of variables to properties. *)
75 type valuation = variable -> property
77 (* A right-hand side, when supplied with a valuation that gives
78 meaning to its free variables, evaluates to a property. More
79 precisely, a right-hand side is a monotone function of
80 valuations to properties. *)
81 type rhs = valuation -> property
83 (* A system of equations is a mapping of variables to right-hand
85 type equations = variable -> rhs
87 (* [lfp eqs] produces the least solution of the system of monotone
90 (* It is guaranteed that, for each variable [v], the application [eqs v] is
91 performed at most once (whereas the right-hand side produced by this
92 application is, in general, evaluated multiple times). This guarantee can
93 be used to perform costly pre-computation, or memory allocation, when [eqs]
94 is applied to its first argument. *)
96 (* When [lfp] is applied to a system of equations [eqs], it performs no
97 actual computation. It produces a valuation, [get], which represents
98 the least solution of the system of equations. The actual fixed point
99 computation takes place, on demand, when [get] is applied. *)
100 val lfp: equations -> valuation