module ArithCmdDo import Data.String import Data.Primitives.Views import Data.Bits import System import System.File %default total data Input = Answer Int | QuitCmd data Command : Type -> Type where PutStr : String -> Command () GetLine : Command String ReadFile : String -> Command (Either FileError String) WriteFile : String -> String -> Command (Either FileError Unit) Pure : ty -> Command ty Bind : Command a -> (a -> Command b) -> Command b Next : Command () -> Command b -> Command b data ConsoleIO : Type -> Type where Quit : a -> ConsoleIO a Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b Seq : Command () -> Inf (ConsoleIO b) -> ConsoleIO b namespace CommandDo export (>>=) : Command a -> (a -> Command b) -> Command b (>>=) = Bind export (>>) : Command () -> Command b -> Command b (>>) = Next namespace ConsoleDo export (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b (>>=) = Do export (>>) : Command () -> Inf (ConsoleIO b) -> ConsoleIO b (>>) = Seq totalReadLine : HasIO io => (file : String) -> io (Either FileError String) totalReadLine fileName = do Right file <- openFile fileName Read | Left e => pure (Left e) Right size <- fileSize file | Left e => do closeFile file pure (Left e) Right result <- fGetChars file size | Left e => do closeFile file pure (Left e) pure (Right result) runCommand : Command a -> IO a runCommand (PutStr str) = putStr str runCommand GetLine = getLine runCommand (ReadFile file) = totalReadLine file runCommand (WriteFile file contents) = writeFile file contents runCommand (Pure val) = pure val runCommand (Bind c f) = do res <- runCommand c runCommand (f res) runCommand (Next c f) = do res <- runCommand c runCommand f readInput : (prompt : String) -> Command Input readInput prompt = do PutStr prompt answer <- GetLine case (toLower answer == "quit") of True => Pure QuitCmd False => Pure (Answer (cast answer)) run : Fuel -> ConsoleIO a -> IO (Maybe a) run Dry _ = pure Nothing run (More fuel) (Quit result) = pure (Just result) run (More fuel) (Do c f) = do res <- runCommand c; run fuel (f res) run (More fuel) (Seq c f) = do runCommand c; run fuel f mutual correct : (nums : Stream Int) -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) correct nums score count = do PutStr "Correct!\n" quiz nums (score + 1) (count + 1) wrong : (nums : Stream Int) -> (ans : Int) -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) wrong nums ans score count = do PutStr ("Wrong, the anwser is " ++ show ans ++ "\n") quiz nums score (count + 1) quiz : Stream Int -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) quiz (num1 :: num2 :: nums) score count = do PutStr ("Score so far: " ++ show score ++ " / " ++ show count ++ "\n") input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ") case input of Answer answer => if answer == num1 * num2 then correct nums score count else wrong nums (num1 * num2) score count QuitCmd => Quit (score, count) randoms : Int -> Stream Int randoms seed = let seed' = 1664525 * seed + 1013904223 in (seed' `shiftR` 2) :: randoms seed' arithInputs : Int -> Stream Int arithInputs seed = map bound (randoms seed) where bound : Int -> Int bound num with (divides num 12) bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1 partial main1 : IO () main1 = do seed <- time Just (score, count) <- run forever (quiz (arithInputs (fromInteger seed)) 0 0) | Nothing => putStrLn "Ran out of fuel" putStrLn ("Final score: " ++ show score ++ " / " ++ show count)