@@ -1,10 +1,52 @@
11module Prelude.Stream
22
3+import Prelude.Functor
34import Prelude.Vect
45
6+%access public
7+%default total
8+
59codata Stream : Type -> Type where
610 (::) : a -> Stream a -> Stream a
711
12+instance Functor Stream where
13+ map f (x::xs) = f x :: map f xs
14+
15+head : Stream a -> a
16+head (x::xs) = x
17+
18+tail : Stream a -> Stream a
19+tail (x::xs) = xs
20+
821take : (n : Nat) -> Stream a -> Vect n a
922take Z _ = []
1023take (S n) (x :: xs) = x :: (take n xs)
24+
25+%assert_total
26+drop : Nat -> Stream a -> Stream a
27+drop Z xs = xs
28+drop (S k) (x::xs) = drop k xs
29+
30+repeat : a -> Stream a
31+repeat x = x :: repeat x
32+
33+iterate : (a -> a) -> a -> Stream a
34+iterate f x = x :: iterate f (f x)
35+
36+index : Nat -> Stream a -> a
37+index Z (x::xs) = x
38+index (S k) (x::xs) = index k xs
39+
40+zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
41+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
42+
43+zip : Stream a -> Stream b -> Stream (a, b)
44+zip = zipWith (\x,y => (x,y))
45+
46+unzip : Stream (a, b) -> (Stream a, Stream b)
47+unzip xs = (map fst xs, map snd xs)
48+
49+diag : Stream (Stream a) -> Stream a
50+diag ((x::xs)::xss) = x :: diag (map tail xss)
51+
52+