maam-0.1.0.0: A monadic framework for abstract interpretation.

Safe HaskellNone
LanguageHaskell2010

Lang.CPS.StateSpace

Documentation

data Addr lτ dτ ψ Source

Constructors

Addr 

Fields

addrLocation :: SGName
 
addrLexicalTime :: lτ ψ
 
addrDynamicTime :: dτ ψ
 

Instances

Isomorphism2 * (FIΣ val lτ dτ ψ) (FIΣ' val lτ dτ ψ) 
Isomorphism2 * (FSΣ val lτ dτ ψ) (FSΣ' val lτ dτ ψ) 
Morphism2 * (FIΣ val lτ dτ ψ) (FIΣ' val lτ dτ ψ) 
Morphism2 * (FIΣ' val lτ dτ ψ) (FIΣ val lτ dτ ψ) 
Morphism2 * (FSΣ val lτ dτ ψ) (FSΣ' val lτ dτ ψ) 
Morphism2 * (FSΣ' val lτ dτ ψ) (FSΣ val lτ dτ ψ) 
Morphism (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) (𝒮 val lτ dτ ψ) 
(Eq (lτ ψ), Eq (dτ ψ)) => Eq (Addr lτ dτ ψ) 
(Ord (lτ ψ), Ord (dτ ψ)) => Ord (Addr lτ dτ ψ) 
(Pretty (lτ ψ), Pretty (dτ ψ)) => Pretty (Addr lτ dτ ψ) 
Isomorphism (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) 
Morphism (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) 

type Env lτ dτ ψ = Map SGName (Addr lτ dτ ψ) Source

type Store val lτ dτ ψ = Map (Addr lτ dτ ψ) (val lτ dτ ψ) Source

data 𝒮 val lτ dτ ψ Source

Constructors

𝒮 

Fields

𝓈lτ :: lτ ψ
 
𝓈dτ :: dτ ψ
 
𝓈ρ :: Env lτ dτ ψ
 
𝓈σ :: Store val lτ dτ ψ
 

Instances

Isomorphism2 * (PSΣ val lτ dτ ψ) (PSΣ' val lτ dτ ψ) 
Morphism2 * (PSΣ val lτ dτ ψ) (PSΣ' val lτ dτ ψ) 
Morphism2 * (PSΣ' val lτ dτ ψ) (PSΣ val lτ dτ ψ) 
Morphism (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) (𝒮 val lτ dτ ψ) 
(Eq (lτ ψ), Eq (dτ ψ), Eq (val lτ dτ ψ)) => Eq (𝒮 val lτ dτ ψ) 
(Ord (lτ ψ), Ord (dτ ψ), Ord (val lτ dτ ψ)) => Ord (𝒮 val lτ dτ ψ) 
(Pretty (lτ0 ψ0), Pretty (dτ0 ψ0), Pretty (Env lτ0 dτ0 ψ0), Pretty (Store val0 lτ0 dτ0 ψ0)) => Pretty (𝒮 val lτ dτ ψ) 
(Initial (lτ ψ), Initial (dτ ψ)) => Initial (𝒮 val lτ dτ ψ) 
Isomorphism (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) 
Morphism (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ, Store val lτ dτ ψ) 
MonadState (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadState (𝒮 val lτ dτ ψ) (FS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadState (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ) 
MonadStateE (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateE (𝒮 val lτ dτ ψ) (FS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateE (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ) 
MonadStateI (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateI (𝒮 val lτ dτ ψ) (FS val lτ dτ ψ) 
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateI (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ) 

𝓈σL :: forall val lτ dτ ψ. Lens (𝒮 val lτ dτ ψ) (Store val lτ dτ ψ) Source

𝓈ρL :: forall val lτ dτ ψ. Lens (𝒮 val lτ dτ ψ) (Env lτ dτ ψ) Source

𝓈dτL :: forall val lτ dτ ψ. Lens (𝒮 val lτ dτ ψ) (dτ ψ) Source

𝓈lτL :: forall val lτ dτ ψ. Lens (𝒮 val lτ dτ ψ) (lτ ψ) Source

data Clo lτ dτ ψ Source

Constructors

Clo 

Fields

cloLoc :: LocNum
 
cloArgs :: [SGName]
 
cloCall :: SGCall
 
cloEnv :: Env lτ dτ ψ
 
cloTime :: lτ ψ
 

Instances

(Eq (lτ ψ), Eq (dτ ψ)) => Eq (Clo lτ dτ ψ) 
(Ord (lτ ψ), Ord (dτ ψ)) => Ord (Clo lτ dτ ψ) 
(Pretty (lτ ψ), Pretty (dτ ψ)) => Pretty (Clo lτ dτ ψ) 

class Val lτ dτ ψ val | val -> lτ, val -> dτ, val -> ψ where Source

Methods

lit :: Lit -> val Source

clo :: Clo lτ dτ ψ -> val Source

op :: Op -> val -> val Source

elimBool :: val -> Set Bool Source

elimClo :: val -> Set (Clo lτ dτ ψ) Source

Instances

(Ord (dτ ψ), Ord (lτ ψ)) => Val lτ dτ ψ (CVal lτ dτ ψ) 
(Ord (lτ ψ), Ord (dτ ψ)) => Val lτ dτ ψ (AVal lτ dτ ψ) 
(Ord (dτ ψ), Ord (lτ ψ)) => Val lτ dτ ψ (Power (* -> *) (* -> *) * AVal lτ dτ ψ) 
(Ord (dτ ψ), Ord (lτ ψ)) => Val lτ dτ ψ (Power (* -> *) (* -> *) * CVal lτ dτ ψ)