Copyright  (c) Sebastian Graf 20172020 

License  ISC 
Maintainer  sgraf1337@gmail.com 
Portability  portable 
Safe Haskell  None 
Language  Haskell2010 
This module provides the solveProblem
function, which solves the description of a
DataFlowFramework
by employing a worklist algorithm.
There's also an interpreter for Denotation
al problems in the form of
evalDenotation
.
Synopsis
 data DependencyM graph domain a
 data Density graph where
 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 worklistbased 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 #  
Defined in Datafix.Worklist.Internal (>>=) :: 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 #  
Defined in Datafix.Worklist.Internal 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 #  
Defined in Datafix.Worklist.Internal 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 
Defined in Datafix.Worklist.Internal type Domain (DependencyM graph domain) :: Type Source #  
(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source #  This allows us to solve 
Defined in Datafix.Worklist.Internal dependOn :: Node > LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source #  
type Domain (DependencyM graph domain) Source #  
Defined in Datafix.Worklist.Internal 
data Density graph where Source #
Specifies the density of the problem, e.g. whether the domain of
Node
s 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.
data IterationBound domain Source #
Expresses that iteration should or shouldn't stop after a point has been iterated a finite number of times.
NeverAbort  Will keep on iterating until a precise, yet conservative approximation
has been reached. Make sure that your 
AbortAfter Int (AbortionFunction domain)  For when your The When your 
:: GraphRef graph  
=> Datafixable domain  
=> DataFlowFramework (DependencyM graph domain)  The description of the 
> Density graph  Describes if the algorithm is free to use a 
> IterationBound domain  Whether the solution algorithm should respect a maximum bound on the
number of iterations per point. Pass 
> DependencyM graph domain a  The action for which we want to compute the solution. May reference

> a 
Computes the (pure) solution of the DependencyM
action act
specified in
the last parameter. act
may reference (via dependOn
) Node
s of the
DataFlowFramework
dff
's fixedpoint, specified as the first parameter.
dff
's fixedpoint is determined by its transfer functions, and
solveProblem
will make sure that all (relevant) Node
s will have reached
their fixedpoint 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 dataflow graph and the
IterationBound
can be specified. Pass Sparse
and NeverAbort
when in
doubt.
If your problem only has finitely many different Node
s , consider using the
FrameworkBuilder
API (e.g. datafix
+ evalDenotation
) for a higherlevel
API that let's you forget about Node
s and instead let's you focus on
building more complex dataflow frameworks.
See Datafix.Tutorial and the examples/
subfolder for examples.
:: Datafixable domain  
=> Forall (Currying (ParamTypes func))  
=> Denotation domain func  A build plan for computing the denotation, possibly involving
fixedpoint iteration factored through calls to 
> IterationBound domain  Whether the solution algorithm should respect a maximum bound on the
number of iterations per point. Pass 
> 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.