Safe Haskell	None
Language	Haskell2010

Hoopl.Dataflow

Contents

Respecting Fuel

Synopsis

Documentation

data DataflowLattice a :: TYPE Lifted -> TYPE Lifted 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 :: TYPE Lifted -> TYPE Lifted Source

Constructors

OldFact a

newtype NewFact a :: TYPE Lifted -> TYPE Lifted Source

Constructors

NewFact a

type family Fact x f :: * Source

Instances

type Fact O f = 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 :: TYPE Lifted 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 :: (TYPE Lifted -> TYPE Lifted) -> (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted Source

Constructors

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

data FwdTransfer n f :: (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted 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

data FwdRewrite m n f :: (TYPE Lifted -> TYPE Lifted) -> (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted 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 Source

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 Source

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 :: (TYPE Lifted -> TYPE Lifted) -> (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted Source

Constructors

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

data BwdTransfer n f :: (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted 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 :: (TYPE Lifted -> TYPE Lifted) -> (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) -> TYPE Lifted -> TYPE Lifted 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 Source

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 Source

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

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 Source

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 Source

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