module MysteryWord2

import Effects
import Data.Vect
-- import Effect.System
import Effect.StdIO
-- import Effect.Random

-- import Data.So

%access public export

letters : String -> List Char
letters str = ltrs [] $ unpack str where
  ltrs : List Char -> List Char -> List Char
  ltrs acc []     = acc
  ltrs acc (c::cs) = ltrs (c::(filter (/=c) acc)) cs

data GState : Type where
  Running : Nat -> Nat -> GState
  NotRunning : GState

data Mystery : GState -> Type where
  Init : Mystery NotRunning
  GameWon : (word : String) -> Mystery NotRunning
  GameLost : (word : String) -> Mystery NotRunning
  MkG : (word : String) ->
        (guesses : Nat) ->
        (got : List Char) ->
        (left : Vect m Char) ->
        Mystery (Running guesses m)

data MysteryRules : Effect where
  Guess : (c : Char) -> sig MysteryRules Bool 
                               (Mystery $ Running (S gss) (S lts))
                               (\inword => if inword 
                                           then (Mystery $ Running (S gss) lts)
                                           else (Mystery $ Running gss (S lts)))
  Won : sig MysteryRules () (Mystery $ Running gss Z) (Mystery NotRunning)
  Lost : sig MysteryRules () (Mystery $ Running Z lts) (Mystery NotRunning)
  NewWord : (word : String) -> sig MysteryRules () (Mystery NotRunning) (Mystery $ Running 6 (length (letters word)))
  Get : sig MysteryRules String (Mystery h)

MYSTERY : GState -> EFFECT
MYSTERY h = MkEff (Mystery h) MysteryRules

initState : (word : String) -> Mystery (Running 6 (length $ letters word))
initState word = MkG word 6 [] (fromList $ letters word)

Show (Mystery h) where
  show Init = "Game is not started yet"
  show (GameWon word) = "Congratulations. You won. Word was " ++ word
  show (GameLost word) = "You lose. Word was " ++ word
  show (MkG word guesses got left) 
       = "Current state is (word: " ++ word ++
         ", guesses: " ++ show guesses ++
         ", got: " ++ show got ++
         ", left: " ++ show left

Handler MysteryRules m where
  handle (MkG word (S guesses) got left) (Guess c) k 
    = case isElem c left of
      (Yes prf) => k True $ MkG word _ (c :: got) (dropElem left prf)
      (No contra) => k False $ MkG word _ got left
  handle (MkG word gss got []) Won k = k () $ GameWon word
  handle (MkG word Z got left) Lost k = k () $ GameLost word
  handle res (NewWord word) k = k () $ initState word
  handle res Get k = k (show res) res
  
words : Vect 10 String
words = ["idris","agda","haskell","miranda",
         "java","javascript","fortran","basic",
         "coffeescript","rust"]

-- use this definition to see the problem
-- game : Eff () [STDIO, MYSTERY (Running (S g) w)]
--               [STDIO, MYSTERY NotRunning]
game : Eff () [MYSTERY (Running (S g) w), STDIO]
              [MYSTERY NotRunning, STDIO]
game {w=Z} = call Won
game {w=S _}
     = do putStrLn !(call Get)
          putStr "Enter guess: "
          let guess = unpack $ trim !getStr
          case nonEmpty guess of
               (Yes prf) => processGuess (Prelude.List.head guess)
               (No contra) => do putStrLn "Invalid input!"
                                 game
  where
    processGuess : Char -> Eff () [MYSTERY (Running (S g) (S w)), STDIO]
                                  [MYSTERY NotRunning, STDIO]
    processGuess {g} {w} c
      = case !(call $ MysteryWord2.Guess c) of
             True => do putStrLn "Good guess!"
                        case w of
                             Z => call Won
                             (S k) => game
             False => do putStrLn "No, sorry"
                         case g of
                              Z => call Lost
                              (S k) => game

-- runGame : Eff () [STDIO, MYSTERY NotRunning]
-- runGame = 
--   do -- srand !time
--      let w = Data.Vect.index 2 words
--      call $ NewWord w
--      game
--      putStrLn !(call Get)



-- Local Variables:
-- idris-load-packages: ("effects")
-- End: