Safe Haskell  Safe 

Language  Haskell2010 
 data O
 data C
 data MaybeO ex t where
 data MaybeC ex t where
 type family IndexedCO ex a b :: *
 data Shape ex where
 data Block n e x where
 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
 emptyBlock :: Block n O O
 blockCons :: n O O > Block n O x > Block n O x
 blockSnoc :: Block n e O > n O O > Block n e O
 blockJoinHead :: n C O > Block n O x > Block n C x
 blockJoinTail :: Block n e O > n O C > Block n e C
 blockJoin :: n C O > Block n O O > n O C > Block n C C
 blockJoinAny :: (MaybeC e (n C O), Block n O O, MaybeC x (n O C)) > Block n e x
 blockAppend :: Block n e O > Block n O x > Block n e x
 firstNode :: Block n C x > n C O
 lastNode :: Block n x C > n O C
 endNodes :: Block n C C > (n C O, n O C)
 blockSplitHead :: Block n C x > (n C O, Block n O x)
 blockSplitTail :: Block n e C > (Block n e O, n O C)
 blockSplit :: Block n C C > (n C O, Block n O O, n O C)
 blockSplitAny :: Block n e x > (MaybeC e (n C O), Block n O O, MaybeC x (n O C))
 replaceFirstNode :: Block n C x > n C O > Block n C x
 replaceLastNode :: Block n x C > n O C > Block n x C
 blockToList :: Block n O O > [n O O]
 blockFromList :: [n O O] > Block n O O
 mapBlock :: (forall e x. n e x > n' e x) > Block n e x > Block n' e x
 mapBlock' :: (forall e x. n e x > n' e x) > Block n e x > Block n' e x
 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
 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
 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
 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
 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
 frontBiasBlock :: Block n e x > Block n e x
 backBiasBlock :: Block n e x > Block n e x
 type Body n = LabelMap (Block n C C)
 type Body' block n = LabelMap (block n C C)
 emptyBody :: Body' block n
 bodyList :: Body' block n > [(Label, block n C C)]
 addBlock :: NonLocal thing => thing C C > LabelMap (thing C C) > LabelMap (thing C C)
 bodyUnion :: forall a. LabelMap a > LabelMap a > LabelMap a
 type Graph = Graph' Block
 data Graph' block n e x where
 class NonLocal thing where
 bodyGraph :: Body n > Graph n C C
 blockGraph :: NonLocal n => Block n e x > Graph n e x
 gUnitOO :: block n O O > Graph' block n O O
 gUnitOC :: block n O C > Graph' block n O C
 gUnitCO :: block n C O > Graph' block n C O
 gUnitCC :: NonLocal (block n) => block n C C > Graph' block n C C
 catGraphNodeOC :: NonLocal n => Graph n e O > n O C > Graph n e C
 catGraphNodeOO :: Graph n e O > n O O > Graph n e O
 catNodeCOGraph :: NonLocal n => n C O > Graph n O x > Graph n C x
 catNodeOOGraph :: n O O > Graph n O x > Graph n O x
 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
 gSplice :: NonLocal n => Graph n e a > Graph n a x > Graph n e x
 mapGraph :: (forall e x. n e x > n' e x) > Graph n e x > Graph n' e x
 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
 foldGraphNodes :: forall n a. (forall e x. n e x > a > a) > forall e x. Graph n e x > a > a
 labelsDefined :: forall block n e x. NonLocal (block n) => Graph' block n e x > LabelSet
 labelsUsed :: forall block n e x. NonLocal (block n) => Graph' block n e x > LabelSet
 externalEntryLabels :: forall n. NonLocal n => LabelMap (Block n C C) > LabelSet
 postorder_dfs :: NonLocal (block n) => Graph' block n O x > [block n C C]
 postorder_dfs_from :: (NonLocal block, LabelsPtr b) => LabelMap (block C C) > b > [block C C]
 postorder_dfs_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) > e > LabelSet > [block C C]
 preorder_dfs :: NonLocal (block n) => Graph' block n O x > [block n C C]
 preorder_dfs_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) > e > LabelSet > [block C C]
 class LabelsPtr l where
 data Label
 freshLabel :: UniqueMonad m => m Label
 data LabelSet
 data LabelMap v
 type FactBase f = LabelMap f
 noFacts :: FactBase f
 lookupFact :: Label > FactBase f > Maybe f
 uniqueToLbl :: Unique > Label
 lblToUnique :: Label > Unique
 data DataflowLattice a = DataflowLattice {}
 type JoinFun a = Label > OldFact a > NewFact a > (ChangeFlag, a)
 newtype OldFact a = OldFact a
 newtype NewFact a = NewFact a
 type family Fact x f :: *
 mkFactBase :: forall f. DataflowLattice f > [(Label, f)] > FactBase f
 data ChangeFlag
 changeIf :: Bool > ChangeFlag
 data FwdPass m n f = FwdPass {
 fp_lattice :: DataflowLattice f
 fp_transfer :: FwdTransfer n f
 fp_rewrite :: FwdRewrite m n f
 newtype FwdTransfer n f = FwdTransfer3 {}
 mkFTransfer :: (forall e x. n e x > f > Fact x f) > FwdTransfer n f
 mkFTransfer3 :: (n C O > f > f) > (n O O > f > f) > (n O C > f > FactBase f) > FwdTransfer n f
 newtype FwdRewrite m n f = FwdRewrite3 {
 getFRewrite3 :: (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)))
 mkFRewrite :: FuelMonad m => (forall e x. n e x > f > m (Maybe (Graph n e x))) > FwdRewrite m n f
 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
 noFwdRewrite :: Monad m => FwdRewrite m n f
 wrapFR :: (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'))) > FwdRewrite m n f > FwdRewrite m' n' f'
 wrapFR2 :: (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))) > FwdRewrite m1 n1 f1 > FwdRewrite m2 n2 f2 > FwdRewrite m3 n3 f3
 data BwdPass m n f = BwdPass {
 bp_lattice :: DataflowLattice f
 bp_transfer :: BwdTransfer n f
 bp_rewrite :: BwdRewrite m n f
 newtype BwdTransfer n f = BwdTransfer3 {}
 mkBTransfer :: (forall e x. n e x > Fact x f > f) > BwdTransfer n f
 mkBTransfer3 :: (n C O > f > f) > (n O O > f > f) > (n O C > FactBase f > f) > BwdTransfer n f
 wrapBR :: (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'))) > BwdRewrite m n f > BwdRewrite m' n' f'
 wrapBR2 :: (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))) > BwdRewrite m1 n1 f1 > BwdRewrite m2 n2 f2 > BwdRewrite m3 n3 f3
 newtype BwdRewrite m n f = BwdRewrite3 {
 getBRewrite3 :: (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)))
 mkBRewrite :: FuelMonad m => (forall e x. n e x > Fact x f > m (Maybe (Graph n e x))) > BwdRewrite m n f
 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
 noBwdRewrite :: Monad m => BwdRewrite m n f
 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)
 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)
Shapes
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
Blocks
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 
Predicates on Blocks
isEmptyBlock :: Block n e x > Bool #
Constructing blocks
emptyBlock :: Block n O O #
blockJoinAny :: (MaybeC e (n C O), Block n O O, MaybeC x (n O C)) > Block n e x #
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.
Deconstructing blocks
blockSplit :: Block n C C > (n C O, Block n O O, n O C) #
Split a closed block into its entry node, open middle block, and exit node.
Modifying blocks
Converting to and from lists
Maps and folds
mapBlock :: (forall e x. n e x > n' e x) > Block n e x > Block n' e x #
map a function over the nodes of a Block
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 #
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 #
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 #
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 #
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 #
Biasing
frontBiasBlock :: Block n e x > Block n e x #
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 #
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.
Body
Graph
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 #
Graph'
is abstracted over the block type, so that we can build
graphs of annotated blocks for example (Compiler.Hoopl.Dataflow
needs this).
Gives access to the anchor points for nonlocal edges as well as the edges themselves
entryLabel :: thing C x > Label #
successors :: thing e C > [Label] #
Constructing graphs
blockGraph :: NonLocal n => Block n e x > Graph n e x #
Splicing graphs
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 #
Maps
mapGraph :: (forall e x. n e x > n' e x) > Graph n e x > Graph n' e x #
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 #
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.
Folds
foldGraphNodes :: forall n a. (forall e x. n e x > a > a) > forall e x. Graph n e x > a > a #
Fold a function over every node in a graph. The fold function must be polymorphic in the shape of the nodes.
Extracting Labels
labelsDefined :: forall block n e x. NonLocal (block n) => Graph' block n e x > LabelSet #
labelsUsed :: forall block n e x. NonLocal (block n) => Graph' block n e x > LabelSet #
Depthfirst traversals
postorder_dfs :: NonLocal (block n) => Graph' block n O x > [block n C C] #
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_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) > e > LabelSet > [block C C] #
preorder_dfs_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) > e > LabelSet > [block C C] #
targetLabels :: l > [Label] #
freshLabel :: UniqueMonad m => m Label #
lookupFact :: Label > FactBase f > Maybe f #
uniqueToLbl :: Unique > Label #
lblToUnique :: Label > Unique #
data DataflowLattice a #
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.
mkFactBase :: forall f. DataflowLattice f > [(Label, f)] > FactBase f #
mkFactBase
creates a FactBase
from a list of (Label
, fact)
pairs. If the same label appears more than once, the relevant facts
are joined.
changeIf :: Bool > ChangeFlag #
FwdPass  

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

mkFRewrite :: FuelMonad m => (forall e x. n e x > f > m (Maybe (Graph n e x))) > FwdRewrite m n f #
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 #
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 #
:: (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  

newtype BwdTransfer n f #
mkBTransfer :: (forall e x. n e x > Fact x f > f) > BwdTransfer n f #
mkBTransfer3 :: (n C O > f > f) > (n O O > f > f) > (n O C > FactBase f > f) > BwdTransfer n f #
:: (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 #
BwdRewrite3  

mkBRewrite :: FuelMonad m => (forall e x. n e x > Fact x f > m (Maybe (Graph n e x))) > BwdRewrite m n f #
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 #
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 #
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) #
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) #
if the graph being analyzed is open at the exit, I don't quite understand the implications of possible other exits
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 rewriterw
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.