mirror of
https://github.com/marcosh/crem.git
synced 2024-10-26 11:52:20 +03:00
Factor Topology out of BaseMachine
This commit is contained in:
parent
739f466589
commit
07c22a94f4
@ -10,6 +10,7 @@
|
||||
module CRM.Example.LockDoor where
|
||||
|
||||
import "crm" CRM.BaseMachine
|
||||
import "crm" CRM.Topology
|
||||
import "singletons-base" Data.Singletons.Base.TH
|
||||
|
||||
$( singletons
|
||||
|
@ -6,6 +6,7 @@
|
||||
module CRM.Example.OneState where
|
||||
|
||||
import "crm" CRM.BaseMachine
|
||||
import "crm" CRM.Topology
|
||||
import "singletons-base" Data.Singletons.Base.TH
|
||||
|
||||
$( singletons
|
||||
|
@ -8,6 +8,7 @@
|
||||
module CRM.Example.Switch where
|
||||
|
||||
import "crm" CRM.BaseMachine
|
||||
import "crm" CRM.Topology
|
||||
import "singletons-base" Data.Singletons.Base.TH
|
||||
|
||||
$( singletons
|
||||
|
@ -1,50 +1,9 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wredundant-constraints
|
||||
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wunused-type-patterns
|
||||
{-# OPTIONS_GHC -Wno-unused-type-patterns #-}
|
||||
|
||||
module CRM.BaseMachine where
|
||||
|
||||
import CRM.Topology
|
||||
import "base" Data.Kind (Type)
|
||||
import "singletons-base" Data.Singletons.Base.TH (singletons)
|
||||
|
||||
-- * Topology
|
||||
|
||||
{- | A `Topology` is a description of the topology of a state machine
|
||||
It contains the collection of allowed transitions
|
||||
-}
|
||||
$( singletons
|
||||
[d|
|
||||
newtype Topology (vertex :: Type) = Topology {edges :: [(vertex, [vertex])]}
|
||||
|]
|
||||
)
|
||||
|
||||
-- ** AllowedTransition
|
||||
|
||||
{- | We expose at the type level the information contained in the topology
|
||||
An instance of `AllowedTransition topology initial final` means that the
|
||||
`topology` allows transitions from the`initial` to the `final` state
|
||||
-}
|
||||
class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex)
|
||||
|
||||
{- | If `a` is the start and `b` is the end of the first edge,
|
||||
then `map` contains an edge from `a` to `b`
|
||||
-}
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, b : l1) : l2)) 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 edge out of `a`
|
||||
-}
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, l1) : l2)) a b => AllowedTransition ('Topology ('(a, x : l1) : l2)) 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
|
||||
-}
|
||||
instance AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x : map)) a b
|
||||
|
||||
-- * Specifying state machines
|
||||
|
||||
|
@ -4,6 +4,7 @@
|
||||
module CRM.Render where
|
||||
|
||||
import CRM.BaseMachine
|
||||
import CRM.Topology
|
||||
import "singletons-base" Data.Singletons (Demote, SingI, SingKind, demote)
|
||||
import "text" Data.Text (Text, pack)
|
||||
|
||||
|
46
src/CRM/Topology.hs
Normal file
46
src/CRM/Topology.hs
Normal file
@ -0,0 +1,46 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wredundant-constraints
|
||||
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wunused-type-patterns
|
||||
{-# OPTIONS_GHC -Wno-unused-type-patterns #-}
|
||||
|
||||
module CRM.Topology where
|
||||
|
||||
import "singletons-base" Data.Singletons.Base.TH (singletons)
|
||||
|
||||
-- * Topology
|
||||
|
||||
{- | A `Topology` is a description of the topology of a state machine
|
||||
It contains the collection of allowed transitions
|
||||
-}
|
||||
$( singletons
|
||||
[d|
|
||||
newtype Topology vertex = Topology {edges :: [(vertex, [vertex])]}
|
||||
|]
|
||||
)
|
||||
|
||||
-- ** AllowedTransition
|
||||
|
||||
{- | We expose at the type level the information contained in the topology
|
||||
An instance of `AllowedTransition topology initial final` means that the
|
||||
`topology` allows transitions from the`initial` to the `final` state
|
||||
-}
|
||||
class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final :: vertex)
|
||||
|
||||
{- | If `a` is the start and `b` is the end of the first edge,
|
||||
then `map` contains an edge from `a` to `b`
|
||||
-}
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, b : l1) : l2)) 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 edge out of `a`
|
||||
-}
|
||||
instance {-# OVERLAPPING #-} AllowedTransition ('Topology ('(a, l1) : l2)) a b => AllowedTransition ('Topology ('(a, x : l1) : l2)) 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
|
||||
-}
|
||||
instance AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x : map)) a b
|
Loading…
Reference in New Issue
Block a user