Deal with 'Delay' in case building properly
We mustn't inspect the laziness type, because we'll never have it. (This
is a bit of a hack and relies on never having two different types of
laziness in the same argument, but since that doesn't make sense anyway,
I believe this is safe!)
Fixes #1295
commit42dcbc3d54bd58f88fd66e8740f6e213f715ccab
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 9 Jun 2014, 20:48 (12 years ago)
parentdb92986
idris.cabal+3
@@ -242,6 +242,9 @@ Extra-source-files:
242242 test/reg044/run
243243 test/reg044/*.idr
244244 test/reg044/expected
245+ test/reg045/run
246+ test/reg045/*.idr
247+ test/reg045/expected
245248
246249 test/basic001/run
247250 test/basic001/*.idr
src/Idris/Core/CaseTree.hs+3
@@ -336,6 +336,9 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
336336toPat :: Bool -> Bool -> [Term] -> [Pat]
337337toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
338338 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']
339342 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
340343 return $ PCon n t args'
341344 -- 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