Safe Haskell	None
Language	Haskell2010

Lang.LamIf.StateSpace

Documentation

data Addr lτ dτ Source

Constructors

Addr
Fields addrLocation :: Name addrLexicalTime :: lτ addrDynamicTime :: dτ

Instances

Isomorphism2 * (FIΣ val lτ dτ) (FIΣ' val lτ dτ)
Morphism2 * (FIΣ val lτ dτ) (FIΣ' val lτ dτ)
Morphism2 * (FIΣ' val lτ dτ) (FIΣ 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τ)
Morphism (𝒮Cxt lτ dτ, Store val lτ dτ) (𝒮 val lτ dτ)
Isomorphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)
Morphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)

type Env lτ dτ = Map Name (Addr lτ dτ) Source

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

data 𝒮Cxt lτ dτ Source

Constructors

𝒮Cxt
Fields 𝓈Cxtlτ :: lτ 𝓈Cxtdτ :: dτ 𝓈Cxtρ :: Env lτ dτ

Instances

Isomorphism2 * (FIΣ val lτ dτ) (FIΣ' val lτ dτ)
Morphism2 * (FIΣ val lτ dτ) (FIΣ' val lτ dτ)
Morphism2 * (FIΣ' val lτ dτ) (FIΣ val lτ dτ)
(Eq lτ, Eq dτ) => Eq (𝒮Cxt lτ dτ)
(Ord lτ, Ord dτ) => Ord (𝒮Cxt lτ dτ)
(Bot lτ, Bot dτ) => Bot (𝒮Cxt lτ dτ)
(Pretty lτ0, Pretty dτ0, Pretty (Env lτ0 dτ0)) => Pretty (𝒮Cxt lτ dτ)
Morphism (𝒮Cxt lτ dτ, Store val lτ dτ) (𝒮 val lτ dτ)
Isomorphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)
Morphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)

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

𝓈CxtdτL :: forall lτ dτ. Lens (𝒮Cxt lτ dτ) dτ Source

𝓈CxtlτL :: forall lτ dτ. Lens (𝒮Cxt lτ dτ) lτ Source

data 𝒮 val lτ dτ Source

Constructors

𝒮
Fields 𝓈Cxt :: 𝒮Cxt lτ dτ 𝓈σ :: Store val lτ dτ

Instances

Isomorphism2 * (FSΣ val lτ dτ) (FSΣ' val lτ dτ)
Isomorphism2 * (PSΣ val lτ dτ) (PSΣ' val lτ dτ)
Morphism2 * (FSΣ val lτ dτ) (FSΣ' val lτ dτ)
Morphism2 * (FSΣ' val lτ dτ) (FSΣ val lτ dτ)
Morphism2 * (PSΣ val lτ dτ) (PSΣ' val lτ dτ)
Morphism2 * (PSΣ' val lτ dτ) (PSΣ val lτ dτ)
Morphism (𝒮Cxt lτ dτ, Store val lτ dτ) (𝒮 val lτ dτ)
(Eq val, Eq lτ, Eq dτ) => Eq (𝒮 val lτ dτ)
(Ord val, Ord lτ, Ord dτ) => Ord (𝒮 val lτ dτ)
(Bot lτ, Bot dτ) => Bot (𝒮 val lτ dτ)
(Pretty (𝒮Cxt lτ0 dτ0), Pretty (Store val0 lτ0 dτ0)) => Pretty (𝒮 val lτ dτ)
Isomorphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)
Morphism (𝒮 val lτ dτ) (𝒮Cxt lτ dτ, Store val lτ dτ)
MonadState (𝒮 val lτ dτ) (PS val lτ dτ)
MonadState (𝒮 val lτ dτ) (FS val lτ dτ)
JoinLattice val => MonadState (𝒮 val lτ dτ) (FI val lτ dτ)

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

𝓈CxtL :: forall val lτ dτ. Lens (𝒮 val lτ dτ) (𝒮Cxt lτ dτ) Source

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

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

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

data Clo lτ dτ Source

Constructors

Clo
Fields cloLoc :: LocNum cloArgs :: [Name] cloCall :: Call 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τ)

data PicoVal lτ dτ Source

Constructors

LitPicoVal Lit
AddrPicoVal (Addr lτ dτ)

Instances

(Eq lτ, Eq dτ) => Eq (PicoVal lτ dτ)
(Ord lτ, Ord dτ) => Ord (PicoVal lτ dτ)
(Pretty Lit, Pretty (Addr lτ0 dτ0)) => Pretty (PicoVal lτ dτ)

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

Methods

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

binop :: BinOp -> val -> val -> val Source

tup :: (PicoVal lτ dτ, PicoVal lτ dτ) -> val Source

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

elimTup :: val -> Set (PicoVal lτ dτ, PicoVal lτ dτ) Source

Instances

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