Copyright | (c) Sebastian Graf 2018 |
---|---|

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
`DataFlowProblem`

by employing a worklist algorithm.
There's also an interpreter for `Denotation`

al problems in the form of
`evalDenotation`

.

- data DependencyM graph domain a
- data Density graph where
- data IterationBound domain
- = NeverAbort
- | AbortAfter Int (AbortionFunction domain)

- solveProblem :: forall domain graph. GraphRef graph => Datafixable domain => DataFlowProblem (DependencyM graph domain) -> Density graph -> IterationBound domain -> Node -> domain
- evalDenotation :: Datafixable domain => Denotation domain -> IterationBound domain -> domain

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

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

=> 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 fixed-point 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 function-valued (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 higher-level API
that let's you forget about `Node`

s and instead let's you focus on building
more complex data-flow frameworks.

:: Datafixable domain | |

=> Denotation domain | A build plan for computing the denotation, possibly involving
fixed-point iteration factored through calls to |

-> IterationBound domain | Whether the solution algorithm should respect a maximum bound on the
number of iterations per point. Pass |

-> 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.