diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean new file mode 100644 index 0000000000..13bd8418c1 --- /dev/null +++ b/tests/compiler/lazylist.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +universes u v w + +inductive LazyList (α : Type u) +| nil {} : LazyList +| cons (hd : α) (tl : LazyList) : LazyList +| delayed (t : Thunk LazyList) : LazyList + +@[extern cpp inline "#2"] +def List.toLazy {α : Type u} : List α → LazyList α +| [] := LazyList.nil +| (h::t) := LazyList.cons h (List.toLazy t) + +namespace LazyList +variables {α : Type u} {β : Type v} {δ : Type w} + +instance : Inhabited (LazyList α) := +⟨nil⟩ + +@[inline] def pure : α → LazyList α +| a := cons a nil + +partial def isEmpty : LazyList α → Bool +| nil := true +| (cons _ _) := false +| (delayed as) := isEmpty as.get + +partial def toList : LazyList α → List α +| nil := [] +| (cons a as) := a :: toList as +| (delayed as) := toList as.get + +partial def head [Inhabited α] : LazyList α → α +| nil := default α +| (cons a as) := a +| (delayed as) := head as.get + +partial def tail : LazyList α → LazyList α +| nil := nil +| (cons a as) := as +| (delayed as) := tail as.get + +partial def append : LazyList α → LazyList α → LazyList α +| nil bs := bs +| (cons a as) bs := delayed (cons a (append as bs)) +| (delayed as) bs := delayed (append as.get bs) + +instance : HasAppend (LazyList α) := +⟨LazyList.append⟩ + +partial def interleave : LazyList α → LazyList α → LazyList α +| nil bs := bs +| (cons a as) bs := delayed (cons a (interleave bs as)) +| (delayed as) bs := delayed (interleave as.get bs) + +partial def map (f : α → β) : LazyList α → LazyList β +| nil := nil +| (cons a as) := delayed (cons (f a) (map as)) +| (delayed as) := delayed (map as.get) + +partial def map₂ (f : α → β → δ) : LazyList α → LazyList β → LazyList δ +| nil _ := nil +| _ nil := nil +| (cons a as) (cons b bs) := delayed (cons (f a b) (map₂ as bs)) +| (delayed as) bs := delayed (map₂ as.get bs) +| as (delayed bs) := delayed (map₂ as bs.get) + +@[inline] def zip : LazyList α → LazyList β → LazyList (α × β) := +map₂ Prod.mk + +partial def join : LazyList (LazyList α) → LazyList α +| nil := nil +| (cons a as) := delayed (append a (join as)) +| (delayed as) := delayed (join as.get) + +@[inline] partial def bind (x : LazyList α) (f : α → LazyList β) : LazyList β := +join (x.map f) + +instance isMonad : Monad LazyList := +{ pure := @LazyList.pure, bind := @LazyList.bind, map := @LazyList.map } + +instance : Alternative LazyList := +{ failure := λ _, nil, + orelse := @LazyList.append, + .. LazyList.isMonad } + +partial def approx : Nat → LazyList α → List α +| 0 as := [] +| _ nil := [] +| (i+1) (cons a as) := a :: approx i as +| (i+1) (delayed as) := approx (i+1) as.get + +partial def iterate (f : α → α) : α → LazyList α +| x := cons x (delayed (iterate (f x))) + +partial def iterate₂ (f : α → α → α) : α → α → LazyList α +| x y := cons x (delayed (iterate₂ y (f x y))) + +partial def filter (p : α → Bool) : LazyList α → LazyList α +| nil := nil +| (cons a as) := delayed (if p a then cons a (filter as) else filter as) +| (delayed as) := delayed (filter as.get) + +end LazyList + +def fib : LazyList Nat := +LazyList.iterate₂ (+) 0 1 + +def iota (i : Nat := 0) : LazyList Nat := +LazyList.iterate Nat.succ i + +def tst : LazyList String := +do x ← [1, 2, 3].toLazy, + y ← [2, 3, 4].toLazy, + guard (x + y > 5), + pure (toString x ++ " + " ++ toString y ++ " = " ++ toString (x+y)) + +def main : IO Unit := +do let n := 40, + IO.println $ tst.isEmpty, + IO.println $ tst.head, + IO.println $ (fib.interleave (iota.map (+100))).approx n, + IO.println $ (((iota.map (+10)).filter (λ v, v % 2 == 0)).approx n) diff --git a/tests/compiler/lazylist.lean.expected.out b/tests/compiler/lazylist.lean.expected.out new file mode 100644 index 0000000000..c1e3a1e445 --- /dev/null +++ b/tests/compiler/lazylist.lean.expected.out @@ -0,0 +1,4 @@ +false +2 + 4 = 6 +[0, 100, 1, 101, 1, 102, 2, 103, 3, 104, 5, 105, 8, 106, 13, 107, 21, 108, 34, 109, 55, 110, 89, 111, 144, 112, 233, 113, 377, 114, 610, 115, 987, 116, 1597, 117, 2584, 118, 4181, 119] +[10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44, 46, 48, 50, 52, 54, 56, 58, 60, 62, 64, 66, 68, 70, 72, 74, 76, 78, 80, 82, 84, 86, 88]