Safe Haskell  Safe 

Language  Haskell2010 
type Body n = LabelMap (Block n C C) Source
A (possibly empty) collection of closed/closed blocks
type Body' block n = LabelMap (block n C C) Source
Body
abstracted over block
emptyBody :: Body' block n Source
bodyList :: Body' block n > [(Label, block n C C)] Source
addBlock :: NonLocal thing => thing C C > LabelMap (thing C C) > LabelMap (thing C C) Source
bodyUnion :: forall a. LabelMap a > LabelMap a > LabelMap a Source
type Graph = Graph' Block Source
A controlflow graph, which may take any of four shapes (O/O, OC, CO, C/C). 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 where Source
Graph'
is abstracted over the block type, so that we can build graphs of annotated blocks for example (Compiler.Hoopl.Dataflow needs this).
GNil :: Graph' block n O O  
GUnit :: block n O O > Graph' block n O O  
GMany :: MaybeO e (block n O C) > Body' block n > MaybeO x (block n C O) > Graph' block n e x 
class NonLocal thing where Source
Gives access to the anchor points for nonlocal edges as well as the edges themselves
bodyGraph :: Body n > Graph n C C Source
blockGraph :: NonLocal n => Block n e x > Graph n e x 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 x Source
catNodeOOGraph :: n O O > Graph n O x > Graph n O x Source
splice :: forall block n e a x. NonLocal (block n) => (forall e x. block n e O > block n O x > block n e x) > Graph' block n e a > Graph' block n a x > Graph' block n e x Source
gSplice :: NonLocal n => Graph n e a > Graph n a x > Graph n e x Source
mapGraph :: (forall e x. n e x > n' e x) > Graph n e x > Graph n' e x Source
Maps over all nodes in a graph.
mapGraphBlocks :: 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 x Source
Function mapGraphBlocks
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.
foldGraphNodes :: forall n a. (forall e x. n e x > a > a) > forall e x. Graph n e x > a > a Source
Fold a function over every node in a graph. The fold function must be polymorphic in the shape of the nodes.
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
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 controlflow 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
class LabelsPtr l where Source
targetLabels :: l > [Label] Source
Used at the type level to indicate an "open" structure with a unique, unnamed controlflow edge flowing in or out. Fallthrough and concatenation are permitted at an open point.
Used at the type level to indicate a "closed" structure which supports control transfer only through the use of named labelsno "fallthrough" is permitted. The number of controlflow edges is unconstrained.
Maybe type indexed by open/closed
Maybe type indexed by closed/open
type family IndexedCO ex a b :: * Source
Either type indexed by closed/open using type families
Dynamic shape value
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.
BlockCO :: n C O > Block n O O > Block n C O  
BlockCC :: n C O > Block n O O > n O C > Block n C C  
BlockOC :: Block n O O > n O C > Block n O C  
BNil :: Block n O O  
BMiddle :: n O O > Block n O O  
BCat :: Block n O O > Block n O O > Block n O O  
BSnoc :: Block n O O > n O O > Block n O O  
BCons :: n O O > Block n O O > Block n O O 
isEmptyBlock :: Block n e x > Bool Source
emptyBlock :: Block n O O Source
blockCons :: n O O > Block n O x > Block n O x Source
blockSnoc :: Block n e O > n O O > Block n e O Source
blockJoinHead :: n C O > Block n O x > Block n C x Source
blockJoinTail :: Block n e O > n O C > Block n e C Source
blockJoin :: n C O > Block n O O > n O C > Block n C C Source
blockJoinAny :: (MaybeC e (n C O), Block n O O, MaybeC x (n O C)) > Block n e x Source
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.
blockAppend :: Block n e O > Block n O x > Block n e x Source
firstNode :: Block n C x > n C O Source
lastNode :: Block n x C > n O C Source
endNodes :: Block n C C > (n C O, n O C) Source
blockSplitHead :: Block n C x > (n C O, Block n O x) Source
blockSplitTail :: Block n e C > (Block n e O, n O C) Source
blockSplit :: Block n C C > (n C O, Block n O O, n O C) Source
Split a closed block into its entry node, open middle block, and exit node.
blockSplitAny :: Block n e x > (MaybeC e (n C O), Block n O O, MaybeC x (n O C)) Source
replaceFirstNode :: Block n C x > n C O > Block n C x Source
replaceLastNode :: Block n x C > n O C > Block n x C Source
blockToList :: Block n O O > [n O O] Source
blockFromList :: [n O O] > Block n O O Source
mapBlock :: (forall e x. n e x > n' e x) > Block n e x > Block n' e x Source
map a function over the nodes of a Block
mapBlock' :: (forall e x. n e x > n' e x) > Block n e x > Block n' e x Source
A strict mapBlock
mapBlock3' :: forall n n' e x. (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 x Source
map over a block, with different functions to apply to first nodes, middle nodes and last nodes respectively. The map is strict.
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 a Source
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 b Source
Fold a function over every node in a block, forward or backward. The fold function must be polymorphic in the shape of the nodes.
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 a Source
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 b Source
frontBiasBlock :: Block n e x > Block n e x Source
A block is "front biased" if the left child of every concatenation operation is a node, not a general block; a frontbiased block is analogous to an ordinary list. If a block is frontbiased, then its nodes can be traversed from front to back without general recusion; tail recursion suffices. Not all shapes can be frontbiased; a closed/open block is inherently backbiased.
backBiasBlock :: Block n e x > Block n e x Source
A block is "back biased" if the right child of every concatenation operation is a node, not a general block; a backbiased block is analogous to a snoclist. If a block is backbiased, then its nodes can be traversed from back to back without general recusion; tail recursion suffices. Not all shapes can be backbiased; an open/closed block is inherently frontbiased.
The type of abstract graphs. Offers extra "smart constructors" that may consume fresh labels during construction.
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 x Source
Take a graph and make it abstract.
(<*>) :: (GraphRep g, NonLocal n) => g n e O > g n O x > g n e x infixl 3 Source
Concatenate two graphs; control flows from left to right.
(*><*) :: (GraphRep g, NonLocal n) => g n e C > g n C x > g n e x infixl 2 Source
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 x Source
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 x Source
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 x Source
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
:: 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 where Source
mkIfThenElse :: HooplNode n => (Label > Label > AGraph n O C) > AGraph n O x > AGraph n O x > AGraph n O x Source
Translate a highlevel ifthenelse construct into an AGraph
. The condition takes as arguments labels on the truefalse branch and returns a singleentry, twoexit graph which exits to the two labels.
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 where Source
For some graphconstruction operations and some optimizations, Hoopl must be able to create controlflow edges using a given node type n
.
mkBranchNode :: Label > n O C Source
Create a branch node, the source of a controlflow edge.
mkLabelNode :: Label > n C O Source
Create a label node, the target (destination) of a controlflow edge.
firstXfer :: NonLocal n => (n C O > f > f) > n C O > FactBase f > f Source
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 f Source
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 f Source
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 f Source
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] > f Source
Join a list of facts.
joinOutFacts :: NonLocal node => DataflowLattice f > node O C > FactBase f > f Source
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:
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.
setNull, setSize, setMember, setEmpty, setSingleton, setInsert, setDelete, setUnion, setDifference, setIntersection, setIsSubsetOf, setFold, setElems, setFromList
setMember :: ElemOf set > set > Bool Source
setSingleton :: ElemOf set > set Source
setInsert :: ElemOf set > set > set Source
setDelete :: ElemOf set > set > set Source
setUnion :: set > set > set Source
setDifference :: set > set > set Source
setIntersection :: set > set > set Source
setIsSubsetOf :: set > set > Bool Source
setFold :: (ElemOf set > b > b) > b > set > b Source
setElems :: set > [ElemOf set] Source
setFromList :: [ElemOf set] > set Source
setInsertList :: IsSet set => [ElemOf set] > set > set Source
setDeleteList :: IsSet set => [ElemOf set] > set > set Source
setUnions :: IsSet set => [set] > set Source
mapNull, mapSize, mapMember, mapLookup, mapFindWithDefault, mapEmpty, mapSingleton, mapInsert, mapInsertWith, mapDelete, mapUnion, mapUnionWithKey, mapDifference, mapIntersection, mapIsSubmapOf, mapMap, mapMapWithKey, mapFold, mapFoldWithKey, mapFilter, mapElems, mapKeys, mapToList, mapFromList, mapFromListWith
mapNull :: map a > Bool Source
mapSize :: map a > Int Source
mapMember :: KeyOf map > map a > Bool Source
mapLookup :: KeyOf map > map a > Maybe a Source
mapFindWithDefault :: a > KeyOf map > map a > a Source
mapSingleton :: KeyOf map > a > map a Source
mapInsert :: KeyOf map > a > map a > map a Source
mapInsertWith :: (a > a > a) > KeyOf map > a > map a > map a Source
mapDelete :: KeyOf map > map a > map a Source
mapUnion :: map a > map a > map a Source
mapUnionWithKey :: (KeyOf map > a > a > a) > map a > map a > map a Source
mapDifference :: map a > map a > map a Source
mapIntersection :: map a > map a > map a Source
mapIsSubmapOf :: Eq a => map a > map a > Bool Source
mapMap :: (a > b) > map a > map b Source
mapMapWithKey :: (KeyOf map > a > b) > map a > map b Source
mapFold :: (a > b > b) > b > map a > b Source
mapFoldWithKey :: (KeyOf map > a > b > b) > b > map a > b Source
mapFilter :: (a > Bool) > map a > map a Source
mapElems :: map a > [a] Source
mapKeys :: map a > [KeyOf map] Source
mapToList :: map a > [(KeyOf map, a)] Source
mapFromList :: [(KeyOf map, a)] > map a Source
mapFromListWith :: (a > a > a) > [(KeyOf map, a)] > map a Source
mapInsertList :: IsMap map => [(KeyOf map, a)] > map a > map a Source
mapDeleteList :: IsMap map => [KeyOf map] > map a > map a Source
mapUnions :: IsMap map => [map a] > map a Source
class Monad m => CheckpointMonad m where Source
Obeys the following law: for all m
do { s < checkpoint; m; restart s } == return ()
type Checkpoint m Source
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.
type JoinFun a = Label > OldFact a > NewFact a > (ChangeFlag, a) Source
OldFact a 
NewFact a 
type family Fact x f :: * Source
mkFactBase :: forall f. DataflowLattice f > [(Label, f)] > FactBase f Source
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
NoChange  
SomeChange 
changeIf :: Bool > ChangeFlag Source
FwdPass  
Fields

newtype FwdTransfer n f Source
FwdTransfer3  
mkFTransfer :: (forall e x. n e x > f > Fact x f) > FwdTransfer n f Source
mkFTransfer3 :: (n C O > f > f) > (n O O > f > f) > (n O C > f > FactBase f) > FwdTransfer n f Source
newtype FwdRewrite m n f Source
FwdRewrite3  
Fields

mkFRewrite :: FuelMonad m => (forall e x. n e x > f > m (Maybe (Graph n e x))) > FwdRewrite m n f Source
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 f Source
Functions passed to mkFRewrite3
should not be aware of the fuel supply. The result returned by mkFRewrite3
respects fuel.
noFwdRewrite :: Monad m => FwdRewrite m n f Source
:: (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' 
:: (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 
BwdPass  
Fields

newtype BwdTransfer n f Source
BwdTransfer3  
mkBTransfer :: (forall e x. n e x > Fact x f > f) > BwdTransfer n f Source
mkBTransfer3 :: (n C O > f > f) > (n O O > f > f) > (n O C > FactBase f > f) > BwdTransfer n f Source
:: (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' 
:: (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 
newtype BwdRewrite m n f Source
BwdRewrite3  
Fields

mkBRewrite :: FuelMonad m => (forall e x. n e x > Fact x f > m (Maybe (Graph n e x))) > BwdRewrite m n f Source
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 f Source
Functions passed to mkBRewrite3
should not be aware of the fuel supply. The result returned by mkBRewrite3
respects fuel.
noBwdRewrite :: Monad m => BwdRewrite m n f Source
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
A value of type FwdRewrite
or BwdRewrite
respects fuel if any function contained within the value satisfies the following properties:
Nothing
.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 runtime error for the argument passed to wrapFR
, wrapFR2
, wrapBR
, or warpBR2
to return a function that does not respect fuel.
freshLabel :: UniqueMonad m => m Label Source
type FactBase f = LabelMap f Source
lookupFact :: Label > FactBase f > Maybe f Source
uniqueToLbl :: Unique > Label Source
lblToUnique :: Label > Unique Source
data Pointed t b a where Source
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:
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.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
a
extended with both top and bottom elements.Pointed C O a
a
extended with a top element only. (Presumably a
comes equipped with a bottom element of its own.)Pointed O C a
a
extended with a bottom element only. Pointed O O a
a
, and therefore not interesting.The advantage of all this GADTishness 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
.
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 a Source
Type a
with a top element adjoined
type WithBot a = Pointed O C a Source
Type a
with a bottom element adjoined
type WithTopAndBot a = Pointed C C a Source
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 f Source
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 f Source
deepFwdRw :: FuelMonad m => (forall e x. n e x > f > m (Maybe (Graph n e x))) > FwdRewrite m n f Source
iterFwdRw :: forall m n f. Monad m => FwdRewrite m n f > FwdRewrite m n f Source
thenBwdRw :: forall m n f. Monad m => BwdRewrite m n f > BwdRewrite m n f > BwdRewrite m n f Source
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 f Source
deepBwdRw :: FuelMonad m => (forall e x. n e x > Fact x f > m (Maybe (Graph n e x))) > BwdRewrite m n f Source
iterBwdRw :: forall m n f. Monad m => BwdRewrite m n f > BwdRewrite m n f Source
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
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 where Source
Monad m => FuelMonad (InfiniteFuelMonad m)  
Monad m => FuelMonad (CheckingFuelMonad m)  
class FuelMonadT fm where Source
runWithFuel :: (Monad m, FuelMonad (fm m)) => Fuel > fm m a > m a Source
liftFuel :: (Monad m, FuelMonad (fm m)) => m a > fm m a Source
data CheckingFuelMonad m a Source
FuelMonadT CheckingFuelMonad  
Monad m => Monad (CheckingFuelMonad m)  
Monad m => Functor (CheckingFuelMonad m)  
Monad m => Applicative (CheckingFuelMonad m)  
CheckpointMonad m => CheckpointMonad (CheckingFuelMonad m)  
UniqueMonad m => UniqueMonad (CheckingFuelMonad m)  
Monad m => FuelMonad (CheckingFuelMonad m)  
type Checkpoint (CheckingFuelMonad m)  
data InfiniteFuelMonad m a Source
FuelMonadT InfiniteFuelMonad  
Monad m => Monad (InfiniteFuelMonad m)  
Monad m => Functor (InfiniteFuelMonad m)  
Monad m => Applicative (InfiniteFuelMonad m)  
CheckpointMonad m => CheckpointMonad (InfiniteFuelMonad m)  
UniqueMonad m => UniqueMonad (InfiniteFuelMonad m)  
Monad m => FuelMonad (InfiniteFuelMonad m)  
type Checkpoint (InfiniteFuelMonad m)  
type SimpleFuelMonad = CheckingFuelMonad SimpleUniqueMonad Source
intToUnique :: Int > Unique Source
class Monad m => UniqueMonad m where Source
freshUnique :: m Unique Source
UniqueMonad SimpleUniqueMonad  
Monad m => UniqueMonad (UniqueMonadT m)  
UniqueMonad m => UniqueMonad (InfiniteFuelMonad m)  
UniqueMonad m => UniqueMonad (CheckingFuelMonad m)  
data SimpleUniqueMonad a Source
runSimpleUniqueMonad :: SimpleUniqueMonad a > a Source
data UniqueMonadT m a Source
Monad m => Monad (UniqueMonadT m)  
Monad m => Functor (UniqueMonadT m)  
Monad m => Applicative (UniqueMonadT m)  
Monad m => UniqueMonad (UniqueMonadT m)  
runUniqueMonadT :: Monad m => UniqueMonadT m a > m a Source
uniqueToInt :: Unique > Int Source
type TraceFn = forall a. String > a > a Source
debugFwdJoins :: forall m n f. Show f => TraceFn > ChangePred > FwdPass m n f > FwdPass m n f Source
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:
Trace
trace
as the 1st argument to the debug combinatorThere 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. _ Join
L: 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 f Source
debugFwdTransfers :: forall m n f. Show f => TraceFn > ShowN n > FPred n f > FwdPass m n f > FwdPass m n f Source
debugBwdTransfers :: forall m n f. Show f => TraceFn > ShowN n > BPred n f > BwdPass m n f > BwdPass m n f Source
showGraph :: forall n e x. Showing n > Graph n e x > String Source
showFactBase :: Show f => FactBase f > String Source
© The University of Glasgow and others
Licensed under a BSDstyle license (see top of the page).
https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/hoopl3.10.2.1/CompilerHoopl.html