05b7fde · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Update for idris 0.9.9.3

commit05b7fdec33dc31ed5207c8873f2b40699bf46efd authorBenjamin Saunders <besaunde@sfu.ca> dateWed 6 Nov 2013, 19:58 (13 years ago) parent4fcacce

3 files changed+37−36

compare with master

unifiedsplit

EmptyTest.idr+2−2 Parser.idr+12−12 Solver.idr+23−22

EmptyTest.idr+2−2

@@ -6,8 +6,8 @@ step : Nat -> IO ()

66step n = do

77 putStrLn $

88 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")

9+ Just xs => ("Solved " <+> show n <+> "^2:\n" <+> show (getWitness xs))

10+ Nothing => ("Failed to solve " <+> show n <+> "^2")

1111 step (S n)

1212

1313main : IO ()

Parser.idr+12−12

@@ -10,7 +10,7 @@ ParseErr = String

1010Parser : Nat -> Type

1111Parser n = Either ParseErr (b : Board n ** LegalBoard b)

1212

13−mapM : Monad m => (a -> m b) -> Vect a n -> m (Vect b n)

13+mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)

1414mapM _ Nil = return Vect.Nil

1515mapM f (x::xs) = do

1616 x' <- f x

@@ -20,21 +20,21 @@ mapM f (x::xs) = do

2020parseToken : String -> Either String (Cell n)

2121parseToken "." = return Nothing

2222parseToken "0" = Left "Got cell 0, expected 1-based numbering"

23−parseToken x = fmap Just (tryParseFin ((cast x) - 1))

23+parseToken x = map Just (tryParseFin ((cast x) - 1))

2424 where

2525 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

26+ tryParseFin {n=Z} _ = Left ("Given cell " ++ x ++ " out of range")

27+ tryParseFin {n=S k} 0 = return fZ

2828 tryParseFin {n=S k} x =

2929 case tryParseFin {n=k} (x-1) of

3030 Left err => Left err

3131 Right fin => return (fS fin)

3232

33−length : Vect a n -> Nat

33+length : Vect n a -> Nat

3434length {n=n} _ = n

3535

36−parseCols : {b : Board n} -> Fin n -> LegalBoard b -> Vect String n -> Parser n

37−parseCols {n=O} _ l _ = Right (_ ** l)

36+parseCols : {b : Board n} -> Fin n -> LegalBoard b -> Vect n String -> Parser n

37+parseCols {n=Z} _ l _ = Right (_ ** l)

3838parseCols {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)

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

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

5050

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

52− helper fO l = step l fO

52+ helper fZ l = step l fZ

5353 helper (fS k) l = do

5454 (_ ** next) <- step l (fS k)

5555 helper (weaken k) next

5656

57−parseRows : (b : Board n) -> LegalBoard b -> Vect String n -> Parser n

58−parseRows {n=O} _ l _ = Right (_ ** l)

57+parseRows : (b : Board n) -> LegalBoard b -> Vect n String -> Parser n

58+parseRows {n=Z} _ l _ = Right (_ ** l)

5959parseRows {n=S k} _ l rs = helper last l

6060 where

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

@@ -63,10 +63,10 @@ parseRows {n=S k} _ l rs = helper last l

6363 let cs = fromList (words (index i rs)) in

6464 case decEq (length cs) (S k) of

6565 No _ => Left "Row length not equal to column height"

66− Yes prf => parseCols i l (replace prf cs)

66+ Yes prf => let foo = (replace {P=\n => Vect n String} prf cs) in parseCols i l foo -- TODO: foo shouldn't be needed

6767

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

69− helper fO l = step fO l

69+ helper fZ l = step fZ l

7070 helper (fS k) l = do

7171 (_ ** next) <- step (fS k) l

7272 helper (weaken k) next

Solver.idr+23−22

@@ -10,7 +10,7 @@ Cell : Nat -> Type

1010Cell n = Maybe (Fin n)

1111

1212data Board : Nat -> Type where

13− MkBoard : {n : Nat} -> Vect (Vect (Cell n) n) n -> Board n

13+ MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n

1414

1515emptyBoard : Board n

1616emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))

@@ -19,10 +19,11 @@ showElt : Cell n -> String

1919showElt Nothing = "."

2020showElt (Just x) = show (1 + (the Int (fromInteger (cast x))))

2121

22−showRow : Vect (Cell n) n -> String

23−showRow xs = unwords (toList (map showElt xs))

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

2425

25−unlines : Vect String n -> String

26+unlines : Vect n String -> String

2627unlines Nil = ""

2728unlines (l::Nil) = l

2829unlines (l::ls) = pack (foldl addLine (unpack l) (map unpack ls))

@@ -33,8 +34,8 @@ unlines (l::ls) = pack (foldl addLine (unpack l) (map unpack ls))

3334instance Show (Board n) where

3435 show (MkBoard rs) = unlines (map showRow rs)

3536

36−updateAt : Fin n -> Vect a n -> (a -> a) -> Vect a n

37−updateAt fO (x::xs) f = f x :: xs

37+updateAt : Fin n -> Vect n a -> (a -> a) -> Vect n a

38+updateAt fZ (x::xs) f = f x :: xs

3839updateAt (fS i) (x::xs) f = x :: updateAt i xs f

3940

4041setCell : Board n -> (Fin n, Fin n) -> Fin n -> Board n

@@ -43,17 +44,17 @@ setCell (MkBoard b) (x, y) value = MkBoard (updateAt y b (\row => updateAt x row

4344getCell : Board n -> (Fin n, Fin n) -> Cell n

4445getCell (MkBoard b) (x, y) = index x (index y b)

4546

46−anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

47+anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

4748anyElim _ f (Here p) = f p

4849anyElim f _ (There p) = f p

4950

50−getRow : Fin n -> Board n -> Vect (Cell n) n

51+getRow : Fin n -> Board n -> Vect n (Cell n)

5152getRow i (MkBoard b) = index i b

5253

53−getCol : Fin n -> Board n -> Vect (Cell n) n

54+getCol : Fin n -> Board n -> Vect n (Cell n)

5455getCol i (MkBoard b) = helper i b

5556 where

56− helper : Fin n -> Vect (Vect a n) m -> Vect a m

57+ helper : Fin n -> Vect m (Vect n a) -> Vect m a

5758 helper _ Nil = Nil

5859 helper i (xs::xss) = index i xs :: helper i xss

5960

@@ -115,8 +116,8 @@ FullBoard (MkBoard b) = All (All Filled) b

115116fullBoard : (b : Board n) -> Dec (FullBoard b)

116117fullBoard (MkBoard b) = all (all filled) b

117118

118−fins : Vect (Fin n) n

119−fins {n=O} = Nil

119+fins : Vect n (Fin n)

120+fins {n=Z} = Nil

120121fins {n=(S m)} = last :: map weaken fins

121122

122123data LegalBoard : Board n -> Type where

@@ -126,21 +127,21 @@ data LegalBoard : Board n -> Type where

126127CompleteBoard : Board n -> Type

127128CompleteBoard b = (LegalBoard b, FullBoard b)

128129

129−indexStep : {i : Fin n} -> {xs : Vect a n} -> {x : a} -> index i xs = index (fS i) (x::xs)

130+indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (fS i) (x::xs)

130131indexStep = refl

131132

132−find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n)

133+find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

133134 -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

134135find _ Nil = Left Nil

135136find d (x::xs) with (d x)

136− | Yes prf = Right (x ** (prf, (fO ** refl)))

137+ | Yes prf = Right (x ** (prf, (fZ ** refl)))

137138 | No prf =

138139 case find d xs of

139140 Right (y ** (prf', (i ** prf''))) =>

140141 Right (y ** (prf', (fS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

141142 Left prf' => Left (prf::prf')

142143

143−findEmptyInRow : (xs : Vect (Cell n) n) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

144+findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

144145findEmptyInRow xs =

145146 case find {P=Empty} empty xs of

146147 Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)

@@ -152,12 +153,12 @@ emptyCell (MkBoard rs) =

152153 Left p => Left p

153154 Right (ri ** (ci ** pf)) => Right ((ci, ri) ** pf)

154155 where

155− helper : (rs : Vect (Vect (Cell n) n) m)

156+ helper : (rs : Vect m (Vect n (Cell n)))

156157 -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))

157158 helper Nil = Left Nil

158159 helper (r::rs) =

159160 case findEmptyInRow r of

160− Right (ci ** pf) => Right (fO ** (ci ** pf))

161+ Right (ci ** pf) => Right (fZ ** (ci ** pf))

161162 Left prf =>

162163 case helper rs of

163164 Left prf' => Left (prf::prf')

@@ -171,12 +172,12 @@ tryValue {b=b} l c _ v =

171172 No prf => Left prf

172173 Yes prf => Right (_ ** Step prf l)

173174

174−nullBoardFull : (b : Board O) -> FullBoard b

175+nullBoardFull : (b : Board Z) -> FullBoard b

175176nullBoardFull (MkBoard Nil) = Nil

176177

177178-- TODO: Prove complete by induction on illegal values wrt. some base state, e.g. every value is illegal for 123\21_\3_2

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

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

180+fillBoard {n=Z} b l = Just (b ** (l, nullBoardFull b))

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

181182 | Left full = Just (b ** (l, full))

182183 | Right (coords ** p) = recurse last

@@ -189,14 +190,14 @@ fillBoard {n=(S n)} b l with (emptyCell b)

189190 Left _ => -- TODO: Prove unsolvable

190191 case v of

191192 fS k => tryAll (weaken k)

192− fO => (v, Nothing)

193+ fZ => (v, Nothing)

193194

194195 %assert_total

195196 recurse : Fin (S n) -> Maybe (b' : Board (S n) ** CompleteBoard b')

196197 recurse start =

197198 case tryAll start of

198199 (_, Nothing) => Nothing

199− (fO, Just (b' ** l')) => fillBoard b' l'

200+ (fZ, Just (b' ** l')) => fillBoard b' l'

200201 (fS next, Just (b' ** l')) =>

201202 case fillBoard b' l' of

202203 Just solution => Just solution