0 | module Data.List.Lazy
  1 |
  2 | import Data.Fuel
  3 | import Data.Stream
  4 | import Data.Colist
  5 | import Data.Colist1
  6 |
  7 | %default total
  8 |
  9 | -- All functions here are public export
 10 | -- because their definitions are pretty much the specification.
 11 |
 12 | public export
 13 | data LazyList : Type -> Type where
 14 |   Nil : LazyList a
 15 |   (::) : (x : a) -> (xs : Lazy (LazyList a)) -> LazyList a
 16 |
 17 | --- Truly lazy functions ---
 18 |
 19 | public export
 20 | foldrLazy : (func : a -> Lazy acc -> acc) -> (init : Lazy acc) -> (input : LazyList a) -> acc
 21 | foldrLazy _  init [] = init
 22 | foldrLazy op init (x::xs) = x `op` foldrLazy op init xs
 23 |
 24 | public export
 25 | (++) : LazyList a -> Lazy (LazyList a) -> LazyList a
 26 | (++) = flip $ foldrLazy (::)
 27 |
 28 | -- Specialized variant of `concatMap` with both `t` and `m` being `LazyList`.
 29 | public export
 30 | bindLazy : (a -> LazyList b) -> LazyList a -> LazyList b
 31 | bindLazy f = foldrLazy ((++) . f) []
 32 |
 33 | public export
 34 | choice : Alternative f => LazyList (f a) -> f a
 35 | choice = foldrLazy (<|>) empty
 36 |
 37 | public export
 38 | choiceMap : Alternative f => (a -> f b) -> LazyList a -> f b
 39 | choiceMap g = foldrLazy ((<|>) . g) empty
 40 |
 41 | public export
 42 | any : (a -> Bool) -> LazyList a -> Bool
 43 | any p = foldrLazy ((||) . p) False
 44 |
 45 | public export
 46 | all : (a -> Bool) -> LazyList a -> Bool
 47 | all p = foldrLazy ((&&) . p) True
 48 |
 49 | --- Interface implementations ---
 50 |
 51 | public export
 52 | Eq a => Eq (LazyList a) where
 53 |   [] == [] = True
 54 |   x :: xs == y :: ys = x == y && xs == ys
 55 |   _ == _ = False
 56 |
 57 | public export
 58 | Ord a => Ord (LazyList a) where
 59 |   compare [] [] = EQ
 60 |   compare [] (x :: xs) = LT
 61 |   compare (x :: xs) [] = GT
 62 |   compare (x :: xs) (y :: ys)
 63 |      = case compare x y of
 64 |             EQ => compare xs ys
 65 |             c => c
 66 |
 67 | export
 68 | Show a => Show (LazyList a) where
 69 |   show []       = "[]"
 70 |   show (h :: t) = "[" ++ show' "" h t ++ "]"
 71 |     where
 72 |       -- Idris didn't like the lazyness involved when using the
 73 |       -- same implementation as for `List`, therefore, this was
 74 |       -- adjusted to first force the head and tail of the list.
 75 |       show' : String -> a -> LazyList a -> String
 76 |       show' acc h Nil       = acc ++ show h
 77 |       show' acc h (x :: xs) = show' (acc ++ show h ++ ", ") x xs
 78 |
 79 | public export
 80 | Semigroup (LazyList a) where
 81 |   xs <+> ys = xs ++ ys
 82 |
 83 | public export
 84 | Monoid (LazyList a) where
 85 |   neutral = []
 86 |
 87 | public export
 88 | Foldable LazyList where
 89 |   foldr op nil [] = nil
 90 |   foldr op nil (x :: xs) = x `op` foldr op nil xs
 91 |
 92 |   foldl op acc [] = acc
 93 |   foldl op acc (x :: xs) = foldl op (acc `op` x) xs
 94 |
 95 |   foldlM fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init
 96 |
 97 |   null []     = True
 98 |   null (_::_) = False
 99 |
100 |   foldMap f [] = neutral
101 |   foldMap f (x :: xs) = f x <+> foldMap f xs
102 |
103 | public export
104 | Functor LazyList where
105 |   map f [] = []
106 |   map f (x :: xs) = f x :: map f xs
107 |
108 | public export
109 | Applicative LazyList where
110 |   pure x = [x]
111 |   fs <*> vs = bindLazy (\f => map f vs) fs
112 |
113 | public export
114 | Alternative LazyList where
115 |   empty = []
116 |   (<|>) = (++)
117 |
118 | public export
119 | Monad LazyList where
120 |   m >>= f = bindLazy f m
121 |
122 | -- There is no Traversable instance for lazy lists.
123 | -- The result of a traversal will be a non-lazy list in general
124 | -- (you can't delay the "effect" of an applicative functor).
125 | public export
126 | traverse : Monad f => (a -> f b) -> LazyList a -> f (List b)
127 | traverse g [] = pure []
128 | traverse g (x::xs) = pure $ !(g x) :: !(traverse g xs)
129 |
130 | public export %inline
131 | for : Monad f => LazyList a -> (a -> f b) -> f (List b)
132 | for = flip traverse
133 |
134 | public export %inline
135 | sequence : Monad f => LazyList (f a) -> f (List a)
136 | sequence = traverse id
137 |
138 | -- Traverse a lazy list with lazy effect lazily
139 | public export
140 | traverse_ : Monad m => (a -> m b) -> LazyList a -> m Unit
141 | traverse_ f = foldrLazy ((>>) . ignore . f) (pure ())
142 |
143 | public export %inline
144 | for_ : Monad m => LazyList a -> (a -> m b) -> m Unit
145 | for_ = flip Lazy.traverse_
146 |
147 | public export %inline
148 | sequence_ : Monad m => LazyList (m a) -> m Unit
149 | sequence_ = Lazy.traverse_ id
150 |
151 | public export
152 | Zippable LazyList where
153 |   zipWith _ [] _ = []
154 |   zipWith _ _ [] = []
155 |   zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
156 |
157 |   zipWith3 _ [] _ _ = []
158 |   zipWith3 _ _ [] _ = []
159 |   zipWith3 _ _ _ [] = []
160 |   zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
161 |
162 |   unzip xs = (fst <$> xs, snd <$> xs)
163 |   unzipWith = unzip .: map
164 |
165 |   unzip3 xs = (fst <$> xs, fst . snd <$> xs, snd . snd <$> xs)
166 |   unzipWith3 = unzip3 .: map
167 |
168 | --- Lists creation ---
169 |
170 | public export
171 | fromList : List a -> LazyList a
172 | fromList []      = []
173 | fromList (x::xs) = x :: fromList xs
174 |
175 | covering
176 | public export
177 | iterate : (f : a -> Maybe a) -> (x : a) -> LazyList a
178 | iterate f x = x :: case f x of
179 |   Nothing => []
180 |   Just y  => iterate f y
181 |
182 | covering
183 | public export
184 | unfoldr : (b -> Maybe (a, b)) -> b -> LazyList a
185 | unfoldr f c = case f c of
186 |   Nothing     => []
187 |   Just (a, n) => a :: unfoldr f n
188 |
189 | public export
190 | iterateN : Nat -> (a -> a) -> a -> LazyList a
191 | iterateN Z     _ _ = []
192 | iterateN (S n) f x = x :: iterateN n f (f x)
193 |
194 | public export
195 | replicate : (n : Nat) -> (x : a) -> LazyList a
196 | replicate Z     _ = []
197 | replicate (S n) x = x :: replicate n x
198 |
199 | --- Functions acquiring parts of list ---
200 |
201 | public export
202 | head' : LazyList a -> Maybe a
203 | head' []     = Nothing
204 | head' (x::_) = Just x
205 |
206 | public export
207 | tail' : LazyList a -> Maybe (LazyList a)
208 | tail' []      = Nothing
209 | tail' (_::xs) = Just xs
210 |
211 | --- Functions for acquiring different types of sublists ---
212 |
213 | public export
214 | take : Nat -> LazyList a -> LazyList a
215 | take (S k) (x::xs) = x :: take k xs
216 | take _ _ = []
217 |
218 | public export
219 | drop : Nat -> LazyList a -> LazyList a
220 | drop Z     xs      = xs
221 | drop (S _) []      = []
222 | drop (S n) (_::xs) = drop n xs
223 |
224 | public export
225 | takeWhile : (a -> Bool) -> LazyList a -> LazyList a
226 | takeWhile p []      = []
227 | takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
228 |
229 | public export
230 | dropWhile : (a -> Bool) -> LazyList a -> LazyList a
231 | dropWhile p []      = []
232 | dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
233 |
234 | public export
235 | filter : (a -> Bool) -> LazyList a -> LazyList a
236 | filter p []      = []
237 | filter p (x::xs) = if p x then x :: filter p xs else filter p xs
238 |
239 | public export
240 | mapMaybe : (a -> Maybe b) -> LazyList a -> LazyList b
241 | mapMaybe f []      = []
242 | mapMaybe f (x::xs) = case f x of
243 |   Nothing => mapMaybe f xs
244 |   Just y  => y :: mapMaybe f xs
245 |
246 | namespace Stream
247 |
248 |   public export
249 |   take : Fuel -> Stream a -> LazyList a
250 |   take Dry _ = []
251 |   take (More f) (x :: xs) = x :: take f xs
252 |
253 | namespace Colist
254 |
255 |   public export
256 |   take : Fuel -> Colist a -> LazyList a
257 |   take Dry _ = []
258 |   take _ [] = []
259 |   take (More f) (x :: xs) = x :: take f xs
260 |
261 | namespace Colist1
262 |
263 |   public export
264 |   take : Fuel -> Colist1 a -> LazyList a
265 |   take fuel as = take fuel (forget as)
266 |
267 | --- Functions for extending lists ---
268 |
269 | public export
270 | mergeReplicate : a -> LazyList a -> LazyList a
271 | mergeReplicate sep []      = []
272 | mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys
273 |
274 | public export
275 | intersperse : a -> LazyList a -> LazyList a
276 | intersperse sep []      = []
277 | intersperse sep (x::xs) = x :: mergeReplicate sep xs
278 |
279 | public export
280 | intercalate : (sep : LazyList a) -> (xss : LazyList (LazyList a)) -> LazyList a
281 | intercalate sep xss = choice $ intersperse sep xss
282 |
283 | --- Functions converting lazy lists to something ---
284 |
285 | public export
286 | toColist : LazyList a -> Colist a
287 | toColist [] = []
288 | toColist (x::xs) = x :: toColist xs
289 |