Safe Haskell  Trustworthy 

 data DataflowLattice a = DataflowLattice {}
 newtype OldFact a = OldFact a
 newtype NewFact a = NewFact a
 type family Fact x f :: *
 mkFactBase :: DataflowLattice f > [(Label, f)] > FactBase f
 data ChangeFlag
 = NoChange
  SomeChange
 data FwdPass m n f = FwdPass {
 fp_lattice :: DataflowLattice f
 fp_transfer :: FwdTransfer n f
 fp_rewrite :: FwdRewrite m n f
 data 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
 getFTransfer3 :: FwdTransfer n f > (n C O > f > f, n O O > f > f, n O C > f > FactBase f)
 data 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 n f. (n C O > f > UniqSM (Maybe (Graph n C O))) > (n O O > f > UniqSM (Maybe (Graph n O O))) > (n O C > f > UniqSM (Maybe (Graph n O C))) > FwdRewrite UniqSM n f
 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)))
 noFwdRewrite :: FwdRewrite UniqSM 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
 data 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
 getBTransfer3 :: BwdTransfer n f > (n C O > f > f, n O O > f > f, n O C > FactBase f > 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
 data 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 n f. (n C O > f > UniqSM (Maybe (Graph n C O))) > (n O O > f > UniqSM (Maybe (Graph n O O))) > (n O C > FactBase f > UniqSM (Maybe (Graph n O C))) > BwdRewrite UniqSM n f
 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)))
 noBwdRewrite :: BwdRewrite UniqSM n f
 analyzeAndRewriteFwd :: forall n f e x. NonLocal n => FwdPass UniqSM n f > MaybeC e [Label] > Graph n e x > Fact e f > UniqSM (Graph n e x, FactBase f, MaybeO x f)
 analyzeAndRewriteBwd :: NonLocal n => BwdPass UniqSM n f > MaybeC e [Label] > Graph n e x > Fact x f > UniqSM (Graph n e x, FactBase f, MaybeO e f)
 analyzeFwd :: forall n f e. NonLocal n => FwdPass UniqSM n f > MaybeC e [Label] > Graph n e C > Fact e f > FactBase f
 analyzeFwdBlocks :: forall n f e. NonLocal n => FwdPass UniqSM n f > MaybeC e [Label] > Graph n e C > Fact e f > FactBase f
 analyzeBwd :: forall n f e. NonLocal n => BwdPass UniqSM n f > MaybeC e [Label] > Graph n e C > Fact C f > FactBase f
Documentation
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 :: 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.
FwdPass  

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 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.
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 n f. (n C O > f > UniqSM (Maybe (Graph n C O))) > (n O O > f > UniqSM (Maybe (Graph n O O))) > (n O C > f > UniqSM (Maybe (Graph n O C))) > FwdRewrite UniqSM 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 :: FwdRewrite UniqSM n fSource
:: (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  

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
:: (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 
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 n f. (n C O > f > UniqSM (Maybe (Graph n C O))) > (n O O > f > UniqSM (Maybe (Graph n O O))) > (n O C > FactBase f > UniqSM (Maybe (Graph n O C))) > BwdRewrite UniqSM n fSource
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 :: BwdRewrite UniqSM n fSource
analyzeAndRewriteFwd :: forall n f e x. NonLocal n => FwdPass UniqSM n f > MaybeC e [Label] > Graph n e x > Fact e f > UniqSM (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 :: NonLocal n => BwdPass UniqSM n f > MaybeC e [Label] > Graph n e x > Fact x f > UniqSM (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
analyzeFwd :: forall n f e. NonLocal n => FwdPass UniqSM n f > MaybeC e [Label] > Graph n e C > Fact e f > FactBase fSource
if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...