Safe Haskell | Trustworthy |
---|---|
Language | Haskell98 |
Hoopl.Dataflow
Contents
- 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
- 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 aSource
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.
Constructors
FwdPass | |
Fields
|
data FwdTransfer n fSource
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 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 fSource
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
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' |
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 |
Constructors
BwdPass | |
Fields
|
data BwdTransfer n fSource
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
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' |
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 fSource
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...