capitalex zrewidował ten Gist . Przejdź do rewizji
1 file changed, 134 insertions
ArithCmdDo.idr(stworzono plik)
| @@ -0,0 +1,134 @@ | |||
| 1 | + | module ArithCmdDo | |
| 2 | + | import Data.String | |
| 3 | + | import Data.Primitives.Views | |
| 4 | + | import Data.Bits | |
| 5 | + | import System | |
| 6 | + | import System.File | |
| 7 | + | %default total | |
| 8 | + | ||
| 9 | + | data Input = Answer Int | |
| 10 | + | | QuitCmd | |
| 11 | + | ||
| 12 | + | data Command : Type -> Type where | |
| 13 | + | PutStr : String -> Command () | |
| 14 | + | GetLine : Command String | |
| 15 | + | ReadFile : String -> Command (Either FileError String) | |
| 16 | + | WriteFile : String -> String -> Command (Either FileError Unit) | |
| 17 | + | ||
| 18 | + | Pure : ty -> Command ty | |
| 19 | + | Bind : Command a -> (a -> Command b) -> Command b | |
| 20 | + | Next : Command () -> Command b -> Command b | |
| 21 | + | ||
| 22 | + | data ConsoleIO : Type -> Type where | |
| 23 | + | Quit : a -> ConsoleIO a | |
| 24 | + | Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b | |
| 25 | + | Seq : Command () -> Inf (ConsoleIO b) -> ConsoleIO b | |
| 26 | + | ||
| 27 | + | namespace CommandDo | |
| 28 | + | export | |
| 29 | + | (>>=) : Command a -> (a -> Command b) -> Command b | |
| 30 | + | (>>=) = Bind | |
| 31 | + | ||
| 32 | + | export | |
| 33 | + | (>>) : Command () -> Command b -> Command b | |
| 34 | + | (>>) = Next | |
| 35 | + | ||
| 36 | + | namespace ConsoleDo | |
| 37 | + | export | |
| 38 | + | (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b | |
| 39 | + | (>>=) = Do | |
| 40 | + | ||
| 41 | + | export | |
| 42 | + | (>>) : Command () -> Inf (ConsoleIO b) -> ConsoleIO b | |
| 43 | + | (>>) = Seq | |
| 44 | + | ||
| 45 | + | totalReadLine : HasIO io => (file : String) -> io (Either FileError String) | |
| 46 | + | totalReadLine fileName | |
| 47 | + | = do Right file <- openFile fileName Read | |
| 48 | + | | Left e => pure (Left e) | |
| 49 | + | Right size <- fileSize file | |
| 50 | + | | Left e => do closeFile file | |
| 51 | + | pure (Left e) | |
| 52 | + | Right result <- fGetChars file size | |
| 53 | + | | Left e => do closeFile file | |
| 54 | + | pure (Left e) | |
| 55 | + | pure (Right result) | |
| 56 | + | ||
| 57 | + | ||
| 58 | + | runCommand : Command a -> IO a | |
| 59 | + | runCommand (PutStr str) | |
| 60 | + | = putStr str | |
| 61 | + | runCommand GetLine | |
| 62 | + | = getLine | |
| 63 | + | runCommand (ReadFile file) | |
| 64 | + | = totalReadLine file | |
| 65 | + | runCommand (WriteFile file contents) | |
| 66 | + | = writeFile file contents | |
| 67 | + | runCommand (Pure val) | |
| 68 | + | = pure val | |
| 69 | + | runCommand (Bind c f) | |
| 70 | + | = do res <- runCommand c | |
| 71 | + | runCommand (f res) | |
| 72 | + | runCommand (Next c f) | |
| 73 | + | = do res <- runCommand c | |
| 74 | + | runCommand f | |
| 75 | + | ||
| 76 | + | ||
| 77 | + | readInput : (prompt : String) -> Command Input | |
| 78 | + | readInput prompt = do PutStr prompt | |
| 79 | + | answer <- GetLine | |
| 80 | + | case (toLower answer == "quit") of | |
| 81 | + | True => Pure QuitCmd | |
| 82 | + | False => Pure (Answer (cast answer)) | |
| 83 | + | ||
| 84 | + | ||
| 85 | + | ||
| 86 | + | run : Fuel -> ConsoleIO a -> IO (Maybe a) | |
| 87 | + | run Dry _ = pure Nothing | |
| 88 | + | run (More fuel) (Quit result) = pure (Just result) | |
| 89 | + | run (More fuel) (Do c f) = do res <- runCommand c; run fuel (f res) | |
| 90 | + | run (More fuel) (Seq c f) = do runCommand c; run fuel f | |
| 91 | + | ||
| 92 | + | ||
| 93 | + | mutual | |
| 94 | + | correct : (nums : Stream Int) -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) | |
| 95 | + | correct nums score count | |
| 96 | + | = do PutStr "Correct!\n" | |
| 97 | + | quiz nums (score + 1) (count + 1) | |
| 98 | + | ||
| 99 | + | wrong : (nums : Stream Int) -> (ans : Int) -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) | |
| 100 | + | wrong nums ans score count | |
| 101 | + | = do PutStr ("Wrong, the anwser is " ++ show ans ++ "\n") | |
| 102 | + | quiz nums score (count + 1) | |
| 103 | + | ||
| 104 | + | quiz : Stream Int -> (score : Nat) -> (count : Nat) -> ConsoleIO (Nat, Nat) | |
| 105 | + | quiz (num1 :: num2 :: nums) score count | |
| 106 | + | = do PutStr ("Score so far: " ++ show score ++ " / " ++ show count ++ "\n") | |
| 107 | + | input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ") | |
| 108 | + | case input of | |
| 109 | + | Answer answer => if answer == num1 * num2 | |
| 110 | + | then correct nums score count | |
| 111 | + | else wrong nums (num1 * num2) score count | |
| 112 | + | QuitCmd => Quit (score, count) | |
| 113 | + | ||
| 114 | + | randoms : Int -> Stream Int | |
| 115 | + | randoms seed = | |
| 116 | + | let | |
| 117 | + | seed' = 1664525 * seed + 1013904223 | |
| 118 | + | in | |
| 119 | + | (seed' `shiftR` 2) :: randoms seed' | |
| 120 | + | ||
| 121 | + | ||
| 122 | + | arithInputs : Int -> Stream Int | |
| 123 | + | arithInputs seed = map bound (randoms seed) | |
| 124 | + | where | |
| 125 | + | bound : Int -> Int | |
| 126 | + | bound num with (divides num 12) | |
| 127 | + | bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1 | |
| 128 | + | ||
| 129 | + | partial | |
| 130 | + | main1 : IO () | |
| 131 | + | main1 = do seed <- time | |
| 132 | + | Just (score, count) <- run forever (quiz (arithInputs (fromInteger seed)) 0 0) | |
| 133 | + | | Nothing => putStrLn "Ran out of fuel" | |
| 134 | + | putStrLn ("Final score: " ++ show score ++ " / " ++ show count) | |
Nowsze
Starsze