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.
Blocks
data Block n e x where Source #
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 Source #
Constructing blocks
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.
Deconstructing blocks
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.
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 Source #
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 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 #
Biasing
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.
Body
Graph
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).
class NonLocal thing where Source #
Gives access to the anchor points for nonlocal edges as well as the edges themselves
Constructing graphs
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 Source #
Maps
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.
Folds
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.
Extracting Labels
Depthfirst traversals
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_from_except :: forall block e. (NonLocal block, LabelsPtr e) => LabelMap (block C C) > e > LabelSet > [block C C] Source #
freshLabel :: UniqueMonad m => m Label Source #
uniqueToLbl :: Unique > Label Source #
lblToUnique :: Label > Unique 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.
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.
changeIf :: Bool > ChangeFlag Source #
FwdPass  

newtype FwdTransfer n f Source #
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  

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  

newtype BwdTransfer n f Source #
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  

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