git.iko.soy/Idris-dev
on master help sign in
Add more Stream operations now that we have them
65ff5feMelvar Chen
libs/base/Prelude.idr+7
compare with master
unifiedsplit
@@ -236,6 +236,10 @@ instance Applicative (Vect k) where
236
236
237 fs <$> vs = zipWith ($) fs vs
237 fs <$> vs = zipWith ($) fs vs
238
238
239+instance Applicative Stream where
240+ pure = repeat
241+ (<$>) = zipWith ($)
242+
239---- Alternative instances
243---- Alternative instances
240
244
241instance Alternative Maybe where
245instance Alternative Maybe where
@@ -271,6 +275,9 @@ instance Monad List where
271instance Monad (Vect n) where
275instance Monad (Vect n) where
272 m >>= f = diag (map f m)
276 m >>= f = diag (map f m)
273
277
278+instance Monad Stream where
279+ s >>= f = diag (map f s)
280+
274---- Traversable instances
281---- Traversable instances
275
282
276instance Traversable Maybe where
283instance Traversable Maybe where
libs/base/Prelude/Stream.idr+42
@@ -1,10 +1,52 @@
1module Prelude.Stream
1module Prelude.Stream
2
2
3+import Prelude.Functor
3import Prelude.Vect
4import Prelude.Vect
4
5
6+%access public
7+%default total
8+
5codata Stream : Type -> Type where
9codata Stream : Type -> Type where
6 (::) : a -> Stream a -> Stream a
10 (::) : a -> Stream a -> Stream a
7
11
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+
8take : (n : Nat) -> Stream a -> Vect n a
21take : (n : Nat) -> Stream a -> Vect n a
9take Z _ = []
22take Z _ = []
10take (S n) (x :: xs) = x :: (take n xs)
23take (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+