git.iko.soy/Idris-dev
on master help sign in
something
134eef4Benjamin Saunders
Parser.idr+7−4
compare with master
unifiedsplit
@@ -39,10 +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− tok <- parseToken (index x cs)
42+ tok <- parseToken {n=S k} (index x cs)
43+ case tok of
44+ Nothing => return (_ ** l)
45+ Just val =>
43− case legalVal b (x, row) tok of
46+ case legalVal b (x, row) val of
44− Yes prf => return (_ ** Step prf l)
47+ Yes prf => return (_ ** Step prf l)
45− No _ => Left ("Illegal cell " ++ index x cs)
48+ No _ => Left ("Illegal cell " ++ index x cs)
46
49
47 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
50 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)
48 helper fO l = step l fO
51 helper fO l = step l fO
Solver.idr+1−1
@@ -219,7 +219,7 @@ tryValue {b=b} l c _ v =
219nullBoardFull : (b : Board O) -> FullBoard b
219nullBoardFull : (b : Board O) -> FullBoard b
220nullBoardFull (MkBoard Nil) = Nil
220nullBoardFull (MkBoard Nil) = Nil
221
221
222−-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\312
222+-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\3_2
223fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')
223fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')
224fillBoard {n=O} b l = Just (b ** (l, nullBoardFull b))
224fillBoard {n=O} b l = Just (b ** (l, nullBoardFull b))
225fillBoard {n=(S n)} b l with (emptyCell b)
225fillBoard {n=(S n)} b l with (emptyCell b)