86782e6 · Idris-dev · git.iko.soy

benchmarks/quasigroups/Main.idr+14−11

compare with master

unifiedsplit

@@ -10,15 +10,18 @@ main = do

10 case args of

11 [_, path] => do

12 f <- readFile path

13+ case f of

14+ Left _err => putStrLn $ "Error reading file: " ++ path

15+ Right f' =>

13− case parse f of

16+ case parse f' of

14− Left err => putStrLn err

17+ Left err => putStrLn err

15− Right (_ ** (board ** legal)) => do

18+ Right (_ ** (board ** legal)) => do

16− putStrLn "Got board:"

19+ putStrLn "Got board:"

17− printLn board

20+ printLn board

18− putStrLn "Solving..."

21+ putStrLn "Solving..."

19− case fillBoard board legal of

22+ case fillBoard board legal of

20− Nothing => putStrLn "No solution found"

23+ Nothing => putStrLn "No solution found"

21− Just (solved ** _) => do

24+ Just (solved ** _) => do

22− putStrLn "Solution found:"

25+ putStrLn "Solution found:"

23− printLn solved

26+ printLn solved

24 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

27 [self] => putStrLn ("Usage: " ++ self ++ " <board file>")

benchmarks/quasigroups/Parser.idr+3−2

@@ -1,6 +1,7 @@

1module Parser

2

3import Decidable.Equality

4+import Data.Vect

4

5

5import Solver

6import Solver

6

7

@@ -61,9 +62,9 @@ parseRows {n=S k} _ l rs = helper last l

61 step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

62 step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

62 step i l =

63 step i l =

63 let cs = fromList (words (index i rs)) in

64 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

65 No _ => Left "Row length not equal to column height"

66 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)

67

68

68 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

69 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

69 helper FZ l = step FZ l

70 helper FZ l = step FZ l

benchmarks/quasigroups/Solver.idr+3−2

@@ -2,6 +2,7 @@ module Solver

2

3import Decidable.Equality

4import Control.Monad.State

5+import Data.Vect

5import Data.Vect.Quantifiers

6import Data.Vect.Quantifiers

6

7

7%default total

8%default total

@@ -95,7 +96,7 @@ legalVal b (x, y) v =

95 case colSafe b x v of

96 case colSafe b x v of

96 No prf' => No (\(_, cf, _) => prf' cf)

97 No prf' => No (\(_, cf, _) => prf' cf)

97 Yes prf' =>

98 Yes prf' =>

98− case empty (getCell b (x, y)) of

99+ case Solver.empty (getCell b (x, y)) of

99 No prf'' => No (\(ef, _, _) => prf'' ef)

100 No prf'' => No (\(ef, _, _) => prf'' ef)

100 Yes prf'' => Yes (prf'', prf', prf)

101 Yes prf'' => Yes (prf'', prf', prf)

101

102

@@ -194,7 +195,7 @@ fillBoard {n=(S n)} b l with (emptyCell b)

194

195

195 %assert_total

196 %assert_total

196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

197− recurse start =

198+ recurse start =

198 case tryAll start of

199 case tryAll start of

199 (_, Nothing) => Nothing

200 (_, Nothing) => Nothing

200 (FZ, Just (b' ** l')) => fillBoard b' l'

201 (FZ, Just (b' ** l')) => fillBoard b' l'