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

git.iko.soy/Idris-dev

on master help sign in

Update for idris 0.9.9.3

05b7fdeBenjamin Saunders13 years ago

EmptyTest.idr+2−2

compare with master

unifiedsplit

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

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

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

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

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

11 step (S n)

13main : IO ()

Parser.idr+12−12

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

10Parser : Nat -> Type

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

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)

14mapM _ Nil = return Vect.Nil

15mapM f (x::xs) = do

16 x' <- f x

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

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

21parseToken "." = return Nothing

22parseToken "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))

24 where

25 tryParseFin : Int -> Either String (Fin n)

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

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

27− tryParseFin {n=S k} 0 = return fO

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

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)

33−length : Vect a n -> Nat

33+length : Vect n a -> Nat

34length {n=n} _ = n

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

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

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

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

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

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

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

51 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

53 helper (fS k) l = do

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

55 helper (weaken k) next

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

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

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

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

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

60 where

61 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

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

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

65 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

68 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

70 helper (fS k) l = do

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

72 helper (weaken k) next

Solver.idr+23−22

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

10Cell n = Maybe (Fin n)

12data 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

15emptyBoard : Board n

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

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

19showElt Nothing = "."

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

22+-- FIXME: Inline type decl should not be necessary here

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

23+showRow : Vect n (Cell n) -> String

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

24+showRow {n=n} xs = unwords (toList (the (Vect n String) (map showElt xs)))

25−unlines : Vect String n -> String

26+unlines : Vect n String -> String

26unlines Nil = ""

27unlines Nil = ""

27unlines (l::Nil) = l

28unlines (l::Nil) = l

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

29unlines (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))

33instance Show (Board n) where

34instance Show (Board n) where

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

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

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

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

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

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

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

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

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

41setCell : 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

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

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

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

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

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

47anyElim _ f (Here p) = f p

48anyElim _ f (Here p) = f p

48anyElim f _ (There p) = f p

49anyElim f _ (There p) = f p

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

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

51getRow i (MkBoard b) = index i b

52getRow i (MkBoard b) = index i b

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

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

54getCol i (MkBoard b) = helper i b

55getCol i (MkBoard b) = helper i b

55 where

56 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

57 helper _ Nil = Nil

58 helper _ Nil = Nil

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

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

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

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

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

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

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

117

118

118−fins : Vect (Fin n) n

119+fins : Vect n (Fin n)

119−fins {n=O} = Nil

120+fins {n=Z} = Nil

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

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

121

122

122data LegalBoard : Board n -> Type where

123data LegalBoard : Board n -> Type where

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

126CompleteBoard : Board n -> Type

127CompleteBoard : Board n -> Type

127CompleteBoard b = (LegalBoard b, FullBoard b)

128CompleteBoard b = (LegalBoard b, FullBoard b)

128

129

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)

130indexStep = refl

131indexStep = refl

131

132

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)

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

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

134find _ Nil = Left Nil

135find _ Nil = Left Nil

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

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

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

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

137 | No prf =

138 | No prf =

138 case find d xs of

139 case find d xs of

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

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

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

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

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

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

142

143

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

144findEmptyInRow xs =

145findEmptyInRow xs =

145 case find {P=Empty} empty xs of

146 case find {P=Empty} empty xs of

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

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

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

152 Left p => Left p

153 Left p => Left p

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

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

154 where

155 where

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

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

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

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

157 helper Nil = Left Nil

158 helper Nil = Left Nil

158 helper (r::rs) =

159 helper (r::rs) =

159 case findEmptyInRow r of

160 case findEmptyInRow r of

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

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

161 Left prf =>

162 Left prf =>

162 case helper rs of

163 case helper rs of

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

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

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

171 No prf => Left prf

172 No prf => Left prf

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

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

173

174

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

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

175nullBoardFull (MkBoard Nil) = Nil

176nullBoardFull (MkBoard Nil) = Nil

176

177

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

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

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

179fillBoard : (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))

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

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

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

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

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

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

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

189 Left _ => -- TODO: Prove unsolvable

190 Left _ => -- TODO: Prove unsolvable

190 case v of

191 case v of

191 fS k => tryAll (weaken k)

192 fS k => tryAll (weaken k)

192− fO => (v, Nothing)

193+ fZ => (v, Nothing)

193

194

194 %assert_total

195 %assert_total

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

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

196 recurse start =

197 recurse start =

197 case tryAll start of

198 case tryAll start of

198 (_, Nothing) => Nothing

199 (_, Nothing) => Nothing

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

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

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

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

201 case fillBoard b' l' of

202 case fillBoard b' l' of

202 Just solution => Just solution

203 Just solution => Just solution