| Safe Haskell | Trustworthy |
|---|
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
- = 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.
Constructors
| FwdPass | |
Fields
| |
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 rewriterwalso 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 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
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 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
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 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...