@@ -0,0 +1,75 @@
1+module Main
2+
3+import Data.Vect.Quantifiers
4+import Decidable.Equality
5+
6+Cell : Nat -> Type
7+Cell n = Maybe (Fin n)
8+
9+data Board : Nat -> Type where
10+ MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
11+
12+emptyBoard : Board n
13+emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
14+
15+Empty : Cell n -> Type
16+Empty {n=n} x = (the (Cell n) Nothing) = x
17+
18+Filled : Cell n -> Type
19+Filled {n=n} = (\x => Not (Empty x))
20+
21+FullBoard : Board n -> Type
22+FullBoard (MkBoard b) = All (All Filled) b
23+
24+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)
25+indexStep = refl
26+
27+find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
28+ -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
29+find _ Nil = Left Nil
30+find d (x::xs) with (d x)
31+ | Yes prf = Right (x ** (prf, (fZ ** refl)))
32+ | No prf =
33+ case find d xs of
34+ Right (y ** (prf', (i ** prf''))) =>
35+ Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
36+ Left prf' => Left (prf::prf')
37+
38+empty : (cell : Cell n) -> Dec (Empty cell)
39+empty Nothing = Yes refl
40+empty (Just _) = No nothingNotJust
41+
42+findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
43+findEmptyInRow xs =
44+ case find {P=Empty} empty xs of
45+ Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
46+ Left p => Left p
47+
48+getCell : Board n -> (Fin n, Fin n) -> Cell n
49+getCell (MkBoard b) (x, y) = index x (index y b)
50+
51+emptyCell : {n : Nat} -> (b : Board n) ->
52+ Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))
53+emptyCell (MkBoard rs) =
54+ case helper rs of
55+ Left p => Left p
56+ Right (ri ** (ci ** pf2)) => Right ((ci, ri) ** pf2)
57+ where
58+ helper : (rs : Vect m (Vect n (Cell n)))
59+ -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))
60+ helper Nil = Left Nil
61+ helper (r::rs) =
62+ case findEmptyInRow r of
63+ Right (ci ** pf3) => Right (fZ ** (ci ** pf3))
64+ Left prf =>
65+ case helper rs of
66+ Left prf' => Left (prf::prf')
67+ Right (ri ** (ci ** pf4)) => Right (fS ri ** (ci ** pf4))
68+
69+
70+main : IO ()
71+main =
72+ case emptyCell (emptyBoard {n=0}) of
73+ Left _ => print "l"
74+ Right _ => print "r"
75+