Copyright  (c) Sebastian Graf 2018 

License  ISC 
Maintainer  sgraf1337@gmail.com 
Portability  portable 
Safe Haskell  None 
Language  Haskell2010 
Internal module, does not follow the PVP. Breaking changes may happen at any minor version.
 newtype DependencyM graph domain a = DM (ReaderT (Env graph domain) IO a)
 data Env graph domain = Env {
 problem :: !(DataFlowProblem (DependencyM graph domain))
 iterationBound :: !(IterationBound domain)
 callStack :: !(IntArgsMonoSet (Products (ParamTypes domain)))
 graph :: !(graph domain)
 referencedPoints :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
 unstable :: !(IORef (IntArgsMonoSet (Products (ParamTypes domain))))
 initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) > DataFlowProblem (DependencyM graph domain) > IterationBound domain > IO (graph domain) > IO (Env graph domain)
 data Density graph where
 type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain > ReturnType domain)
 abortWithTop :: forall domain. Currying (ParamTypes domain) (ReturnType domain > ReturnType domain) => BoundedMeetSemiLattice (ReturnType domain) => AbortionFunction domain
 data IterationBound domain
 = NeverAbort
  AbortAfter Int (AbortionFunction domain)
 zoomIORef :: State s a > ReaderT (IORef s) IO a
 zoomReferencedPoints :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a
 zoomUnstable :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a
 enqueueUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO ()
 deleteUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO ()
 highestPriorityUnstableNode :: k ~ Products (ParamTypes domain) => MonoMapKey k => ReaderT (Env graph domain) IO (Maybe (Int, k))
 withCall :: Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO a > ReaderT (Env graph domain) IO a
 recompute :: forall domain graph dom cod depm. dom ~ ParamTypes domain => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph => Datafixable domain => Int > Products dom > ReaderT (Env graph domain) IO cod
 dependOn :: forall domain graph depm. depm ~ DependencyM graph domain => Datafixable domain => GraphRef graph => Node > LiftedFunc domain depm
 optimisticApproximation :: GraphRef graph => Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 scheme1 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 scheme2 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain)
 whileJust_ :: Monad m => m (Maybe a) > (a > m b) > m ()
 work :: GraphRef graph => Datafixable domain => ReaderT (Env graph domain) IO ()
 solveProblem :: forall domain graph. GraphRef graph => Datafixable domain => DataFlowProblem (DependencyM graph domain) > Density graph > IterationBound domain > Node > domain
Documentation
newtype DependencyM graph domain a Source #
The concrete MonadDependency
for this worklistbased 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.
DM (ReaderT (Env graph domain) IO a)  Why does this use This ultimately leaks badly into the exported interface in Also, this means more explicit type signatures as we have to make clear to
the typechecker that So, bottom line: We resort to 
Monad (DependencyM graph domain) Source #  
Functor (DependencyM graph domain) Source #  
Applicative (DependencyM graph domain) Source #  
Datafixable domain => MonadDomain (DependencyM graph domain) Source #  The 
(Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source #  This allows us to solve 
type Domain (DependencyM graph domain) Source #  
data Env graph domain Source #
The iteration state of 'DependencyM'/'solveProblem'.
Env  

initialEnv :: IntArgsMonoSet (Products (ParamTypes domain)) > DataFlowProblem (DependencyM graph domain) > IterationBound domain > IO (graph domain) > IO (Env graph domain) Source #
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.
type AbortionFunction domain = Arrows (ParamTypes domain) (ReturnType domain > ReturnType domain) Source #
A function that computes a sufficiently conservative approximation of a point in the abstract domain for when the solution algorithm decides to have iterated the node often enough.
When domain
is a 'BoundedMeetSemilattice'/'BoundedLattice', the
simplest abortion function would be to constantly return top
.
As is the case for LiftedFunc
and ChangeDetector
, this
carries little semantic meaning if viewed in isolation, so here
are a few examples for how the synonym expands:
AbortionFunction Int ~ Int > Int AbortionFunction (String > Int) ~ String > Int > Int AbortionFunction (a > b > c > PowerSet) ~ a > b > c > PowerSet > PowerSet
E.g., the current value of the point is passed in (the tuple (a, b, c, PowerSet)
)
and the function returns an appropriate conservative approximation in that
point.
abortWithTop :: forall domain. Currying (ParamTypes domain) (ReturnType domain > ReturnType domain) => BoundedMeetSemiLattice (ReturnType domain) => AbortionFunction domain Source #
Aborts iteration of a value by const
antly returning the top
element
of the assumed BoundedMeetSemiLattice
of the ReturnType
.
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 
zoomReferencedPoints :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a Source #
zoomUnstable :: State (IntArgsMonoSet (Products (ParamTypes domain))) a > ReaderT (Env graph domain) IO a Source #
enqueueUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO () Source #
deleteUnstable :: k ~ Products (ParamTypes domain) => MonoMapKey k => Int > k > ReaderT (Env graph domain) IO () Source #
highestPriorityUnstableNode :: k ~ Products (ParamTypes domain) => MonoMapKey k => ReaderT (Env graph domain) IO (Maybe (Int, k)) Source #
withCall :: Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO a > ReaderT (Env graph domain) IO a Source #
recompute :: forall domain graph dom cod depm. dom ~ ParamTypes domain => cod ~ ReturnType domain => depm ~ DependencyM graph domain => GraphRef graph => Datafixable domain => Int > Products dom > ReaderT (Env graph domain) IO cod Source #
The first of the two major functions of this module.
recompute node args
iterates the value of the passed node
at the point args
by invoking its transfer function.
It does so in a way that respects the IterationBound
.
This function is not exported, and is only called by work
and dependOn
, for when the iteration strategy decides that
the node
needs to be (and can be) reiterated.
It performs tracking of which Node
s the transfer function
depended on, do that the worklist algorithm can do its magic.
dependOn :: forall domain graph depm. depm ~ DependencyM graph domain => Datafixable domain => GraphRef graph => Node > LiftedFunc domain depm Source #
optimisticApproximation :: GraphRef graph => Datafixable domain => Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Compute an optimistic approximation for a point of a given node that is as precise as possible, given the other points of that node we already computed.
E.g., it is always valid to return bottom
from this, but in many cases
we can be more precise since we possibly have computed points for the node
that are lower bounds to the current point.
scheme1 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Let the worklist algorithm figure things out.
scheme2 :: GraphRef graph => Datafixable domain => Maybe (ReturnType domain) > Int > Products (ParamTypes domain) > ReaderT (Env graph domain) IO (ReturnType domain) Source #
Descend into \(\bot\) nodes when there is no cycle to discover the set of reachable nodes as quick as possible. Do *not* descend into unstable, non(bot) nodes.
whileJust_ :: Monad m => m (Maybe a) > (a > m b) > m () Source #
As long as the supplied Maybe expression returns "Just _", the loop
body will be called and passed the value contained in the Just
. Results
are discarded.
Taken from whileJust_
.
work :: GraphRef graph => Datafixable domain => ReaderT (Env graph domain) IO () Source #
Defined as 'work = whileJust_ highestPriorityUnstableNode (uncurry recompute)'.
Tries to dequeue the highestPriorityUnstableNode
and recompute
s the value of
one of its unstable
points, until the worklist is empty, indicating that a
fixedpoint has been reached.
:: GraphRef graph  
=> Datafixable domain  
=> DataFlowProblem (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 
> Node  The 
> domain 
Computes a solution to the described DataFlowProblem
by iterating
transfer functions until a fixedpoint is reached.
It does do by employing a worklist algorithm, iterating unstable Node
s
only.
Node
s become unstable when the point of another Node
their transfer function
dependOn
ed changed.
The sole initially unstable Node
is the last parameter, and if your
domain
is functionvalued (so the returned Arrows
expands to a function),
then any further parameters specify the exact point in the Node
s transfer
function you are interested in.
If your problem only has finitely many different Node
s , consider using
the ProblemBuilder
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.