mirror of
https://github.com/marcosh/crem.git
synced 2024-09-11 12:36:19 +03:00
Render a base state machine
Add tests Remove Mk from constructors
This commit is contained in:
parent
24c4870359
commit
739f466589
@ -9,6 +9,8 @@ language: GHC2021 # https://downloads.haskell.org/ghc/latest/docs/users_guide/ex
|
||||
|
||||
default-extensions:
|
||||
- DerivingStrategies # https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/deriving_strategies.html#extension-DerivingStrategies
|
||||
- LambdaCase # https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/lambda_case.html#extension-LambdaCase
|
||||
- OverloadedStrings # https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/overloaded_strings.html#extension-OverloadedStrings
|
||||
- PackageImports # https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/package_qualified_imports.html#extension-PackageImports
|
||||
|
||||
# Options inspired by: https://medium.com/mercury-bank/enable-all-the-warnings-a0517bc081c3
|
||||
@ -26,10 +28,10 @@ ghc-options:
|
||||
- -Wno-implicit-prelude # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wimplicit-prelude
|
||||
- -Wno-missing-kind-signatures # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wmissing-kind-signatures
|
||||
- -Wno-missing-export-lists # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wmissing-export-lists
|
||||
- -Wno-missing-home-modules # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wmissing-home-modules
|
||||
- -Wno-missing-import-lists # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wmissing-import-lists
|
||||
# - -Wno-unused-type-patterns
|
||||
# - -Wno-missed-specialisations
|
||||
# - -Wno-all-missed-specialisations
|
||||
- -Wno-all-missed-specialisations # https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wall-missed-specialisations
|
||||
# - -Wno-orphans
|
||||
# TODO: do we still need these?
|
||||
# - -fwrite-ide-info
|
||||
@ -38,6 +40,7 @@ ghc-options:
|
||||
dependencies:
|
||||
- base
|
||||
- singletons-base
|
||||
- text
|
||||
|
||||
library:
|
||||
source-dirs: src
|
||||
|
@ -2,6 +2,10 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wall-missed-specialisations
|
||||
{-# OPTIONS_GHC -Wno-all-missed-specialisations #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wmissing-deriving-strategies
|
||||
{-# OPTIONS_GHC -Wno-missing-deriving-strategies #-}
|
||||
|
||||
module CRM.Example.LockDoor where
|
||||
|
||||
@ -18,7 +22,7 @@ $( singletons
|
||||
|
||||
lockDoorTopology :: Topology LockDoorVertex
|
||||
lockDoorTopology =
|
||||
MkTopology
|
||||
Topology
|
||||
[ (IsLockOpen, [IsLockOpen, IsLockClosed])
|
||||
, (IsLockClosed, [IsLockClosed, IsLockOpen, IsLockLocked])
|
||||
, (IsLockLocked, [IsLockLocked, IsLockClosed])
|
||||
@ -39,24 +43,24 @@ data LockDoorEvent
|
||||
| LockLocked
|
||||
| LockUnlocked
|
||||
|
||||
lockDoorMachine :: StateMachine LockDoorTopology LockDoorCommand LockDoorEvent
|
||||
lockDoorMachine :: BaseMachine LockDoorTopology LockDoorCommand LockDoorEvent
|
||||
lockDoorMachine =
|
||||
MkStateMachine
|
||||
{ initialState = MkInitialState SIsLockClosed
|
||||
BaseMachine
|
||||
{ initialState = InitialState SIsLockClosed
|
||||
, action = \case
|
||||
SIsLockOpen -> \case
|
||||
LockOpen -> MkActionResult SIsLockOpen LockNoOp
|
||||
LockClose -> MkActionResult SIsLockClosed LockClosed
|
||||
LockLock -> MkActionResult SIsLockOpen LockNoOp
|
||||
LockUnlock -> MkActionResult SIsLockOpen LockNoOp
|
||||
LockOpen -> ActionResult SIsLockOpen LockNoOp
|
||||
LockClose -> ActionResult SIsLockClosed LockClosed
|
||||
LockLock -> ActionResult SIsLockOpen LockNoOp
|
||||
LockUnlock -> ActionResult SIsLockOpen LockNoOp
|
||||
SIsLockClosed -> \case
|
||||
LockOpen -> MkActionResult SIsLockOpen LockOpened
|
||||
LockClose -> MkActionResult SIsLockClosed LockNoOp
|
||||
LockLock -> MkActionResult SIsLockLocked LockLocked
|
||||
LockUnlock -> MkActionResult SIsLockClosed LockNoOp
|
||||
LockOpen -> ActionResult SIsLockOpen LockOpened
|
||||
LockClose -> ActionResult SIsLockClosed LockNoOp
|
||||
LockLock -> ActionResult SIsLockLocked LockLocked
|
||||
LockUnlock -> ActionResult SIsLockClosed LockNoOp
|
||||
SIsLockLocked -> \case
|
||||
LockOpen -> MkActionResult SIsLockLocked LockNoOp
|
||||
LockClose -> MkActionResult SIsLockLocked LockNoOp
|
||||
LockLock -> MkActionResult SIsLockLocked LockNoOp
|
||||
LockUnlock -> MkActionResult SIsLockClosed LockUnlocked
|
||||
}
|
||||
LockOpen -> ActionResult SIsLockLocked LockNoOp
|
||||
LockClose -> ActionResult SIsLockLocked LockNoOp
|
||||
LockLock -> ActionResult SIsLockLocked LockNoOp
|
||||
LockUnlock -> ActionResult SIsLockClosed LockUnlocked
|
||||
}
|
||||
|
@ -12,13 +12,13 @@ $( singletons
|
||||
[d|
|
||||
-- topology with a single vertex and one edge from the vertex to itself
|
||||
singleVertexTopology :: Topology ()
|
||||
singleVertexTopology = MkTopology [((), [()])]
|
||||
singleVertexTopology = Topology [((), [()])]
|
||||
|]
|
||||
)
|
||||
|
||||
oneVertexMachine :: StateMachine SingleVertexTopology () ()
|
||||
oneVertexMachine :: BaseMachine SingleVertexTopology () ()
|
||||
oneVertexMachine =
|
||||
MkStateMachine
|
||||
{ initialState = MkInitialState STuple0
|
||||
, action = \STuple0 _ -> MkActionResult STuple0 ()
|
||||
BaseMachine
|
||||
{ initialState = InitialState STuple0
|
||||
, action = \STuple0 _ -> ActionResult STuple0 ()
|
||||
}
|
||||
|
@ -2,6 +2,8 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
-- https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wall-missed-specialisations
|
||||
{-# OPTIONS_GHC -Wno-all-missed-specialisations #-}
|
||||
|
||||
module CRM.Example.Switch where
|
||||
|
||||
@ -14,18 +16,20 @@ $( singletons
|
||||
-- other
|
||||
switchTopology :: Topology Bool
|
||||
switchTopology =
|
||||
MkTopology
|
||||
Topology
|
||||
[ (True, [False])
|
||||
, (False, [True])
|
||||
]
|
||||
|]
|
||||
)
|
||||
|
||||
switchMachine :: StateMachine SwitchTopology () ()
|
||||
switchMachine :: BaseMachine SwitchTopology () ()
|
||||
switchMachine =
|
||||
MkStateMachine
|
||||
{ initialState = MkInitialState SFalse
|
||||
BaseMachine
|
||||
{ initialState = InitialState SFalse
|
||||
, action = \case
|
||||
SFalse () -> MkActionResult STrue ()
|
||||
STrue () -> MkActionResult SFalse ()
|
||||
SFalse -> \case
|
||||
() -> ActionResult STrue ()
|
||||
STrue -> \case
|
||||
() -> ActionResult SFalse ()
|
||||
}
|
||||
|
75
spec/CRM/RenderSpec.hs
Normal file
75
spec/CRM/RenderSpec.hs
Normal file
@ -0,0 +1,75 @@
|
||||
module CRM.RenderSpec where
|
||||
|
||||
import CRM.Example.LockDoor
|
||||
import CRM.Example.OneState
|
||||
import CRM.Example.Switch
|
||||
import "crm" CRM.Render
|
||||
import "text" Data.Text as Text (unlines)
|
||||
import "hspec" Test.Hspec (Spec, describe, it, shouldBe)
|
||||
|
||||
spec :: Spec
|
||||
spec =
|
||||
describe "Render" $ do
|
||||
describe "renderMermaid" $ do
|
||||
it "should render correctly a graph" $ do
|
||||
renderMermaid (Graph [(1 :: Int, 1), (1, 2), (1, 3), (2, 3), (3, 1)])
|
||||
`shouldBe` Text.unlines
|
||||
[ "stateDiagram-v2"
|
||||
, "1 --> 1"
|
||||
, "1 --> 2"
|
||||
, "1 --> 3"
|
||||
, "2 --> 3"
|
||||
, "3 --> 1"
|
||||
]
|
||||
|
||||
describe "topologyAsGraph" $ do
|
||||
it "should render the topology with a single vertex" $ do
|
||||
topologyAsGraph singleVertexTopology
|
||||
`shouldBe` Graph
|
||||
[ ((), ())
|
||||
]
|
||||
|
||||
it "should render the switch topology" $ do
|
||||
topologyAsGraph switchTopology
|
||||
`shouldBe` Graph
|
||||
[ (True, False)
|
||||
, (False, True)
|
||||
]
|
||||
|
||||
it "should render the lockDoor topology" $ do
|
||||
topologyAsGraph lockDoorTopology
|
||||
`shouldBe` Graph
|
||||
[ (IsLockOpen, IsLockOpen)
|
||||
, (IsLockOpen, IsLockClosed)
|
||||
, (IsLockClosed, IsLockClosed)
|
||||
, (IsLockClosed, IsLockOpen)
|
||||
, (IsLockClosed, IsLockLocked)
|
||||
, (IsLockLocked, IsLockLocked)
|
||||
, (IsLockLocked, IsLockClosed)
|
||||
]
|
||||
|
||||
describe "baseMachineAsGraph" $ do
|
||||
it "should render the machine with a single vertex" $ do
|
||||
baseMachineAsGraph oneVertexMachine
|
||||
`shouldBe` Graph
|
||||
[ ((), ())
|
||||
]
|
||||
|
||||
it "should render the switch machine" $ do
|
||||
baseMachineAsGraph switchMachine
|
||||
`shouldBe` Graph
|
||||
[ (True, False)
|
||||
, (False, True)
|
||||
]
|
||||
|
||||
it "should render the lockDoor machine" $ do
|
||||
baseMachineAsGraph lockDoorMachine
|
||||
`shouldBe` Graph
|
||||
[ (IsLockOpen, IsLockOpen)
|
||||
, (IsLockOpen, IsLockClosed)
|
||||
, (IsLockClosed, IsLockClosed)
|
||||
, (IsLockClosed, IsLockOpen)
|
||||
, (IsLockClosed, IsLockLocked)
|
||||
, (IsLockLocked, IsLockLocked)
|
||||
, (IsLockLocked, IsLockClosed)
|
||||
]
|
@ -1 +1,2 @@
|
||||
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
|
||||
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
|
||||
{-# OPTIONS_GHC -Wno-prepositive-qualified-module #-}
|
||||
|
@ -19,7 +19,7 @@ import "singletons-base" Data.Singletons.Base.TH (singletons)
|
||||
-}
|
||||
$( singletons
|
||||
[d|
|
||||
newtype Topology (vertex :: Type) = MkTopology {edges :: [(vertex, [vertex])]}
|
||||
newtype Topology (vertex :: Type) = Topology {edges :: [(vertex, [vertex])]}
|
||||
|]
|
||||
)
|
||||
|
||||
@ -34,32 +34,32 @@ class AllowedTransition (topology :: Topology vertex) (initial :: vertex) (final
|
||||
{- | 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 ('MkTopology ('(a, b : l1) : l2)) a 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 ('MkTopology ('(a, l1) : l2)) a b => AllowedTransition ('MkTopology ('(a, x : l1) : l2)) a b
|
||||
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 ('MkTopology map) a b => AllowedTransition ('MkTopology (x : map)) a b
|
||||
instance AllowedTransition ('Topology map) a b => AllowedTransition ('Topology (x : map)) a b
|
||||
|
||||
-- * Specifying state machines
|
||||
|
||||
{- | A `StateMachine topology input output` describes a state machine with
|
||||
{- | A `BaseMachine topology input output` describes a state machine with
|
||||
allowed transitions constrained by a given `topology`.
|
||||
A state machine is composed by an `initialState` and an `action`, which
|
||||
defines the `output` and the new `state` given the current `state` and an
|
||||
`input`
|
||||
-}
|
||||
data
|
||||
StateMachine
|
||||
BaseMachine
|
||||
(topology :: Topology vertex)
|
||||
(input :: Type)
|
||||
(output :: Type) = forall state.
|
||||
MkStateMachine
|
||||
BaseMachine
|
||||
{ initialState :: InitialState state
|
||||
, action
|
||||
:: forall initialVertex
|
||||
@ -73,7 +73,7 @@ data
|
||||
actual initial data of type `state vertex`
|
||||
-}
|
||||
data InitialState (state :: vertex -> Type) where
|
||||
MkInitialState :: state vertex -> InitialState state
|
||||
InitialState :: state vertex -> InitialState state
|
||||
|
||||
{- | The result of an action of the state machine.
|
||||
An `ActionResult topology state initialVertex output` contains an `output` and a `state finalVertex`,
|
||||
@ -86,7 +86,7 @@ data
|
||||
(initialVertex :: vertex)
|
||||
(output :: Type)
|
||||
where
|
||||
MkActionResult
|
||||
ActionResult
|
||||
:: AllowedTransition topology initialVertex finalVertex
|
||||
=> state finalVertex
|
||||
-> output
|
||||
|
37
src/CRM/Render.hs
Normal file
37
src/CRM/Render.hs
Normal file
@ -0,0 +1,37 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
|
||||
module CRM.Render where
|
||||
|
||||
import CRM.BaseMachine
|
||||
import "singletons-base" Data.Singletons (Demote, SingI, SingKind, demote)
|
||||
import "text" Data.Text (Text, pack)
|
||||
|
||||
-- * Graph
|
||||
|
||||
-- | A graph is just a list of edges between vertices of type `a`
|
||||
newtype Graph a = Graph [(a, a)]
|
||||
deriving stock (Eq, Show)
|
||||
|
||||
-- | We can render a `Graph a` as [mermaid](https://mermaid.js.org/) state diagram
|
||||
renderMermaid :: Show a => Graph a -> Text
|
||||
renderMermaid (Graph l) =
|
||||
"stateDiagram-v2\n"
|
||||
<> foldMap (\(a1, a2) -> pack (show a1) <> " --> " <> pack (show a2) <> "\n") l
|
||||
|
||||
-- | Turn a `Topology` into a `Graph`
|
||||
topologyAsGraph :: Topology v -> Graph v
|
||||
topologyAsGraph (Topology edges) = Graph $ edges >>= edgify
|
||||
where
|
||||
edgify :: (v, [v]) -> [(v, v)]
|
||||
edgify (v, vs) = (v,) <$> vs
|
||||
|
||||
{- | Interpret a `BaseMachine` as a `Graph` using the information contained in
|
||||
its topology
|
||||
-}
|
||||
baseMachineAsGraph
|
||||
:: forall tag topology input output
|
||||
. (Demote (Topology tag) ~ Topology tag, SingKind tag, SingI topology)
|
||||
=> BaseMachine (topology :: Topology tag) input output
|
||||
-> Graph tag
|
||||
baseMachineAsGraph _ = topologyAsGraph (demote @topology)
|
Loading…
Reference in New Issue
Block a user