0 | module Data.Stream
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import public Data.Zippable
  5 |
  6 | %default total
  7 |
  8 | ||| Drop the first n elements from the stream
  9 | ||| @ n how many elements to drop
 10 | public export
 11 | drop : (n : Nat) -> Stream a -> Stream a
 12 | drop Z     xs = xs
 13 | drop (S k) (x::xs) = drop k xs
 14 |
 15 | ||| An infinite stream of repetitions of the same thing
 16 | public export
 17 | repeat : a -> Stream a
 18 | repeat x = x :: repeat x
 19 |
 20 | ||| Generate an infinite stream by repeatedly applying a function
 21 | ||| @ f the function to iterate
 22 | ||| @ x the initial value that will be the head of the stream
 23 | public export
 24 | iterate : (f : a -> a) -> (x : a) -> Stream a
 25 | iterate f x = x :: iterate f (f x)
 26 |
 27 | public export
 28 | unfoldr : (b -> (a, b)) -> b -> Stream a
 29 | unfoldr f c = let (a, n) = f c in a :: unfoldr f n
 30 |
 31 | ||| All of the natural numbers, in order
 32 | public export
 33 | nats : Stream Nat
 34 | nats = iterate S Z
 35 |
 36 | ||| Get the nth element of a stream
 37 | public export
 38 | index : Nat -> Stream a -> a
 39 | index Z     (x::xs) = x
 40 | index (S k) (x::xs) = index k xs
 41 |
 42 | ---------------------------
 43 | -- Zippable --
 44 | ---------------------------
 45 |
 46 | public export
 47 | Zippable Stream where
 48 |   zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
 49 |
 50 |   zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs
 51 |
 52 |   unzipWith f xs = unzip (map f xs)
 53 |
 54 |   unzip xs = (map fst xs, map snd xs)
 55 |
 56 |   unzipWith3 f xs = unzip3 (map f xs)
 57 |
 58 |   unzip3 xs = (map (\(x, _, _) => x) xs, map (\(_, x, _) => x) xs, map (\(_, _, x) => x) xs)
 59 |
 60 | export
 61 | zipWithIndexLinear : (0 f : _) -> (xs, ys : Stream a) -> (i : Nat) -> index i (zipWith f xs ys) = f (index i xs) (index i ys)
 62 | zipWithIndexLinear f (_::xs) (_::ys) Z     = Refl
 63 | zipWithIndexLinear f (_::xs) (_::ys) (S k) = zipWithIndexLinear f xs ys k
 64 |
 65 | export
 66 | zipWith3IndexLinear : (0 f : _) -> (xs, ys, zs : Stream a) -> (i : Nat) -> index i (zipWith3 f xs ys zs) = f (index i xs) (index i ys) (index i zs)
 67 | zipWith3IndexLinear f (_::xs) (_::ys) (_::zs) Z     = Refl
 68 | zipWith3IndexLinear f (_::xs) (_::ys) (_::zs) (S k) = zipWith3IndexLinear f xs ys zs k
 69 |
 70 | ||| Return the diagonal elements of a stream of streams
 71 | export
 72 | diag : Stream (Stream a) -> Stream a
 73 | diag ((x::xs)::xss) = x :: diag (map tail xss)
 74 |
 75 | ||| Produce a Stream of left folds of prefixes of the given Stream
 76 | ||| @ f the combining function
 77 | ||| @ acc the initial value
 78 | ||| @ xs the Stream to process
 79 | export
 80 | scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
 81 | scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
 82 |
 83 | ||| Produce a Stream repeating a sequence
 84 | ||| @ xs the sequence to repeat
 85 | ||| @ ok proof that the list is non-empty
 86 | export
 87 | cycle : (xs : List a) -> {auto 0 ok : NonEmpty xs} -> Stream a
 88 | cycle (x :: xs) = x :: cycle' xs
 89 |   where cycle' : List a -> Stream a
 90 |         cycle' []        = x :: cycle' xs
 91 |         cycle' (y :: ys) = y :: cycle' ys
 92 |
 93 | --------------------------------------------------------------------------------
 94 | -- Interleavings
 95 | --------------------------------------------------------------------------------
 96 |
 97 | -- zig, zag, and cantor are taken from the paper
 98 | -- Applications of Applicative Proof Search
 99 | -- by Liam O'Connor
100 |
101 | public export
102 | zig : List1 (Stream a) -> Stream (Stream a) -> Stream a
103 |
104 | public export
105 | zag : List1 a -> List1 (Stream a) -> Stream (Stream a) -> Stream a
106 |
107 | zig xs = zag (head <$> xs) (tail <$> xs)
108 |
109 | zag (x ::: []) zs (l :: ls) = x :: zig (l ::: forget zs) ls
110 | zag (x ::: (y :: xs)) zs ls = x :: zag (y ::: xs) zs ls
111 |
112 | public export
113 | cantor : Stream (Stream a) -> Stream a
114 | cantor (l :: ls) = zig (l ::: []) ls
115 |
116 | namespace DPair
117 |
118 |   ||| Explore the plane corresponding to all possible pairings
119 |   ||| using Cantor's zig zag traversal
120 |   public export
121 |   planeWith : {0 p : a -> Type} ->
122 |               ((x : a) -> p x -> c) ->
123 |               Stream a -> ((x : a) -> Stream (p x)) ->
124 |               Stream c
125 |   planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
126 |
127 |   ||| Explore the plane corresponding to all possible pairings
128 |   ||| using Cantor's zig zag traversal
129 |   public export
130 |   plane : {0 p : a -> Type} ->
131 |           Stream a -> ((x : a) -> Stream (p x)) ->
132 |           Stream (x : a ** p x)
133 |   plane = planeWith (\ x, prf => (x ** prf))
134 |
135 | namespace Pair
136 |
137 |   ||| Explore the plane corresponding to all possible pairings
138 |   ||| using Cantor's zig zag traversal
139 |   public export
140 |   planeWith : (a -> b -> c) ->
141 |               Stream a -> (a -> Stream b) ->
142 |               Stream c
143 |   planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)
144 |
145 |   ||| Explore the plane corresponding to all possible pairings
146 |   ||| using Cantor's zig zag traversal
147 |   public export
148 |   plane : Stream a -> (a -> Stream b) -> Stream (a, b)
149 |   plane = Pair.planeWith (,)
150 |
151 | --------------------------------------------------------------------------------
152 | -- Example
153 | --------------------------------------------------------------------------------
154 |
155 | -- Exploring the Nat*Nat top right quadrant of the plane
156 | -- using Cantor's zig-zag traversal:
157 | example :
158 |      take 10 (plane Stream.nats (const Stream.nats))
159 |      === [ (0, 0)
160 |          , (1, 0), (0, 1)
161 |          , (2, 0), (1, 1), (0, 2)
162 |          , (3, 0), (2, 1), (1, 2), (0, 3)
163 |          ]
164 | example = Refl
165 |
166 | --------------------------------------------------------------------------------
167 | -- Implementations
168 | --------------------------------------------------------------------------------
169 |
170 | export
171 | Applicative Stream where
172 |   pure = repeat
173 |   (<*>) = zipWith apply
174 |
175 | export
176 | Monad Stream where
177 |   s >>= f = diag (map f s)
178 |
179 | --------------------------------------------------------------------------------
180 | -- Properties
181 | --------------------------------------------------------------------------------
182 |
183 | lengthTake : (n : Nat) -> (xs : Stream a) -> length (take n xs) = n
184 | lengthTake Z _ = Refl
185 | lengthTake (S n) (x :: xs) = cong S (lengthTake n xs)
186 |