Crem.Topology

A Topology is a list of allowed transition for a state machine. We are using it to enforce that only allowed transitions could be performed.

Documentation

newtype Topology vertex

A Topology is a description of the topology of a state machine It contains the collection of allowed transitions. Since we are using this information at the type level, and then we want to bring it down to the value level, we wrap it in singletons

Constructors

Topology

Fields

• edges :: [(vertex, [vertex])]

Instances

SingKind vertex => SingKind (Topology vertex)

Defined in Crem.Topology

Associated Types

type Demote (Topology vertex) = (r :: Type)

Methods

fromSing :: forall (a :: Topology vertex). Sing a -> Demote (Topology vertex)

toSing :: Demote (Topology vertex) -> SomeSing (Topology vertex)

SingI1 ('Topology :: [(vertex, [vertex])] -> Topology vertex)

Defined in Crem.Topology

Methods

liftSing :: forall (x :: k1). Sing x -> Sing ('Topology x)

SingI n => SingI ('Topology n :: Topology vertex)

Defined in Crem.Topology

Methods

sing :: Sing ('Topology n)

SingI (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type)

Defined in Crem.Topology

Methods

sing :: Sing TopologySym0

SuppressUnusedWarnings (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type)

Defined in Crem.Topology

Methods

suppressUnusedWarnings :: ()

type Demote (Topology vertex)

Defined in Crem.Topology

type Demote (Topology vertex) = Topology (Demote vertex)

type Sing

Defined in Crem.Topology

type Sing = STopology :: Topology vertex -> Type

type Apply (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type) (a6989586621679067816 :: [(vertex, [vertex])])

Defined in Crem.Topology

type Apply (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type) (a6989586621679067816 :: [(vertex, [vertex])]) = 'Topology a6989586621679067816

data TopologySym0 :: (~>) [(vertex, [vertex])] (Topology vertex)

Instances

SingI (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type)

Defined in Crem.Topology

Methods

sing :: Sing TopologySym0

SuppressUnusedWarnings (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type)

Defined in Crem.Topology

Methods

suppressUnusedWarnings :: ()

type Apply (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type) (a6989586621679067816 :: [(vertex, [vertex])])

Defined in Crem.Topology

type Apply (TopologySym0 :: TyFun [(vertex, [vertex])] (Topology vertex) -> Type) (a6989586621679067816 :: [(vertex, [vertex])]) = 'Topology a6989586621679067816

data STopology :: forall vertex. Topology vertex -> Type where

Constructors

STopology :: forall vertex (n :: [(vertex, [vertex])]). (Sing n) -> STopology (Topology n :: Topology vertex)

data AllowTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex) where

An value of type of AllowedTransition topology initial final is a proof that the topology allows transitions from the initial to the final state

Constructors

AllowIdentityEdge :: AllowTransition topology a a

We always allow an edge from a vertex to itself

AllowFirstEdge :: AllowTransition ('Topology ('(a, b ': l1) ': l2)) a b

If a is the start and b is the end of the first edge, then map contains an edge from a to b

AllowAddingEdge :: AllowTransition ('Topology ('(a, l1) ': l2)) a b -> AllowTransition ('Topology ('(a, x ': l1) ': l2)) a b

If we know that we have an edge from a to b in a topology, then we also have an edge from a to b if we add another edge out of a

AllowAddingVertex :: AllowTransition ('Topology map) a b -> AllowTransition ('Topology (x ': map)) a b

If we know that we have an edge from a to b in map, then we also have an edge from a to b if we add another vertex

class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex) where

The AllowedTransition type class enables to automatically perform proof search for a AllowTransition term. It has an instance for every constructor of AllowTransition

Methods

allowsTransition :: AllowTransition topology initial final

Instances

AllowedTransition (topology :: Topology vertex) (a :: vertex) (a :: vertex)

Defined in Crem.Topology

Methods

allowsTransition :: AllowTransition topology a a

AllowedTransition ('Topology ('(a, b ': l1) ': l2) :: Topology vertex) (a :: vertex) (b :: vertex)

Defined in Crem.Topology

Methods

allowsTransition :: AllowTransition ('Topology ('(a, b ': l1) ': l2)) a b

AllowedTransition ('Topology ('(a, l1) ': l2)) a b => AllowedTransition ('Topology ('(a, x ': l1) ': l2) :: Topology vertex) (a :: vertex) (b :: vertex)

Defined in Crem.Topology

Methods

allowsTransition :: AllowTransition ('Topology ('(a, x ': l1) ': l2)) a b

AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x ': map) :: Topology vertex) (a :: vertex) (b :: vertex)

Defined in Crem.Topology

Methods

allowsTransition :: AllowTransition ('Topology (x ': map)) a b

trivialTopology :: Topology a

sTrivialTopology :: Sing (TrivialTopologySym0 :: Topology a) :: Type

type family TrivialTopology :: Topology a where ...

The trivial topology only allows identity transitions. Given a type a for vertices, only trivial transitions, i.e. staying at the same vertex, are allowed

Equations

TrivialTopology = Apply TopologySym0 NilSym0

allowAllTopology :: (Bounded a, Enum a) => Topology a

sAllowAllTopology :: (SBounded a, SEnum a) => Sing (AllowAllTopologySym0 :: Topology a) :: Type

type family AllowAllTopology :: Topology a where ...

Equations

AllowAllTopology = Apply TopologySym0 (Apply (Apply (>>=@#@$) (Apply (Apply EnumFromToSym0 MinBoundSym0) MaxBoundSym0)) Lambda_6989586621679106594Sym0)