134eef4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

something

commit134eef4749bb08bcfc8b535cf82c7055394f960b authorBenjamin Saunders <besaunde@sfu.ca> dateWed 26 Jun 2013, 22:56 (13 years ago) parentfb9af01

2 files changed+8−5

unifiedsplit

Parser.idr+7−4

@@ -39,10 +39,13 @@ parseCols {n=S k} row l cs = helper last l

3939 where

4040 step : {b : Board (S k)} -> LegalBoard b -> Fin (S k) -> Parser (S k)

4141 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)

42+ tok <- parseToken {n=S k} (index x cs)

43+ case tok of

44+ Nothing => return (_ ** l)

45+ Just val =>

46+ case legalVal b (x, row) val of

47+ Yes prf => return (_ ** Step prf l)

48+ No _ => Left ("Illegal cell " ++ index x cs)

4649

4750 helper : {b : Board (S k)} -> Fin (S k) -> LegalBoard b -> Parser (S k)

4851 helper fO l = step l fO

Solver.idr+1−1

@@ -219,7 +219,7 @@ tryValue {b=b} l c _ v =

219219nullBoardFull : (b : Board O) -> FullBoard b

220220nullBoardFull (MkBoard Nil) = Nil

221221

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

223223fillBoard : (b : Board n) -> LegalBoard b -> Maybe (b' : Board n ** CompleteBoard b')

224224fillBoard {n=O} b l = Just (b ** (l, nullBoardFull b))

225225fillBoard {n=(S n)} b l with (emptyCell b)