maam-0.3.0.0: Monadic Abstracting Abstract Machines (MAAM) built on Galois Transformers

Safe HaskellNone
LanguageHaskell2010

Lang.LamIf.Semantics

Documentation

data LamIfState val Source

Constructors

LamIfState 

Fields

env :: Env
 
κAddr :: Maybe ExpAddr
 
time :: Time
 
store :: Store val
 
κStore :: KStore val
 

Instances

κStoreL :: forall val. Lens (LamIfState val) (KStore val) Source

storeL :: forall val. Lens (LamIfState val) (Store val) Source

timeL :: forall val. Lens (LamIfState val) Time Source

κAddrL :: forall val. Lens (LamIfState val) (Maybe ExpAddr) Source

envL :: forall val. Lens (LamIfState val) Env Source

data LamIfEnv Source

Constructors

LamIfEnv 

Fields

currentExp :: Exp
 
timeParam :: TimeParam
 

timeParamL :: Lens LamIfEnv TimeParam Source

currentExpL :: Lens LamIfEnv Exp Source

class (POrd val, JoinLattice val, Val val, Monad m, MonadState (LamIfState val) m, MonadJoinLattice m) => MonadLamIf val m | m -> val Source

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (PathSensitiveM val) Source 
(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowInsensitiveM val) Source 
(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowSensitiveM val) Source 

type ParamsM m = ReaderT LamIfEnv m Source

atom :: MonadLamIf val m => Atom -> ParamsM m AtomVal Source

atomVal :: MonadLamIf val m => AtomVal -> ParamsM m val Source

push :: MonadLamIf val m => Frame -> ParamsM m () Source

pop :: MonadLamIf val m => ParamsM m Frame Source

bind :: MonadLamIf val m => Name -> val -> ParamsM m () Source

tickL :: MonadLamIf val m => Exp -> Lens LamIfEnv (Maybe ℕ) -> Lens (LamIfState val) [Exp] -> ParamsM m () Source

tickO :: MonadLamIf val m => Exp -> ParamsM m () Source

refine :: MonadLamIf val m => Name -> val -> ParamsM m () Source

delZeroM :: MonadLamIf val m => Name -> ParamsM m () Source

stackReturn :: MonadLamIf val m => Maybe Atom -> AtomVal -> ParamsM m Exp Source

tickK :: MonadLamIf val m => ParamsM m () Source

step :: MonadLamIf val m => TimeParam -> Exp -> m Exp Source

gc :: MonadLamIf val m => Exp -> m () Source

class (MonadLamIf val m, Inject ι ς, GaloisTransformer ς m) => ExecutionLamIf val ι ς m | m -> val, m -> ς Source

Instances

(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 

type LFPLamIf ς = (POrd (ς Exp), JoinLattice (ς Exp), Difference (ς Exp)) Source

ex :: (ExecutionLamIf val ι ς' m, LFPLamIf ς) => TimeParam -> (ς Exp ⇄ ς' Exp) -> (Exp -> m Exp) -> ς Exp -> ς Exp Source

exDiffs :: (ExecutionLamIf val ι ς' m, LFPLamIf ς) => TimeParam -> (ς Exp ⇄ ς' Exp) -> (Exp -> m Exp) -> ς Exp -> Stream (ς Exp) Source