git.iko.soy/Idris-dev
on master help sign in
Basic solver working
commitca7d80a9f59c063ae8b0aae7e869f8790162f4e7 authorBenjamin Saunders <besaunde@sfu.ca> dateMon 8 Apr 2013, 17:16 (14 years ago)
5 files changed+378
compare with master
unifiedsplit
Complete.idr+25 EmptyTest.idr+14 ParseTest.idr+16 Parser.idr+75 Solver.idr+248
Complete.idrnew file+25
@@ -0,0 +1,25 @@
1+module Main
2+
3+import System
4+import Parser
5+import Solver
6+
7+main : IO ()
8+main = do
9+ args <- getArgs
10+ case args of
11+ [_, path] => do
12+ putStrLn ("Reading " ++ path)
13+ f <- readFile path
14+ case parse f of
15+ Left err => putStrLn err
16+ Right (_ ** (board ** legal)) => do
17+ putStrLn "Got board:"
18+ print board
19+ putStrLn "Solving..."
20+ case fillBoard board legal of
21+ Nothing => putStrLn "No solution found"
22+ Just (solved ** _) => do
23+ putStrLn "Solution found:"
24+ print solved
25+ _ => putStrLn "Expected path"
EmptyTest.idrnew file+14
@@ -0,0 +1,14 @@
1+module Main
2+
3+import Solver
4+
5+step : Nat -> IO ()
6+step n = do
7+ putStrLn $
8+ case fillBoard {n=n} emptyBoard Base of
9+ Just xs => ("Solved " <+> show (the Int (cast n)) <+> "^2:\n" <+> show (getWitness xs))
10+ Nothing => ("Failed to solve " <+> show (the Int (cast n)) <+> "^2")
11+ step (S n)
12+
13+main : IO ()
14+main = step 0
ParseTest.idrnew file+16
@@ -0,0 +1,16 @@
1+module Main
2+
3+import Parser
4+import System
5+
6+main : IO ()
7+main = do
8+ args <- getArgs
9+ case args of
10+ [_, path] => do
11+ putStrLn ("Reading " ++ path)
12+ f <- readFile path
13+ case parse f of
14+ Left err => putStrLn err
15+ Right (size ** (board ** _)) => putStrLn ("Got board:\n" ++ show board)
16+ _ => putStrLn "Expected path"
Parser.idrnew file+75
@@ -0,0 +1,75 @@
1+module Parser
2+
3+import Decidable.Equality
4+
5+import Solver
6+
7+ParseErr : Type
8+ParseErr = String
9+
10+Parser : Nat -> Type
11+Parser n = Either ParseErr (b : Board n ** LegalBoard b)
12+
13+mapM : Monad m => (a -> m b) -> Vect a n -> m (Vect b n)
14+mapM _ Nil = return Vect.Nil
15+mapM f (x::xs) = do
16+ x' <- f x
17+ xs' <- mapM f xs
18+ return (Vect.(::) x' xs')
19+
20+parseToken : String -> Either String (Cell n)
21+parseToken "." = return Nothing
22+parseToken "0" = Left "Got cell 0, expected 1-based numbering"
23+parseToken x = fmap Just (tryParseFin ((cast x) - 1))
24+ where
25+ tryParseFin : Int -> Either String (Fin n)
26+ tryParseFin {n=O} _ = Left ("Given cell " ++ x ++ " out of range")
27+ tryParseFin {n=S k} 0 = return fO
28+ tryParseFin {n=S k} x =
29+ case tryParseFin {n=k} (x-1) of
30+ Left err => Left err
31+ Right fin => return (fS fin)
32+
33+length : Vect a n -> Nat
34+length {n=n} _ = n
35+
36+parseCols : {b : Board n} -> Fin n -> LegalBoard b -> Vect String n -> Parser n
37+parseCols {n=O} _ l _ = Right (_ ** l)
38+parseCols {n=S k} row l cs = helper last l
39+ where
40+ step : {b : Board (S k)} -> LegalBoard b -> Fin (S k) -> Parser (S k)
41+ step {b=b} l x = do
42+ tok <- parseToken (index x cs)
43+ case legalVal b (x, row) tok of
44+ Yes prf => return (_ ** Step prf l)
45+ No _ => Left ("Illegal cell " ++ index x cs)
46+
47+ helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
48+ helper fO l = step l fO
49+ helper (fS k) l = do
50+ (_ ** next) <- step l (fS k)
51+ helper (weaken k) next
52+
53+parseRows : (b : Board n) -> LegalBoard b -> Vect String n -> Parser n
54+parseRows {n=O} _ l _ = Right (_ ** l)
55+parseRows {n=S k} _ l rs = helper last l
56+ where
57+ step : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
58+ step i l =
59+ let cs = fromList (words (index i rs)) in
60+ case decEq (length cs) (S k) of
61+ No _ => Left "Row length not equal to column height"
62+ Yes prf => parseCols i l (replace prf cs)
63+
64+ helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
65+ helper fO l = step fO l
66+ helper (fS k) l = do
67+ (_ ** next) <- step (fS k) l
68+ helper (weaken k) next
69+
70+parse : String -> Either String (n : Nat ** (b : Board n ** LegalBoard b))
71+parse str =
72+ let rows = fromList (lines str) in
73+ case parseRows {n=length rows} emptyBoard Base rows of
74+ Left msg => Left msg
75+ Right board => return (_ ** board)
Solver.idrnew file+248
@@ -0,0 +1,248 @@
1+module Solver
2+
3+import Decidable.Equality
4+import Control.Monad.State
5+import Debug.Trace
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 (Vect (Cell n) n) 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 (cast x)))
21+
22+showRow : Vect (Cell n) n -> String
23+showRow xs = unwords (toList (map showElt xs))
24+
25+unlines : Vect String n -> String
26+unlines Nil = ""
27+unlines (l::Nil) = l
28+unlines (l::ls) = pack (foldl addLine (unpack l) (map unpack ls))
29+ where
30+ addLine : List Char -> List Char -> List Char
31+ addLine w s = w ++ ('\n' :: s)
32+
33+instance Show (Board n) where
34+ show (MkBoard rs) = unlines (map showRow rs)
35+
36+updateAt : Fin n -> Vect a n -> (a -> a) -> Vect a n
37+updateAt fO (x::xs) f = f x :: xs
38+updateAt (fS i) (x::xs) f = x :: updateAt i xs f
39+
40+setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n
41+setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row (const (Just value))))
42+
43+getCell : Board n -> (Fin n, Fin n) -> Cell n
44+getCell (MkBoard b) (x, y) = index x (index y b)
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+
54+anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
55+anyElim _ f (Here p) = f p
56+anyElim f _ (There p) = f p
57+
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+
95+getRow : Fin n -> Board n -> Vect (Cell n) n
96+getRow i (MkBoard b) = index i b
97+
98+getCol : Fin n -> Board n -> Vect (Cell n) n
99+getCol i (MkBoard b) = helper i b
100+ where
101+ helper : Fin n -> Vect (Vect a n) m -> Vect a m
102+ helper _ Nil = Nil
103+ helper i (xs::xss) = index i xs :: helper i xss
104+
105+LegalNeighbors : Cell n -> Cell n -> Type
106+LegalNeighbors (Just x) (Just y) = Not (x = y)
107+LegalNeighbors _ _ = ()
108+
109+legalNeighbors : (x : Cell n) -> (y : Cell n) -> Dec (LegalNeighbors x y)
110+legalNeighbors (Just x) (Just y) with (decEq x y)
111+ | Yes prf = No (\pf => pf prf)
112+ | No prf = Yes prf
113+legalNeighbors Nothing (Just _) = Yes ()
114+legalNeighbors (Just _) Nothing = Yes ()
115+legalNeighbors Nothing Nothing = Yes ()
116+
117+rowSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getRow r b))
118+rowSafe b r v = all (legalNeighbors (Just v)) (getRow r b)
119+
120+colSafe : (b : Board n) -> (r : Fin n) -> (val : Fin n) -> Dec (All (LegalNeighbors (Just val)) (getCol r b))
121+colSafe b r v = all (legalNeighbors (Just v)) (getCol r b)
122+
123+Empty : Cell n -> Type
124+Empty {n=n} x = (the (Cell n) Nothing) = x
125+
126+empty : (cell : Cell n) -> Dec (Empty cell)
127+empty Nothing = Yes refl
128+empty (Just _) = No nothingNotJust
129+
130+-- Predicate for legal cell assignments
131+LegalVal : Board n -> (Fin n, Fin n) -> Fin n -> Type
132+LegalVal b (x, y) val = (Empty (getCell b (x, y)), All (LegalNeighbors (Just val)) (getCol x b), All (LegalNeighbors (Just val)) (getRow y b))
133+
134+legalVal : (b : Board n) -> (coord : (Fin n, Fin n)) -> (val : Fin n) -> Dec (LegalVal b coord val)
135+legalVal b (x, y) v =
136+ case rowSafe b y v of
137+ No prf => No (\(_, _, rf) => prf rf)
138+ Yes prf =>
139+ case colSafe b x v of
140+ No prf' => No (\(_, cf, _) => prf' cf)
141+ Yes prf' =>
142+ case empty (getCell b (x, y)) of
143+ No prf'' => No (\(ef, _, _) => prf'' ef)
144+ Yes prf'' => Yes (prf'', prf', prf)
145+
146+
147+Filled : Cell n -> Type
148+--Filled {n=n} x = Not (Empty x) -- TODO: Find out why this doesn't work
149+Filled {n=n} = (\x => Not (Empty x))
150+--Filled {n=n} x = the (Maybe (Fin n)) Nothing = x -> _|_
151+--Filled {n=n} = \x => the (Maybe (Fin n)) Nothing = x -> _|_
152+
153+filled : (cell : Cell n) -> Dec (Filled cell)
154+filled Nothing = No (\f => f refl)
155+filled (Just _) = Yes nothingNotJust
156+
157+FullBoard : Board n -> Type
158+FullBoard (MkBoard b) = All (All Filled) b
159+
160+fullBoard : (b : Board n) -> Dec (FullBoard b)
161+fullBoard (MkBoard b) = all (all filled) b
162+
163+fins : Vect (Fin n) n
164+fins {n=O} = Nil
165+fins {n=(S m)} = last :: map weaken fins
166+
167+data LegalBoard : Board n -> Type where
168+ Base : LegalBoard (emptyBoard {n})
169+ Step : {b : Board n} -> {coords : (Fin n, Fin n)} -> {v : Fin n} -> LegalVal b coords v -> LegalBoard b -> LegalBoard (setCell b coords v)
170+
171+CompleteBoard : Board n -> Type
172+CompleteBoard b = (LegalBoard b, FullBoard b)
173+
174+indexStep : {i : Fin n} -> {xs : Vect a n} -> {x : a} -> index i xs = index (fS i) (x::xs)
175+indexStep = refl
176+
177+find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n)
178+ -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
179+find _ Nil = Left Nil
180+find d (x::xs) with (d x)
181+ | Yes prf = Right (x ** (prf, (fO ** refl)))
182+ | No prf =
183+ case find d xs of
184+ Right (y ** (prf', (i ** prf''))) =>
185+ Right (y ** (prf', (fS i ** replace (indexStep {x=x}) prf'')))
186+ Left prf' => Left (prf::prf')
187+
188+findEmptyInRow : (xs : Vect (Cell n) n) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
189+findEmptyInRow xs =
190+ case find {P=Empty} empty xs of
191+ Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
192+ Left p => Left p
193+
194+emptyCell : (b : Board n) -> Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))
195+emptyCell (MkBoard rs) =
196+ case helper rs of
197+ Left p => Left p
198+ Right (ri ** (ci ** pf)) => Right ((ci, ri) ** pf)
199+ where
200+ helper : (rs : Vect (Vect (Cell n) n) m)
201+ -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))
202+ helper Nil = Left Nil
203+ helper (r::rs) =
204+ case findEmptyInRow r of
205+ Right (ci ** pf) => Right (fO ** (ci ** pf))
206+ Left prf =>
207+ case helper rs of
208+ Left prf' => Left (prf::prf')
209+ Right (ri ** (ci ** pf)) => Right (fS ri ** (ci ** pf))
210+
211+
212+tryValue : {b : Board (S n)} -> LegalBoard b -> (c : (Fin (S n), Fin (S n))) -> Empty (getCell b c) -> (v : Fin (S n))
213+ -> Either (Not (LegalVal b c v)) (b' : Board (S n) ** LegalBoard b')
214+tryValue {b=b} l c _ v =
215+ case legalVal b c v of
216+ No prf => Left prf
217+ Yes prf => Right (_ ** Step prf l)
218+
219+nullBoardFull : (b : Board O) -> FullBoard b
220+nullBoardFull (MkBoard Nil) = Nil
221+
222+-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\312
223+fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')
224+fillBoard {n=O} b l = Just (b ** (l, nullBoardFull b))
225+fillBoard {n=(S n)} b l with (emptyCell b)
226+ | Left full = Just (b ** (l, full))
227+ | Right (coords ** p) = recurse last
228+ where
229+ %assert_total
230+ tryAll : (v : Fin (S n)) -> (Fin (S n), Maybe (b' : Board (S n) ** LegalBoard b'))
231+ tryAll v = --trace ("Trying " ++ show (the Int (cast v))) $
232+ case tryValue l coords p v of
233+ Right success => (v, Just success)
234+ Left _ => -- TODO: Prove unsolvable
235+ case v of
236+ fS k => tryAll (weaken k)
237+ fO => (v, Nothing)
238+
239+ %assert_total
240+ recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')
241+ recurse start =
242+ case tryAll start of
243+ (_, Nothing) => Nothing
244+ (fO, Just (b' ** l')) => fillBoard b' l'
245+ (fS next, Just (b' ** l')) =>
246+ case fillBoard b' l' of
247+ Just solution => Just solution
248+ Nothing => recurse (weaken next)