Lang.CPS.StateSpace

Documentation

data Addr lτ dτ ψ

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τ ψ)

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

data 𝒮 val lτ dτ ψ

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τ ψ)

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

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

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

data Clo lτ dτ ψ

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

Methods

lit :: Lit -> val

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

op :: Op -> val -> val

elimBool :: val -> Set Bool

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

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τ ψ)