source: Deliverables/D2.2/8051/src/utilities/Fix.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 4.2 KB
Line 
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
29module 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
37end
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
55module type PROPERTY = sig
56  type property
57  val bottom: property
58  val equal: property -> property -> bool
59  val is_maximal: property -> bool
60end
61
62(* -------------------------------------------------------------------------- *)
63
64(* The code is parametric in an implementation of maps over variables and in
65   an implementation of properties. *)
66
67module 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 
Note: See TracBrowser for help on using the repository browser.