diff --git a/tests/playground/lazylist.lean b/tests/playground/lazylist.lean index 1d4e13069d..916a9a6fb8 100644 --- a/tests/playground/lazylist.lean +++ b/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 := -iterate Nat.succ i +def iota (i : UInt32 := 0) : LazyList UInt32 := +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 $ [1, 2, 3].toLazy.cycle, - IO.println $ [1, 2, 3].toLazy.cycle.inits, - IO.println $ ((iota.filter (λ v, v % 5 == 0)).approx 50000).foldl (+) 0, - IO.println $ (primes.approx 1000).foldl (+) 0, - IO.println $ tst.head, - IO.println $ fib.interleave (iota.map (+100)), - IO.println $ ((iota.map (+10)).filter (λ v, v % 2 == 0)), + -- IO.println $ tst.isEmpty, + -- IO.println $ [1, 2, 3].toLazy.cycle, + -- IO.println $ [1, 2, 3].toLazy.cycle.inits, + -- IO.println $ ((iota.filter (λ v, v % 5 == 0)).approx 50000).foldl (+) 0, + IO.println $ (primes.approx 2000).foldl (+) 0, + -- IO.println $ tst.head, + -- IO.println $ fib.interleave (iota.map (+100)), + -- IO.println $ ((iota.map (+10)).filter (λ v, v % 2 == 0)), pure () diff --git a/tests/playground/primes.hs b/tests/playground/primes.hs new file mode 100644 index 0000000000..6ca61f4c3f --- /dev/null +++ b/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))