datafix-0.0.0.2: Fixing data-flow problems

Copyright(c) Sebastian Graf 2018
LicenseISC
Maintainersgraf1337@gmail.com
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

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.