Copyright	(c) Sebastian Graf 2018
License	ISC
Maintainer	sgraf1337@gmail.com
Portability	portable
Safe Haskell	None
Language	Haskell2010

Datafix.Worklist

Description

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

Synopsis

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 DataFlowProblem as mutable state while solveProblem makes sure we will eventually halt with a conservative approximation.

Instances

Monad (DependencyM graph domain) Source #
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 #
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 #
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.
Associated Types type Domain (DependencyM graph domain :: * -> ) :: Source #
(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source #	This allows us to solve `MonadDependency m => DataFlowProblem m` descriptions with `solveProblem`.
Methods dependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source #
type Domain (DependencyM graph domain) Source #
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
=> DataFlowProblem (DependencyM graph domain)	The description of the `DataFlowProblem` to solve.
-> 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.
-> Node	The `Node` that is initially assumed to be unstable. This should be the `Node` you are interested in, e.g. `Node 42` if you are interested in the value of `fib 42` for a hypothetical `fibProblem`, or the `Node` denoting the root expression of your data-flow analysis you specified via the `DataFlowProblem`.
-> domain

Computes a solution to the described DataFlowProblem by iterating transfer functions until a fixed-point is reached.

It does do by employing a worklist algorithm, iterating unstable Nodes only. Nodes become unstable when the point of another Node their transfer function dependOned changed.

The sole initially unstable Node is the last parameter, and if your domain is function-valued (so the returned Arrows expands to a function), then any further parameters specify the exact point in the Nodes transfer function you are interested in.

If your problem only has finitely many different Nodes , consider using the ProblemBuilder 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.

evalDenotation Source #

Arguments

:: Datafixable domain
=> Denotation domain	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.
-> domain

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

It does so by building up the DataFlowProblem 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 is for.