dcd4007 · Idris-dev · git.iko.soy

src/Core/CaseTree.hs+1−1

compare with master

unifiedsplit

@@ -277,7 +277,7 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

277 toPat' (P _ n _) args | reflect

278 = do args' <- mapM (\x -> toPat' x []) args

279 return $ PReflected n args'

280− toPat' _ _ = return PAny

280+ toPat' t _ = return PAny

281

282 fixedN IT8 = "Bits8"

283 fixedN IT16 = "Bits16"

src/Core/Typecheck.hs+4−2

@@ -186,13 +186,15 @@ check' holes ctxt env top = chk env top where

186 let tv' = normalise ctxt env tv

187 let tt' = normalise ctxt env tt

188 lift $ isType ctxt env tt'

189+ -- Normalised version, for erasure purposes (it's easier

190+ -- to tell if it's a collapsible variable)

189− return (PVar tv)

191+ return (PVar tv')

190 checkBinder (PVTy t)

192 checkBinder (PVTy t)

191 = do (tv, tt) <- chk env t

193 = do (tv, tt) <- chk env t

192 let tv' = normalise ctxt env tv

194 let tv' = normalise ctxt env tv

193 let tt' = normalise ctxt env tt

195 let tt' = normalise ctxt env tt

194 lift $ isType ctxt env tt'

196 lift $ isType ctxt env tt'

195− return (PVTy tv)

197+ return (PVTy tv')

196

198

197 discharge n (Lam t) scv sct

199 discharge n (Lam t) scv sct

198 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

200 = return (Bind n (Lam t) scv, Bind n (Pi t) sct)

src/Idris/DataOpts.hs+3

@@ -248,6 +248,9 @@ instance Optimisable (TT Name) where

248

249 stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x

250 = do i <- getIState

251+ -- NOTE: This assumes that 'ty' is in normal form, which it

252+ -- has to be before now because we're not keeping track of

253+ -- an environment so we can't do it here.

251 case lookupCtxt ty (idris_optimisation i) of

254 case lookupCtxt ty (idris_optimisation i) of

252 [oi] -> if collapsible oi

255 [oi] -> if collapsible oi

253 then do t' <- stripCollapsed t

256 then do t' <- stripCollapsed t

src/Idris/ElabTerm.hs−1

@@ -506,7 +506,6 @@ elab ist info pattern tcgen fn tm

506 mkCaseName n = SN (CaseN n)

507-- mkCaseName (UN x) = UN (x ++ "_case")

508-- mkCaseName (MN i x) = MN i (x ++ "_case")

509−-- mkCaseName (SN s) =

510 mkN n@(NS _ _) = n

509 mkN n@(NS _ _) = n

511 mkN n = case namespace info of

510 mkN n = case namespace info of

512 Just xs@(_:_) -> NS n xs

511 Just xs@(_:_) -> NS n xs

test/reg025/expectednew file+1

@@ -0,0 +1 @@

1+l

test/reg025/reg025.idrnew file+75

@@ -0,0 +1,75 @@

1+module Main

2+

3+import Data.Vect.Quantifiers

4+import Decidable.Equality

5+

6+Cell : Nat -> Type

7+Cell n = Maybe (Fin n)

8+

9+data Board : Nat -> Type where

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

11+

12+emptyBoard : Board n

13+emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))

14+

15+Empty : Cell n -> Type

16+Empty {n=n} x = (the (Cell n) Nothing) = x

17+

18+Filled : Cell n -> Type

19+Filled {n=n} = (\x => Not (Empty x))

20+

21+FullBoard : Board n -> Type

22+FullBoard (MkBoard b) = All (All Filled) b

23+

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

25+indexStep = refl

26+

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

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

29+find _ Nil = Left Nil

30+find d (x::xs) with (d x)

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

32+ | No prf =

33+ case find d xs of

34+ Right (y ** (prf', (i ** prf''))) =>

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

36+ Left prf' => Left (prf::prf')

37+

38+empty : (cell : Cell n) -> Dec (Empty cell)

39+empty Nothing = Yes refl

40+empty (Just _) = No nothingNotJust

41+

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

43+findEmptyInRow xs =

44+ case find {P=Empty} empty xs of

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

46+ Left p => Left p

47+

48+getCell : Board n -> (Fin n, Fin n) -> Cell n

49+getCell (MkBoard b) (x, y) = index x (index y b)

50+

51+emptyCell : {n : Nat} -> (b : Board n) ->

52+ Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))

53+emptyCell (MkBoard rs) =

54+ case helper rs of

55+ Left p => Left p

56+ Right (ri ** (ci ** pf2)) => Right ((ci, ri) ** pf2)

57+ where

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

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

60+ helper Nil = Left Nil

61+ helper (r::rs) =

62+ case findEmptyInRow r of

63+ Right (ci ** pf3) => Right (fZ ** (ci ** pf3))

64+ Left prf =>

65+ case helper rs of

66+ Left prf' => Left (prf::prf')

67+ Right (ri ** (ci ** pf4)) => Right (fS ri ** (ci ** pf4))

68+

69+

70+main : IO ()

71+main =

72+ case emptyCell (emptyBoard {n=0}) of

73+ Left _ => print "l"

74+ Right _ => print "r"

75+

test/reg025/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ reg025.idr -o reg025

3+./reg025

4+rm -f reg025 *.ibc