Like 0
Fork 0

Last active 7 months ago

capitalex's Avatar capitalex revised this gist 7 months ago. Go to revision

1 file changed, 134 insertions

ArithCmdDo.idr(file created)

@@ -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)
Newer Older

Powered by Opengist ⋅ Load: 17ms⋅

English