Guess.idr

import Data.Vect

data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkWordState : (word : String) ->
                   (missing : Vect letters Char) ->
                   WordState guesses_remaining letters

data Finished : Type where
     Lost : (game : WordState 0 (S letters)) -> Finished
     Won : (game : WordState (S guesses) 0) -> Finished

processGuess : (letter : Char) ->
               WordState (S guesses) (S letters) ->
               Either (WordState guesses (S letters))
               (WordState (S guesses) letters)

readGuess : IO Char

game' : WordState (S guesses) (S letters) -> IO Finished
game' st = do c <- readGuess
              case processGuess c st of
                   Left newst@(MkWordState {guesses_remaining = Z} _ _) =>
                     pure (Lost newst)
                   Left newst@(MkWordState {guesses_remaining = (S k)} _ _) =>
                     game' newst
                   Right newst@(MkWordState {letters = Z} _ _) =>
                     pure (Won newst)
                   Right newst@(MkWordState {letters = (S k)} _ _) =>
                     game' newst