Safe Haskell	Safe

Compiler.Hoopl

Contents

Respecting Fuel

Synopsis

Documentation

data O Source

Used at the type level to indicate an open structure with a unique, unnamed control-flow edge flowing in or out. Fallthrough and concatenation are permitted at an open point.

Instances

IfThenElseable O
ShapeLifter C O
ShapeLifter O C
ShapeLifter O O

data C Source

Used at the type level to indicate a closed structure which supports control transfer only through the use of named labels---no fallthrough is permitted. The number of control-flow edges is unconstrained.

Instances

IfThenElseable C
ShapeLifter C O
ShapeLifter O C
NonLocal n => LabelsPtr (n e C)

data Block n e x whereSource

A sequence of nodes. May be any of four shapes (OO, OC, CO, CC). Open at the entry means single entry, mutatis mutandis for exit. A closedclosed block is a basic/ block and can't be extended further. Clients should avoid manipulating blocks and should stick to either nodes or graphs.

Constructors

BFirst :: n C O -> Block n C O
BMiddle :: n O O -> Block n O O
BLast :: n O C -> Block n O C
BCat :: Block n O O -> Block n O O -> Block n O O
BHead :: Block n C O -> n O O -> Block n C O
BTail :: n O O -> Block n O C -> Block n O C
BClosed :: Block n C O -> Block n O C -> Block n C C

Instances

GraphRep Graph
NonLocal n => NonLocal (Block n)

type Body n = LabelMap (Block n C C)Source

A (possibly empty) collection of closed/closed blocks

newtype Body' block n Source

Constructors

Body (LabelMap (block n C C))

type Graph = Graph' Block Source

A control-flow graph, which may take any of four shapes (OO, OC, CO, CC). A graph open at the entry has a single, distinguished, anonymous entry point; if a graph is closed at the entry, its entry point(s) are supplied by a context.

data Graph' block n e x whereSource

Constructors

GNil :: Graph' block n O O
GUnit :: block n O O -> Graph' block n O O
GMany :: MaybeO e (block n O C) -> LabelMap (block n C C) -> MaybeO x (block n C O) -> Graph' block n e x

Instances

GraphRep Graph

data MaybeO ex t whereSource

Maybe type indexed by open/closed

Constructors

JustO :: t -> MaybeO O t
NothingO :: MaybeO C t

Instances

Functor (MaybeO ex)

data MaybeC ex t whereSource

Maybe type indexed by closed/open

Constructors

JustC :: t -> MaybeC C t
NothingC :: MaybeC O t

Instances

Functor (MaybeC ex)

data Shape ex whereSource

Dynamic shape value

Constructors

Closed :: Shape C
Open :: Shape O

type family IndexedCO ex a b :: *Source

Either type indexed by closed/open using type families

class NonLocal thing whereSource

Gives access to the anchor points for nonlocal edges as well as the edges themselves

Methods

entryLabel Source

Arguments

:: thing C x
-> Label	The label of a first node or block

successors Source

Arguments

:: thing e C
-> [Label]	Gives control-flow successors

Instances

NonLocal n => NonLocal (Block n)
NonLocal n => NonLocal (DBlock f n)

emptyBody :: LabelMap (thing C C)Source

addBlock :: NonLocal thing => thing C C -> LabelMap (thing C C) -> LabelMap (thing C C)Source

bodyList :: NonLocal (block n) => Body' block n -> [(Label, block n C C)]Source

mapGraph :: (forall e x. n e x -> n' e x) -> Graph n e x -> Graph n' e xSource

Maps over all nodes in a graph.

mapMaybeO :: (forall e x. n e x -> n' e x) -> MaybeO ex (Block n e x) -> MaybeO ex (Block n' e x)Source

mapMaybeC :: (forall e x. n e x -> n' e x) -> MaybeC ex (Block n e x) -> MaybeC ex (Block n' e x)Source

mapBlock :: (forall e x. n e x -> n' e x) -> Block n e x -> Block n' e xSource

data AGraph n e x Source

The type of abstract graphs. Offers extra smart constructors that may consume fresh labels during construction.

Instances

GraphRep AGraph

graphOfAGraph :: AGraph n e x -> forall m. UniqueMonad m => m (Graph n e x)Source

Take an abstract AGraph and make a concrete (if monadic) Graph.

aGraphOfGraph :: Graph n e x -> AGraph n e xSource

Take a graph and make it abstract.

(<*>) :: (GraphRep g, NonLocal n) => g n e O -> g n O x -> g n e xSource

Concatenate two graphs; control flows from left to right.

(|*><*|) :: (GraphRep g, NonLocal n) => g n e C -> g n C x -> g n e xSource

Splice together two graphs at a closed point; nothing is known about control flow.

catGraphs :: (GraphRep g, NonLocal n) => [g n O O] -> g n O O Source

Conveniently concatenate a sequence of open/open graphs using <*>.

addEntrySeq :: NonLocal n => AGraph n O C -> AGraph n C x -> AGraph n O xSource

Deprecated: use |*><*| instead

addExitSeq :: NonLocal n => AGraph n e C -> AGraph n C O -> AGraph n e O Source

Deprecated: use |*><*| instead

addBlocks :: HooplNode n => AGraph n e x -> AGraph n C C -> AGraph n e xSource

Extend an existing AGraph with extra basic blocks out of line. No control flow is implied. Simon PJ should give example use case.

unionBlocks :: NonLocal n => AGraph n C C -> AGraph n C C -> AGraph n C C Source

Deprecated: use |*><*| instead

emptyGraph :: GraphRep g => g n O O Source

An empty graph that is open at entry and exit. It is the left and right identity of <*>.

emptyClosedGraph :: GraphRep g => g n C C Source

An empty graph that is closed at entry and exit. It is the left and right identity of |*><*|.

withFresh :: Uniques u => (u -> AGraph n e x) -> AGraph n e xSource

mkFirst :: GraphRep g => n C O -> g n C O Source

Create a graph from a first node

mkMiddle :: GraphRep g => n O O -> g n O O Source

Create a graph from a middle node

mkMiddles :: (GraphRep g, NonLocal n) => [n O O] -> g n O O Source

Conveniently concatenate a sequence of middle nodes to form an open/open graph.

mkLast :: GraphRep g => n O C -> g n O C Source

Create a graph from a last node

mkBranch :: (GraphRep g, HooplNode n) => Label -> g n O C Source

Create a graph that branches to a label

mkLabel :: (GraphRep g, HooplNode n) => Label -> g n C O Source

Create a graph that defines a label

mkWhileDo Source

Arguments

:: HooplNode n
=> (Label -> Label -> AGraph n O C)	loop condition
-> AGraph n O O	body of the loop
-> AGraph n O O	the final while loop

class IfThenElseable x whereSource

Methods

mkIfThenElse Source

Arguments

:: HooplNode n
=> (Label -> Label -> AGraph n O C)	branch condition
-> AGraph n O x	code in the then branch
-> AGraph n O x	code in the else branch
-> AGraph n O x	resulting if-then-else construct

Translate a high-level if-then-else construct into an AGraph. The condition takes as arguments labels on the true-false branch and returns a single-entry, two-exit graph which exits to the two labels.

Instances

IfThenElseable C
IfThenElseable O

mkEntry :: GraphRep g => Block n O C -> g n O C Source

Create a graph containing only an entry sequence

mkExit :: GraphRep g => Block n C O -> g n C O Source

Create a graph containing only an exit sequence

class NonLocal n => HooplNode n whereSource

For some graph-construction operations and some optimizations, Hoopl must be able to create control-flow edges using a given node type n.

Methods

mkBranchNode :: Label -> n O C Source

Create a branch node, the source of a control-flow edge.

mkLabelNode :: Label -> n C O Source

Create a label node, the target (destination) of a control-flow edge.

firstXfer :: NonLocal n => (n C O -> f -> f) -> n C O -> FactBase f -> fSource

A utility function so that a transfer function for a first node can be given just a fact; we handle the lookup. This function is planned to be made obsolete by changes in the dataflow interface.

distributeXfer :: NonLocal n => DataflowLattice f -> (n O C -> f -> f) -> n O C -> f -> FactBase fSource

This utility function handles a common case in which a transfer function produces a single fact out of a last node, which is then distributed over the outgoing edges.

distributeFact :: NonLocal n => n O C -> f -> FactBase fSource

This utility function handles a common case in which a transfer function for a last node takes the incoming fact unchanged and simply distributes that fact over the outgoing edges.

distributeFactBwd :: NonLocal n => n C O -> f -> FactBase fSource

This utility function handles a common case in which a backward transfer function takes the incoming fact unchanged and tags it with the node's label.

successorFacts :: NonLocal n => n O C -> FactBase f -> [f]Source

List of (unlabelled) facts from the successors of a last node

joinFacts :: DataflowLattice f -> Label -> [f] -> fSource

Join a list of facts.

joinOutFacts :: NonLocal node => DataflowLattice f -> node O C -> FactBase f -> fSource

Deprecated: should be replaced by 'joinFacts lat l (successorFacts n f)'; as is, it uses the wrong Label

joinMaps :: Ord k => JoinFun v -> JoinFun (Map k v)Source

It's common to represent dataflow facts as a map from variables to some fact about the locations. For these maps, the join operation on the map can be expressed in terms of the join on each element of the codomain:

foldGraphNodes :: forall n a. (forall e x. n e x -> a -> a) -> forall e x. Graph n e x -> a -> aSource

Fold a function over every node in a graph. The fold function must be polymorphic in the shape of the nodes.

foldBlockNodesF :: forall n a. (forall e x. n e x -> a -> a) -> forall e x. Block n e x -> IndexedCO e a a -> IndexedCO x a aSource

foldBlockNodesB :: forall n a. (forall e x. n e x -> a -> a) -> forall e x. Block n e x -> IndexedCO x a a -> IndexedCO e a aSource

foldBlockNodesF3 :: forall n a b c. (n C O -> a -> b, n O O -> b -> b, n O C -> b -> c) -> forall e x. Block n e x -> IndexedCO e a b -> IndexedCO x c bSource

Fold a function over every node in a block, forward or backward. The fold function must be polymorphic in the shape of the nodes.

foldBlockNodesB3 :: forall n a b c. (n C O -> b -> c, n O O -> b -> b, n O C -> a -> b) -> forall e x. Block n e x -> IndexedCO x a b -> IndexedCO e c bSource

tfFoldBlock :: forall n bc bo c e x. (n C O -> bc, n O O -> IndexedCO e bc bo -> IndexedCO e bc bo, n O C -> IndexedCO e bc bo -> c) -> Block n e x -> bo -> IndexedCO x c (IndexedCO e bc bo)Source

A fold function that relies on the IndexedCO type function. Note that the type parameter e is available to the functions that are applied to the middle and last nodes.

data ScottBlock n a Source

Constructors

ScottBlock (n C O -> a C O) (n O O -> a O O) (n O C -> a O C) (forall e x. a e O -> a O x -> a e x)

scottFoldBlock :: forall n a e x. ScottBlock n a -> Block n e x -> a e xSource

fbnf3 :: forall n a b c. (n C O -> a -> b, n O O -> b -> b, n O C -> b -> c) -> forall e x. Block n e x -> IndexedCO e a b -> IndexedCO x c bSource

blockToNodeList :: Block n e x -> (MaybeC e (n C O), [n O O], MaybeC x (n O C))Source

Deprecated: What justifies these functions? Can they be eliminated? Replaced with folds?

Convert a block to a list of nodes. The entry and exit node is or is not present depending on the shape of the block.

The blockToNodeList function cannot be currently expressed using foldBlockNodesB, because it returns IndexedCO e a b, which means two different types depending on the shape of the block entry. But blockToNodeList returns one of four possible types, depending on the shape of the block entry *and* exit.

blockOfNodeList :: (MaybeC e (n C O), [n O O], MaybeC x (n O C)) -> Block n e xSource

Deprecated: What justifies these functions? Can they be eliminated? Replaced with folds?

Convert a list of nodes to a block. The entry and exit node must or must not be present depending on the shape of the block.

blockToNodeList' :: Block n e x -> (MaybeC e (n C O), [n O O], MaybeC x (n O C))Source

blockToNodeList'' :: Block n e x -> (MaybeC e (n C O), [n O O], MaybeC x (n O C))Source

blockToNodeList''' :: forall n e x. (IndexedCO e (NodeList' C O n) (NodeList' O O n) ~ NodeList' e O n, IndexedCO x (NodeList' e C n) (NodeList' e O n) ~ NodeList' e x n) => Block n e x -> NodeList' e x nSource

analyzeAndRewriteFwdBody :: forall m n f entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries) => FwdPass m n f -> entries -> Body n -> FactBase f -> m (Body n, FactBase f)Source

Forward dataflow analysis and rewriting for the special case of a Body. A set of entry points must be supplied; blocks not reachable from the set are thrown away.

analyzeAndRewriteBwdBody :: forall m n f entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries) => BwdPass m n f -> entries -> Body n -> FactBase f -> m (Body n, FactBase f)Source

Backward dataflow analysis and rewriting for the special case of a Body. A set of entry points must be supplied; blocks not reachable from the set are thrown away.

analyzeAndRewriteFwdOx :: forall m n f x. (CheckpointMonad m, NonLocal n) => FwdPass m n f -> Graph n O x -> f -> m (Graph n O x, FactBase f, MaybeO x f)Source

Forward dataflow analysis and rewriting for the special case of a graph open at the entry. This special case relieves the client from having to specify a type signature for NothingO, which beginners might find confusing and experts might find annoying.

analyzeAndRewriteBwdOx :: forall m n f x. (CheckpointMonad m, NonLocal n) => BwdPass m n f -> Graph n O x -> Fact x f -> m (Graph n O x, FactBase f, f)Source

Backward dataflow analysis and rewriting for the special case of a graph open at the entry. This special case relieves the client from having to specify a type signature for NothingO, which beginners might find confusing and experts might find annoying.

noEntries :: MaybeC O Label Source

A value that can be used for the entry point of a graph open at the entry.

data BlockResult n x whereSource

Constructors

NoBlock :: BlockResult n x
BodyBlock :: Block n C C -> BlockResult n x
ExitBlock :: Block n C O -> BlockResult n O

lookupBlock :: NonLocal n => Graph n e x -> Label -> BlockResult n xSource

class IsSet set whereSource

Associated Types

type ElemOf set Source

Methods

setNull :: set -> Bool Source

setSize :: set -> Int Source

setMember :: ElemOf set -> set -> Bool Source

setEmpty :: setSource

setSingleton :: ElemOf set -> setSource

setInsert :: ElemOf set -> set -> setSource

setDelete :: ElemOf set -> set -> setSource

setUnion :: set -> set -> setSource

setDifference :: set -> set -> setSource

setIntersection :: set -> set -> setSource

setIsSubsetOf :: set -> set -> Bool Source

setFold :: (ElemOf set -> b -> b) -> b -> set -> bSource

setElems :: set -> [ElemOf set]Source

setFromList :: [ElemOf set] -> setSource

Instances

IsSet UniqueSet
IsSet LabelSet

setInsertList :: IsSet set => [ElemOf set] -> set -> setSource

setDeleteList :: IsSet set => [ElemOf set] -> set -> setSource

setUnions :: IsSet set => [set] -> setSource

class IsMap map whereSource

Associated Types

type KeyOf map Source

Methods

mapNull :: map a -> Bool Source

mapSize :: map a -> Int Source

mapMember :: KeyOf map -> map a -> Bool Source

mapLookup :: KeyOf map -> map a -> Maybe aSource

mapFindWithDefault :: a -> KeyOf map -> map a -> aSource

mapEmpty :: map aSource

mapSingleton :: KeyOf map -> a -> map aSource

mapInsert :: KeyOf map -> a -> map a -> map aSource

mapDelete :: KeyOf map -> map a -> map aSource

mapUnion :: map a -> map a -> map aSource

mapUnionWithKey :: (KeyOf map -> a -> a -> a) -> map a -> map a -> map aSource

mapDifference :: map a -> map a -> map aSource

mapIntersection :: map a -> map a -> map aSource

mapIsSubmapOf :: Eq a => map a -> map a -> Bool Source

mapMap :: (a -> b) -> map a -> map bSource

mapMapWithKey :: (KeyOf map -> a -> b) -> map a -> map bSource

mapFold :: (a -> b -> b) -> b -> map a -> bSource

mapFoldWithKey :: (KeyOf map -> a -> b -> b) -> b -> map a -> bSource

mapElems :: map a -> [a]Source

mapKeys :: map a -> [KeyOf map]Source

mapToList :: map a -> [(KeyOf map, a)]Source

mapFromList :: [(KeyOf map, a)] -> map aSource

Instances

IsMap UniqueMap
IsMap LabelMap

mapInsertList :: IsMap map => [(KeyOf map, a)] -> map a -> map aSource

mapDeleteList :: IsMap map => [KeyOf map] -> map a -> map aSource

mapUnions :: IsMap map => [map a] -> map aSource

class Monad m => CheckpointMonad m whereSource

Obeys the following law: for all m do { s <- checkpoint; m; restart s } == return ()

Associated Types

type Checkpoint m Source

Methods

checkpoint :: m (Checkpoint m)Source

restart :: Checkpoint m -> m ()Source

Instances

CheckpointMonad SimpleUniqueMonad
CheckpointMonad m => CheckpointMonad (InfiniteFuelMonad m)
CheckpointMonad m => CheckpointMonad (CheckingFuelMonad m)

data DataflowLattice a Source

A transfer function might want to use the logging flag to control debugging, as in for example, it updates just one element in a big finite map. We don't want Hoopl to show the whole fact, and only the transfer function knows exactly what changed.

Constructors

DataflowLattice
Fields fact_name :: String fact_bot :: a fact_join :: JoinFun a

type JoinFun a = Label -> OldFact a -> NewFact a -> (ChangeFlag, a)Source

newtype OldFact a Source

Constructors

OldFact a

newtype NewFact a Source

Constructors

NewFact a

type family Fact x f :: *Source

mkFactBase :: forall f. DataflowLattice f -> [(Label, f)] -> FactBase fSource

mkFactBase creates a FactBase from a list of (Label, fact) pairs. If the same label appears more than once, the relevant facts are joined.

data ChangeFlag Source

Constructors

NoChange
SomeChange

Instances

Eq ChangeFlag
Ord ChangeFlag

changeIf :: Bool -> ChangeFlag Source

data FwdPass m n f Source

Constructors

FwdPass
Fields fp_lattice :: DataflowLattice f fp_transfer :: FwdTransfer n f fp_rewrite :: FwdRewrite m n f

data FwdTransfer n f Source

mkFTransfer :: (forall e x. n e x -> f -> Fact x f) -> FwdTransfer n fSource

mkFTransfer3 :: (n C O -> f -> f) -> (n O O -> f -> f) -> (n O C -> f -> FactBase f) -> FwdTransfer n fSource

getFTransfer3 :: FwdTransfer n f -> (n C O -> f -> f, n O O -> f -> f, n O C -> f -> FactBase f)Source

Respecting Fuel

A value of type FwdRewrite or BwdRewrite respects fuel if any function contained within the value satisfies the following properties:

When fuel is exhausted, it always returns Nothing.
When it returns Just g rw, it consumes exactly one unit of fuel, and new rewrite rw also respects fuel.

Provided that functions passed to mkFRewrite, mkFRewrite3, mkBRewrite, and mkBRewrite3 are not aware of the fuel supply, the results respect fuel.

It is an unchecked run-time error for the argument passed to wrapFR, wrapFR2, wrapBR, or warpBR2 to return a function that does not respect fuel.

data FwdRewrite m n f Source

mkFRewrite :: FuelMonad m => (forall e x. n e x -> f -> m (Maybe (Graph n e x))) -> FwdRewrite m n fSource

Functions passed to mkFRewrite should not be aware of the fuel supply. The result returned by mkFRewrite respects fuel.

mkFRewrite3 :: forall m n f. FuelMonad m => (n C O -> f -> m (Maybe (Graph n C O))) -> (n O O -> f -> m (Maybe (Graph n O O))) -> (n O C -> f -> m (Maybe (Graph n O C))) -> FwdRewrite m n fSource

Functions passed to mkFRewrite3 should not be aware of the fuel supply. The result returned by mkFRewrite3 respects fuel.

getFRewrite3 :: FwdRewrite m n f -> (n C O -> f -> m (Maybe (Graph n C O, FwdRewrite m n f)), n O O -> f -> m (Maybe (Graph n O O, FwdRewrite m n f)), n O C -> f -> m (Maybe (Graph n O C, FwdRewrite m n f)))Source

noFwdRewrite :: Monad m => FwdRewrite m n fSource

wrapFR Source

Arguments

:: (forall e x. (n e x -> f -> m (Maybe (Graph n e x, FwdRewrite m n f))) -> n' e x -> f' -> m' (Maybe (Graph n' e x, FwdRewrite m' n' f')))	This argument may assume that any function passed to it respects fuel, and it must return a result that respects fuel.
-> FwdRewrite m n f
-> FwdRewrite m' n' f'

wrapFR2 Source

Arguments

:: (forall e x. (n1 e x -> f1 -> m1 (Maybe (Graph n1 e x, FwdRewrite m1 n1 f1))) -> (n2 e x -> f2 -> m2 (Maybe (Graph n2 e x, FwdRewrite m2 n2 f2))) -> n3 e x -> f3 -> m3 (Maybe (Graph n3 e x, FwdRewrite m3 n3 f3)))	This argument may assume that any function passed to it respects fuel, and it must return a result that respects fuel.
-> FwdRewrite m1 n1 f1
-> FwdRewrite m2 n2 f2
-> FwdRewrite m3 n3 f3

data BwdPass m n f Source

Constructors

BwdPass
Fields bp_lattice :: DataflowLattice f bp_transfer :: BwdTransfer n f bp_rewrite :: BwdRewrite m n f

data BwdTransfer n f Source

mkBTransfer :: (forall e x. n e x -> Fact x f -> f) -> BwdTransfer n fSource

mkBTransfer3 :: (n C O -> f -> f) -> (n O O -> f -> f) -> (n O C -> FactBase f -> f) -> BwdTransfer n fSource

getBTransfer3 :: BwdTransfer n f -> (n C O -> f -> f, n O O -> f -> f, n O C -> FactBase f -> f)Source

wrapBR Source

Arguments

:: (forall e x. Shape x -> (n e x -> Fact x f -> m (Maybe (Graph n e x, BwdRewrite m n f))) -> n' e x -> Fact x f' -> m' (Maybe (Graph n' e x, BwdRewrite m' n' f')))	This argument may assume that any function passed to it respects fuel, and it must return a result that respects fuel.
-> BwdRewrite m n f
-> BwdRewrite m' n' f'

wrapBR2 Source

Arguments

:: (forall e x. Shape x -> (n1 e x -> Fact x f1 -> m1 (Maybe (Graph n1 e x, BwdRewrite m1 n1 f1))) -> (n2 e x -> Fact x f2 -> m2 (Maybe (Graph n2 e x, BwdRewrite m2 n2 f2))) -> n3 e x -> Fact x f3 -> m3 (Maybe (Graph n3 e x, BwdRewrite m3 n3 f3)))	This argument may assume that any function passed to it respects fuel, and it must return a result that respects fuel.
-> BwdRewrite m1 n1 f1
-> BwdRewrite m2 n2 f2
-> BwdRewrite m3 n3 f3

data BwdRewrite m n f Source

mkBRewrite :: FuelMonad m => (forall e x. n e x -> Fact x f -> m (Maybe (Graph n e x))) -> BwdRewrite m n fSource

Functions passed to mkBRewrite should not be aware of the fuel supply. The result returned by mkBRewrite respects fuel.

mkBRewrite3 :: forall m n f. FuelMonad m => (n C O -> f -> m (Maybe (Graph n C O))) -> (n O O -> f -> m (Maybe (Graph n O O))) -> (n O C -> FactBase f -> m (Maybe (Graph n O C))) -> BwdRewrite m n fSource

Functions passed to mkBRewrite3 should not be aware of the fuel supply. The result returned by mkBRewrite3 respects fuel.

getBRewrite3 :: BwdRewrite m n f -> (n C O -> f -> m (Maybe (Graph n C O, BwdRewrite m n f)), n O O -> f -> m (Maybe (Graph n O O, BwdRewrite m n f)), n O C -> FactBase f -> m (Maybe (Graph n O C, BwdRewrite m n f)))Source

noBwdRewrite :: Monad m => BwdRewrite m n fSource

analyzeAndRewriteFwd :: forall m n f e x entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries) => FwdPass m n f -> MaybeC e entries -> Graph n e x -> Fact e f -> m (Graph n e x, FactBase f, MaybeO x f)Source

if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...

analyzeAndRewriteBwd :: (CheckpointMonad m, NonLocal n, LabelsPtr entries) => BwdPass m n f -> MaybeC e entries -> Graph n e x -> Fact x f -> m (Graph n e x, FactBase f, MaybeO e f)Source

if the graph being analyzed is open at the exit, I don't quite understand the implications of possible other exits

data Label Source

Instances

Eq Label
Ord Label
Show Label
LabelsPtr Label
Uniques Label

freshLabel :: UniqueMonad m => m Label Source

data LabelSet Source

Instances

Eq LabelSet
Ord LabelSet
Show LabelSet
IsSet LabelSet
LabelsPtr LabelSet

data LabelMap v Source

Instances

IsMap LabelMap
Eq v => Eq (LabelMap v)
Ord v => Ord (LabelMap v)
Show v => Show (LabelMap v)

type FactBase f = LabelMap fSource

noFacts :: FactBase fSource

lookupFact :: Label -> FactBase f -> Maybe fSource

uniqueToLbl :: Unique -> Label Source

lblToUnique :: Label -> Unique Source

data Pointed t b a whereSource

Adds top, bottom, or both to help form a lattice

The type parameters t and b are used to say whether top and bottom elements have been added. The analogy with Block is nearly exact:

A Block is closed at the entry if and only if it has a first node; a Pointed is closed at the top if and only if it has a top element.
A Block is closed at the exit if and only if it has a last node; a Pointed is closed at the bottom if and only if it has a bottom element.

We thus have four possible types, of which three are interesting:

Pointed C C a: Type a extended with both top and bottom elements.
Pointed C O a: Type a extended with a top element only. (Presumably a comes equipped with a bottom element of its own.)
Pointed O C a: Type a extended with a bottom element only.
Pointed O O a: Isomorphic to a, and therefore not interesting.

The advantage of all this GADT-ishness is that the constructors Bot, Top, and PElem can all be used polymorphically.

A 'Pointed t b' type is an instance of Functor and Show.

Constructors

Bot :: Pointed t C a
PElem :: a -> Pointed t b a
Top :: Pointed C b a

Instances

Functor (Pointed t b)
Eq a => Eq (Pointed t b a)
Ord a => Ord (Pointed t b a)
Show a => Show (Pointed t b a)

addPoints :: String -> JoinFun a -> DataflowLattice (Pointed t C a)Source

Given a join function and a name, creates a semi lattice by adding a bottom element, and possibly a top element also. A specialized version of addPoints'.

addPoints' :: forall a t. String -> (Label -> OldFact a -> NewFact a -> (ChangeFlag, Pointed t C a)) -> DataflowLattice (Pointed t C a)Source

A more general case for creating a new lattice

addTop :: DataflowLattice a -> DataflowLattice (WithTop a)Source

Given a join function and a name, creates a semi lattice by adding a top element but no bottom element. Caller must supply the bottom element.

addTop' :: forall a. String -> a -> (Label -> OldFact a -> NewFact a -> (ChangeFlag, WithTop a)) -> DataflowLattice (WithTop a)Source

A more general case for creating a new lattice

liftJoinTop :: JoinFun a -> JoinFun (WithTop a)Source

extendJoinDomain :: forall a. (Label -> OldFact a -> NewFact a -> (ChangeFlag, WithTop a)) -> JoinFun (WithTop a)Source

type WithTop a = Pointed C O aSource

Type a with a top element adjoined

type WithBot a = Pointed O C aSource

Type a with a bottom element adjoined

type WithTopAndBot a = Pointed C C aSource

Type a with top and bottom elements adjoined

thenFwdRw :: forall m n f. Monad m => FwdRewrite m n f -> FwdRewrite m n f -> FwdRewrite m n fSource

deepFwdRw3 :: FuelMonad m => (n C O -> f -> m (Maybe (Graph n C O))) -> (n O O -> f -> m (Maybe (Graph n O O))) -> (n O C -> f -> m (Maybe (Graph n O C))) -> FwdRewrite m n fSource

deepFwdRw :: FuelMonad m => (forall e x. n e x -> f -> m (Maybe (Graph n e x))) -> FwdRewrite m n fSource

iterFwdRw :: forall m n f. Monad m => FwdRewrite m n f -> FwdRewrite m n fSource

thenBwdRw :: forall m n f. Monad m => BwdRewrite m n f -> BwdRewrite m n f -> BwdRewrite m n fSource

deepBwdRw3 :: FuelMonad m => (n C O -> f -> m (Maybe (Graph n C O))) -> (n O O -> f -> m (Maybe (Graph n O O))) -> (n O C -> FactBase f -> m (Maybe (Graph n O C))) -> BwdRewrite m n fSource

deepBwdRw :: FuelMonad m => (forall e x. n e x -> Fact x f -> m (Maybe (Graph n e x))) -> BwdRewrite m n fSource

iterBwdRw :: forall m n f. Monad m => BwdRewrite m n f -> BwdRewrite m n fSource

pairFwd :: forall m n f f'. Monad m => FwdPass m n f -> FwdPass m n f' -> FwdPass m n (f, f')Source

pairBwd :: forall m n f f'. Monad m => BwdPass m n f -> BwdPass m n f' -> BwdPass m n (f, f')Source

pairLattice :: forall f f'. DataflowLattice f -> DataflowLattice f' -> DataflowLattice (f, f')Source

type Fuel = Int Source

infiniteFuel :: Fuel Source

fuelRemaining :: FuelMonad m => m Fuel Source

Find out how much fuel remains after a computation. Can be subtracted from initial fuel to get total consumption.

withFuel :: FuelMonad m => Maybe a -> m (Maybe a)Source

class Monad m => FuelMonad m whereSource

Methods

getFuel :: m Fuel Source

setFuel :: Fuel -> m ()Source

Instances

Monad m => FuelMonad (InfiniteFuelMonad m)
Monad m => FuelMonad (CheckingFuelMonad m)

class FuelMonadT fm whereSource

Methods

runWithFuel :: (Monad m, FuelMonad (fm m)) => Fuel -> fm m a -> m aSource

liftFuel :: (Monad m, FuelMonad (fm m)) => m a -> fm m aSource

Instances

FuelMonadT InfiniteFuelMonad
FuelMonadT CheckingFuelMonad

data CheckingFuelMonad m a Source

Instances

FuelMonadT CheckingFuelMonad
Monad m => Monad (CheckingFuelMonad m)
CheckpointMonad m => CheckpointMonad (CheckingFuelMonad m)
UniqueMonad m => UniqueMonad (CheckingFuelMonad m)
Monad m => FuelMonad (CheckingFuelMonad m)

data InfiniteFuelMonad m a Source

Instances

FuelMonadT InfiniteFuelMonad
Monad m => Monad (InfiniteFuelMonad m)
CheckpointMonad m => CheckpointMonad (InfiniteFuelMonad m)
UniqueMonad m => UniqueMonad (InfiniteFuelMonad m)
Monad m => FuelMonad (InfiniteFuelMonad m)

type SimpleFuelMonad = CheckingFuelMonad SimpleUniqueMonad Source

data Unique Source

Instances

Eq Unique
Ord Unique
Show Unique
Uniques Unique

intToUnique :: Int -> Unique Source

data UniqueSet Source

Instances

Eq UniqueSet
Ord UniqueSet
Show UniqueSet
IsSet UniqueSet

data UniqueMap v Source

Instances

IsMap UniqueMap
Eq v => Eq (UniqueMap v)
Ord v => Ord (UniqueMap v)
Show v => Show (UniqueMap v)

class Monad m => UniqueMonad m whereSource

Methods

freshUnique :: m Unique Source

Instances

UniqueMonad SimpleUniqueMonad
Monad m => UniqueMonad (UniqueMonadT m)
UniqueMonad m => UniqueMonad (InfiniteFuelMonad m)
UniqueMonad m => UniqueMonad (CheckingFuelMonad m)

data SimpleUniqueMonad a Source

Instances

Monad SimpleUniqueMonad
CheckpointMonad SimpleUniqueMonad
UniqueMonad SimpleUniqueMonad

runSimpleUniqueMonad :: SimpleUniqueMonad a -> aSource

data UniqueMonadT m a Source

Instances

Monad m => Monad (UniqueMonadT m)
Monad m => UniqueMonad (UniqueMonadT m)

runUniqueMonadT :: Monad m => UniqueMonadT m a -> m aSource

uniqueToInt :: Unique -> Int Source

gUnitOO :: block n O O -> Graph' block n O O Source

gUnitOC :: block n O C -> Graph' block n O C Source

gUnitCO :: block n C O -> Graph' block n C O Source

gUnitCC :: NonLocal (block n) => block n C C -> Graph' block n C C Source

catGraphNodeOC :: NonLocal n => Graph n e O -> n O C -> Graph n e C Source

catGraphNodeOO :: Graph n e O -> n O O -> Graph n e O Source

catNodeCOGraph :: NonLocal n => n C O -> Graph n O x -> Graph n C xSource

catNodeOOGraph :: n O O -> Graph n O x -> Graph n O xSource

graphMapBlocks :: forall block n block' n' e x. (forall e x. block n e x -> block' n' e x) -> Graph' block n e x -> Graph' block' n' e xSource

Function graphMapBlocks enables a change of representation of blocks, nodes, or both. It lifts a polymorphic block transform into a polymorphic graph transform. When the block representation stabilizes, a similar function should be provided for blocks.

blockMapNodes :: (forall e x. n e x -> n' e x) -> Block n e x -> Block n' e xSource

blockMapNodes3 :: (n C O -> n' C O, n O O -> n' O O, n O C -> n' O C) -> Block n e x -> Block n' e xSource

Function blockMapNodes enables a change of nodes in a block.

blockGraph :: NonLocal n => Block n e x -> Graph n e xSource

postorder_dfs :: NonLocal (block n) => Graph' block n O x -> [block n C C]Source

Traversal: postorder_dfs returns a list of blocks reachable from the entry of enterable graph. The entry and exit are *not* included. The list has the following property:

Say a back reference exists if one of a block's control-flow successors precedes it in the output list

Then there are as few back references as possible

The output is suitable for use in a forward dataflow problem. For a backward problem, simply reverse the list. (postorder_dfs is sufficiently tricky to implement that one doesn't want to try and maintain both forward and backward versions.)

postorder_dfs_from :: (NonLocal block, LabelsPtr b) => LabelMap (block C C) -> b -> [block C C]Source

postorder_dfs_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) -> e -> LabelSet -> [block C C]Source

preorder_dfs :: NonLocal (block n) => Graph' block n O x -> [block n C C]Source

preorder_dfs_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) -> e -> LabelSet -> [block C C]Source

labelsDefined :: forall block n e x. NonLocal (block n) => Graph' block n e x -> LabelSet Source

labelsUsed :: forall block n e x. NonLocal (block n) => Graph' block n e x -> LabelSet Source

externalEntryLabels :: forall n. NonLocal n => LabelMap (Block n C C) -> LabelSet Source

class LabelsPtr l whereSource

Methods

targetLabels :: l -> [Label]Source

Instances

LabelsPtr LabelSet
LabelsPtr Label
LabelsPtr l => LabelsPtr [l]
NonLocal n => LabelsPtr (n e C)

type TraceFn = forall a. String -> a -> aSource

debugFwdJoins :: forall m n f. Show f => TraceFn -> ChangePred -> FwdPass m n f -> FwdPass m n fSource

Debugging combinators: Each combinator takes a dataflow pass and produces a dataflow pass that can output debugging messages. You provide the function, we call it with the applicable message.

The most common use case is probably to:

import Trace
pass trace as the 1st argument to the debug combinator
pass 'const true' as the 2nd argument to the debug combinator

There are two kinds of debugging messages for a join, depending on whether the join is higher in the lattice than the old fact: 1. If the join is higher, we show: + JoinL: f1 join f2 = f' where: + indicates a change L is the label where the join takes place f1 is the old fact at the label f2 is the new fact we are joining to f1 f' is the result of the join 2. _ JoinL: f2 <= f1 where: _ indicates no change L is the label where the join takes place f1 is the old fact at the label (which remains unchanged) f2 is the new fact we joined with f1

debugBwdJoins :: forall m n f. Show f => TraceFn -> ChangePred -> BwdPass m n f -> BwdPass m n fSource

debugFwdTransfers :: forall m n f. Show f => TraceFn -> ShowN n -> FPred n f -> FwdPass m n f -> FwdPass m n fSource

debugBwdTransfers :: forall m n f. Show f => TraceFn -> ShowN n -> BPred n f -> BwdPass m n f -> BwdPass m n fSource

showGraph :: forall n e x. NonLocal n => Showing n -> Graph n e x -> String Source

showFactBase :: Show f => FactBase f -> String Source