Safe Haskell	None
Language	Haskell2010

Lang.CPS.Monads

Documentation

type PSΣ' val lτ dτ ψ = (ID :.: ListSet) :.: (,) (𝒮 val lτ dτ ψ) Source

newtype PSΣ val lτ dτ ψ a Source

Constructors

PSΣ
Fields runPSΣ :: ListSet (a, 𝒮 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τ ψ)
(TimeC lτ, TimeC dτ) => Inject (PSΣ val lτ dτ Ψ)
MonadStep (PSΣ val lτ dτ ψ) (PS val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (PSΣ val lτ dτ Ψ) (PSΣ𝒫 val lτ dτ Ψ) (PS val lτ dτ Ψ)
JoinLattice (PSΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), Ord (val lτ dτ ψ)) => PartialOrder (PSΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), Ord (val lτ dτ ψ), Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (PSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (PSΣ val lτ dτ ψ a) (PSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (PSΣ𝒫 val lτ dτ ψ a) (PSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (PSΣ val lτ dτ ψ a) (PSΣ𝒫 val lτ dτ ψ a)

newtype PSΣ𝒫 val lτ dτ ψ a Source

Constructors

PSΣ𝒫
Fields runPSΣ𝒫 :: Set (a, 𝒮 val lτ dτ ψ)

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (PSΣ val lτ dτ Ψ) (PSΣ𝒫 val lτ dτ Ψ) (PS val lτ dτ Ψ)
JoinLattice (PSΣ𝒫 val lτ dτ ψ a)
PartialOrder (PSΣ𝒫 val lτ dτ ψ a)
(Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (PSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (PSΣ val lτ dτ ψ a) (PSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (PSΣ𝒫 val lτ dτ ψ a) (PSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (PSΣ val lτ dτ ψ a) (PSΣ𝒫 val lτ dτ ψ a)

newtype PS val lτ dτ ψ a Source

Constructors

FSPS
Fields runPS :: IsoMonadStep (PSΣ val lτ dτ ψ) (PSΣ' val lτ dτ ψ) (StateT (𝒮 val lτ dτ ψ) (ListSetT ID)) a

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (PS val lτ dτ Ψ)
MonadPlus (PS val lτ dτ ψ)
MonadZero (PS val lτ dτ ψ)
Monad (PS val lτ dτ ψ)
Bind (PS val lτ dτ ψ)
Applicative (PS val lτ dτ ψ)
Product (PS val lτ dτ ψ)
Functor (PS val lτ dτ ψ)
Unit (PS val lτ dτ ψ)
MonadState (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ)
MonadStateE (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ)
MonadStateI (𝒮 val lτ dτ ψ) (PS val lτ dτ ψ)
MonadStep (PSΣ val lτ dτ ψ) (PS val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (PSΣ val lτ dτ Ψ) (PSΣ𝒫 val lτ dτ Ψ) (PS val lτ dτ Ψ)

data PI𝒮 lτ dτ ψ Source

Constructors

PI𝒮
Fields pilτ :: lτ ψ pidτ :: dτ ψ piρ :: Env lτ 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 (PI𝒮 lτ dτ ψ)
(Ord (lτ ψ), Ord (dτ ψ)) => Ord (PI𝒮 lτ dτ ψ)
(Pretty (lτ0 ψ0), Pretty (dτ0 ψ0), Pretty (Env lτ0 dτ0 ψ0)) => Pretty (PI𝒮 lτ dτ ψ)
(Initial (lτ ψ), Initial (dτ ψ)) => Initial (PI𝒮 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 FSΣ' val lτ dτ ψ = (ListSet :.: (ID :.: (,) (Store val lτ dτ ψ))) :.: (,) (PI𝒮 lτ dτ ψ) Source

newtype FSΣ val lτ dτ ψ a Source

Constructors

FSΣ
Fields runFSΣ :: ListSet (a, 𝒮 val lτ dτ ψ)

Instances

Isomorphism2 * (FSΣ val lτ dτ ψ) (FSΣ' val lτ dτ ψ)
Morphism2 * (FSΣ val lτ dτ ψ) (FSΣ' val lτ dτ ψ)
Morphism2 * (FSΣ' val lτ dτ ψ) (FSΣ val lτ dτ ψ)
(TimeC lτ, TimeC dτ) => Inject (FSΣ val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStep (FSΣ val lτ dτ ψ) (FS val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FSΣ val lτ dτ Ψ) (FSΣ𝒫 val lτ dτ Ψ) (FS val lτ dτ Ψ)
JoinLattice (FSΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), Ord (val lτ dτ ψ)) => PartialOrder (FSΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), Ord (val lτ dτ ψ), Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (FSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (FSΣ val lτ dτ ψ a) (FSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FSΣ𝒫 val lτ dτ ψ a) (FSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FSΣ val lτ dτ ψ a) (FSΣ𝒫 val lτ dτ ψ a)

newtype FSΣ𝒫 val lτ dτ ψ a Source

Constructors

FSΣ𝒫
Fields runFSΣ𝒫 :: Set (a, 𝒮 val lτ dτ ψ)

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FSΣ val lτ dτ Ψ) (FSΣ𝒫 val lτ dτ Ψ) (FS val lτ dτ Ψ)
JoinLattice (FSΣ𝒫 val lτ dτ ψ a)
PartialOrder (FSΣ𝒫 val lτ dτ ψ a)
(Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (FSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (FSΣ val lτ dτ ψ a) (FSΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FSΣ𝒫 val lτ dτ ψ a) (FSΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FSΣ val lτ dτ ψ a) (FSΣ𝒫 val lτ dτ ψ a)

newtype FS val lτ dτ ψ a Source

Constructors

FS
Fields runFS :: IsoMonadStep (FSΣ val lτ dτ ψ) (FSΣ' val lτ dτ ψ) (AddStateT (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ) (ListSetT (StateT (Store val lτ dτ ψ) ID))) a

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (FS val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadPlus (FS val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadZero (FS val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Monad (FS val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Bind (FS val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Applicative (FS val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Product (FS val lτ dτ ψ)
Functor (FS val lτ dτ ψ)
Unit (FS 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τ ψ)) => MonadStateE (𝒮 val lτ dτ ψ) (FS 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τ ψ)) => MonadStep (FSΣ val lτ dτ ψ) (FS val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FSΣ val lτ dτ Ψ) (FSΣ𝒫 val lτ dτ Ψ) (FS val lτ dτ Ψ)

type FIΣ' val lτ dτ ψ = ((ID :.: (,) (Store val lτ dτ ψ)) :.: ListSet) :.: (,) (PI𝒮 lτ dτ ψ) Source

newtype FIΣ val lτ dτ ψ a Source

Constructors

FIΣ
Fields runFIΣ :: (ListSet (a, PI𝒮 lτ dτ ψ), Store val 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τ ψ)
(TimeC lτ, TimeC dτ) => Inject (FIΣ val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStep (FIΣ val lτ dτ ψ) (FI val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FIΣ val lτ dτ Ψ) (FIΣ𝒫 val lτ dτ Ψ) (FI val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => JoinLattice (FIΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), PartialOrder (val lτ dτ ψ)) => PartialOrder (FIΣ val lτ dτ ψ a)
(Ord a, Ord (lτ ψ), Ord (dτ ψ), Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (FIΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (FIΣ val lτ dτ ψ a) (FIΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FIΣ𝒫 val lτ dτ ψ a) (FIΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FIΣ val lτ dτ ψ a) (FIΣ𝒫 val lτ dτ ψ a)

newtype FIΣ𝒫 val lτ dτ ψ a Source

Constructors

FIΣ𝒫
Fields runFIΣ𝒫 :: (Set (a, PI𝒮 lτ dτ ψ), Store val lτ dτ ψ)

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FIΣ val lτ dτ Ψ) (FIΣ𝒫 val lτ dτ Ψ) (FI val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => JoinLattice (FIΣ𝒫 val lτ dτ ψ a)
(Ord (lτ ψ), Ord (dτ ψ), PartialOrder (val lτ dτ ψ)) => PartialOrder (FIΣ𝒫 val lτ dτ ψ a)
(Pretty a, Pretty (lτ ψ), Pretty (dτ ψ), Pretty (val lτ dτ ψ)) => Pretty (FIΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Isomorphism (FIΣ val lτ dτ ψ a) (FIΣ𝒫 val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FIΣ𝒫 val lτ dτ ψ a) (FIΣ val lτ dτ ψ a)
(Ord (val lτ dτ ψ), Ord (lτ ψ), Ord (dτ ψ), Ord a) => Morphism (FIΣ val lτ dτ ψ a) (FIΣ𝒫 val lτ dτ ψ a)

newtype FI val lτ dτ ψ a Source

Constructors

FIPI
Fields runFI :: IsoMonadStep (FIΣ val lτ dτ ψ) (FIΣ' val lτ dτ ψ) (AddStateT (𝒮 val lτ dτ ψ) (PI𝒮 lτ dτ ψ) (ListSetT (StateT (Store val lτ dτ ψ) ID))) a

Instances

(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Analysis val lτ dτ (FI val lτ dτ Ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadPlus (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadZero (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Monad (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Bind (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Applicative (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => Product (FI val lτ dτ ψ)
Functor (FI val lτ dτ ψ)
Unit (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadState (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateE (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStateI (𝒮 val lτ dτ ψ) (FI val lτ dτ ψ)
(Eq (val lτ dτ ψ), JoinLattice (val lτ dτ ψ)) => MonadStep (FIΣ val lτ dτ ψ) (FI val lτ dτ ψ)
(TimeC lτ, TimeC dτ, ValC lτ dτ val) => Execution (FIΣ val lτ dτ Ψ) (FIΣ𝒫 val lτ dτ Ψ) (FI val lτ dτ Ψ)