42dcbc3 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -242,6 +242,9 @@ Extra-source-files:

242 test/reg044/run

243 test/reg044/*.idr

244 test/reg044/expected

245+ test/reg045/run

246+ test/reg045/*.idr

247+ test/reg045/expected

245

248

246 test/basic001/run

249 test/basic001/run

247 test/basic001/*.idr

250 test/basic001/*.idr

src/Idris/Core/CaseTree.hs+3

@@ -336,6 +336,9 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

336toPat :: Bool -> Bool -> [Term] -> [Pat]

337toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []

338 where

339+ toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]

340+ | n == txt "Delay" = do arg' <- toPat' arg []

341+ return $ PCon nm t [PAny, PAny, arg']

339 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

342 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args

340 return $ PCon n t args'

343 return $ PCon n t args'

341 -- n + 1

344 -- n + 1

test/reg045/expectednew file+1

@@ -0,0 +1 @@

1+[1, 2, 3]

test/reg045/reg045.idrnew file+19

@@ -0,0 +1,19 @@

1+module Main

2+

3+data ListZ : Type -> Type where

4+ (::) : a -> Lazy (ListZ a) -> ListZ a

5+ Nil : ListZ a

6+

7+instance Show a => Show (ListZ a) where

8+ show xs = "[" ++ show' "" xs ++ "]"

9+ where

10+ show' acc Nil = acc

11+ show' acc (x :: Nil) = acc ++ show x

12+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

13+

14+foo : ListZ Nat

15+foo = (1 :: 2 :: 3 :: Nil)

16+

17+main : IO ()

18+main = print foo

19+

test/reg045/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ reg045.idr -o reg045

3+./reg045

4+rm -f reg045 *.ibc