module Data.Stream import Data.List ||| The first element of an infinite streampublic exporthead : Stream a -> ahead (x::xs) = x ||| Drop the first n elements from the stream||| @ n how many elements to droppublic exportdrop : (n : Nat) -> Stream a -> Stream adrop Z     xs = xsdrop (S k) (x::xs) = drop k xs ||| An infinite stream of repetitions of the same thingpublic exportrepeat : a -> Stream arepeat x = x :: repeat x ||| Generate an infinite stream by repeatedly applying a function||| @ f the function to iterate||| @ x the initial value that will be the head of the streampublic exportiterate : (f : a -> a) -> (x : a) -> Stream aiterate f x = x :: iterate f (f x) ||| Get the nth element of a streampublic exportindex : Nat -> Stream a -> aindex Z     (x::xs) = xindex (S k) (x::xs) = index k xs ||| Combine two streams element-wise using a function.|||||| @ f the function to combine elements with||| @ xs the first stream of elements||| @ ys the second stream of elementsexportzipWith : (f : a -> b -> c) -> (xs : Stream a) -> (ys : Stream b) -> Stream czipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys ||| Combine three streams by applying a function element-wise along themexportzipWith3 : (a -> b -> c -> d) -> Stream a -> Stream b -> Stream c -> Stream dzipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs ||| Create a stream of pairs from two streamsexportzip : Stream a -> Stream b -> Stream (a, b)zip = zipWith (\x,y => (x,y)) ||| Combine three streams into a stream of tuples elementwiseexportzip3 : Stream a -> Stream b -> Stream c -> Stream (a, b, c)zip3 = zipWith3 (\x,y,z => (x,y,z)) ||| Create a pair of streams from a stream of pairsexportunzip : Stream (a, b) -> (Stream a, Stream b)unzip xs = (map fst xs, map snd xs) ||| Split a stream of three-element tuples into three streamsexportunzip3 : Stream (a, b, c) -> (Stream a, Stream b, Stream c)unzip3 xs = (map (\(x,_,_) => x) xs, map (\(_,x,_) => x) xs, map (\(_,_,x) => x) xs) ||| Return the diagonal elements of a stream of streamsexportdiag : Stream (Stream a) -> Stream adiag ((x::xs)::xss) = x :: diag (map tail xss) ||| Produce a Stream of left folds of prefixes of the given Stream||| @ f the combining function||| @ acc the initial value||| @ xs the Stream to processexportscanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream ascanl f acc (x :: xs) = acc :: scanl f (f acc x) xs ||| Produce a Stream repeating a sequence||| @ xs the sequence to repeat||| @ ok proof that the list is non-emptyexportcycle : (xs : List a) -> {auto ok : NonEmpty xs} -> Stream acycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs  where cycle' : List a -> Stream a        cycle' []        = x :: cycle' xs        cycle' (y :: ys) = y :: cycle' ys public exportpartialtakeUntil : (n -> Bool) -> Stream n -> List ntakeUntil p (x :: xs)    = if p x         then [x]         else x :: takeUntil p xs public exportpartialtakeBefore : (n -> Bool) -> Stream n -> List ntakeBefore p (x :: xs)    = if p x         then []         else x :: takeBefore p xs exportApplicative Stream where  pure = repeat  (<*>) = zipWith apply exportMonad Stream where  s >>= f = diag (map f s)