From 2273f57386c6ffbb7911ad606ec03f7870584352 Mon Sep 17 00:00:00 2001
From: Marco Perone <marco.perone@tweag.io>
Date: Wed, 18 Jan 2023 12:42:04 +0100
Subject: [PATCH] implement unrestrictedMachine

add example of an unrestricted machine with boolean state
---
 spec/CRM/Example/BooleanStateMachine.hs | 25 +++++++++++++++++++++++++
 spec/CRM/StateMachineSpec.hs            | 15 ++++++++++++++-
 src/CRM/BaseMachine.hs                  | 13 +++++++++++++
 src/CRM/StateMachine.hs                 | 15 +++++++++++++++
 src/CRM/Topology.hs                     | 10 ++++++++++
 5 files changed, 77 insertions(+), 1 deletion(-)
 create mode 100644 spec/CRM/Example/BooleanStateMachine.hs

diff --git a/spec/CRM/Example/BooleanStateMachine.hs b/spec/CRM/Example/BooleanStateMachine.hs
new file mode 100644
index 0000000..e99317d
--- /dev/null
+++ b/spec/CRM/Example/BooleanStateMachine.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+
+module CRM.Example.BooleanStateMachine where
+
+import "crm" CRM.BaseMachine
+import "crm" CRM.StateMachine
+import "singletons-base" Data.Singletons.Base.TH
+
+booleanStateMachine
+  :: forall a
+   . SBool a
+  -> StateMachine Int Int
+booleanStateMachine initialState =
+  unrestrictedMachine @Bool
+    ( \state input -> case state of
+        SFalse ->
+          if even input
+            then ActionResult SFalse (input + 1)
+            else ActionResult STrue (input * 3)
+        STrue ->
+          if even input
+            then ActionResult STrue (input - 1)
+            else ActionResult SFalse (input * 5)
+    )
+    (InitialState initialState)
diff --git a/spec/CRM/StateMachineSpec.hs b/spec/CRM/StateMachineSpec.hs
index cafa10f..f6b2ad8 100644
--- a/spec/CRM/StateMachineSpec.hs
+++ b/spec/CRM/StateMachineSpec.hs
@@ -1,5 +1,6 @@
 module CRM.StateMachineSpec where
 
+import CRM.Example.BooleanStateMachine (booleanStateMachine)
 import CRM.Example.LockDoor
 import CRM.Example.Switch (switchMachine)
 import "crm" CRM.StateMachine
@@ -8,7 +9,6 @@ import "hspec" Test.Hspec (Expectation, Spec, describe, it, shouldBe)
 
 shouldOutput :: (Eq b, Show b) => (b, StateMachine a b) -> b -> Expectation
 shouldOutput (output, _) expectedOutput = output `shouldBe` expectedOutput
-
 spec :: Spec
 spec =
   describe "StateMachine" $ do
@@ -66,3 +66,16 @@ spec =
           let
             runOnce = snd $ run (Basic $ lockDoorMachine SIsLockLocked) LockUnlock
           run runOnce LockOpen `shouldOutput` LockOpened
+
+      describe "boolean state machine" $ do
+        it "outputs 1 when it is in a False state and receives a 0" $ do
+          run (booleanStateMachine SFalse) 0 `shouldOutput` 1
+
+        it "outputs 3 when it is in a False state and receives a 1" $ do
+          run (booleanStateMachine SFalse) 1 `shouldOutput` 3
+
+        it "outputs -1 when it is in a True state and receives a 0" $ do
+          run (booleanStateMachine STrue) 0 `shouldOutput` (-1)
+
+        it "outputs 5 when it is in a True state and receives a 1" $ do
+          run (booleanStateMachine STrue) 1 `shouldOutput` 5
diff --git a/src/CRM/BaseMachine.hs b/src/CRM/BaseMachine.hs
index 6cba0f2..f0ca535 100644
--- a/src/CRM/BaseMachine.hs
+++ b/src/CRM/BaseMachine.hs
@@ -123,6 +123,19 @@ statelessBase f =
 identity :: BaseMachine TrivialTopology a a
 identity = statelessBase id
 
+-- ** Unfold
+
+-- | a machine modelled with explicit state, where every transition is allowed
+unrestrictedBaseMachine
+  :: (forall initialVertex. state initialVertex -> a -> ActionResult (AllowAllTopology @vertex) state initialVertex b)
+  -> InitialState (state :: vertex -> Type)
+  -> BaseMachine (AllowAllTopology @vertex) a b
+unrestrictedBaseMachine action initialState =
+  BaseMachine
+    { initialState = initialState
+    , action = action
+    }
+
 -- ** Run a machine
 
 -- | Given an `input`, run the machine to get an output and a new version of
diff --git a/src/CRM/StateMachine.hs b/src/CRM/StateMachine.hs
index 08515b9..a4c2661 100644
--- a/src/CRM/StateMachine.hs
+++ b/src/CRM/StateMachine.hs
@@ -7,8 +7,10 @@ import CRM.BaseMachine as BaseMachine
 import CRM.Topology
 import "base" Control.Category (Category (..))
 import "base" Data.Bifunctor (bimap)
+import "base" Data.Kind (Type)
 import "profunctors" Data.Profunctor (Choice (..), Profunctor (..), Strong (..))
 import "singletons-base" Data.Singletons (Demote, SingI, SingKind)
+import Prelude hiding ((.))
 
 -- | A `StateMachine` is a [Mealy machine](https://en.wikipedia.org/wiki/Mealy_machine)
 -- with inputs of type `input` and outputs of type `output`
@@ -35,9 +37,22 @@ data StateMachine input output where
     -> StateMachine c d
     -> StateMachine (Either a c) (Either b d)
 
+-- | a state machine which does not rely on state
 stateless :: (a -> b) -> StateMachine a b
 stateless f = Basic $ statelessBase f
 
+-- | a machine modelled with explicit state, where every transition is allowed
+unrestrictedMachine
+  :: (Demote vertex ~ vertex, SingKind vertex, SingI (AllowAllTopology @vertex), Show vertex)
+  => ( forall initialVertex
+        . state initialVertex
+       -> a
+       -> ActionResult (AllowAllTopology @vertex) state initialVertex b
+     )
+  -> InitialState (state :: vertex -> Type)
+  -> StateMachine a b
+unrestrictedMachine action state = Basic $ unrestrictedBaseMachine action state
+
 -- * Category
 
 instance Category StateMachine where
diff --git a/src/CRM/Topology.hs b/src/CRM/Topology.hs
index 475543f..9955210 100644
--- a/src/CRM/Topology.hs
+++ b/src/CRM/Topology.hs
@@ -10,6 +10,7 @@
 module CRM.Topology where
 
 import "singletons-base" Data.Singletons.Base.TH
+import "singletons-base" Prelude.Singletons
 
 -- * Topology
 
@@ -68,3 +69,12 @@ $( singletons
       trivialTopology = Topology []
       |]
  )
+
+-- ** Allow all topology
+
+$( singletons
+    [d|
+      allowAllTopology :: (Bounded a, Enum a) => Topology a
+      allowAllTopology = Topology [(a, [minBound .. maxBound]) | a <- [minBound .. maxBound]]
+      |]
+ )