git.iko.soy/Idris-dev
on master help sign in
Fix quasigroups compile time issues
commit86782e6226382280deae141dead2b7423b91fc6a authorPaul Koerbitz <p.koerbitz@smartreporting.de> dateSun 3 Jan 2016, 13:23 (11 years ago) parentbccb453
3 files changed+20−15
compare with master
unifiedsplit
benchmarks/quasigroups/Main.idr+14−11 benchmarks/quasigroups/Parser.idr+3−2 benchmarks/quasigroups/Solver.idr+3−2
benchmarks/quasigroups/Main.idr+14−11
@@ -10,15 +10,18 @@ main = do
1010 case args of
1111 [_, path] => do
1212 f <- readFile path
13− case parse f of
14− Left err => putStrLn err
15− Right (_ ** (board ** legal)) => do
16− putStrLn "Got board:"
17− printLn board
18− putStrLn "Solving..."
19− case fillBoard board legal of
20− Nothing => putStrLn "No solution found"
21− Just (solved ** _) => do
22− putStrLn "Solution found:"
23− printLn solved
13+ case f of
14+ Left _err => putStrLn $ "Error reading file: " ++ path
15+ Right f' =>
16+ case parse f' of
17+ Left err => putStrLn err
18+ Right (_ ** (board ** legal)) => do
19+ putStrLn "Got board:"
20+ printLn board
21+ putStrLn "Solving..."
22+ case fillBoard board legal of
23+ Nothing => putStrLn "No solution found"
24+ Just (solved ** _) => do
25+ putStrLn "Solution found:"
26+ printLn solved
2427 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")
benchmarks/quasigroups/Parser.idr+3−2
@@ -1,6 +1,7 @@
11module Parser
22
33import Decidable.Equality
4+import Data.Vect
45
56import Solver
67
@@ -61,9 +62,9 @@ parseRows {n=S k} _ l rs = helper last l
6162 step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
6263 step i l =
6364 let cs = fromList (words (index i rs)) in
64− case decEq (length cs) (S k) of
65+ case decEq (Parser.length cs) (S k) of
6566 No _ => Left "Row length not equal to column height"
66− Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed
67+ Yes prf => parseCols i l (replace {P=\n => Vect n String} prf cs)
6768
6869 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
6970 helper FZ l = step FZ l
benchmarks/quasigroups/Solver.idr+3−2
@@ -2,6 +2,7 @@ module Solver
22
33import Decidable.Equality
44import Control.Monad.State
5+import Data.Vect
56import Data.Vect.Quantifiers
67
78%default total
@@ -95,7 +96,7 @@ legalVal b (x, y) v =
9596 case colSafe b x v of
9697 No prf' => No (\(_, cf, _) => prf' cf)
9798 Yes prf' =>
98− case empty (getCell b (x, y)) of
99+ case Solver.empty (getCell b (x, y)) of
99100 No prf'' => No (\(ef, _, _) => prf'' ef)
100101 Yes prf'' => Yes (prf'', prf', prf)
101102
@@ -194,7 +195,7 @@ fillBoard {n=(S n)} b l with (emptyCell b)
194195
195196 %assert_total
196197 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
197− recurse start =
198+ recurse start =
198199 case tryAll start of
199200 (_, Nothing) => Nothing
200201 (FZ, Just (b' ** l')) => fillBoard b' l'