Example of State Machine using Control.ST

Vend.idr

import Data.Fuel
import Control.ST

%default total

{-}

Rewrite Vend.idr using Control.ST
this example was useful for some parts
https://github.com/owickstrom/fsm-your-compiler-wants-in/blob/master/src/listings/idris/Checkout.idr

Improvements
- better error messages (expected this state, but this is the actual state)
- less boiler plate code (~100 lines less in this example)
- better syntax for describing states

A few things tricky things
- Can handle multiple resources, but this complicates the types
- type signature for Loop is a bit more confusing
  STLoop m () [remove machine (Machine {m} (pounds, chocs))]
  is the only thing that seems to work
- can't find implmentation errors, for types that should work?
  e.g STLoop m () [machine ::: Machine s1 -> Machine s2]
  there is possibly a good reason for this
  
{-}

namespace Protocol
  VendState : Type
  VendState = (Nat, Nat)

  data CoinResult = Inserted | Rejected

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

  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)

  interface CMD (m: Type -> Type) where
    Machine : VendState -> Type

    insertCoin : ST m CoinResult
      [machine ::: Machine (p, c) :->
        \res => Machine (case res of
            Inserted => (S p, c)
            Rejected => (p, c)
          )
      ]
    vend : ST m () [machine ::: Machine (S p, S c) :-> Machine (p, c)]
    getCoins : ST m () [machine ::: Machine (p, c) :-> Machine (0, c)]
    refill : (bars : Nat) -> ST m () [
          machine ::: Machine (0, c) :-> Machine (0, bars + c)
      ]

    init : ST m Var [ST.add (Machine (0, 0))]
    terminate : (machine : Var) -> ST m () [remove machine (Machine (p, c))]
    show : ST m () [machine ::: Machine state]

{- Test interface -}

getCandy : (ConsoleIO m, CMD m) => ST m () []
getCandy = do
  machine <- init
  refill 10
  Inserted <- insertCoin
    | Rejected => do
        putStrLn "failure"
        terminate machine
  vend
  terminate machine

CMD IO where
  Machine x = State VendState

  insertCoin = do
    putStrLn "Accept (y/n)?"
    case (!getStr) of
      "y" => pure Inserted
      _ => pure Rejected
  vend = pure ()
  getCoins = pure ()
  refill x = pure ()
  init = do
    putStrLn "Machine Initialized"
    new (0, 0)
  terminate machine = do
    putStrLn "Machine Terminated"
    delete machine
  show {state} = do
    putStrLn (show state)

using (ConsoleIO m, CMD m)
  mutual
    program : STLoop m () []
    program = do
      machine <- init
      vendLoop machine

    -- why do I need to include implicit m for Machine?
    vendLoop : (machine : Var) -> STLoop m () [remove machine (Machine {m} (p, c))]
    vendLoop machine = do
      show
      putStrLn "vend / coin / refill / change / quit"
      putStr ">> "
      case parse (!getStr) of
        Just COIN => insertCoin machine
        Just VEND => vend machine
        Just CHANGE => change machine
        Just (REFILL n) => refill n machine
        Just QUIT => do
          putStrLn "Exiting"
          terminate machine
          -- why is this pure necissary?
          pure ()
        Nothing => do
          putStrLn "Invalid input"
          vendLoop machine

    insertCoin : (machine : Var) -> STLoop m () [remove machine (Machine {m} (pounds, chocs))]
    insertCoin machine = do
      case (!insertCoin) of
        Inserted => vendLoop machine
        Rejected => vendLoop machine

    vend : (machine : Var) -> STLoop m () [remove machine (Machine {m} (pounds, chocs))]
    vend {pounds=S p} {chocs=S c} machine = do
      Protocol.vend
      putStrLn "Enjoy!"
      vendLoop machine
    vend {pounds=Z} machine = do
      putStrLn "Insert a coin"
      vendLoop machine
    vend {chocs=Z} machine = do
      putStrLn "Out of order"
      vendLoop machine

    change : (machine : Var) -> STLoop m () [remove machine (Machine {m} (pounds, chocs))]
    change machine = do
      Protocol.getCoins
      putStrLn "returned coins"
      vendLoop machine

    refill : Nat -> (machine : Var) -> STLoop m () [remove machine (Machine {m} (pounds, chocs))]
    refill {pounds = Z} num machine = do
      Protocol.refill num
      vendLoop machine
    refill _ machine = do
      putStrLn "Can't refill - coins in the machine"
      vendLoop machine

partial
main : IO ()
main = runLoop forever program (putStrLn "Execution Ended.")