git.iko.soy/Idris-dev
on master help sign in
Update for idris 0.9.8.1
4fcacceBenjamin Saunders
Parser.idr+4−3
compare with master
unifiedsplit
@@ -39,12 +39,13 @@ parseCols {n=S k} row l cs = helper last l
39 where
39 where
40 step : {b : Board (S k)} -> LegalBoard b -> Fin (S k) -> Parser (S k)
40 step : {b : Board (S k)} -> LegalBoard b -> Fin (S k) -> Parser (S k)
41 step {b=b} l x = do
41 step {b=b} l x = do
42+ let here = (x, row) -- TODO: Determine why naming this makes idris smarter
42 tok <- parseToken {n=S k} (index x cs)
43 tok <- parseToken {n=S k} (index x cs)
43 case tok of
44 case tok of
44 Nothing => return (_ ** l)
45 Nothing => return (_ ** l)
45− Just val =>
46+ Just t =>
46− case legalVal b (x, row) val of
47+ case legalVal b here t of
47− Yes prf => return (_ ** Step prf l)
48+ Yes prf => Right (_ ** Step prf l)
48 No _ => Left ("Illegal cell " ++ index x cs)
49 No _ => Left ("Illegal cell " ++ index x cs)
49
50
50 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
51 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
Solver.idr+3−48
@@ -2,7 +2,7 @@ module Solver
2
2
3import Decidable.Equality
3import Decidable.Equality
4import Control.Monad.State
4import Control.Monad.State
5−import Debug.Trace
5+import Data.Vect.Quantifiers
6
6
7%default total
7%default total
8
8
@@ -17,7 +17,7 @@ emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
17
17
18showElt : Cell n -> String
18showElt : Cell n -> String
19showElt Nothing = "."
19showElt Nothing = "."
20−showElt (Just x) = show (1 + (the Int (cast x)))
20+showElt (Just x) = show (1 + (the Int (fromInteger (cast x))))
21
21
22showRow : Vect (Cell n) n -> String
22showRow : Vect (Cell n) n -> String
23showRow xs = unwords (toList (map showElt xs))
23showRow xs = unwords (toList (map showElt xs))
@@ -43,55 +43,10 @@ setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row
43getCell : Board n -> (Fin n, Fin n) -> Cell n
43getCell : Board n -> (Fin n, Fin n) -> Cell n
44getCell (MkBoard b) (x, y) = index x (index y b)
44getCell (MkBoard b) (x, y) = index x (index y b)
45
45
46−data Any : (P : a -> Type) -> Vect a n -> Type where
47− Here : {P : a -> Type} -> {xs : Vect a n} -> P x -> Any P (x :: xs)
48− There : {P : a -> Type} -> {xs : Vect a n} -> Any P xs -> Any P (x :: xs)
49−
50−anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
51−anyNilAbsurd Here impossible
52−anyNilAbsurd There impossible
53−
54anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
46anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
55anyElim _ f (Here p) = f p
47anyElim _ f (Here p) = f p
56anyElim f _ (There p) = f p
48anyElim f _ (There p) = f p
57
49
58−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (Any P xs)
59−any _ Nil = No anyNilAbsurd
60−any p (x::xs) with (p x)
61− | Yes prf = Yes (Here prf)
62− | No prf =
63− case any p xs of
64− Yes prf' => Yes (There prf')
65− No prf' => No (anyElim prf' prf)
66−
67−Not : Type -> Type
68−Not a = a -> _|_
69−
70−data All : (P : a -> Type) -> Vect a n -> Type where
71− Nil : {P : a -> Type} -> All P Nil
72− (::) : {P : a -> Type} -> {xs : Vect a n} -> P x -> All P xs -> All P (x :: xs)
73−
74−negAnyAll : {P : a -> Type} -> {xs : Vect a n} -> Not (Any P xs) -> All (\x => Not (P x)) xs
75−negAnyAll {xs=Nil} _ = Nil
76−negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
77−
78−notAllHere : {P : a -> Type} -> {xs : Vect a n} -> (P x -> _|_) -> All P (x :: xs) -> _|_
79−notAllHere _ Nil impossible
80−notAllHere np (p :: _) = np p
81−
82−notAllThere : {P : a -> Type} -> {xs : Vect a n} -> (All P xs -> _|_) -> All P (x :: xs) -> _|_
83−notAllThere _ Nil impossible
84−notAllThere np (_ :: ps) = np ps
85−
86−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)
87−all _ Nil = Yes Nil
88−all d (x::xs) with (d x)
89− | No prf = No (notAllHere prf)
90− | Yes prf =
91− case all d xs of
92− Yes prf' => Yes (prf :: prf')
93− No prf' => No (notAllThere prf')
94−
95getRow : Fin n -> Board n -> Vect (Cell n) n
50getRow : Fin n -> Board n -> Vect (Cell n) n
96getRow i (MkBoard b) = index i b
51getRow i (MkBoard b) = index i b
97
52
@@ -182,7 +137,7 @@ find d (x::xs) with (d x)
182 | No prf =
137 | No prf =
183 case find d xs of
138 case find d xs of
184 Right (y ** (prf', (i ** prf''))) =>
139 Right (y ** (prf', (i ** prf''))) =>
185− Right (y ** (prf', (fS i ** replace (indexStep {x=x}) prf'')))
140+ Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
186 Left prf' => Left (prf::prf')
141 Left prf' => Left (prf::prf')
187
142
188findEmptyInRow : (xs : Vect (Cell n) n) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
143findEmptyInRow : (xs : Vect (Cell n) n) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))