example of state machine in Idris

vend.idr

%default total

VendState : Type
VendState = (Nat, Nat)

data Input =
  COIN
  | VEND
  | CHANGE
  | REFILL Nat
  | QUIT

data CoinResult = Inserted | Rejected

{-}
MachineCmd is are commands which may be carried out, and the effect they would have on state
Represents a State machine, with multiple possible outputs
You may combine any valid finite sequence of cmds into single cmd
However, you must account for all possible outcomes

Remember that it is *not* a function, it is a composition of data

Would be interesting if CMD was a Functor
Difficult because 3 type arguments (compared to List for example)
{-}

data MachineCmd : (ty: Type) -> VendState -> (ty -> VendState) -> Type where
  InsertCoin : MachineCmd CoinResult (pounds, chocs)
    (\res => case res of
      Inserted => (S pounds, chocs)
      Rejected => (pounds, chocs))
  Vend : MachineCmd () (S pounds, S chocs) (const (pounds, chocs))
  GetCoins : MachineCmd () (pounds, chocs) (const (Z, chocs))
  Refill : (bars : Nat) -> MachineCmd () (Z, chocs) (const (Z, bars + chocs))

  Display : String -> MachineCmd () state (const state)
  GetInput : MachineCmd Input state (const state)
  ShowState : MachineCmd () state (const state)

  {-}Pure is useful for "glue". {-}
  Pure : (res : ty) -> MachineCmd ty (state_fn res) state_fn
  (>>=) : MachineCmd a state1 state2_fn ->
          ((res : a) -> MachineCmd b (state2_fn res) state3_fn) ->
          MachineCmd b state1 state3_fn


{-}
This is an example of a MachineCmd composed of a sequence of valid Cmds

Pure type "MachineCmd ty (state_fn res) state_fn" confused me for a while.
In the example below consider why writing the wrong answer for Pure is illegal
Hint: Pure can change result but not state
{-}

insertN : (n : Nat) ->
          MachineCmd Nat (p, c) (\res => (res + p, c))
insertN Z = Pure 0
insertN (S Z) = do
  res <- InsertCoin
  case res of
    Inserted => Pure 1
    Rejected => Pure 0
insertN (S (S n)) = do
  firstN <- insertN (S n)
  res <- InsertCoin
  case res of
    Inserted => Pure (S firstN)
    Rejected => Pure (firstN)

{-}
MachineLoop is a valid sequence of cmds that may be recursive + infinite
Include Exit to allow graceful stopping
{-}

namespace Loop
  data MachineLoop : (ty : Type) -> VendState -> (ty -> VendState) -> Type where
    (>>=) : MachineCmd a state1 state2_fn ->
         ((res : a) -> Inf (MachineLoop b (state2_fn res) state3_fn)) ->
         MachineLoop b state1 state3_fn
    Exit : MachineLoop () (Z, Z) (const (Z, Z))

{-}
machineLoop is the sequence of cmds that are actually used in the application
{-}

mutual
  machineLoop : MachineLoop () (pounds, chocs) (const (Z, Z))
  machineLoop {pounds} {chocs} = do
    ShowState
    input <- GetInput
    case input of
      VEND => vend
      REFILL num => refill num
      COIN => insertCoin
      CHANGE => change
      QUIT => exit

  vend : MachineLoop () (pounds, chocs) (const (0, 0))
  vend {pounds=S p} {chocs=S c} = do
    Vend
    Display "Enjoy!"
    machineLoop
  vend {pounds=Z} = do
    Display "Insert a coin"
    machineLoop
  vend {chocs=Z} = do
    Display "Out of order"
    machineLoop

  refill : (num : Nat) -> MachineLoop () (pounds, chocs) (const (0, 0))
  refill {pounds = Z} num = do
    Refill num
    machineLoop
  refill _ = do
    Display "Can't refill - coins in the machine"
    machineLoop

  insertCoin : MachineLoop () (pounds, chocs) (const (0, 0))
  insertCoin = do
    res <- InsertCoin
    case res of
      Inserted => do
        Display "Inserted Coin"
        machineLoop
      Rejected => do
        Display "Rejected Coin"
        machineLoop

  change : MachineLoop () (pounds, chocs) (const (0, 0))
  change = do
    GetCoins
    Display "Returned Coins"
    machineLoop

  exit : MachineLoop () (pounds, chocs) (const (0, 0))
  exit {pounds=Z} {chocs=Z} = Exit
  exit = do
    Display "Items remaining in machine"
    machineLoop

{-}
Main purpose of this is  to parameterise VendState

Why do we need this?
In runCmd we want to specify vendState, and make guarantees about it
(e.g. result is from applying cmd to inState)
In data constructor we would simply say (inState: VendState)
but we cannot do this for function definitions.
So instead we create new datatype.
{-}

data Machine : VendState -> Type where
  Starting: Machine (Z, Z)
  IncCoin : Machine (S p, c)
  EmptyCoins : Machine (Z, c)
  Running : Machine (p, c)

Show (Machine state) where
  show m {state} = show state

{-}
Result is the outcome of running a CMD
OK stores transistion option (e.g Inserted) + resulting state
OutOfFuel is also an option, to allow runCmd to be total
{-}

data Result : (ty : Type) -> (ty -> VendState) -> Type where
  OK : (res : ty) -> Machine (outstate_fn res) ->
       Result ty outstate_fn
  OutOfFuel : Result ty outstate_fn

{-}
Shortcut for run, which needs to return IO action
{-}

ok : (res : ty) -> Machine (outstate_fn res) -> IO (Result ty outstate_fn)
ok res st = pure (OK res st)

{-}
Convert String to Input + Arg
{-}

parseInput : String -> String -> Maybe Input
parseInput "vend" "" = Just VEND
parseInput "coin" "" = Just COIN
parseInput "refill" "" = Nothing
parseInput "refill" amount =
  case all isDigit (unpack amount) of
    False => Nothing
    True => Just (REFILL (cast amount))
parseInput "change" "" = Just CHANGE
parseInput "quit" "" = Just QUIT
parseInput _ _ = Nothing

parse : String -> Maybe Input
parse input = case span (/= ' ') input of
  (cmd, args) => parseInput cmd (ltrim args)

{-}
Needed to keep runCMD total
{-}

data Fuel = Dry | More (Lazy Fuel)

{-}
Evaluate finite sequence of Cmds, given input state
Converts sequence of commnads to sequence of IO actions

Since we are now in "runtime" we can choose which option to take in state machine.

The type guarantees that result matches one of outstate_fn options
e.g. (0, 0) + InsertCoin -> Accepted (1, 0) or Rejected (0, 0)
{-}

runCmd : Fuel -> Machine inState -> MachineCmd ty inState outstate_fn ->
         IO (Result ty outstate_fn)
runCmd fuel state InsertCoin = do
  putStr "Accept (y/n) "
  ans <- getLine
  if ans == "y"
    then
      {-}Inserted -> (S p, c){-}
      ok Inserted IncCoin
    else
      {-}Rejected -> (p, c){-}
      ok Rejected Running
runCmd fuel state Vend = ok () Running
runCmd fuel state GetCoins = ok () EmptyCoins
runCmd fuel state (Refill bars) = ok () Running
runCmd fuel state (Display str) = do
  putStrLn str
  ok () state
  
{-}
Note: unlike other options, this uses Fuel
The reason for this is that it is recursive
without using fuel it would not be total as it could loop forever
(e.g. user enters wrong input forever)
{-}

runCmd (More fuel) state GetInput = do
  putStrLn "vend / coin / refill / change / quit"
  putStr ">> "
  line <- getLine
  case parse line of
    Nothing => do
      putStrLn "Invalid input"
      runCmd fuel state GetInput
    Just input => ok input state
runCmd fuel state ShowState = do
  putStrLn (show state)
  ok () state
runCmd fuel state (Pure res) = ok res state
runCmd fuel state (cmd >>= next) = do
  OK cmdRes newSt <- runCmd fuel state cmd
    | OutOfFuel => pure OutOfFuel
  runCmd fuel newSt (next cmdRes)
runCmd Dry _ _ = pure OutOfFuel

{-}
Evaluate infinite sequence of CMDs
MachineLoop can only be >>= or Exit

3 options because we ignore Dry + Exit option
May run out of fuel either at beginning or during execution
{-}

run : Fuel -> Machine instate -> MachineLoop ty instate outstate_fn ->
      IO (Result ty outstate_fn)
run Dry _ _ = pure OutOfFuel
run (More fuel) st (cmd >>= next) = do
  OK cmdRes newSt <- runCmd fuel st cmd
    | OutOfFuel => pure OutOfFuel
  run fuel newSt (next cmdRes)
run (More fuel) st Exit = ok () st

{-}
If the program hangs, we can limit our search to the next 7 lines
{-}

partial
forever : Fuel
forever = More forever

main : IO ()
main = do
  run forever Starting machineLoop
  pure ()