Safe Haskell	None
Language	Haskell2010

Lang.LamIf.Monads

Documentation

newtype InjectLamIf val a Source

Constructors

InjectLamIf
Fields runInjectLamIf :: (a, LamIfState val)

Instances

Inject * (InjectLamIf val) (PathSensitiveΣᵇ val) Source
Inject * (InjectLamIf val) (FlowInsensitiveΣᵇ val) Source
Inject * (InjectLamIf val) (FlowSensitiveΣᵇ val) Source
(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val) Source

isoInjectLamIf :: InjectLamIf val a ⇄ (a, LamIfState val) Source

newtype PathSensitiveΣᵇ val a Source

Constructors

PathSensitiveΣᵇ
Fields runPathSensitiveΣᵇ :: PolyStateΠ (LamIfState val) (NondetJoinΠ ID) a

Instances

Inject * (InjectLamIf val) (PathSensitiveΣᵇ val) Source
(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val) Source
GaloisTransformer (PathSensitiveΣᵇ val) (PathSensitiveM val) Source

isoPathSensitiveΣᵇ :: PathSensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfState val) (NondetJoinΠ ID) a Source

isoPathSensitiveΣᵇ2 :: PathSensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfState val) (NondetJoinΠ ID) Source

newtype PathSensitiveΣ val a Source

Constructors

PathSensitiveΣ
Fields runPathSensitiveΣ :: 𝒫 (a, LamIfState val)

Instances

JoinLattice (PathSensitiveΣ val a) Source
Difference (PathSensitiveΣ val a) Source
Join (PathSensitiveΣ val a) Source
Bot (PathSensitiveΣ val a) Source
POrd (PathSensitiveΣ val a) Source
(Pretty val, Pretty a) => Pretty (PathSensitiveΣ val a) Source

isoPathSensitiveΣ :: (Ord val, Ord a) => PathSensitiveΣ val a ⇄ PathSensitiveΣᵇ val a Source

newtype PathSensitiveM val a Source

Constructors

PathSensitiveM
Fields runPathSensitiveM :: PolyStateT (LamIfState val) (NondetJoinT ID) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (PathSensitiveM val) Source
(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val) Source
Monad (PathSensitiveM val) Source
Functor (PathSensitiveM val) Source
MonadJoinLattice (PathSensitiveM val) Source
MonadJoin (PathSensitiveM val) Source
MonadBot (PathSensitiveM val) Source
MonadState (LamIfState val) (PathSensitiveM val) Source
GaloisTransformer (PathSensitiveΣᵇ val) (PathSensitiveM val) Source

isoPathSensitiveM :: PathSensitiveM val a ⇄ PolyStateT (LamIfState val) (NondetJoinT ID) a Source

isoPathSensitiveM2 :: PathSensitiveM val ↝⇄ PolyStateT (LamIfState val) (NondetJoinT ID) Source

data LamIfContext val Source

Constructors

LamIfContext
Fields ctxEnv :: Env ctxΚAddr :: Maybe ExpAddr ctxTime :: Time

Instances

Eq (LamIfContext k val) Source
Ord (LamIfContext k val) Source
(Pretty Env, Pretty (Maybe ExpAddr), Pretty Time) => Pretty (LamIfContext k val) Source

data LamIfStores val Source

Constructors

LamIfStores
Fields storesStore :: Store val storesΚStore :: KStore val

Instances

Eq val => Eq (LamIfStores val) Source
Ord val => Ord (LamIfStores val) Source
Join val => JoinLattice (LamIfStores val) Source
Difference val => Difference (LamIfStores val) Source
Join val => Join (LamIfStores val) Source
Bot (LamIfStores val) Source
POrd val => POrd (LamIfStores val) Source
(Pretty (Store val0), Pretty (KStore val0)) => Pretty (LamIfStores val) Source

splitLamIfState :: LamIfState val -> (LamIfContext val, LamIfStores val) Source

combineLamIfState :: (LamIfContext val, LamIfStores val) -> LamIfState val Source

isoSplitLamIfState :: LamIfState val ⇄ (LamIfContext val, LamIfStores val) Source

isoCombineLamIfState :: (a, LamIfState val) ⇄ ((a, LamIfContext val), LamIfStores val) Source

newtype FlowSensitiveΣᵇ val a Source

Constructors

FlowSensitiveΣᵇ
Fields runFlowSensitiveΣᵇ :: PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID) a

Instances

Inject * (InjectLamIf val) (FlowSensitiveΣᵇ val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val) Source
Join val => GaloisTransformer (FlowSensitiveΣᵇ val) (FlowSensitiveM val) Source

isoFlowSensitiveΣᵇ :: FlowSensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID) a Source

isoFlowSensitiveΣ2ᵇ :: FlowSensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID) Source

newtype FlowSensitiveΣ val a Source

Constructors

FlowSensitiveΣ
Fields runFlowSensitiveΣ :: (a, LamIfContext val) ⇰ LamIfStores val

Instances

Join val => JoinLattice (FlowSensitiveΣ val a) Source
Difference val => Difference (FlowSensitiveΣ val a) Source
Join val => Join (FlowSensitiveΣ val a) Source
Bot (FlowSensitiveΣ val a) Source
POrd val => POrd (FlowSensitiveΣ val a) Source
(Pretty val, Pretty a) => Pretty (FlowSensitiveΣ val a) Source

isoFlowSensitiveΣ :: (Ord a, Join val) => FlowSensitiveΣ val a ⇄ FlowSensitiveΣᵇ val a Source

newtype FlowSensitiveM val a Source

Constructors

FlowSensitiveM
Fields runFlowSensitiveM :: PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowSensitiveM val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val) Source
Join val => Monad (FlowSensitiveM val) Source
Functor (FlowSensitiveM val) Source
Join val => MonadJoinLattice (FlowSensitiveM val) Source
Join val => MonadJoin (FlowSensitiveM val) Source
Join val => MonadBot (FlowSensitiveM val) Source
Join val => MonadState (LamIfState val) (FlowSensitiveM val) Source
Join val => GaloisTransformer (FlowSensitiveΣᵇ val) (FlowSensitiveM val) Source

isoFlowSensitiveM :: FlowSensitiveM val a ⇄ PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID) a Source

isoFlowSensitiveM2 :: FlowSensitiveM val ↝⇄ PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID) Source

newtype FlowInsensitiveΣᵇ val a Source

Constructors

FlowInsensitiveΣᵇ
Fields runFlowInsensitiveΣᵇ :: PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID)) a

Instances

Inject * (InjectLamIf val) (FlowInsensitiveΣᵇ val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val) Source
Join val => GaloisTransformer (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val) Source

isoFlowInsensitiveΣᵇ :: FlowInsensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID)) a Source

isoFlowInsensitiveΣᵇ2 :: FlowInsensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID)) Source

newtype FlowInsensitiveΣ val a Source

Constructors

FlowInsensitiveΣ
Fields runFlowInsensitiveΣ :: (𝒫 (a, LamIfContext val), LamIfStores val)

Instances

Join val => JoinLattice (FlowInsensitiveΣ val a) Source
Difference val => Difference (FlowInsensitiveΣ val a) Source
Join val => Join (FlowInsensitiveΣ val a) Source
Bot (FlowInsensitiveΣ val a) Source
POrd val => POrd (FlowInsensitiveΣ val a) Source
(Pretty val, Pretty a) => Pretty (FlowInsensitiveΣ val a) Source

isoFlowInsensitiveΣ :: Ord a => FlowInsensitiveΣ val a ⇄ FlowInsensitiveΣᵇ val a Source

newtype FlowInsensitiveM val a Source

Constructors

FlowInsensitiveM
Fields runFlowInsensitiveM :: PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID)) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowInsensitiveM val) Source
(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val) Source
Join val => Monad (FlowInsensitiveM val) Source
Functor (FlowInsensitiveM val) Source
Join val => MonadJoinLattice (FlowInsensitiveM val) Source
Join val => MonadJoin (FlowInsensitiveM val) Source
Join val => MonadBot (FlowInsensitiveM val) Source
Join val => MonadState (LamIfState val) (FlowInsensitiveM val) Source
Join val => GaloisTransformer (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val) Source

isoFlowInsensitiveM :: FlowInsensitiveM val a ⇄ PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID)) a Source

isoFlowInsensitiveM2 :: FlowInsensitiveM val ↝⇄ PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID)) Source

data MonadParam where Source

Constructors

MonadParam :: forall val ς' ς m. P m -> (ς Exp ⇄ ς' Exp) -> (ς Exp -> Doc) -> W (ExecutionLamIf val (InjectLamIf val) ς' m, LFPLamIf ς) -> MonadParam

pathSensitive :: DomainParam -> MonadParam Source

flowSensitive :: DomainParam -> MonadParam Source

flowInsensitive :: DomainParam -> MonadParam Source