Ch 14 Question

ch14gist.idr

module Main

import Data.Vect

namespace ATM

  total
  PIN : Type
  PIN = Vect 4 Char

  data State 
    = Ready 
    | CardInserted
    | Session
  
  data PINCheck
    = Correct
    | Incorrect

  data HasCard : ATM.State -> Type where
    HasCardInserted : HasCard CardInserted
    HasSession      : HasCard Session
    
  total
  tryPIN : ATM.State -> ATM.State -> PINCheck -> ATM.State
  tryPIN success failure Correct   = success
  tryPIN success failure Incorrect = failure
  
  data Command 
    :  (ty : Type) 
    -> ATM.State 
    -> (ty -> ATM.State) 
    -> Type
  where
    InsertCard :                   ATM.Command ()       Ready        (const CardInserted)
    EjectCard  : {auto prf : HasCard state}  
                                -> ATM.Command ()       state        (const Ready)
    GetPIN     :                   ATM.Command PIN      CardInserted (const CardInserted)
    CheckPIN   : PIN            -> ATM.Command PINCheck CardInserted (tryPIN Session CardInserted)
    GetAmount  :                   ATM.Command Nat      state        (const state)
    Dispense   : (amount : Nat) -> ATM.Command ()       Session      (const Session)
    Message    : String         -> ATM.Command ()       state        (const state)
    Pure       : (res : ty)     -> ATM.Command ty       (fn res)     fn
    (>>=)      
      :  ATM.Command a s1 s2f 
      -> ((res : a) -> ATM.Command b (s2f res) s3f) 
      -> ATM.Command b s1 s3f

  total
  atm : Command () Ready (const Ready)
  atm = do
    InsertCard
    pin      <- GetPIN
    cash     <- GetAmount
    Correct  <- CheckPIN pin | EjectCard -- <-- fails to typecheck here
    Dispense cash
    EjectCard

  total  
  testPIN : Vect 4 Char 
  testPIN = ['1', '2', '3', '4']
  
  total
  readVect : (n : Nat) -> IO (Vect n Char)
  readVect Z     = do
    discard <- getLine
    pure []  
  readVect (S k) = do
    ch  <- getChar
    chs <- readVect k
    pure (ch :: chs)

  total
  run : ATM.Command res inState outState_fn -> IO res
  run InsertCard = do
    putStrLn "Please insert your card (press enter)"
    x <- getLine
    pure ()
  run EjectCard = putStrLn "Card Ejected"
  run GetPIN    = do
    putStr "Enter PIN: "
    readVect 4
  run (CheckPIN pin) = if pin == testPIN
    then pure Correct
    else pure Incorrect 
  run GetAmount = do
    putStr "How much would you like? "
    x <- getLine
    pure (cast x)
  run (Dispense amount) = putStrLn ("Here is " ++ show amount)
  run (Message msg)     = putStrLn msg
  run (Pure res)        = pure res
  run (x >>= f)         = do x' <- run x ; run (f x')