MAAM.GaloisTransformer

Documentation

class GaloisTransformer ς m | m -> ς where

Methods

αGT :: forall a b. (ς a -> ς b) -> a -> m b

γGT :: forall a b. (a -> m b) -> ς a -> ς b

Instances

GaloisTransformer ID ID

(GaloisTransformer ς m, Functorial * JoinLattice m) => GaloisTransformer (NondetJoinΠ ς) (NondetJoinT m)

GaloisTransformer (PathSensitiveΣᵇ val) (PathSensitiveM val)

Join val => GaloisTransformer (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

Join val => GaloisTransformer (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

GaloisTransformer ς m => GaloisTransformer (StateΠ s ς) (StateT s m)

GaloisTransformer ς m => GaloisTransformer (PolyStateΠ s ς) (PolyStateT s m)

(GaloisTransformer ς m, Functorial * JoinLattice m, JoinLattice s) => GaloisTransformer (FlowJoinΠ s ς) (FlowJoinT s m)

class Inject ι ς | ς -> ι where

Methods

inject :: ι a -> ς a

Instances

Inject * ID ID

(Inject * ι ς, Functor ς) => Inject * ι (NondetJoinΠ ς)

Inject * (InjectLamIf val) (PathSensitiveΣᵇ val)

Inject * (InjectLamIf val) (FlowInsensitiveΣᵇ val)

Inject * (InjectLamIf val) (FlowSensitiveΣᵇ val)

(Inject * ι ς, Functor ς) => Inject * (StateI s ι) (FlowJoinΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (PolyStateΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (StateΠ s ς)

isoToStateTMorph :: ((a, s) -> m (b, s)) -> a -> StateT s m b

isoFromStateTMorph :: (a -> StateT s m b) -> (a, s) -> m (b, s)

newtype PolyStateT s m a

Constructors

PolyStateT

Fields

runPolyStateT :: StateT s m a

Instances

Polymorphic * * JoinLattice m => Polymorphic * * JoinLattice (PolyStateT s m)

Functor m => MonadState s (PolyStateT s m)

Monad m => Monad (PolyStateT s m)

Functor m => Functor (PolyStateT s m)

MonadJoinLattice m => MonadJoinLattice (PolyStateT s m)

MonadJoin m => MonadJoin (PolyStateT s m)

MonadBot m => MonadBot (PolyStateT s m)

GaloisTransformer ς m => GaloisTransformer (PolyStateΠ s ς) (PolyStateT s m)

Polymorphic * * JoinLattice m => JoinLattice (PolyStateT s m a)

Polymorphic * * JoinLattice m => Join (PolyStateT s m a)

Polymorphic * * JoinLattice m => Bot (PolyStateT s m a)

isoToPolyStateTMorph :: ((a, s) -> m (b, s)) -> a -> PolyStateT s m b

isoFromPolyStateTMorph :: (a -> PolyStateT s m b) -> (a, s) -> m (b, s)

isoToNondetJoinTMorph :: (a -> m (𝒫ᵇ b)) -> a -> NondetJoinT m b

isoFromNondetJoinTMorph :: (a -> NondetJoinT m b) -> a -> m (𝒫ᵇ b)

isoToFlowJoinTMorph :: ((a, s) -> m (b ⇰♭⊔ s)) -> a -> FlowJoinT s m b

isoFromFlowJoinTMorph :: (a -> FlowJoinT s m b) -> (a, s) -> m (b ⇰♭⊔ s)

newtype StateΠ s ς a

Constructors

StateΠ

Fields

runStateΠ :: ς (a, s)

Instances

(Functorial * JoinLattice ς, JoinLattice s) => Functorial * JoinLattice (StateΠ s ς)

(OrdFunctorial POrd ς, POrd s, Ord s) => OrdFunctorial POrd (StateΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (StateΠ s ς)

Functor ς => Functor (StateΠ s ς)

GaloisTransformer ς m => GaloisTransformer (StateΠ s ς) (StateT s m)

(Functorial * JoinLattice ς, JoinLattice s, JoinLattice a) => JoinLattice (StateΠ s ς a)

Difference (ς (a, s)) => Difference (StateΠ s ς a)

(Functorial * JoinLattice ς, JoinLattice s, JoinLattice a) => Join (StateΠ s ς a)

(Functorial * JoinLattice ς, JoinLattice s, JoinLattice a) => Bot (StateΠ s ς a)

(OrdFunctorial POrd ς, POrd s, POrd a, Ord s, Ord a) => POrd (StateΠ s ς a)

Pretty (ς0 (a0, s0)) => Pretty (StateΠ s ς a)

isoToStateΠMorph :: (ς (a, s) -> ς (b, s)) -> StateΠ s ς a -> StateΠ s ς b

isoFromStateΠMorph :: (StateΠ s ς a -> StateΠ s ς b) -> ς (a, s) -> ς (b, s)

newtype PolyStateΠ s ς a

Constructors

PolyStateΠ

Fields

runPolyStateΠ :: ς (a, s)

Instances

Polymorphic * * JoinLattice ς => Polymorphic * * JoinLattice (PolyStateΠ s ς)

(OrdPolymorphic * POrd ς, Ord s) => OrdPolymorphic * POrd (PolyStateΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (PolyStateΠ s ς)

Functor ς => Functor (PolyStateΠ s ς)

GaloisTransformer ς m => GaloisTransformer (PolyStateΠ s ς) (PolyStateT s m)

Polymorphic * * JoinLattice ς => JoinLattice (PolyStateΠ s ς a)

Difference (ς (a, s)) => Difference (PolyStateΠ s ς a)

Polymorphic * * JoinLattice ς => Join (PolyStateΠ s ς a)

Polymorphic * * JoinLattice ς => Bot (PolyStateΠ s ς a)

(OrdPolymorphic * POrd ς, Ord s, Ord a) => POrd (PolyStateΠ s ς a)

Pretty (ς0 (a0, s0)) => Pretty (PolyStateΠ s ς a)

isoPolyStateΠ :: PolyStateΠ s ς a ⇄ ς (a, s)

isoToPolyStateΠMorph :: (ς (a, s) -> ς (b, s)) -> PolyStateΠ s ς a -> PolyStateΠ s ς b

isoFromPolyStateΠMorph :: (PolyStateΠ s ς a -> PolyStateΠ s ς b) -> ς (a, s) -> ς (b, s)

newtype NondetJoinΠ ς a

Constructors

NondetJoinΠ

Fields

runNondetJoinΠ :: ς (𝒫ᵇ a)

Instances

Functorial * JoinLattice ς => Polymorphic * * JoinLattice (NondetJoinΠ ς)

OrdFunctorial POrd ς => OrdPolymorphic * POrd (NondetJoinΠ ς)

(Inject * ι ς, Functor ς) => Inject * ι (NondetJoinΠ ς)

(GaloisTransformer ς m, Functorial * JoinLattice m) => GaloisTransformer (NondetJoinΠ ς) (NondetJoinT m)

Functorial * JoinLattice ς => JoinLattice (NondetJoinΠ ς a)

Difference (ς (𝒫ᵇ a)) => Difference (NondetJoinΠ ς a)

Functorial * JoinLattice ς => Join (NondetJoinΠ ς a)

Functorial * JoinLattice ς => Bot (NondetJoinΠ ς a)

(OrdFunctorial POrd ς, Ord a) => POrd (NondetJoinΠ ς a)

Pretty (ς0 (𝒫ᵇ a0)) => Pretty (NondetJoinΠ ς a)

isoNondetJoinΠ :: NondetJoinΠ ς a ⇄ ς (𝒫ᵇ a)

isoToNondetJoinΠMorph :: (ς (𝒫ᵇ a) -> ς (𝒫ᵇ b)) -> NondetJoinΠ ς a -> NondetJoinΠ ς b

isoFromNondetJoinΠMorph :: (NondetJoinΠ ς a -> NondetJoinΠ ς b) -> ς (𝒫ᵇ a) -> ς (𝒫ᵇ b)

newtype FlowJoinΠ s ς a

Constructors

FlowJoinΠ

Fields

runFlowJoinΠ :: ς (a ⇰♭⊔ s)

Instances

Functorial * JoinLattice ς => Polymorphic * * JoinLattice (FlowJoinΠ s ς)

(OrdFunctorial POrd ς, POrd s, JoinLattice s, Ord s) => OrdPolymorphic * POrd (FlowJoinΠ s ς)

(Inject * ι ς, Functor ς) => Inject * (StateI s ι) (FlowJoinΠ s ς)

(GaloisTransformer ς m, Functorial * JoinLattice m, JoinLattice s) => GaloisTransformer (FlowJoinΠ s ς) (FlowJoinT s m)

Functorial * JoinLattice ς => JoinLattice (FlowJoinΠ s ς a)

Difference (ς ((⇰♭⊔) a s)) => Difference (FlowJoinΠ s ς a)

Functorial * JoinLattice ς => Join (FlowJoinΠ s ς a)

Functorial * JoinLattice ς => Bot (FlowJoinΠ s ς a)

(OrdFunctorial POrd ς, POrd s, JoinLattice s, Ord s, Ord a) => POrd (FlowJoinΠ s ς a)

Pretty (ς0 ((⇰♭⊔) a0 s0)) => Pretty (FlowJoinΠ s ς a)

isoToFlowJoinΠMorph :: (ς (a ⇰♭⊔ s) -> ς (b ⇰♭⊔ s)) -> FlowJoinΠ s ς a -> FlowJoinΠ s ς b

isoFromFlowJoinΠMorph :: (FlowJoinΠ s ς a -> FlowJoinΠ s ς b) -> ς (a ⇰♭⊔ s) -> ς (b ⇰♭⊔ s)

newtype StateI s ι a

Constructors

StateI

Fields

runStateI :: ι (a, s)

Instances

(Inject * ι ς, Functor ς) => Inject * (StateI s ι) (FlowJoinΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (PolyStateΠ s ς)

Inject * ι ς => Inject * (StateI s ι) (StateΠ s ς)

isoStateI :: StateI s ι a ⇄ ι (a, s)

type NondetJoinI ι = ι

type FlowJoinI = StateI

isoαGT :: GaloisTransformer ς₁ m₁ => (ς₂ ↝⇄ ς₁) -> (m₂ ↝⇄ m₁) -> forall a b. (ς₂ a -> ς₂ b) -> a -> m₂ b

isoγGT :: GaloisTransformer ς₁ m₁ => (ς₂ ↝⇄ ς₁) -> (m₂ ↝⇄ m₁) -> forall a b. (a -> m₂ b) -> ς₂ a -> ς₂ b

isoInject :: Inject ι₁ ς₁ => (ι₂ ↝⇄ ι₁) -> (ς₂ ↝⇄ ς₁) -> forall a. ι₂ a -> ς₂ a