Safe Haskell	None
Language	Haskell2010

Lang.LamIf.Semantics

Documentation

type Ψ = LocNum Source

type TimeC τ = (Time Ψ τ, Bot τ, Ord τ, Pretty τ) Source

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

type MonadC val lτ dτ m = (Monad m, MonadBot m, MonadPlus m, MonadState (𝒮 val lτ dτ) m) Source

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τ Source

Instances

(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τ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (PS val lτ dτ)

type GC m = Call -> m () Source

type CreateClo lτ dτ m = LocNum -> [Name] -> Call -> m (Clo lτ dτ) Source

type TimeFilter = Call -> Bool Source

new :: Analysis val lτ dτ m => Name -> m (Addr lτ dτ) Source

bind :: Analysis val lτ dτ m => Name -> val -> Map Name (Addr lτ dτ) -> m (Map Name (Addr lτ dτ)) Source

bindM :: Analysis val lτ dτ m => Name -> val -> m () Source

rebind :: Analysis val lτ dτ m => Name -> val -> m () Source

rebindPico :: Analysis val lτ dτ m => PrePico Name -> val -> m () Source

addr :: Analysis val lτ dτ m => Addr lτ dτ -> m val Source

var :: Analysis val lτ dτ m => Name -> m val Source

lam :: Analysis val lτ dτ m => CreateClo lτ dτ m -> LocNum -> [Name] -> Call -> m val Source

picoRef :: Analysis val lτ dτ m => Pico -> m (PicoVal lτ dτ) Source

picoVal :: Analysis val lτ dτ m => PicoVal lτ dτ -> m val Source

pico :: Analysis val lτ dτ m => Pico -> m val Source

atom :: Analysis val lτ dτ m => CreateClo lτ dτ m -> Atom -> m val Source

apply :: Analysis val lτ dτ m => TimeFilter -> Call -> PrePico Name -> val -> [val] -> m Call Source

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

onlyStuck :: (MonadStep ς m, Analysis val lτ dτ m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> Call -> m Call Source

type StateSpaceC ς' = (PartialOrder (ς' Call), JoinLattice (ς' Call), Difference (ς' Call), Pretty (ς' Call)) Source

class (MonadStep ς m, Inject ς, Isomorphism (ς Call) (ς' Call), StateSpaceC ς') => Execution ς ς' m | m -> ς, m -> ς' Source

Instances

(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τ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (PSΣ val lτ dτ) (PSΣ𝒫 val lτ dτ) (PS val lτ dτ)

liftς :: Execution ς ς' m => (Call -> m Call) -> ς' Call -> ς' Call Source

injectς :: forall ς ς' a. (Inject ς, Isomorphism (ς a) (ς' a)) => P ς -> a -> ς' a Source

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

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

execCollectHistory :: forall val lτ dτ m ς ς'. (Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> Call -> [ς' Call] Source

execCollectDiffs :: forall val lτ dτ m ς ς'. (Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> Call -> [ς' Call] Source

execOnlyStuck :: (Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> Call -> ς' Call Source

nogc :: Monad m => Call -> m () Source

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

callTouched :: (TimeC lτ, TimeC dτ) => Env lτ dτ -> Set Name -> Set (Addr lτ dτ) Source

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

picoValTouched :: (TimeC lτ, TimeC dτ) => PicoVal lτ dτ -> Set (Addr lτ dτ) Source

tupleTouched :: (TimeC lτ, TimeC dτ) => (PicoVal lτ dτ, PicoVal lτ dτ) -> Set (Addr lτ dτ) Source

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

linkClo :: Analysis val lτ dτ m => LocNum -> [Name] -> Call -> m (Clo lτ dτ) Source

copyClo :: Analysis val lτ dτ m => LocNum -> [Name] -> Call -> m (Clo lτ dτ) Source

type UniTime τ = W (TimeC τ) Source

data ExTime where Source

Constructors

ExTime :: forall τ. UniTime τ -> ExTime

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

data ExVal where Source

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

data ExMonad where Source

Constructors

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

newtype AllGC Source

Constructors

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

newtype AllCreateClo Source

Constructors

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

data Options Source

Constructors

Options
Fields ltimeOp :: ExTime dtimeOp :: ExTime valOp :: ExVal monadOp :: ExMonad gcOp :: AllGC createCloOp :: AllCreateClo ltimeFilterOp :: TimeFilter dtimeFilterOp :: TimeFilter

withOptions :: forall a. Options -> ((Analysis val lτ dτ m, Execution ς ς' m) => GC m -> CreateClo lτ dτ m -> TimeFilter -> TimeFilter -> a) -> a Source