ArithCmdDo.idr - Opengist

修订 e820f0e5753d5a1b1ca6b7cebb6d02b9d53553b2

ArithCmdDo.idr · 4.1 KiB · Idris 原始文件 Playground

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)

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)