Safe Haskell	None
Language	Haskell2010

Hoopl.Dataflow

Contents

Respecting Fuel

Synopsis

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.

Constructors

DataflowLattice
Fields fact_name :: String fact_bot :: a fact_join :: JoinFun a

newtype OldFact a :: * -> * Source #

Constructors

OldFact a

newtype NewFact a :: * -> * Source #

Constructors

NewFact a

type family Fact x f :: * Source #

Instances

type Fact O f
type Fact O f = f
type Fact C f
type Fact C f = FactBase f

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

data ChangeFlag :: * Source #

Constructors

NoChange
SomeChange

Instances

Eq ChangeFlag
Methods (==) :: ChangeFlag -> ChangeFlag -> Bool # (/=) :: ChangeFlag -> ChangeFlag -> Bool #
Ord ChangeFlag
Methods compare :: ChangeFlag -> ChangeFlag -> Ordering # (<) :: ChangeFlag -> ChangeFlag -> Bool # (<=) :: ChangeFlag -> ChangeFlag -> Bool # (>) :: ChangeFlag -> ChangeFlag -> Bool # (>=) :: ChangeFlag -> ChangeFlag -> Bool # max :: ChangeFlag -> ChangeFlag -> ChangeFlag # min :: ChangeFlag -> ChangeFlag -> ChangeFlag #

data FwdPass m n f :: (* -> *) -> (* -> * -> *) -> * -> * Source #

Constructors

FwdPass
Fields fp_lattice :: DataflowLattice f fp_transfer :: FwdTransfer n f fp_rewrite :: FwdRewrite m n f

data 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 #

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 rewrite rw 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 f :: (* -> *) -> (* -> * -> *) -> * -> * Source #

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

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 f #

wrapFR Source #

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'

wrapFR2 Source #

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

data BwdPass m n f :: (* -> *) -> (* -> * -> *) -> * -> * Source #

Constructors

BwdPass
Fields bp_lattice :: DataflowLattice f bp_transfer :: BwdTransfer n f bp_rewrite :: BwdRewrite m n f

data 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 #

getBTransfer3 :: BwdTransfer n f -> (n C O -> f -> f, n O O -> f -> f, n O C -> FactBase f -> f) Source #

wrapBR 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'

wrapBR2 Source #

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 f Source #

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 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))) Source #

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) #

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) #

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 f #

if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...

analyzeFwdBlocks :: forall n f e. NonLocal n => FwdPass UniqSM n f -> MaybeC e [Label] -> Graph n e C -> Fact e f -> FactBase f #

if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...

analyzeBwd :: forall n f e. NonLocal n => BwdPass UniqSM n f -> MaybeC e [Label] -> Graph n e C -> Fact C f -> FactBase f #

if the graph being analyzed is open at the entry, there must be no other entry point, or all goes horribly wrong...