package fix

You can search for identifiers within the package.

in-package search v0.2.0

package fix

fix
- Fix
  - DATA_FLOW_GRAPH
  - DataFlow
    
    ForHashedType
    
    G
    
    P
    
    T
    
    ForIntSegment
    
    G
    
    K
    
    P
    
    ForOrderedType
    
    G
    
    P
    
    T
    
    ForType
    
    G
    
    P
    
    T
    
    Run
    
    G
    
    M
    
    P
  - FINITE_TYPE
  - Fix
    
    ForHashedType
    
    P
    
    T
    
    ForOrderedType
    
    P
    
    T
    
    ForType
    
    P
    
    T
    
    Make
    
    M
    
    P
  - GRAPH
  - Gensym
  - Glue
    
    ArraysAsImperativeMaps
    
    K
    
    CHAR
    
    HashTablesAsImperativeMaps
    
    H
    
    INT
    
    InjectHashedType
    
    I
    
    U
    
    InjectImperativeMaps
    
    I
    
    J
    
    M
    
    InjectMinimalImperativeMaps
    
    I
    
    M
    
    InjectOrderedType
    
    I
    
    U
    
    MinimalSemiLattice
    
    P
    
    PersistentMapsToImperativeMaps
    
    M
    
    STRING
    
    TrivialHashedType
    
    T
    
    TrivialOrderedType
    
    T
    
    WeakHashTablesAsImperativeMaps
    
    H
  - GraphNumbering
    
    ForHashedType
    
    G
    
    T
    
    ForOrderedType
    
    G
    
    T
    
    ForType
    
    G
    
    T
    
    Make
    
    G
    
    M
  - HashCons
    
    ForHashedType
    
    T
    
    ForHashedTypeWeak
    
    T
    
    Make
    
    M
    
    SERVICE
  - IMPERATIVE_MAPS
  - INJECTION
  - MEMOIZER
  - MINIMAL_IMPERATIVE_MAPS
  - MINIMAL_SEMI_LATTICE
  - Make
    
    M
    
    P
  - Memoize
    
    Char
    
    ForHashedType
    
    T
    
    ForOrderedType
    
    T
    
    ForType
    
    T
    
    Int
    
    Make
    
    M
    
    String
  - NUMBERING
  - Numbering
    
    ForHashedType
    
    Done
    
    T
    
    ForOrderedType
    
    Done
    
    T
    
    ForType
    
    Done
    
    T
    
    Make
    
    Done
    
    M
  - ONGOING_NUMBERING
  - PERSISTENT_MAPS
  - PROPERTY
  - Prop
    
    Boolean
    
    Option
    
    X
    
    Set
    
    X
  - SEMI_LATTICE
  - SOLUTION
  - SOLVER
  - TABULATOR
  - TWO_PHASE_NUMBERING
    
    Done
  - TYPE
  - Tabulate
    
    ForHashedType
    
    F
    
    T
    
    ForIntSegment
    
    K
    
    ForOrderedType
    
    F
    
    T
    
    ForType
    
    F
    
    Make
    
    F
    
    M

Legend:
Library
Module
Module type
Parameter
Class
Class type

module type TYPE = sig ... end

An ordered type. A hashed type. These are standard notions.

module type OrderedType = Map.OrderedType

module type HashedType = Hashtbl.HashedType

A type whose elements can be enumerated.

module type FINITE_TYPE = sig ... end

Association maps.

Following the convention of the ocaml standard library, find raises the exception Not_found when the key is not in the domain of the map. In contrast, get returns an option.

Persistent maps. The empty map is a constant. Insertion creates a new map.

This is a fragment of the standard signature Map.S.

module type PERSISTENT_MAPS = sig ... end

Imperative maps. A fresh empty map is produced by create. Insertion updates a map in place. clear empties an existing map.

The order of the arguments to add and find is consistent with the order used in PERSISTENT_MAPS above. Thus, it departs from the convention used in OCaml's Hashtbl module.

module type MINIMAL_IMPERATIVE_MAPS = sig ... end

module type IMPERATIVE_MAPS = sig ... end

The signature PROPERTY is used by Fix.Make, the least fixed point computation algorithm.

The type property must form a partial order. It must be equipped with a least element bottom and with an equality test equal. (In the function call equal p q, it is permitted to assume that p <= q holds.) We do not require an ordering test leq. We do not require a join operation lub. We do require the ascending chain condition: every monotone sequence must eventually stabilize.

The function is_maximal determines whether a property p is maximal with respect to the partial order. Only a conservative check is required: in any event, it is permitted for is_maximal p to be false. If is_maximal p is true, then p must have no strict upper bound. In particular, in the case where properties form a lattice, this means that p must be the top element.

module type PROPERTY = sig ... end

The signature SEMI_LATTICE offers separate leq and join functions. The functor Glue.MinimalSemiLattice can be used, if necessary, to convert this signature to MINIMAL_SEMI_LATTICE.

module type SEMI_LATTICE = sig ... end

The signature MINIMAL_SEMI_LATTICE is used by Fix.DataFlow.

module type MINIMAL_SEMI_LATTICE = sig ... end

The type of a fixed point combinator that constructs a value of type 'a.

type 'a fix = ('a -> 'a) -> 'a

Memoizers -- higher-order functions that construct memoizing functions.

module type MEMOIZER = sig ... end

Tabulators: higher-order functions that construct tabulated functions.

Like memoization, tabulation guarantees that, for every key x, the image f x is computed at most once. Unlike memoization, where this computation takes place on demand, in the case of tabulation, the computation of every f x takes place immediately, when tabulate is invoked. The graph of the function f, a table, is constructed and held in memory.

module type TABULATOR = sig ... end

Solvers: higher-order functions that compute the least solution of a monotone system of equations.

module type SOLVER = sig ... end

The signature SOLUTION is used to describe the result of Fix.DataFlow.

module type SOLUTION = sig ... end

Directed, rooted graphs.

module type GRAPH = sig ... end

The signature DATA_FLOW_GRAPH is used to describe a data flow analysis problem. It is used to describe the input to Fix.DataFlow.

The function foreach_root describes the root nodes of the data flow graph as well as the properties associated with them.

The function foreach_successor describes the edges of the data flow graph as well as the manner in which a property at the source of an edge is transformed into a property at the target. The property at the target must of course be a monotonic function of the property at the source.

module type DATA_FLOW_GRAPH = sig ... end

Numberings.

An ongoing numbering of (a subset of) a type t offers a function encode which maps a value of type t to a unique integer code. If applied twice to the same value, encode returns the same code; if applied to a value that has never been encountered, it returns a fresh code. The function current returns the next available code, which is also the number of values that have been encoded so far. The function has_been_encoded tests whether a value has been encoded already.

module type ONGOING_NUMBERING = sig ... end

A numbering of (a subset of) a type t is a triple of an integer n and two functions encode and decode which represent an isomorphism between this subset of t and the interval [0..n).

module type NUMBERING = sig ... end

A combination of the above two signatures. According to this signature, a numbering process is organized in two phases. During the first phase, the numbering is ongoing; one can encode keys, but not decode. Applying the functor Done() ends the first phase. A fixed numbering then becomes available, which gives access to the total number n of encoded keys and to both encode and decode functions.

module type TWO_PHASE_NUMBERING = sig ... end

Injections.

An injection of t into u is an injective function of type t -> u. Because encode is injective, encode x can be thought of as the identity of the object x.

module type INJECTION = sig ... end

module Glue : sig ... end

Glue contains glue code that helps build various implementations of association maps.

module Memoize : sig ... end

Memoize offers a number of combinators that help construct possibly recursive memoizing functions, that is, functions that lazily record their input/output graph, so as to avoid repeated computation.

module Numbering : sig ... end

Numbering offers a facility for assigning a unique number to each value in a certain finite set and translating (both ways) between values and their numbers.

module GraphNumbering : sig ... end

GraphNumbering offers a facility for discovering and numbering the reachable vertices in a finite directed graph.

module Tabulate : sig ... end

Tabulate offers facilities for tabulating a function, that is, eagerly evaluating this function at every point in its domain, so as to obtain an equivalent function that can be queried in constant time.

module Gensym : sig ... end

Gensym offers a simple facility for generating fresh integer identifiers.

module HashCons : sig ... end

HashCons offers support for setting up a hash-consed data type, that is, a data type whose values carry unique integer identifiers.

module DataFlow : sig ... end

DataFlow performs a forward data flow analysis over a directed graph.

module Prop : sig ... end

Prop offers a number of ready-made implementations of the signature PROPERTY.

module Fix : sig ... end

Fix offers support for computing the least solution of a set of monotone equations, as described in the unpublished paper "Lazy Least Fixed Points in ML". In other words, it allows defining a recursive function of type variable -> property, where cyclic dependencies between variables are allowed, and properties must be equipped with a partial order. The function thus obtained performs the fixed point computation on demand, in an incremental manner, and is memoizing.

module Make (M : sig ... end) (P : sig ... end) : sig ... end