define composition of state machines

This commit is contained in:
Marco Perone 2023-01-10 16:42:13 +01:00
parent 088077963a
commit 75fd22d4c9
5 changed files with 70 additions and 19 deletions

20
spec/CRM/GraphSpec.hs Normal file
View File

@ -0,0 +1,20 @@
module CRM.GraphSpec where
import "crm" CRM.Graph
import "hspec" Test.Hspec (Spec, describe, it, shouldBe)
spec :: Spec
spec =
describe "Graph" $ do
describe "productGraph" $ do
it "computes correctly the product of two graphs" $
do
productGraph
(Graph [(1 :: Int, 1), (1, 2)])
(Graph [('a', 'b'), ('c', 'd')])
`shouldBe` Graph
[ ((1, 'a'), (1, 'b'))
, ((1, 'c'), (1, 'd'))
, ((1, 'a'), (2, 'b'))
, ((1, 'c'), (2, 'd'))
]

View File

@ -3,6 +3,7 @@ module CRM.RenderSpec where
import CRM.Example.LockDoor
import CRM.Example.OneState
import CRM.Example.Switch
import "crm" CRM.Graph
import "crm" CRM.Render
import "crm" CRM.StateMachine
import "text" Data.Text as Text (unlines)

34
src/CRM/Graph.hs Normal file
View File

@ -0,0 +1,34 @@
module CRM.Graph where
-- * Graph
-- | A graph is just a list of edges between vertices of type `a`
newtype Graph a = Graph [(a, a)]
deriving stock (Eq, Show)
{- | The product graph.
It has as vertices the product of the set of vertices of the initial graph.
It has as edge from `(a1, b1)` to `(a2, b2)` if and only if there is an edge
from `a1` to `a2` and an edge from `b1` to `b2`
-}
productGraph :: Graph a -> Graph b -> Graph (a, b)
productGraph (Graph edges1) (Graph edges2) =
Graph $
( \((initialEdge1, finalEdge1), (initialEdge2, finalEdge2)) ->
((initialEdge1, initialEdge2), (finalEdge1, finalEdge2))
)
<$> [(edge1, edge2) | edge1 <- edges1, edge2 <- edges2]
-- * UntypedGraph
-- A data type to represent a graph which is not tracking the vertex type
data UntypedGraph = forall a. (Show a) => UntypedGraph (Graph a)
instance Show UntypedGraph where
show :: UntypedGraph -> String
show (UntypedGraph graph) = show graph
-- same as `productGraph` but for `UntypedGraph`
untypedProductGraph :: UntypedGraph -> UntypedGraph -> UntypedGraph
untypedProductGraph (UntypedGraph graph1) (UntypedGraph graph2) =
UntypedGraph (productGraph graph1 graph2)

View File

@ -5,17 +5,12 @@
module CRM.Render where
import CRM.BaseMachine
import CRM.Graph
import CRM.StateMachine
import CRM.Topology
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) =
@ -39,13 +34,6 @@ baseMachineAsGraph
-> Graph vertex
baseMachineAsGraph _ = topologyAsGraph (demote @topology)
-- A data type to represent a graph which is not tracking the vertex type
data UntypedGraph = forall a. (Show a) => UntypedGraph (Graph a)
instance Show UntypedGraph where
show :: UntypedGraph -> String
show (UntypedGraph graph) = show graph
-- Render an `UntypedGraph` to the Mermaid format
renderUntypedMermaid :: UntypedGraph -> Text
renderUntypedMermaid (UntypedGraph graph) = renderMermaid graph
@ -56,3 +44,7 @@ renderUntypedMermaid (UntypedGraph graph) = renderMermaid graph
machineAsGraph :: StateMachine input output -> UntypedGraph
machineAsGraph (Basic baseMachine) =
UntypedGraph (baseMachineAsGraph baseMachine)
machineAsGraph (Compose machine1 machine2) =
untypedProductGraph
(machineAsGraph machine1)
(machineAsGraph machine2)

View File

@ -18,17 +18,21 @@ data StateMachine input output where
. (Demote (Topology vertex) ~ Topology vertex, SingKind vertex, SingI topology, Show vertex)
=> BaseMachine topology input output
-> StateMachine input output
Compose
:: StateMachine a b
-> StateMachine b c
-> StateMachine a c
-- * SemiCategory
-- infixr 1 >>>
-- infixr 1 <<<
infixr 1 >>>
infixr 1 <<<
-- (>>>) :: StateMachine a b -> StateMachine b c -> StateMachine a c
-- (>>>) = _
(>>>) :: StateMachine a b -> StateMachine b c -> StateMachine a c
(>>>) = Compose
-- (<<<) :: StateMachine b c -> StateMachine a b -> StateMachine a c
-- (<<<) = flip (>>>)
(<<<) :: StateMachine b c -> StateMachine a b -> StateMachine a c
(<<<) = flip (>>>)
-- * Profunctor