Module Fixpoint

module Fixpoint: sig .. end
Fixpoint computation implemented using the work list algorithm. This module makes writing data-flow analysis easy.

One of the simplest fixpoint analysis is that of reachability. Given a directed graph module G, its analysis can be implemented as follows:

      module Reachability = Graph.Fixpoint.Make(G)
          (struct
            type vertex = G.E.vertex
            type edge = G.E.t
            type g = G.t
            type data = bool
            let direction = Graph.Fixpoint.Forward
            let equal = (=)
            let join = (||)
            let analyze _ = (fun x -> x)
          end)
    

The types for vertex, edge and g are those of the graph to be analyzed. The data type is bool: It will tell if the vertex is reachable from the start vertex. The equal operation for bool is simply structural equality; the join operation is logical or. The analyze function is very simple, too: If the predecessor vertex is reachable, so is the successor vertex of the edge.

To use the analysis, an instance of a graph g is required. For this analysis a predicate is_root_vertex : G.E.vertex -> bool is required to initialize the reachability of the root vertex to true and of all other vertices to false.

      let g = ...
        let result = Reachability.analyze is_root_vertex g
    

The result is a map of type G.E.vertex -> bool that can be queried for every vertex to tell if the vertex is reachable from the root vertex.
Author(s): Markus W. Weissmann
See also


module type G = sig .. end
Minimal graph signature for work list algorithm
type direction = 
| Forward
| Backward (*Type of an analysis*)
module type Analysis = sig .. end
module Make: 
functor (G : G) ->
functor (A : Analysis with type g = G.t with type edge = G.E.t with type vertex = G.V.t) -> sig .. end