re-order the vending machine example

Chapter13/Vending.idr

@@ -1,3 +1,5 @@
+-- Specify the state with a type, transitions with commands,
+-- and entry points with an enumerated type.
 VendState : Type
 VendState = (Nat, Nat)
 
@@ -6,14 +8,6 @@ data Input = COIN
            | CHANGE 
            | REFILL Nat
 
-strToInput : String -> Maybe Input
-strToInput "insert" = Just COIN
-strToInput "vend" = Just VEND
-strToInput "change" = Just CHANGE
-strToInput x = if all isDigit (unpack x)
-                  then Just (REFILL (cast x))
-                  else Nothing
-
 data MachineCmd : Type -> VendState -> VendState -> Type where
      InsertCoin : MachineCmd () (pounds, chocs)     (S pounds, chocs)
      Vend       : MachineCmd () (S pounds, S chocs) (pounds, chocs)
@@ -34,42 +28,12 @@ data MachineIO : VendState -> Type where
      Do : MachineCmd a state1 state2 ->
           (a -> Inf (MachineIO state2)) -> MachineIO state1
 
-runMachine : MachineCmd ty inState outState -> IO ty
-runMachine InsertCoin = putStrLn "Coin inserted"
-runMachine Vend = putStrLn "Please take your chocolate"
-runMachine {inState = (pounds, _)} GetCoins 
-     = putStrLn (show pounds ++ " coins returned")
-runMachine (Display str) = putStrLn str
-runMachine (Refill bars)
-     = putStrLn ("Chocolate remaining: " ++ show bars)
-runMachine {inState = (pounds, chocs)} GetInput
-     = do putStrLn ("Coins: " ++ show pounds ++ "; " ++
-                    "Stock: " ++ show chocs)
-          putStr "> "
-          x <- getLine
-          pure (strToInput x)
-runMachine (Pure x) = pure x
-runMachine (cmd >>= prog) = do x <- runMachine cmd
-                               runMachine (prog x)
-
-data Fuel = Dry | More (Lazy Fuel)
-
-partial
-forever : Fuel
-forever = More forever
-
-run : Fuel -> MachineIO state -> IO ()
-run (More fuel) (Do c f) 
-     = do res <- runMachine c
-          run fuel (f res)
-run Dry p = pure ()
-
-
 namespace MachineDo
   (>>=) : MachineCmd a state1 state2 ->
           (a -> Inf (MachineIO state2)) -> MachineIO state1
   (>>=) = Do
 
+-- Define the handlers and vending machine loop.
 mutual
   vend : MachineIO (pounds, chocs)
   vend {pounds = S p} {chocs = S c} = do Vend
@@ -88,8 +52,8 @@ mutual
 
   machineLoop : MachineIO (pounds, chocs)
   machineLoop =
-       do Just x <- GetInput | Nothig => do Display "Invalid input"
-                                            machineLoop
+       do Just x <- GetInput | Nothing => do Display "Invalid input"
+                                             machineLoop
           case x of
               COIN => do InsertCoin
                          machineLoop
@@ -99,6 +63,44 @@ mutual
                            machineLoop
               REFILL num => refill num
 
+-- A console interpreter for our vending machine, which is just one possible implementation.
+strToInput : String -> Maybe Input
+strToInput "insert" = Just COIN
+strToInput "vend" = Just VEND
+strToInput "change" = Just CHANGE
+strToInput x = if all isDigit (unpack x)
+                  then Just (REFILL (cast x))
+                  else Nothing
+
+runMachine : MachineCmd ty inState outState -> IO ty
+runMachine InsertCoin = putStrLn "Coin inserted"
+runMachine Vend = putStrLn "Please take your chocolate"
+runMachine {inState = (pounds, _)} GetCoins
+     = putStrLn (show pounds ++ " coins returned")
+runMachine (Display str) = putStrLn str
+runMachine (Refill bars)
+     = putStrLn ("Chocolate remaining: " ++ show bars)
+runMachine {inState = (pounds, chocs)} GetInput
+     = do putStrLn ("Coins: " ++ show pounds ++ "; " ++
+                    "Stock: " ++ show chocs)
+          putStr "> "
+          x <- getLine
+          pure (strToInput x)
+runMachine (Pure x) = pure x
+runMachine (cmd >>= prog) = do x <- runMachine cmd
+                               runMachine (prog x)
+
+data Fuel = Dry | More (Lazy Fuel)
+
+partial
+forever : Fuel
+forever = More forever
+
+run : Fuel -> MachineIO state -> IO ()
+run (More fuel) (Do c f)
+     = do res <- runMachine c
+          run fuel (f res)
+run Dry p = pure ()
+
 main : IO ()
 main = run forever (machineLoop {pounds = 0} {chocs = 1})
-