test(tests/playground/lazylist): perf tests

tests/playground/lazylist.lean

@@ -61,12 +61,12 @@ partial def interleave : LazyList α → LazyList α → LazyList α
 | (cons a as)  bs  := cons a (delayed (interleave bs as))
 | (delayed as) bs  := interleave as.get bs
 
-partial def map (f : α → β) : LazyList α → LazyList β
+@[specialize] partial def map (f : α → β) : LazyList α → LazyList β
 | nil          := nil
 | (cons a as)  := cons (f a) (delayed (map as))
 | (delayed as) := map as.get
 
-partial def map₂ (f : α → β → δ) : LazyList α → LazyList β → LazyList δ
+@[specialize] partial def map₂ (f : α → β → δ) : LazyList α → LazyList β → LazyList δ
 | nil          _            := nil
 | _            nil          := nil
 | (cons a as)  (cons b bs)  := cons (f a b) (delayed (map₂ as bs))
@@ -98,13 +98,13 @@ partial def approx : Nat → LazyList α → List α
 | (i+1) (cons a as)  := a :: approx i as
 | (i+1) (delayed as) := approx (i+1) as.get
 
-partial def iterate (f : α → α) : α → LazyList α
+@[specialize] partial def iterate (f : α → α) : α → LazyList α
 | x := cons x (delayed (iterate (f x)))
 
-partial def iterate₂ (f : α → α → α) : α → α → LazyList α
+@[specialize] partial def iterate₂ (f : α → α → α) : α → α → LazyList α
 | x y := cons x (delayed (iterate₂ y (f x y)))
 
-partial def filter (p : α → Bool) : LazyList α → LazyList α
+@[specialize] partial def filter (p : α → Bool) : LazyList α → LazyList α
 | nil          := nil
 | (cons a as)  := if p a then cons a (delayed (filter as)) else filter as
 | (delayed as) := filter as.get
@@ -149,28 +149,28 @@ do x ← [1, 2, 3].toLazy,
 
 open LazyList
 
-def iota (i : Nat := 0) : LazyList Nat :=
+def iota (i : UInt32 := 0) : LazyList UInt32 :=
-iterate Nat.succ i
+iterate (+1) i
 
 set_option pp.implicit true
--- set_option trace.compiler.boxed true
+set_option trace.compiler.boxed true
 
-partial def sieve : LazyList Nat → LazyList Nat
+partial def sieve : LazyList UInt32 → LazyList UInt32
 | nil          := nil
 | (cons a as)  := cons a (delayed (sieve (filter (λ b, b % a != 0) as)))
 | (delayed as) := sieve as.get
 
-partial def primes : LazyList Nat :=
+partial def primes : LazyList UInt32 :=
 sieve (iota 2)
 
 def main : IO Unit :=
 do let n := 10,
-   IO.println $ tst.isEmpty,
+   -- IO.println $ tst.isEmpty,
-   IO.println $ [1, 2, 3].toLazy.cycle,
+   -- IO.println $ [1, 2, 3].toLazy.cycle,
-   IO.println $ [1, 2, 3].toLazy.cycle.inits,
+   -- IO.println $ [1, 2, 3].toLazy.cycle.inits,
-   IO.println $ ((iota.filter (λ v, v % 5 == 0)).approx 50000).foldl (+) 0,
+   -- IO.println $ ((iota.filter (λ v, v % 5 == 0)).approx 50000).foldl (+) 0,
-   IO.println $ (primes.approx 1000).foldl (+) 0,
+   IO.println $ (primes.approx 2000).foldl (+) 0,
-   IO.println $ tst.head,
+   -- IO.println $ tst.head,
-   IO.println $ fib.interleave (iota.map (+100)),
+   -- IO.println $ fib.interleave (iota.map (+100)),
-   IO.println $ ((iota.map (+10)).filter (λ v, v % 2 == 0)),
+   -- IO.println $ ((iota.map (+10)).filter (λ v, v % 2 == 0)),
    pure ()

tests/playground/primes.hs

@@ -0,0 +1,8 @@
+sieve :: [Int] -> [Int]
+sieve (p : xs) = p : sieve (filter (\ a -> a `mod` p /= 0) xs)
+
+primes :: [Int]
+primes = sieve [2..]
+
+main =
+  print (sum (take 2000 primes))