bundles/menhirLib/menhir-20120123/src/Fix.mli

   1 (**************************************************************************)
   2 (*                                                                        *)
   3 (*  Menhir                                                                *)
   4 (*                                                                        *)
   5 (*  François Pottier, INRIA Rocquencourt                                  *)
   6 (*  Yann Régis-Gianas, PPS, Université Paris Diderot                      *)
   7 (*                                                                        *)
   8 (*  Copyright 2005-2008 Institut National de Recherche en Informatique    *)
   9 (*  et en Automatique. All rights reserved. This file is distributed      *)
  10 (*  under the terms of the Q Public License version 1.0, with the change  *)
  11 (*  described in file LICENSE.                                            *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This code is described in the paper ``Lazy Least Fixed Points in ML''. *)
  16
  17 (* -------------------------------------------------------------------------- *)
  18
  19 (* Maps. *)
  20
  21 (* We require imperative maps, that is, maps that can be updated in place.
  22    An implementation of persistent maps, such as the one offered by ocaml's
  23    standard library, can easily be turned into an implementation of imperative
  24    maps, so this is a weak requirement. *)
  25
  26 module type IMPERATIVE_MAPS = sig
  27   type key
  28   type 'data t
  29   val create: unit -> 'data t
  30   val clear: 'data t -> unit
  31   val add: key -> 'data -> 'data t -> unit
  32   val find: key -> 'data t -> 'data
  33   val iter: (key -> 'data -> unit) -> 'data t -> unit
  34 end
  35
  36 (* -------------------------------------------------------------------------- *)
  37
  38 (* Properties. *)
  39
  40 (* Properties must form a partial order, equipped with a least element, and
  41    must satisfy the ascending chain condition: every monotone sequence
  42    eventually stabilizes. *)
  43
  44 (* [is_maximal] determines whether a property [p] is maximal with respect to
  45    the partial order. Only a conservative check is required: in any event, it
  46    is permitted for [is_maximal p] to return [false]. If [is_maximal p]
  47    returns [true], then [p] must have no upper bound other than itself. In
  48    particular, if properties form a lattice, then [p] must be the top
  49    element. This feature, not described in the paper, enables a couple of
  50    minor optimizations. *)
  51
  52 module type PROPERTY = sig
  53   type property
  54   val bottom: property
  55   val equal: property -> property -> bool
  56   val is_maximal: property -> bool
  57 end
  58
  59 (* -------------------------------------------------------------------------- *)
  60
  61 (* The code is parametric in an implementation of maps over variables and in
  62    an implementation of properties. *)
  63
  64 module Make
  65   (M : IMPERATIVE_MAPS)
  66   (P : PROPERTY)
  67   : sig
  68     type variable = M.key
  69     type property = P.property
  70
  71     (* A valuation is a mapping of variables to properties. *)
  72     type valuation = variable -> property
  73
  74     (* A right-hand side, when supplied with a valuation that gives
  75        meaning to its free variables, evaluates to a property. More
  76        precisely, a right-hand side is a monotone function of
  77        valuations to properties. *)
  78     type rhs = valuation -> property
  79
  80     (* A system of equations is a mapping of variables to right-hand
  81        sides. *)
  82     type equations = variable -> rhs
  83
  84     (* [lfp eqs] produces the least solution of the system of monotone
  85        equations [eqs]. *)
  86
  87     (* It is guaranteed that, for each variable [v], the application [eqs v] is
  88        performed at most once (whereas the right-hand side produced by this
  89        application is, in general, evaluated multiple times). This guarantee can
  90        be used to perform costly pre-computation, or memory allocation, when [eqs]
  91        is applied to its first argument. *)
  92
  93     (* When [lfp] is applied to a system of equations [eqs], it performs no
  94        actual computation. It produces a valuation, [get], which represents
  95        the least solution of the system of equations. The actual fixed point
  96        computation takes place, on demand, when [get] is applied. *)
  97     val lfp: equations -> valuation
  98   end
  99