Lang.CPS.Semantics

Documentation

type Ψ = LocNum

type TimeC τ = (Time τ, Initial (τ Ψ), Ord (τ Ψ), Pretty (τ Ψ))

type ValC lτ dτ val = (Val lτ dτ Ψ (val lτ dτ Ψ), Ord (val lτ dτ Ψ), PartialOrder (val lτ dτ Ψ), JoinLattice (val lτ dτ Ψ), Pretty (val lτ dτ Ψ))

type MonadC val lτ dτ m = (Monad m, MonadZero m, MonadPlus m, MonadState (𝒮 val lτ dτ Ψ) m)

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

Instances

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

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (FI val lτ dτ Ψ)

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (FS val lτ dτ Ψ)

type GC m = SGCall -> m ()

type CreateClo lτ dτ m = LocNum -> [SGName] -> SGCall -> m (Clo lτ dτ Ψ)

type TimeFilter = SGCall -> Bool

new :: Analysis val lτ dτ m => SGName -> m (Addr lτ dτ Ψ)

bind :: Analysis val lτ dτ m => SGName -> val lτ dτ Ψ -> Map SGName (Addr lτ dτ Ψ) -> m (Map SGName (Addr lτ dτ Ψ))

bindM :: Analysis val lτ dτ m => SGName -> val lτ dτ Ψ -> m ()

var :: Analysis val lτ dτ m => SGName -> m (val lτ dτ Ψ)

lam :: Analysis val lτ dτ m => CreateClo lτ dτ m -> LocNum -> [SGName] -> SGCall -> m (val lτ dτ Ψ)

pico :: Analysis val lτ dτ m => SGPico -> m (val lτ dτ Ψ)

atom :: Analysis val lτ dτ m => CreateClo lτ dτ m -> SGAtom -> m (val lτ dτ Ψ)

apply :: Analysis val lτ dτ m => TimeFilter -> SGCall -> val lτ dτ Ψ -> [val lτ dτ Ψ] -> m SGCall

call :: Analysis val lτ dτ m => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> SGCall -> m SGCall

nogc :: Monad m => SGCall -> m ()

closureTouched :: (TimeC lτ, TimeC dτ) => Clo lτ dτ Ψ -> Set (Addr lτ dτ Ψ)

addrTouched :: (TimeC lτ, TimeC dτ, ValC lτ dτ val) => Map (Addr lτ dτ Ψ) (val lτ dτ Ψ) -> Addr lτ dτ Ψ -> Set (Addr lτ dτ Ψ)

currClosure :: Analysis val lτ dτ m => SGCall -> m (Clo lτ dτ Ψ)

yesgc :: Analysis val lτ dτ m => SGCall -> m ()

linkClo :: Analysis val lτ dτ m => LocNum -> [SGName] -> SGCall -> m (Clo lτ dτ Ψ)

copyClo :: Analysis val lτ dτ m => LocNum -> [SGName] -> SGCall -> m (Clo lτ dτ Ψ)

type MonadStateSpaceC ς ς' m = (MonadStep ς m, Inject ς, Isomorphism (ς SGCall) (ς' SGCall))

type StateSpaceC ς' = (PartialOrder (ς' SGCall), JoinLattice (ς' SGCall), Pretty (ς' SGCall))

class (MonadStateSpaceC ς ς' m, StateSpaceC ς') => Execution ς ς' m | m -> ς, m -> ς'

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (PSΣ val lτ dτ Ψ) (PSΣ𝒫 val lτ dτ Ψ) (PS val lτ dτ Ψ)

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FIΣ val lτ dτ Ψ) (FIΣ𝒫 val lτ dτ Ψ) (FI val lτ dτ Ψ)

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FSΣ val lτ dτ Ψ) (FSΣ𝒫 val lτ dτ Ψ) (FS val lτ dτ Ψ)

exec :: forall val lτ dτ ς ς' m. (Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> SGCall -> ς' SGCall

execCollect :: forall val lτ dτ ς ς' m. (Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> SGCall -> ς' SGCall

type UniTime τ = W (TimeC τ)

data ExTime where

Constructors

ExTime :: forall τ. UniTime τ -> ExTime

type UniVal val = forall lτ dτ. (TimeC lτ, TimeC dτ) => W (ValC lτ dτ val)

data ExVal where

Constructors

ExVal :: forall val. UniVal val -> ExVal

type UniMonad ς ς' m = forall val lτ dτ. (TimeC lτ, TimeC dτ, ValC lτ dτ val) => W (Analysis val lτ dτ (m val lτ dτ Ψ), Execution (ς val lτ dτ Ψ) (ς' val lτ dτ Ψ) (m val lτ dτ Ψ))

data ExMonad where

Constructors

ExMonad :: forall ς ς' m. UniMonad ς ς' m -> ExMonad

newtype AllGC

Constructors

AllGC

Fields

runAllGC :: forall val lτ dτ m. Analysis val lτ dτ m => GC m

newtype AllCreateClo

Constructors

AllCreateClo

Fields

runAllCreateClo :: forall val lτ dτ m. Analysis val lτ dτ m => CreateClo lτ dτ m

data Options

Constructors

Options

Fields

ltimeOp :: ExTime

dtimeOp :: ExTime

valOp :: ExVal

monadOp :: ExMonad

gcOp :: AllGC

createCloOp :: AllCreateClo

ltimeFilterOp :: TimeFilter

dtimeFilterOp :: TimeFilter

data ExSigma where

Constructors

ExSigma :: StateSpaceC ς => ς SGCall -> ExSigma

runWithOptions :: Options -> SGCall -> ExSigma