Lang.Hask.Semantics

Documentation

data Moment lτ dτ

Constructors

Moment

Fields

timeLex :: lτ

timeDyn :: dτ

Instances

(Eq lτ, Eq dτ) => Eq (Moment lτ dτ)

(Ord lτ, Ord dτ) => Ord (Moment lτ dτ)

(Time ψ lτ, Time ψ dτ) => Bot (Moment lτ dτ)

(Pretty lτ0, Pretty dτ0) => Pretty (Moment lτ dτ)

timeDynL :: forall lτ dτ. Lens (Moment lτ dτ) dτ

timeLexL :: forall lτ dτ. Lens (Moment lτ dτ) lτ

data Addr lτ dτ

Constructors

Addr

Fields

addrName :: Name

addrTime :: Moment lτ dτ

Instances

(Eq lτ, Eq dτ) => Eq (Addr lτ dτ)

(Ord lτ, Ord dτ) => Ord (Addr lτ dτ)

(Pretty Name, Pretty (Moment lτ0 dτ0)) => Pretty (Addr lτ dτ)

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

type Store ν lτ dτ = Map (Addr lτ dτ) (ν lτ dτ)

data ArgVal lτ dτ

Constructors

AddrVal (Addr lτ dτ)

LitVal Literal

TypeVal

Instances

(Eq lτ, Eq dτ) => Eq (ArgVal lτ dτ)

(Ord lτ, Ord dτ) => Ord (ArgVal lτ dτ)

(Pretty (Addr lτ0 dτ0), Pretty Literal) => Pretty (ArgVal lτ dτ)

data Data lτ dτ

Constructors

Data

Fields

dataCon :: DataCon

dataArgs :: [ArgVal lτ dτ]

Instances

(Eq lτ, Eq dτ) => Eq (Data lτ dτ)

(Ord lτ, Ord dτ) => Ord (Data lτ dτ)

(Pretty DataCon, Pretty [ArgVal lτ0 dτ0]) => Pretty (Data lτ dτ)

data FunClo lτ dτ

Constructors

FunClo

Fields

funCloLamArg :: Name

funCloKonArg :: Name

funCloBody :: Call

funCloEnv :: Env lτ dτ

funCloTime :: lτ

Instances

(Eq lτ, Eq dτ) => Eq (FunClo lτ dτ)

(Ord lτ, Ord dτ) => Ord (FunClo lτ dτ)

(Pretty Name, Pretty Call, Pretty (Env lτ0 dτ0), Pretty lτ0) => Pretty (FunClo lτ dτ)

data Ref lτ dτ

Constructors

Ref

Fields

refAddr :: Addr lτ dτ

Instances

(Eq lτ, Eq dτ) => Eq (Ref lτ dτ)

(Ord lτ, Ord dτ) => Ord (Ref lτ dτ)

Pretty (Addr lτ0 dτ0) => Pretty (Ref lτ dτ)

data KonClo lτ dτ

Constructors

KonClo

Fields

konCloArg :: Name

konCloBody :: Call

konCloEnv :: Env lτ dτ

Instances

(Eq lτ, Eq dτ) => Eq (KonClo lτ dτ)

(Ord lτ, Ord dτ) => Ord (KonClo lτ dτ)

(Pretty Name, Pretty Call, Pretty (Env lτ0 dτ0)) => Pretty (KonClo lτ dτ)

data ThunkClo lτ dτ

Constructors

ThunkClo

Fields

thunkCloKonXLoc :: Int

thunkCloKonXArg :: Name

thunkCloKonKArg :: Name

thunkCloFun :: Pico

thunkCloArg :: Pico

thunkCloEnv :: Env lτ dτ

thunkCloTime :: lτ

Instances

(Eq lτ, Eq dτ) => Eq (ThunkClo lτ dτ)

(Ord lτ, Ord dτ) => Ord (ThunkClo lτ dτ)

(Pretty Int, Pretty Name, Pretty Pico, Pretty (Env lτ0 dτ0), Pretty lτ0) => Pretty (ThunkClo lτ dτ)

data KonMemoClo lτ dτ

Constructors

KonMemoClo

Fields

konMemoCloLoc :: Addr lτ dτ

konMemoCloThunk :: ThunkClo lτ dτ

konMemoCloArg :: Name

konMemoCloBody :: Call

konMemoCloEnv :: Env lτ dτ

Instances

(Eq lτ, Eq dτ) => Eq (KonMemoClo lτ dτ)

(Ord lτ, Ord dτ) => Ord (KonMemoClo lτ dτ)

(Pretty (Addr lτ0 dτ0), Pretty (ThunkClo lτ0 dτ0), Pretty Name, Pretty Call, Pretty (Env lτ0 dτ0)) => Pretty (KonMemoClo lτ dτ)

data Forced lτ dτ

Constructors

Forced

Fields

forcedVal :: ArgVal lτ dτ

Instances

(Eq lτ, Eq dτ) => Eq (Forced lτ dτ)

(Ord lτ, Ord dτ) => Ord (Forced lτ dτ)

Pretty (ArgVal lτ0 dτ0) => Pretty (Forced lτ dτ)

class Val lτ dτ γν αν | αν -> γν where

Methods

botI :: αν lτ dτ

litI :: Literal -> αν lτ dτ

litTestE :: Literal -> αν lτ dτ -> γν Bool

dataI :: Data lτ dτ -> αν lτ dτ

dataAnyI :: DataCon -> αν lτ dτ

dataE :: αν lτ dτ -> γν (Data lτ dτ)

funCloI :: FunClo lτ dτ -> αν lτ dτ

funCloE :: αν lτ dτ -> γν (FunClo lτ dτ)

refI :: Ref lτ dτ -> αν lτ dτ

refAnyI :: αν lτ dτ

refE :: αν lτ dτ -> γν (Ref lτ dτ)

konCloI :: KonClo lτ dτ -> αν lτ dτ

konCloE :: αν lτ dτ -> γν (KonClo lτ dτ)

konMemoCloI :: KonMemoClo lτ dτ -> αν lτ dτ

konMemoCloE :: αν lτ dτ -> γν (KonMemoClo lτ dτ)

thunkCloI :: ThunkClo lτ dτ -> αν lτ dτ

thunkCloE :: αν lτ dτ -> γν (ThunkClo lτ dτ)

forcedI :: Forced lτ dτ -> αν lτ dτ

forcedE :: αν lτ dτ -> γν (Forced lτ dτ)

Instances

(Ord lτ, Ord dτ) => Val lτ dτ ConstructiveClassical OCVal

(Ord lτ, Ord dτ, Ord (ν lτ dτ), Val lτ dτ ConstructiveClassical ν) => Val lτ dτ SetWithTop (SumOfProdVal * * ν)

data 𝒮 ν lτ dτ

Constructors

𝒮

Fields

𝓈Env :: Env lτ dτ

𝓈Store :: Store ν lτ dτ

𝓈Time :: Moment lτ dτ

Instances

Isomorphism2 * (PSΣ ν lτ dτ) (PSΣ' ν lτ dτ)

Morphism2 * (PSΣ ν lτ dτ) (PSΣ' ν lτ dτ)

Morphism2 * (PSΣ' ν lτ dτ) (PSΣ ν lτ dτ)

(Eq lτ, Eq dτ, Eq (ν lτ dτ)) => Eq (𝒮 ν lτ dτ)

(Ord lτ, Ord dτ, Ord (ν lτ dτ)) => Ord (𝒮 ν lτ dτ)

(Time ψ lτ, Time ψ dτ) => Bot (𝒮 ν lτ dτ)

(Pretty (Env lτ0 dτ0), Pretty (Store ν0 lτ0 dτ0), Pretty (Moment lτ0 dτ0)) => Pretty (𝒮 ν lτ dτ)

MonadState (𝒮 ν lτ dτ) (PS ν lτ dτ)

𝓈TimeL :: forall ν lτ dτ. Lens (𝒮 ν lτ dτ) (Moment lτ dτ)

𝓈StoreL :: forall ν lτ dτ. Lens (𝒮 ν lτ dτ) (Store ν lτ dτ)

𝓈EnvL :: forall ν lτ dτ. Lens (𝒮 ν lτ dτ) (Env lτ dτ)

type TimeC lτ dτ = (Ord lτ, Ord dτ, Time Int lτ, Time Int dτ)

type ValC ν lτ dτ = (JoinLattice (ν lτ dτ), Meet (ν lτ dτ), Neg (ν lτ dτ), Val lτ dτ SetWithTop ν)

type MonadC ν lτ dτ m = (Monad m, MonadBot m, MonadTop m, MonadPlus m, MonadState (𝒮 ν lτ dτ) m)

class (MonadC ν lτ dτ m, ValC ν lτ dτ, TimeC lτ dτ) => Analysis ν lτ dτ m | m -> ν, m -> lτ, m -> dτ

Instances

(TimeC lτ dτ, ValC ν lτ dτ) => Analysis ν lτ dτ (PS ν lτ dτ)

tickLex :: Analysis ν lτ dτ m => Call -> m ()

tickDyn :: Analysis ν lτ dτ m => Call -> m ()

alloc :: Analysis ν lτ dτ m => Name -> m (Addr lτ dτ)

bindJoin :: Analysis ν lτ dτ m => Name -> ν lτ dτ -> m ()

updateRef :: Analysis ν lτ dτ m => Addr lτ dτ -> ν lτ dτ -> ν lτ dτ -> m ()

refine :: Analysis ν lτ dτ m => ArgVal lτ dτ -> ν lτ dτ -> m ()

extract :: Analysis ν lτ dτ m => (a -> ν lτ dτ) -> (ν lτ dτ -> SetWithTop a) -> ArgVal lτ dτ -> m a

extractIsLit :: Analysis ν lτ dτ m => Literal -> ArgVal lτ dτ -> m ()

addr :: Analysis ν lτ dτ m => Addr lτ dτ -> m (ν lτ dτ)

argVal :: Analysis ν lτ dτ m => ArgVal lτ dτ -> m (ν lτ dτ)

varAddr :: Analysis ν lτ dτ m => Name -> m (Addr lτ dτ)

var :: Analysis ν lτ dτ m => Name -> m (ν lτ dτ)

pico :: Analysis ν lτ dτ m => Pico -> m (ν lτ dτ)

picoArg :: Analysis ν lτ dτ m => Pico -> m (ArgVal lτ dτ)

atom :: Analysis ν lτ dτ m => Atom -> m (ν lτ dτ)

forceThunk :: forall ν lτ dτ m. Analysis ν lτ dτ m => Name -> ArgVal lτ dτ -> Call -> m Call

call :: Analysis ν lτ dτ m => Call -> m Call