diff --git a/Chapter13/Vending.idr b/Chapter13/Vending.idr index 209dac1..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) @@ -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}) -