@@ -0,0 +1,204 @@
1+module Solver
2+
3+import Decidable.Equality
4+import Control.Monad.State
5+import Data.Vect.Quantifiers
6+
7+%default total
8+
9+Cell : Nat -> Type
10+Cell n = Maybe (Fin n)
11+
12+data Board : Nat -> Type where
13+ MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
14+
15+emptyBoard : Board n
16+emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
17+
18+showElt : Cell n -> String
19+showElt Nothing = "."
20+showElt (Just x) = show (1 + (the Int (fromInteger (cast x))))
21+
22+-- FIXME: Inline type decl should not be necessary here
23+showRow : Vect n (Cell n) -> String
24+showRow {n=n} xs = unwords (toList (the (Vect n String) (map showElt xs)))
25+
26+unlines : Vect n String -> String
27+unlines Nil = ""
28+unlines (l::Nil) = l
29+unlines (l::ls) = pack (foldl addLine (unpack l) (map unpack ls))
30+ where
31+ addLine : List Char -> List Char -> List Char
32+ addLine w s = w ++ ('\n' :: s)
33+
34+instance Show (Board n) where
35+ show (MkBoard rs) = unlines (map showRow rs)
36+
37+updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a
38+updateAt fZ (x::xs) f = f x :: xs
39+updateAt (fS i) (x::xs) f = x :: updateAt i xs f
40+
41+setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n
42+setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))
43+
44+getCell : Board n -> (Fin n, Fin n) -> Cell n
45+getCell (MkBoard b) (x, y) = index x (index y b)
46+
47+anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
48+anyElim _ f (Here p) = f p
49+anyElim f _ (There p) = f p
50+
51+getRow : Fin n -> Board n -> Vect n (Cell n)
52+getRow i (MkBoard b) = index i b
53+
54+getCol : Fin n -> Board n -> Vect n (Cell n)
55+getCol i (MkBoard b) = helper i b
56+ where
57+ helper : Fin n -> Vect m (Vect n a) -> Vect m a
58+ helper _ Nil = Nil
59+ helper i (xs::xss) = index i xs :: helper i xss
60+
61+LegalNeighbors : Cell n -> Cell n -> Type
62+LegalNeighbors (Just x) (Just y) = Not (x = y)
63+LegalNeighbors _ _ = ()
64+
65+legalNeighbors : (x : Cell n) -> (y : Cell n) -> Dec (LegalNeighbors x y)
66+legalNeighbors (Just x) (Just y) with (decEq x y)
67+ | Yes prf = No (\pf => pf prf)
68+ | No prf = Yes prf
69+legalNeighbors Nothing (Just _) = Yes ()
70+legalNeighbors (Just _) Nothing = Yes ()
71+legalNeighbors Nothing Nothing = Yes ()
72+
73+rowSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getRow r b))
74+rowSafe b r v = all (legalNeighbors (Just v)) (getRow r b)
75+
76+colSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getCol r b))
77+colSafe b r v = all (legalNeighbors (Just v)) (getCol r b)
78+
79+Empty : Cell n -> Type
80+Empty {n=n} x = (the (Cell n) Nothing) = x
81+
82+empty : (cell : Cell n) -> Dec (Empty cell)
83+empty Nothing = Yes refl
84+empty (Just _) = No nothingNotJust
85+
86+-- Predicate for legal cell assignments
87+LegalVal : Board n -> (Fin n, Fin n) -> Fin n -> Type
88+LegalVal b (x, y) val = (Empty (getCell b (x, y)), All (LegalNeighbors (Just val)) (getCol x b), All (LegalNeighbors (Just val)) (getRow y b))
89+
90+legalVal : (b : Board n) -> (coord : (Fin n, Fin n)) -> (val : Fin n) -> Dec (LegalVal b coord val)
91+legalVal b (x, y) v =
92+ case rowSafe b y v of
93+ No prf => No (\(_, _, rf) => prf rf)
94+ Yes prf =>
95+ case colSafe b x v of
96+ No prf' => No (\(_, cf, _) => prf' cf)
97+ Yes prf' =>
98+ case empty (getCell b (x, y)) of
99+ No prf'' => No (\(ef, _, _) => prf'' ef)
100+ Yes prf'' => Yes (prf'', prf', prf)
101+
102+
103+Filled : Cell n -> Type
104+--Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work
105+Filled {n=n} = (\x => Not (Empty x))
106+--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> _|_
107+--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_
108+
109+filled : (cell : Cell n) -> Dec (Filled cell)
110+filled Nothing = No (\f => f refl)
111+filled (Just _) = Yes nothingNotJust
112+
113+FullBoard : Board n -> Type
114+FullBoard (MkBoard b) = All (All Filled) b
115+
116+fullBoard : (b : Board n) -> Dec (FullBoard b)
117+fullBoard (MkBoard b) = all (all filled) b
118+
119+fins : Vect n (Fin n)
120+fins {n=Z} = Nil
121+fins {n=(S m)} = last :: map weaken fins
122+
123+data LegalBoard : Board n -> Type where
124+ Base : LegalBoard (emptyBoard {n})
125+ Step : {b : Board n} -> {coords : (Fin n, Fin n)} -> {v : Fin n} -> LegalVal b coords v -> LegalBoard b -> LegalBoard (setCell b coords v)
126+
127+CompleteBoard : Board n -> Type
128+CompleteBoard b = (LegalBoard b, FullBoard b)
129+
130+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)
131+indexStep = refl
132+
133+find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
134+ -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
135+find _ Nil = Left Nil
136+find d (x::xs) with (d x)
137+ | Yes prf = Right (x ** (prf, (fZ ** refl)))
138+ | No prf =
139+ case find d xs of
140+ Right (y ** (prf', (i ** prf''))) =>
141+ Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
142+ Left prf' => Left (prf::prf')
143+
144+findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
145+findEmptyInRow xs =
146+ case find {P=Empty} empty xs of
147+ Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
148+ Left p => Left p
149+
150+emptyCell : (b : Board n) -> Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))
151+emptyCell (MkBoard rs) =
152+ case helper rs of
153+ Left p => Left p
154+ Right (ri ** (ci ** pf)) => Right ((ci, ri) ** pf)
155+ where
156+ helper : (rs : Vect m (Vect n (Cell n)))
157+ -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))
158+ helper Nil = Left Nil
159+ helper (r::rs) =
160+ case findEmptyInRow r of
161+ Right (ci ** pf) => Right (fZ ** (ci ** pf))
162+ Left prf =>
163+ case helper rs of
164+ Left prf' => Left (prf::prf')
165+ Right (ri ** (ci ** pf)) => Right (fS ri ** (ci ** pf))
166+
167+
168+tryValue : {b : Board (S n)} -> LegalBoard b -> (c : (Fin (S n), Fin (S n))) -> Empty (getCell b c) -> (v : Fin (S n))
169+ -> Either (Not (LegalVal b c v)) (b' : Board (S n) ** LegalBoard b')
170+tryValue {b=b} l c _ v =
171+ case legalVal b c v of
172+ No prf => Left prf
173+ Yes prf => Right (_ ** Step prf l)
174+
175+nullBoardFull : (b : Board Z) -> FullBoard b
176+nullBoardFull (MkBoard Nil) = Nil
177+
178+-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\3_2
179+fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')
180+fillBoard {n=Z} b l = Just (b ** (l, nullBoardFull b))
181+fillBoard {n=(S n)} b l with (emptyCell b)
182+ | Left full = Just (b ** (l, full))
183+ | Right (coords ** p) = recurse last
184+ where
185+ %assert_total
186+ tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))
187+ tryAll v = --trace ("Trying " ++ show (the Int (cast v))) $
188+ case tryValue l coords p v of
189+ Right success => (v, Just success)
190+ Left _ => -- TODO: Prove unsolvable
191+ case v of
192+ fS k => tryAll (weaken k)
193+ fZ => (v, Nothing)
194+
195+ %assert_total
196+ recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
197+ recurse start =
198+ case tryAll start of
199+ (_, Nothing) => Nothing
200+ (fZ, Just (b' ** l')) => fillBoard b' l'
201+ (fS next, Just (b' ** l')) =>
202+ case fillBoard b' l' of
203+ Just solution => Just solution
204+ Nothing => recurse (weaken next)