datafix-0.0.1.0: Fixing data-flow problems

Copyright (c) Sebastian Graf 2017-2020 ISC sgraf1337@gmail.com portable None Haskell2010

Datafix.Worklist

Description

This module provides the solveProblem function, which solves the description of a DataFlowFramework 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 DataFlowFramework as mutable state while solveProblem makes sure we will eventually halt with a conservative approximation.

Instances
 Monad (DependencyM graph domain) Source # Instance detailsDefined in Datafix.Worklist.Internal 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 # Instance detailsDefined in Datafix.Worklist.Internal Methodsfmap :: (a -> b) -> DependencyM graph domain a -> DependencyM graph domain b #(<\$) :: a -> DependencyM graph domain b -> DependencyM graph domain a # Applicative (DependencyM graph domain) Source # Instance detailsDefined in Datafix.Worklist.Internal Methodspure :: 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. Instance detailsDefined in Datafix.Worklist.Internal Associated Typestype Domain (DependencyM graph domain) :: Type Source # (Datafixable domain, GraphRef graph) => MonadDependency (DependencyM graph domain) Source # This allows us to solve MonadDependency m => DataFlowFramework m descriptions with solveProblem. Instance detailsDefined in Datafix.Worklist.Internal MethodsdependOn :: Node -> LiftedFunc (Domain (DependencyM graph domain)) (DependencyM graph domain) Source # type Domain (DependencyM graph domain) Source # Instance detailsDefined in Datafix.Worklist.Internal 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.

Arguments

 :: GraphRef graph => Datafixable domain => DataFlowFramework (DependencyM graph domain) The description of the DataFlowFramework. -> 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. -> DependencyM graph domain a The action for which we want to compute the solution. May reference Nodes from the DataFlowFramework. If you just want to know the value of Node 42, use dependOn @(DependecyM _ domain) (Node 42). -> a

Computes the (pure) solution of the DependencyM action act specified in the last parameter. act may reference (via dependOn) Nodes of the DataFlowFramework dff's fixed-point, specified as the first parameter.

dff's fixed-point is determined by its transfer functions, and solveProblem will make sure that all (relevant) Nodes will have reached their fixed-point 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 data-flow graph and the IterationBound can be specified. Pass Sparse and NeverAbort when in doubt.

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

See Datafix.Tutorial and the examples/ subfolder for examples.

Arguments

 :: Datafixable domain => Forall (Currying (ParamTypes func)) => Denotation domain func 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. -> 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.