diff --git a/docs/app/index.rst b/docs/app/index.rst index 1418cf6..c90fc76 100644 --- a/docs/app/index.rst +++ b/docs/app/index.rst @@ -25,14 +25,14 @@ explicit about how an operation handles failure. Also, if we do want to support exceptions, we also want to explain how exceptions and linearity (see Section :ref:`sect-multiplicites`) interact. -In this tutorial, we describe a parameterised type ``App`` and a related +In this tutorial, we describe a parameterised type ``App`` and a related parameterised type ``App1``, which together allow us to structure larger applications, taking into account both exceptions and linearity. The aims of ``App`` and ``App1`` are that they should: * make it possible to express what interactions a function does, in its type, without too much notational overhead. -* have little or no performance overhead compared to writing in \texttt{IO}. +* have little or no performance overhead compared to writing in *IO*. * be compatible with other libraries and techniques for describing effects, such as algebraic effects or monad transformers. * be sufficiently easy to use and performant that it can be the basis of @@ -47,4 +47,3 @@ programs, then show how to extend it with exceptions, state, and other interfaces. [To be continued...] - diff --git a/docs/typedd/typedd.rst b/docs/typedd/typedd.rst index e053b0f..fa853a2 100644 --- a/docs/typedd/typedd.rst +++ b/docs/typedd/typedd.rst @@ -20,7 +20,7 @@ Chapter 2 --------- The Prelude is smaller than Idris 1, and many functions have been moved to -the base libraries instead. So: +the base libraries instead. So: In ``Average.idr``, add: @@ -60,7 +60,7 @@ For the reasons described above: .. code-block:: idris tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a - + Chapter 5 --------- @@ -205,7 +205,7 @@ what it allows to unify. So, ``x`` and ``xs`` need to be explicit arguments to data SnocList : List a -> Type where Empty : SnocList [] Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x]) - + Correspondingly, they need to be explicit when matching. For example: .. code-block:: idris @@ -239,7 +239,7 @@ recursive with application in Idris 1 probably shouldn't have allowed this! isSuffix [] input2 | (Empty, s) = True isSuffix input1 [] | (s, Empty) = False isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec, Snoc ysrec) - = if x == y + = if x == y then isSuffix xs ys | (xsrec, ysrec) else False @@ -248,7 +248,7 @@ know about looking inside pairs. In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets this through! I think perhaps it's too "helpful" when solving unification -problems. To fix it, add an extra parameter ``scheme`` to ``StoreView``, and change +problems. To fix it, add an extra parameter ``schema`` to ``StoreView``, and change the type of ``SNil`` to be explicit that the ``empty`` is the function defined in ``DataStore``. Also add ``entry`` and ``store`` as explicit arguments to ``SAdd``: @@ -282,8 +282,6 @@ In ``TestStore.idr``: Chapter 11 ---------- -Remove ``%default total`` throughout - it's not yet implemented. - In ``Streams.idr`` add ``import Data.Stream`` for ``iterate``. In ``Arith.idr`` and ``ArithTotal.idr``, the ``Divides`` view now has explicit @@ -306,8 +304,6 @@ export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``. Chapter 12 ---------- -Remove ``%default total`` throughout, at least until it's implemented. - For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``. Also the ``(>>=)`` operators need to be set as ``export`` since they are in their own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional @@ -316,15 +312,140 @@ arguments ``div`` and ``rem``. Chapter 13 ---------- -TODO +In ``StackIO.idr``: + ++ ``tryAdd`` pattern matches on ``height``, so it needs to be written in its + type: + +.. code-block:: idris + + tryAdd : {height : _} -> StackIO height + ++ ``height`` is also an implicit argument to ``stackCalc``, but is used by the + definition, so add it to its type: + +.. code-block:: idris + + stackCalc : {height : _} -> StackIO height + ++ In ``StackDo`` namespace, export ``(>>=)``: + +.. code-block:: idris + + namespace StackDo + export + (>>=) : StackCmd a height1 height2 -> + (a -> Inf (StackIO height2)) -> StackIO height1 + (>>=) = Do + +In ``Vending.idr``: + ++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput`` ++ In ``MachineCmd`` type, add an implicit argument to ``(>>=)`` data constructor: + +.. code-block:: idris + + (>>=) : {state2 : _} -> + MachineCmd a state1 state2 -> + (a -> MachineCmd b state2 state3) -> + MachineCmd b state1 state3 + ++ In ``MachineIO`` type, add an implicit argument to ``Do`` data constructor: + +.. code-block:: idris + + data MachineIO : VendState -> Type where + Do : {state1 : _} -> + MachineCmd a state1 state2 -> + (a -> Inf (MachineIO state2)) -> MachineIO state1 + ++ ``runMachine`` pattern matches on ``inState``, so it needs to be written in its + type: + +.. code-block:: idris + + runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty + ++ In ``MachineDo`` namespace, add an implicit argument to ``(>>=)`` and export it: + +.. code-block:: idris + + namespace MachineDo + export + (>>=) : {state1 : _} -> + MachineCmd a state1 state2 -> + (a -> Inf (MachineIO state2)) -> MachineIO state1 + (>>=) = Do + ++ ``vend`` and ``refill`` pattern match on ``pounds`` and ``chocs``, so they need to be written in + their type: + +.. code-block:: idris + + vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) + refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs) + ++ ``pounds`` and ``chocs`` are implicit arguments to ``machineLoop``, but are used by the + definition, so add them to its type: + +.. code-block:: idris + + machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) Chapter 14 ---------- -TODO +In ``ATM.idr``: + ++ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM`` + +In ``ATM.idr``, add: + +.. code-block:: idris + + import Data.Strings -- for `toUpper` + import Data.List -- for `nub` + ++ In ``Loop`` namespace, export ``GameLoop`` type and its data constructors: + +.. code-block:: idris + + namespace Loop + public export + data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where + (>>=) : GameCmd a state1 state2_fn -> + ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) -> + GameLoop b state1 state3_fn + Exit : GameLoop () NotRunning (const NotRunning) + ++ ``letters`` and ``guesses`` are used by ``gameLoop``, so they need to be written in its type: + +.. code-block:: idris + + gameLoop : {letters : _} -> {guesses : _} -> + GameLoop () (Running (S guesses) (S letters)) (const NotRunning) + ++ In ``Game`` type, add an implicit argument ``letters`` to ``InProgress`` data constructor: + +.. code-block:: idris + + data Game : GameState -> Type where + GameStart : Game NotRunning + GameWon : (word : String) -> Game NotRunning + GameLost : (word : String) -> Game NotRunning + InProgress : {letters : _} -> (word : String) -> (guesses : Nat) -> + (missing : Vect letters Char) -> Game (Running guesses letters) + ++ ``removeElem`` pattern matches on ``n``, so it needs to be written in its type: + +.. code-block:: idris + + removeElem : {n : _} -> + (value : a) -> (xs : Vect (S n) a) -> + {auto prf : Elem value xs} -> + Vect n a Chapter 15 ---------- TODO - diff --git a/tests/Main.idr b/tests/Main.idr index d2fd182..6f2b5ea 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -84,7 +84,7 @@ typeddTests : List String typeddTests = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05", "chapter06", "chapter07", "chapter08", "chapter09", "chapter10", - "chapter11", "chapter12"] + "chapter11", "chapter12", "chapter13", "chapter14"] chezTests : List String chezTests diff --git a/tests/typedd-book/chapter11/ArithCmd.idr b/tests/typedd-book/chapter11/ArithCmd.idr index bc8d789..6de57a2 100644 --- a/tests/typedd-book/chapter11/ArithCmd.idr +++ b/tests/typedd-book/chapter11/ArithCmd.idr @@ -2,7 +2,7 @@ import Data.Primitives.Views import Data.Strings import System --- %default total +%default total data Command : Type -> Type where PutStr : String -> Command () diff --git a/tests/typedd-book/chapter11/ArithCmdDo.idr b/tests/typedd-book/chapter11/ArithCmdDo.idr index db71f5b..e2a3a18 100644 --- a/tests/typedd-book/chapter11/ArithCmdDo.idr +++ b/tests/typedd-book/chapter11/ArithCmdDo.idr @@ -2,7 +2,7 @@ import Data.Primitives.Views import Data.Strings import System --- %default total +%default total data Command : Type -> Type where PutStr : String -> Command () diff --git a/tests/typedd-book/chapter11/ArithTotal.idr b/tests/typedd-book/chapter11/ArithTotal.idr index bdf9c06..3c26ebf 100644 --- a/tests/typedd-book/chapter11/ArithTotal.idr +++ b/tests/typedd-book/chapter11/ArithTotal.idr @@ -1,7 +1,7 @@ import Data.Primitives.Views import System --- %default total +%default total data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO diff --git a/tests/typedd-book/chapter11/Greet.idr b/tests/typedd-book/chapter11/Greet.idr index 3df0dae..2dc31ab 100644 --- a/tests/typedd-book/chapter11/Greet.idr +++ b/tests/typedd-book/chapter11/Greet.idr @@ -1,4 +1,4 @@ --- %default total +%default total data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO diff --git a/tests/typedd-book/chapter11/InfIO.idr b/tests/typedd-book/chapter11/InfIO.idr index 4864106..8a02a5c 100644 --- a/tests/typedd-book/chapter11/InfIO.idr +++ b/tests/typedd-book/chapter11/InfIO.idr @@ -1,4 +1,4 @@ --- %default total +%default total data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO diff --git a/tests/typedd-book/chapter11/RunIO.idr b/tests/typedd-book/chapter11/RunIO.idr index 47bd4d9..70c45db 100644 --- a/tests/typedd-book/chapter11/RunIO.idr +++ b/tests/typedd-book/chapter11/RunIO.idr @@ -1,4 +1,4 @@ --- %default total +%default total data RunIO : Type -> Type where Quit : a -> RunIO a diff --git a/tests/typedd-book/chapter12/ArithState.idr b/tests/typedd-book/chapter12/ArithState.idr index 86a5097..ea4db61 100644 --- a/tests/typedd-book/chapter12/ArithState.idr +++ b/tests/typedd-book/chapter12/ArithState.idr @@ -2,7 +2,7 @@ import Data.Primitives.Views import Data.Strings import System --- %default total +%default total record Score where constructor MkScore diff --git a/tests/typedd-book/chapter13/Door.idr b/tests/typedd-book/chapter13/Door.idr new file mode 100644 index 0000000..507acb1 --- /dev/null +++ b/tests/typedd-book/chapter13/Door.idr @@ -0,0 +1,18 @@ +data DoorState = DoorOpen | DoorClosed + +data DoorCmd : Type -> + DoorState -> DoorState -> + Type where + Open : DoorCmd () DoorClosed DoorOpen + Close : DoorCmd () DoorOpen DoorClosed + RingBell : DoorCmd () DoorClosed DoorClosed + + Pure : ty -> DoorCmd ty state state + (>>=) : DoorCmd a state1 state2 -> + (a -> DoorCmd b state2 state3) -> + DoorCmd b state1 state3 + +doorProg : DoorCmd () DoorClosed DoorClosed +doorProg = do RingBell + Open + Close diff --git a/tests/typedd-book/chapter13/Stack.idr b/tests/typedd-book/chapter13/Stack.idr new file mode 100644 index 0000000..7289d7f --- /dev/null +++ b/tests/typedd-book/chapter13/Stack.idr @@ -0,0 +1,33 @@ +import Data.Vect + +data StackCmd : Type -> Nat -> Nat -> Type where + Push : Integer -> StackCmd () height (S height) + Pop : StackCmd Integer (S height) height + Top : StackCmd Integer (S height) (S height) + + Pure : ty -> StackCmd ty height height + (>>=) : StackCmd a height1 height2 -> + (a -> StackCmd b height2 height3) -> + StackCmd b height1 height3 + +runStack : (stk : Vect inHeight Integer) -> + StackCmd ty inHeight outHeight -> + (ty, Vect outHeight Integer) +runStack stk (Push val) = ((), val :: stk) +runStack (val :: stk) Pop = (val, stk) +runStack (val :: stk) Top = (val, val :: stk) +runStack stk (Pure x) = (x, stk) +runStack stk (x >>= f) = let (x', newStk) = runStack stk x in + runStack newStk (f x') + +testAdd : StackCmd Integer 0 0 +testAdd = do Push 10 + Push 20 + val1 <- Pop + val2 <- Pop + Pure (val1 + val2) + +doAdd : StackCmd () (S (S height)) (S height) +doAdd = do val1 <- Pop + val2 <- Pop + Push (val1 + val2) diff --git a/tests/typedd-book/chapter13/StackIO.idr b/tests/typedd-book/chapter13/StackIO.idr new file mode 100644 index 0000000..598b0d6 --- /dev/null +++ b/tests/typedd-book/chapter13/StackIO.idr @@ -0,0 +1,94 @@ +import Data.Vect + +data StackCmd : Type -> Nat -> Nat -> Type where + Push : Integer -> StackCmd () height (S height) + Pop : StackCmd Integer (S height) height + Top : StackCmd Integer (S height) (S height) + + GetStr : StackCmd String height height + PutStr : String -> StackCmd () height height + + Pure : ty -> StackCmd ty height height + (>>=) : StackCmd a height1 height2 -> + (a -> StackCmd b height2 height3) -> + StackCmd b height1 height3 + +runStack : (stk : Vect inHeight Integer) -> + StackCmd ty inHeight outHeight -> + IO (ty, Vect outHeight Integer) +runStack stk (Push val) = pure ((), val :: stk) +runStack (val :: stk) Pop = pure (val, stk) +runStack (val :: stk) Top = pure (val, val :: stk) +runStack stk GetStr = do x <- getLine + pure (x, stk) +runStack stk (PutStr x) = do putStr x + pure ((), stk) +runStack stk (Pure x) = pure (x, stk) +runStack stk (x >>= f) = do (x', newStk) <- runStack stk x + runStack newStk (f x') + +testAdd : StackCmd () 0 0 +testAdd = do Push 10 + x <- GetStr + Push (cast x) + val1 <- Pop + val2 <- Pop + PutStr (show (val1 + val2) ++ "\n") + +data StackIO : Nat -> Type where + Do : StackCmd a height1 height2 -> + (a -> Inf (StackIO height2)) -> StackIO height1 + +namespace StackDo + export + (>>=) : StackCmd a height1 height2 -> + (a -> Inf (StackIO height2)) -> StackIO height1 + (>>=) = Do + +data Fuel = Dry | More (Lazy Fuel) + +partial +forever : Fuel +forever = More forever + +run : Fuel -> Vect height Integer -> StackIO height -> IO () +run Dry _ _ = pure () +run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c + run fuel newStk (f res) + +doAdd : StackCmd () (S (S height)) (S height) +doAdd = do val1 <- Pop + val2 <- Pop + Push (val1 + val2) + +data StkInput = Number Integer + | Add + +strToInput : String -> Maybe StkInput +strToInput "" = Nothing +strToInput "add" = Just Add +strToInput x = if all isDigit (unpack x) + then Just (Number $ cast x) + else Nothing + +mutual + tryAdd : {height : _} -> StackIO height + tryAdd {height = S (S h)} = do doAdd + result <- Top + PutStr (show result ++ "\n") + stackCalc + tryAdd = do PutStr "Fewer than two items on the stack\n" + stackCalc + + stackCalc : {height : _} -> StackIO height + stackCalc = do PutStr "> " + input <- GetStr + case strToInput input of + Nothing => do PutStr "Invalid input\n" + stackCalc + Just (Number x) => do Push x + stackCalc + Just Add => tryAdd + +main : IO () +main = run forever [] stackCalc diff --git a/tests/typedd-book/chapter13/Vending.idr b/tests/typedd-book/chapter13/Vending.idr new file mode 100644 index 0000000..53ec601 --- /dev/null +++ b/tests/typedd-book/chapter13/Vending.idr @@ -0,0 +1,109 @@ +import Data.Strings + +VendState : Type +VendState = (Nat, Nat) + +data Input = COIN + | VEND + | 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 (stringToNatOrZ 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) + GetCoins : MachineCmd () (pounds, chocs) (Z, chocs) + + Refill : (bars : Nat) -> + MachineCmd () (Z, chocs) (Z, bars + chocs) + + Display : String -> MachineCmd () state state + GetInput : MachineCmd (Maybe Input) state state + + Pure : ty -> MachineCmd ty state state + (>>=) : {state2 : _} -> + MachineCmd a state1 state2 -> + (a -> MachineCmd b state2 state3) -> + MachineCmd b state1 state3 + +data MachineIO : VendState -> Type where + Do : {state1 : _} -> + MachineCmd a state1 state2 -> + (a -> Inf (MachineIO state2)) -> MachineIO state1 + +runMachine : {inState : _} -> 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) +namespace MachineDo + export + (>>=) : {state1 : _} -> + MachineCmd a state1 state2 -> + (a -> Inf (MachineIO state2)) -> MachineIO state1 + (>>=) = Do + +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 () + +mutual + vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) + 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 stock" + machineLoop + + refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs) + refill {pounds = Z} num = do Refill num + machineLoop + refill _ = do Display "Can't refill: Coins in machine" + machineLoop + + machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) + machineLoop = do Just x <- GetInput + | Nothing => do Display "Invalid input" + machineLoop + case x of + COIN => do InsertCoin + machineLoop + VEND => vend + CHANGE => do GetCoins + Display "Change returned" + machineLoop + REFILL num => refill num + +main : IO () +main = run forever (machineLoop {pounds = 0} {chocs = 1}) diff --git a/tests/typedd-book/chapter13/expected b/tests/typedd-book/chapter13/expected new file mode 100644 index 0000000..ff3e8c5 --- /dev/null +++ b/tests/typedd-book/chapter13/expected @@ -0,0 +1,4 @@ +1/1: Building Door (Door.idr) +1/1: Building Stack (Stack.idr) +1/1: Building StackIO (StackIO.idr) +1/1: Building Vending (Vending.idr) diff --git a/tests/typedd-book/chapter13/run b/tests/typedd-book/chapter13/run new file mode 100755 index 0000000..0001163 --- /dev/null +++ b/tests/typedd-book/chapter13/run @@ -0,0 +1,6 @@ +$1 Door.idr --check +$1 Stack.idr --check +$1 StackIO.idr --check +$1 Vending.idr --check + +rm -rf build diff --git a/tests/typedd-book/chapter14/ATM.idr b/tests/typedd-book/chapter14/ATM.idr new file mode 100644 index 0000000..30f06bc --- /dev/null +++ b/tests/typedd-book/chapter14/ATM.idr @@ -0,0 +1,91 @@ +import Data.Vect +import Data.Strings + +data ATMState = Ready | CardInserted | Session + +data PINCheck = CorrectPIN | IncorrectPIN + +PIN : Type +PIN = Vect 4 Char + +data HasCard : ATMState -> Type where + HasCI : HasCard CardInserted + HasSession : HasCard Session + +data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where + InsertCard : ATMCmd () Ready (const CardInserted) + EjectCard : {auto prf : HasCard state} -> + ATMCmd () state (const Ready) + GetPIN : ATMCmd PIN CardInserted (const CardInserted) + + CheckPIN : PIN -> ATMCmd PINCheck CardInserted (\check => case check of + CorrectPIN => Session + IncorrectPIN => CardInserted) + + GetAmount : ATMCmd Nat state (const state) + Dispense : (amount : Nat) -> ATMCmd () Session (const Session) + + Message : String -> ATMCmd () state (const state) + Pure : (res : ty) -> ATMCmd ty (state_fn res) state_fn + (>>=) : ATMCmd a state1 state2_fn -> + ((res : a) -> ATMCmd b (state2_fn res) state3_fn) -> + ATMCmd b state1 state3_fn + +readVect : (n : Nat) -> IO (Vect n Char) +readVect Z = do discard <- getLine -- rest of input up to enter + pure [] +readVect (S k) = do ch <- getChar + chs <- readVect k + pure (ch :: chs) + +testPIN : Vect 4 Char +testPIN = ['1', '2', '3', '4'] + +insertEject : ATMCmd () Ready (const Ready) +insertEject = do InsertCard + EjectCard -- ?insertEject_rhs + +-- badATM : ATMCmd () Ready (const Ready) +-- badATM = EjectCard + +runATM : ATMCmd res inState outState_fn -> IO res +runATM InsertCard = do putStrLn "Please insert your card (press enter)" + x <- getLine + pure () +runATM EjectCard = putStrLn "Card ejected" +runATM GetPIN = do putStr "Enter PIN: " + readVect 4 +runATM (CheckPIN pin) = if pin == testPIN + then pure CorrectPIN + else pure IncorrectPIN +runATM GetAmount = do putStr "How much would you like? " + x <- getLine + pure (stringToNatOrZ x) +runATM (Dispense amount) = putStrLn ("Here is " ++ show amount) +runATM (Message msg) = putStrLn msg +runATM (Pure res) = pure res +runATM (x >>= f) = do x' <- runATM x + runATM (f x') + +atm : ATMCmd () Ready (const Ready) +atm = do InsertCard + pin <- GetPIN + pinOK <- CheckPIN pin + case pinOK of + CorrectPIN => do cash <- GetAmount + Dispense cash + EjectCard + IncorrectPIN => EjectCard + +atm_alt : ATMCmd () Ready (const Ready) +atm_alt = do InsertCard + pin <- GetPIN + cash <- GetAmount + pinOK <- CheckPIN pin + Message "Checking Card" + case pinOK of + CorrectPIN => do Dispense cash + EjectCard + Message "Please remove your card and cash" + IncorrectPIN => do Message "Incorrect PIN" + EjectCard diff --git a/tests/typedd-book/chapter14/DoorJam.idr b/tests/typedd-book/chapter14/DoorJam.idr new file mode 100644 index 0000000..693a049 --- /dev/null +++ b/tests/typedd-book/chapter14/DoorJam.idr @@ -0,0 +1,48 @@ +data DoorState = DoorClosed | DoorOpen + +data DoorResult = OK | Jammed + +data DoorCmd : (ty : Type) -> + DoorState -> + (ty -> DoorState) -> + Type where + Open : DoorCmd DoorResult DoorClosed (\res => case res of + OK => DoorOpen + Jammed => DoorClosed) + Close : DoorCmd () DoorOpen (const DoorClosed) + RingBell : DoorCmd () DoorClosed (const DoorClosed) + + Display : String -> DoorCmd () state (const state) + + Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn + (>>=) : DoorCmd a state1 state2_fn -> + ((res: a) -> DoorCmd b (state2_fn res) state3_fn) -> + DoorCmd b state1 state3_fn + +logOpen : DoorCmd DoorResult DoorClosed + (\res => case res of + OK => DoorOpen + Jammed => DoorClosed) +logOpen = do Display "Trying to open the door" + OK <- Open | Jammed => do Display "Jammed" + Pure Jammed + Display "Success" + Pure OK + +doorProg : DoorCmd () DoorClosed (const DoorClosed) +doorProg = do RingBell + jam <- Open + Display "Trying to open the door" + case jam of + OK => do Display "Glad To Be Of Service" + Close + Jammed => Display "Door Jammed" + +doorProg2 : DoorCmd () DoorClosed (const DoorClosed) +doorProg2 = do RingBell + OK <- Open | Jammed => Display "Door Jammed" + Display "Glad To Be Of Service" + Close + OK <- Open | Jammed => Display "Door Jammed" + Display "Glad To Be Of Service" + Close diff --git a/tests/typedd-book/chapter14/Hangman.idr b/tests/typedd-book/chapter14/Hangman.idr new file mode 100644 index 0000000..0c8c024 --- /dev/null +++ b/tests/typedd-book/chapter14/Hangman.idr @@ -0,0 +1,141 @@ +import Data.Vect +import Data.List +import Data.Strings + +%default total + +data GameState : Type where + NotRunning : GameState + Running : (guesses : Nat) -> (letters : Nat) -> GameState + +letters : String -> List Char +letters str = nub (map toUpper (unpack str)) + +data GuessResult = Correct | Incorrect + +data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where + NewGame : (word : String) -> + GameCmd () NotRunning (const (Running 6 (length (letters word)))) + + Won : GameCmd () (Running (S guesses) 0) (const NotRunning) + Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning) + + Guess : (c : Char) -> + GameCmd GuessResult + (Running (S guesses) (S letters)) + (\res => case res of + Correct => Running (S guesses) letters + Incorrect => Running guesses (S letters)) + + ShowState : GameCmd () state (const state) + Message : String -> GameCmd () state (const state) + ReadGuess : GameCmd Char state (const state) + + Pure : (res : ty) -> GameCmd ty (state_fn res) state_fn + (>>=) : GameCmd a state1 state2_fn -> + ((res : a) -> GameCmd b (state2_fn res) state3_fn) -> + GameCmd b state1 state3_fn + +namespace Loop + public export + data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where + (>>=) : GameCmd a state1 state2_fn -> + ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) -> + GameLoop b state1 state3_fn + Exit : GameLoop () NotRunning (const NotRunning) + +gameLoop : {letters : _} -> {guesses : _} -> + GameLoop () (Running (S guesses) (S letters)) (const NotRunning) +gameLoop {guesses} {letters} = do ShowState + g <- ReadGuess + ok <- Guess g + case ok of + Correct => case letters of + Z => do Won + ShowState + Exit + S k => do Message "Correct" + gameLoop + Incorrect => case guesses of + Z => do Lost + ShowState + Exit + S k => do Message "Incorrect" + gameLoop + +hangman : GameLoop () NotRunning (const NotRunning) +hangman = do NewGame "testing" + gameLoop + +data Game : GameState -> Type where + GameStart : Game NotRunning + GameWon : (word : String) -> Game NotRunning + GameLost : (word : String) -> Game NotRunning + InProgress : {letters : _} -> (word : String) -> (guesses : Nat) -> + (missing : Vect letters Char) -> Game (Running guesses letters) + +Show (Game g) where + show GameStart = "Starting" + show (GameWon word) = "Game won: word was " ++ word + show (GameLost word) = "Game lost: word was " ++ word + show (InProgress word guesses missing) = "\n" ++ pack (map hideMissing (unpack word)) + ++ "\n" ++ show guesses ++ " guesses left " + where + hideMissing : Char -> Char + hideMissing c = if c `elem` missing then '-' else c + +data Fuel = Dry | More (Lazy Fuel) + +removeElem : {n : _} -> (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a +removeElem value (value :: ys) {prf = Here} = ys +removeElem {n = Z} value (y :: []) {prf = There later} = absurd later +removeElem {n = (S k)} value (y :: ys) {prf = There later} = y :: removeElem value ys + +data GameResult : (ty : Type) -> (ty -> GameState) -> Type where + OK : (res : ty) -> Game (outState_fn res) -> GameResult ty outState_fn + OutOfFuel : GameResult ty outState_fn + +ok : (res : ty) -> Game (outstate_fn res) -> IO (GameResult ty outstate_fn) +ok res st = pure (OK res st) + +runCmd : Fuel -> Game inState -> GameCmd ty inState outState_fn -> IO (GameResult ty outState_fn) +runCmd fuel state (NewGame word) = ok () (InProgress (toUpper word) _ (fromList (letters word))) +runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word) +runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word) +runCmd fuel (InProgress word _ missing) (Guess c) = case isElem c missing of + Yes prf => ok Correct (InProgress word _ (removeElem c missing)) + No contra => ok Incorrect (InProgress word _ missing) +runCmd fuel state ShowState = do printLn state + ok () state +runCmd fuel state (Message str) = do putStrLn str + ok () state +runCmd (More fuel) state ReadGuess = do putStr "Guess: " + input <- getLine + case unpack input of + [x] => if isAlpha x + then ok (toUpper x) state + else do putStrLn "Invalid input" + runCmd fuel state ReadGuess + _ => do putStrLn "Invalid input" + runCmd fuel state ReadGuess +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 + +run : Fuel -> Game inState -> GameLoop ty inState outState_fn -> IO (GameResult ty outState_fn) +run Dry _ _ = pure OutOfFuel +run (More fuel) st Exit = ok () st +run (More fuel) st (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel st cmd + | OutOfFuel => pure OutOfFuel + run fuel newSt (next cmdRes) + +partial +forever : Fuel +forever = More forever + +partial +main : IO () +main = do run forever GameStart hangman + pure () diff --git a/tests/typedd-book/chapter14/expected b/tests/typedd-book/chapter14/expected new file mode 100644 index 0000000..89f309f --- /dev/null +++ b/tests/typedd-book/chapter14/expected @@ -0,0 +1,3 @@ +1/1: Building DoorJam (DoorJam.idr) +1/1: Building ATM (ATM.idr) +1/1: Building Hangman (Hangman.idr) diff --git a/tests/typedd-book/chapter14/run b/tests/typedd-book/chapter14/run new file mode 100755 index 0000000..b575403 --- /dev/null +++ b/tests/typedd-book/chapter14/run @@ -0,0 +1,5 @@ +$1 DoorJam.idr --check +$1 ATM.idr --check +$1 Hangman.idr --check + +rm -rf build