Copyright	(c) Sebastian Graf 2017-2020
License	ISC
Maintainer	[email protected]
Portability	portable
Safe Haskell	None
Language	Haskell2010

Datafix.Worklist

Description

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.

Synopsis

data DependencyM graph domain a
data Density graph where
- Sparse :: Density Ref
- Dense :: Node -> Density Ref
data IterationBound domain
- = NeverAbort
- | AbortAfter Int (AbortionFunction domain)
solveProblem :: forall domain graph a. GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) -> Density graph -> IterationBound domain -> DependencyM graph domain a -> a
evalDenotation :: forall domain func. Datafixable domain => Forall (Currying (ParamTypes func)) => Denotation domain func -> IterationBound domain -> func

Documentation

data DependencyM graph domain a Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #	The `Domain` is extracted from a type parameter.
Instance details Defined in Datafix.Worklist.Internal Associated Types type Domain (DependencyM graph domain) :: Type Source #
(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source #	This allows us to solve `MonadDependency m => DataFlowFramework m` descriptions with `solveProblem`.
Instance details Defined in Datafix.Worklist.Internal Methods dependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source #
type Domain (DependencyM graph domain) Source #
Instance details Defined in Datafix.Worklist.Internal type Domain (DependencyM graph domain) = domain

data Density graph where Source #

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 Source #

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 Source #

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 `Node`s 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 Source #

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.