Datafix.Worklist

This module provides the solveProblem function, which solves the description of a DataFlowFramework by employing a worklist algorithm. There's also an interpreter for Denotational problems in the form of evalDenotation.

Documentation

data DependencyM graph domain a

The concrete MonadDependency for this worklist-based solver.

This essentially tracks the current approximation of the solution to the DataFlowFramework as mutable state while solveProblem makes sure we will eventually halt with a conservative approximation.

Instances

Monad (DependencyM graph domain)

Defined in Datafix.Worklist.Internal

Methods

(>>=) :: DependencyM graph domain a -> (a -> DependencyM graph domain b) -> DependencyM graph domain b

(>>) :: DependencyM graph domain a -> DependencyM graph domain b -> DependencyM graph domain b

return :: a -> DependencyM graph domain a

fail :: String -> DependencyM graph domain a

Functor (DependencyM graph domain)

Defined in Datafix.Worklist.Internal

Methods

fmap :: (a -> b) -> DependencyM graph domain a -> DependencyM graph domain b

(<$) :: a -> DependencyM graph domain b -> DependencyM graph domain a

Applicative (DependencyM graph domain)

Defined in Datafix.Worklist.Internal

Methods

pure :: a -> DependencyM graph domain a

(<*>) :: DependencyM graph domain (a -> b) -> DependencyM graph domain a -> DependencyM graph domain b

liftA2 :: (a -> b -> c) -> DependencyM graph domain a -> DependencyM graph domain b -> DependencyM graph domain c

(*>) :: DependencyM graph domain a -> DependencyM graph domain b -> DependencyM graph domain b

(<*) :: DependencyM graph domain a -> DependencyM graph domain b -> DependencyM graph domain a

Datafixable domain => MonadDomain (DependencyM graph domain)

The Domain is extracted from a type parameter.

Defined in Datafix.Worklist.Internal

Associated Types

type Domain (DependencyM graph domain) :: Type

(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain)

This allows us to solve MonadDependency m => DataFlowFramework m descriptions with solveProblem.

Defined in Datafix.Worklist.Internal

Methods

dependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain)

type Domain (DependencyM graph domain)

Defined in Datafix.Worklist.Internal

type Domain (DependencyM graph domain) = domain

data Density graph where

Specifies the density of the problem, e.g. whether the domain of Nodes can be confined to a finite range, in which case solveProblem tries to use a Data.Vector based graph representation rather than one based on Data.IntMap.

Constructors

Sparse :: Density Ref

Dense :: Node -> Density Ref

data IterationBound domain

Expresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.

Constructors

NeverAbort

Will keep on iterating until a precise, yet conservative approximation has been reached. Make sure that your domain satisfies the ascending chain condition, e.g. that fixed-point iteration always comes to a halt!

AbortAfter Int (AbortionFunction domain)

For when your domain doesn't satisfy the ascending chain condition or when you are sensitive about solution performance.

The Integer determines the maximum number of iterations of a single point of a Node (with which an entire function with many points may be associated) before iteration aborts in that point by calling the supplied AbortionFunction. The responsibility of the AbortionFunction is to find a sufficiently conservative approximation for the current value at that point.

When your ReturnType is an instance of BoundedMeetSemiLattice, abortWithTop might be a worthwhile option. A more sophisticated solution would trim the current value to a certain cut-off depth, depending on the first parameter, instead.

solveProblem

Arguments

:: GraphRef graph

=> Datafixable domain

=> DataFlowFramework (DependencyM graph domain)

The description of the DataFlowFramework.

-> Density graph

Describes if the algorithm is free to use a Dense, Vector-based graph representation or has to go with a Sparse one based on IntMap.

-> IterationBound domain

Whether the solution algorithm should respect a maximum bound on the number of iterations per point. Pass NeverAbort if you don't care.

-> DependencyM graph domain a

The action for which we want to compute the solution. May reference Nodes from the DataFlowFramework. If you just want to know the value of Node 42, use `dependOn @(DependecyM _ domain) (Node 42)`.

-> a

Computes the (pure) solution of the DependencyM action act specified in the last parameter. act may reference (via dependOn) Nodes of the DataFlowFramework dff's fixed-point, specified as the first parameter.

dff's fixed-point is determined by its transfer functions, and solveProblem will make sure that all (relevant) Nodes will have reached their fixed-point according to their transfer function before computing the solution for act.

We try to be smart in saving unnecessary iterations of transfer functions by employing a worklist algorithm. For function domains, where each Node denotes a monotone function, each point's dependencies' will be tracked individually.

Apart from dff and act, the Density of the data-flow graph and the IterationBound can be specified. Pass Sparse and NeverAbort when in doubt.

If your problem only has finitely many different Nodes , consider using the FrameworkBuilder API (e.g. datafix + evalDenotation) for a higher-level API that let's you forget about Nodes and instead let's you focus on building more complex data-flow frameworks.

See Datafix.Tutorial and the examples/ subfolder for examples.

evalDenotation

Arguments

:: Datafixable domain

=> Forall (Currying (ParamTypes func))

=> Denotation domain func

A build plan for computing the denotation, possibly involving fixed-point iteration factored through calls to datafix.

-> IterationBound domain

Whether the solution algorithm should respect a maximum bound on the number of iterations per point. Pass NeverAbort if you don't care.

-> func

evalDenotation denot ib returns a value in domain that is described by the denotation denot.

It does so by building up the DataFlowFramework corresponding to denot and solving the resulting problem with solveProblem, the documentation of which describes in detail how to arrive at a stable denotation and what the IterationBound ib, domain ~ Domain (DepM m) is for.