diff --git a/tests/Main.idr b/tests/Main.idr index 52016ca93..44c46caef 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -128,7 +128,7 @@ idrisTests = MkTestPool "Misc" [] Nothing "import001", "import002", "import003", "import004", "import005", "import006", "import007", "import008", "import009", -- Implicit laziness, lazy evaluation - "lazy001", "lazy002", "lazy003", "lazy004", + "lazy001", "lazy002", "lazy003", "lazy004", "lazy005", -- Namespace blocks "namespace001", "namespace002", "namespace003", "namespace004", "namespace005", -- Parameters blocks diff --git a/tests/idris2/misc/lazy005/LiftedBot.idr b/tests/idris2/misc/lazy005/LiftedBot.idr new file mode 100644 index 000000000..89e4cfbef --- /dev/null +++ b/tests/idris2/misc/lazy005/LiftedBot.idr @@ -0,0 +1,28 @@ +import Data.List.Lazy + +import Debug.Trace + +showHead : Show a => LazyList a -> String +showHead [] = "Empty" +showHead (x::xs) = show x + +%inline +(::) : Maybe a -> Lazy (LazyList a) -> LazyList a +Nothing :: xs = xs +Just x :: xs = x :: xs + +bot : a +bot = bot + +fufu : a -> Maybe a +fufu = Just + +g : LazyList Nat +g = [ fufu 6 + , fufu bot + ] + +-- Note that this should finish in finite time, as tail containing +-- `bot` is lazy and should never be computed +main : IO Unit +main = printLn $ showHead g diff --git a/tests/idris2/misc/lazy005/LiftedTrace.idr b/tests/idris2/misc/lazy005/LiftedTrace.idr new file mode 100644 index 000000000..b7c747809 --- /dev/null +++ b/tests/idris2/misc/lazy005/LiftedTrace.idr @@ -0,0 +1,22 @@ +import Data.List.Lazy + +import Debug.Trace + +%default total + +%inline +(::) : Maybe a -> Lazy (LazyList a) -> LazyList a +Nothing :: xs = xs +Just x :: xs = x :: xs + +fufu : a -> Maybe a +fufu = Just + +g : LazyList Nat +g = trace "--- outmost ---" + [ fufu $ trace "pure 6" 6 + , fufu $ trace "pure 5" 5 + ] + +main : IO Unit +main = printLn g diff --git a/tests/idris2/misc/lazy005/expected b/tests/idris2/misc/lazy005/expected new file mode 100644 index 000000000..5331dca10 --- /dev/null +++ b/tests/idris2/misc/lazy005/expected @@ -0,0 +1,5 @@ +pure 6 +--- outmost --- +pure 5 +[6, 5] +"6" diff --git a/tests/idris2/misc/lazy005/run b/tests/idris2/misc/lazy005/run new file mode 100755 index 000000000..ff9f52ca8 --- /dev/null +++ b/tests/idris2/misc/lazy005/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +idris2 -p contrib --exec main LiftedTrace.idr +idris2 -p contrib --exec main LiftedBot.idr