@@ -2,7 +2,7 @@ module Solver
22
33import Decidable.Equality
44import Control.Monad.State
5−import Debug.Trace
5+import Data.Vect.Quantifiers
66
77%default total
88
@@ -17,7 +17,7 @@ emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
1717
1818showElt : Cell n -> String
1919showElt Nothing = "."
20−showElt (Just x) = show (1 + (the Int (cast x)))
20+showElt (Just x) = show (1 + (the Int (fromInteger (cast x))))
2121
2222showRow : Vect (Cell n) n -> String
2323showRow xs = unwords (toList (map showElt xs))
@@ -43,55 +43,10 @@ setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row
4343getCell : Board n -> (Fin n, Fin n) -> Cell n
4444getCell (MkBoard b) (x, y) = index x (index y b)
4545
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−
5446anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
5547anyElim _ f (Here p) = f p
5648anyElim f _ (There p) = f p
5749
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−
9550getRow : Fin n -> Board n -> Vect (Cell n) n
9651getRow i (MkBoard b) = index i b
9752
@@ -182,7 +137,7 @@ find d (x::xs) with (d x)
182137 | No prf =
183138 case find d xs of
184139 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'')))
186141 Left prf' => Left (prf::prf')
187142
188143findEmptyInRow : (xs : Vect (Cell n) n) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))