Ch14 Verified Guessing Game

gggist.idr

module Main

import Data.Vect

namespace Game

  data State : Type where
    NotRunning : State
    Running    : (guesses : Nat) -> (letters : Nat) -> State
    
  total
  letters : String -> List Char
  letters str = nub (map toUpper (unpack str))
  
  total
  beginGame : String -> (a -> State)
  beginGame word = const (Running 6 (length (letters word)))

  total  
  endGame : (a -> State)
  endGame = const NotRunning
  
  total
  losing : Nat -> State
  losing guesses = Running 0 (S guesses)
  
  total
  winning : Nat -> State
  winning guesses = Running (S guesses) 0
  
  total
  playing : Nat -> Nat -> State
  playing guesses letters = Running (S guesses) (S letters)
  
  data GuessResult
    = Correct
    | Incorrect
  
  total
  tryGuess : Nat -> Nat -> GuessResult -> State
  tryGuess guesses letters Correct   = Running (S guesses) letters
  tryGuess guesses letters Incorrect = Running guesses     (S letters)

  
  data Command
    :  (ty : Type) 
    -> State 
    -> (ty -> State) 
    -> Type
  where
    NewGame : (word : String) -> Command ()          NotRunning                beginGame
    Won     :                    Command ()          (winning guesses)         endGame
    Lost    :                    Command ()          (losing  guesses)         endGame
    Guess   : (c : Char)      -> Command GuessResult (playing guesses letters) (tryGuess guesses letters)
    Pure    : (res : ty)      -> Command ty          (state_fn res)            state_fn
    Show    :                    Command ()          state                     (const state)
    Message : String          -> Command ()          state                     (const state)
    Read    :                    Command Char        state                     (const state)
    (>>=)
      :  (Command a s1 s2f)
      -> ((res : a) -> Command b (s2f res) s3f)
      -> Command b s1 s3f
  

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

  namespace Loop
    data Loop
      :  (ty : Type) 
      -> State 
      -> (ty -> State)
      -> Type
    where
      (>>=) 
        :  Command a s1 s2f 
        -> ((res : a) -> Inf (Loop b (s2f res) s3f))
        -> Loop b s1 s3f
      Exit : Loop () NotRunning endGame
        
    loop : Loop () (playing guesses letters) endGame
    loop {guesses} {letters} = do
      Show
      g  <- Read
      ok <- Guess g
      case ok of
        Correct => case letters of
          Z => do
            Won
            Show
            Exit
          S k => do
            Message "Correct"
            loop
        Incorrect => case guesses of
          Z => do
            Lost
            Show
            Exit
          (S k) => do
            Message "Incorrect"
            loop

  data Game : State -> Type where
    Start : Game NotRunning
    Win   : (word : String) -> Game NotRunning
    Loss  : (word : String) -> Game NotRunning
    InProgress 
      :  (word : String) 
      -> (guesses : Nat) 
      -> (missing : Vect letters Char) 
      -> Game (Running guesses letters)

  Show (Game g) where
    show Start                             = "Starting"
    show (Win        word)                 = "Win:  word was " ++ word
    show (Loss       word)                 = "Loss: word was " ++ word
    show (InProgress word guesses missing) =
      "\n" 
      ++ pack (map (hideMissing) (unpack word))
      ++ "\n"
      ++ show guesses
      ++ " guesses remain"
    where
      hideMissing : Char -> Char
      hideMissing c = if c `elem` missing then '-' else c
      
  data Result
    :  (ty  : Type)
    -> (ty -> State)
    -> Type
  where
    OK        
      :  (res : ty)
      -> Game (outstate_fn res) 
      -> Result ty outstate_fn
    OutOfFuel : Result ty outstate_fn

  data Fuel = Dry | More (Lazy Fuel)
  
  ok : (res : ty) -> Game (outstate_fn res) -> IO (Result ty outstate_fn)
  ok res st = pure (OK res st)
  
  runCmd 
    :  Fuel
    -> Game instate
    -> Command ty instate outstate_fn
    -> IO (Result ty outstate_fn)
  
  run 
    :  Fuel 
    -> Game instate
    -> Loop ty instate outstate_fn
    -> IO (Result ty outstate_fn)
  run Dry _ _ = pure OutOfFuel
  run (More fuel) st (cmd >>= next) = do
    OK cmdRes newSt <- runCmd fuel st cmd | OutOfFuel => pure OutOfFuel
    run fuel newSt (next cmdRes)
  run (More fuel) st Exit = ok () st