src/utilities/Fix.mli

   1
   2 (** This module provides a generic algorithm to compute the least
   3     solution of a system of monotonic equations. *)
   4
   5 (**************************************************************************)
   6 (*                                                                        *)
   7 (*  Fix                                                                   *)
   8 (*                                                                        *)
   9 (*  Author:  François Pottier, INRIA Paris-Rocquencourt                   *)
  10 (*  Version: 20091201                                                     *)
  11 (*                                                                        *)
  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).    *)
  15 (*                                                                        *)
  16 (**************************************************************************)
  17
  18 (* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)
  19
  20 (* -------------------------------------------------------------------------- *)
  21
  22 (* Maps. *)
  23
  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. *)
  28
  29 module type IMPERATIVE_MAPS = sig
  30   type key
  31   type 'data t
  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
  37 end
  38
  39 (* -------------------------------------------------------------------------- *)
  40
  41 (* Properties. *)
  42
  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. *)
  46
  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. *)
  54
  55 module type PROPERTY = sig
  56   type property
  57   val bottom: property
  58   val equal: property -> property -> bool
  59   val is_maximal: property -> bool
  60 end
  61
  62 (* -------------------------------------------------------------------------- *)
  63
  64 (* The code is parametric in an implementation of maps over variables and in
  65    an implementation of properties. *)
  66
  67 module Make
  68   (M : IMPERATIVE_MAPS)
  69   (P : PROPERTY)
  70   : sig
  71     type variable = M.key
  72     type property = P.property
  73
  74     (* A valuation is a mapping of variables to properties. *)
  75     type valuation = variable -> property
  76
  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
  82
  83     (* A system of equations is a mapping of variables to right-hand
  84        sides. *)
  85     type equations = variable -> rhs
  86
  87     (* [lfp eqs] produces the least solution of the system of monotone
  88        equations [eqs]. *)
  89
  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. *)
  95
  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
 101   end
 102