From 6fc90519a6cc21d0930dd5e3e7d7590d6ae5a246 Mon Sep 17 00:00:00 2001
From: Neil Vyas <vyas.neil.nv@gmail.com>
Date: Sun, 26 Mar 2017 15:48:23 -0700
Subject: [PATCH 1/3] fix `Nothig` typo

---
 Chapter13/Vending.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Chapter13/Vending.idr b/Chapter13/Vending.idr
index 209dac1..10bee76 100644
--- a/Chapter13/Vending.idr
+++ b/Chapter13/Vending.idr
@@ -88,8 +88,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

From e4000d685ee917b3a8134a4d1823f008fefcf9c3 Mon Sep 17 00:00:00 2001
From: Neil Vyas <neil.vyas@affirm.com>
Date: Sun, 26 Mar 2017 16:42:02 -0700
Subject: [PATCH 2/3] reordering definitions to be more sensible

---
 Chapter13/Vending.idr | 78 +++++++++++++++++++++----------------------
 1 file changed, 38 insertions(+), 40 deletions(-)

diff --git a/Chapter13/Vending.idr b/Chapter13/Vending.idr
index 10bee76..309dc61 100644
--- a/Chapter13/Vending.idr
+++ b/Chapter13/Vending.idr
@@ -6,14 +6,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,37 +26,6 @@ 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
@@ -99,6 +60,43 @@ mutual
                            machineLoop
               REFILL num => refill num
 
+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})
-

From 63613570bab513af0eb09bbad5d2cc179b5dd9bc Mon Sep 17 00:00:00 2001
From: Neil Vyas <neil.vyas@affirm.com>
Date: Sun, 26 Mar 2017 16:42:29 -0700
Subject: [PATCH 3/3] comments to mark the different layers of specification ->
 implementation

---
 Chapter13/Vending.idr | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Chapter13/Vending.idr b/Chapter13/Vending.idr
index 309dc61..0381e9b 100644
--- a/Chapter13/Vending.idr
+++ b/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)
 
@@ -31,6 +33,7 @@ namespace MachineDo
           (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
@@ -60,6 +63,7 @@ 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