
   0 | ||| Utilities for working with chunks of data.
   1 | |||
   2 | ||| It is suggested to import this qualified `import FS.Chunk as C` or
   3 | ||| via the catch-all module `FS` and use qualified names such
   4 | ||| as `C.filter` for those functions that overlap with the ones
   5 | ||| from `FS.Pull`.
   6 | module FS.Chunk
   7 | 
   8 | import FS.Core as P
   9 | import FS.Pull as P
  10 | import Data.List
  11 | import Data.Maybe
  12 | import Data.Nat
  13 | 
  14 | %default total
  15 | 
  16 | --------------------------------------------------------------------------------
  17 | -- Chunk Size
  18 | --------------------------------------------------------------------------------
  19 | 
  20 | ||| Pulls and streams produce their output in chunks (lists of value)
  21 | ||| for reasons of efficiency, because the whole streaming machinery
  22 | ||| comes with quite a bit of a performance overhead.
  23 | |||
  24 | ||| Many functions for generating pure streams
  25 | ||| and pulls therefore take an auto-implicit value of type `ChunkSize`.
  26 | ||| If not provided explicitly, this defaults to 128.
  27 | public export
  28 | record ChunkSize where
  29 |   [noHints]
  30 |   constructor CS
  31 |   size        : Nat
  32 |   {auto 0 prf : IsSucc size}
  33 | 
  34 | export %inline
  35 | Eq ChunkSize where
  36 |   CS x == CS y = x == y
  37 | 
  38 | export %inline
  39 | Ord ChunkSize where
  40 |   compare (CS x) (CS y) = compare x y
  41 | 
  42 | export %inline
  43 | Show ChunkSize where
  44 |   show = show . size
  45 | 
  46 | export
  47 | fromInteger : (n : Integer) -> ChunkSize
  48 | fromInteger n =
  49 |   case cast {to = Nat} n of
  50 |     k@(S _) => CS k
  51 |     0       => CS 1
  52 | 
  53 | public export %inline %hint
  54 | defaultChunkSize : ChunkSize
  55 | defaultChunkSize = 128
  56 | 
  57 | --------------------------------------------------------------------------------
  58 | -- Chunk
  59 | --------------------------------------------------------------------------------
  60 | 
  61 | public export
  62 | data SplitRes : Type -> Type where
  63 |   Middle : (pre, post : c) -> SplitRes c
  64 |   All    : Nat -> SplitRes c
  65 | 
  66 | ||| A `Chunk c o` is a container type `c` holding elements of type `o`.
  67 | |||
  68 | ||| Examples include `List a` with element type `a` and `ByteString` with
  69 | ||| element type `Bits8`.
  70 | public export
  71 | interface Monoid c => Chunk (0 c,o : Type) | c where
  72 |   unfoldChunk    : ChunkSize => (s ->  Either r (o,s)) -> s -> UnfoldRes r s c
  73 |   replicateChunk : ChunkSize => o -> c
  74 |   isEmpty        : c -> Bool
  75 |   unconsChunk    : c -> Maybe (o, Maybe c)
  76 |   splitChunkAt   : Nat -> c -> SplitRes c
  77 |   breakChunk     : BreakInstruction -> (o -> Bool) -> c -> BreakRes c
  78 |   filterChunk    : (o -> Bool) -> c -> Maybe c
  79 | 
  80 | export
  81 | nonEmpty : Chunk c o => c -> Maybe c
  82 | nonEmpty v = if isEmpty v then Nothing else Just v
  83 | 
  84 | --------------------------------------------------------------------------------
  85 | -- Creating streams of chunks
  86 | --------------------------------------------------------------------------------
  87 | 
  88 | ||| Like `unfold` but generates chunks of values of up to the given size.
  89 | export %inline
  90 | unfold : ChunkSize => Chunk c o => s -> (s -> Either r (o,s)) -> Pull f c es r
  91 | unfold init g = P.unfold init (unfoldChunk g)
  92 | 
  93 | ||| Like `P.fill` but generates chunks of values of up to the given size.
  94 | export
  95 | fill : ChunkSize => (0 c : _) -> Chunk c o => o -> Pull f c es ()
  96 | fill _ v = P.fill (replicateChunk v)
  97 | 
  98 | ||| Like `P.iterate` but generates chunks of values of up to the given size.
  99 | export
 100 | iterate : ChunkSize => (0 c : _) -> Chunk c o => o -> (o -> o) -> Pull f c es ()
 101 | iterate _ v f = unfold v (\x => Right (x, f x))
 102 | 
 103 | ||| Like `P.replicate` but generates chunks of values of up to the given size.
 104 | export
 105 | replicate : ChunkSize => (0 c : _) -> Chunk c o => Nat -> o -> Stream f es c
 106 | replicate _ n v =
 107 |   Chunk.unfold n $ \case
 108 |     0   => Left ()
 109 |     S k => Right (v,k)
 110 | 
 111 | --------------------------------------------------------------------------------
 112 | -- Splitting Streams
 113 | --------------------------------------------------------------------------------
 114 | 
 115 | parameters {auto chnk : Chunk c o}
 116 | 
 117 |   ||| Splits the very first element from the head of a `Pull`
 118 |   export
 119 |   uncons : Pull f c es r -> Pull f q es (Either r (o, Pull f c es r))
 120 |   uncons p =
 121 |     assert_total $ P.uncons p >>= \case
 122 |       Left x => pure (Left x)
 123 |       Right (vs,q) => case unconsChunk vs of
 124 |         Just (el,rem) => pure $ Right (el,consMaybe rem q)
 125 |         Nothing => Chunk.uncons q
 126 | 
 127 |   ||| Emits the first `n` elements of a `Pull`, returning the remainder.
 128 |   export
 129 |   splitAt : Nat -> Pull f c es r -> Pull f c es (Pull f c es r)
 130 |   splitAt 0 p = pure p
 131 |   splitAt k p =
 132 |     assert_total $ P.uncons p >>= \case
 133 |       Left v      => pure (pure v)
 134 |       Right (vs,q) => case splitChunkAt k vs of
 135 |         Middle pre post => cons pre (pure $ cons post q)
 136 |         All n           => cons vs (Chunk.splitAt n q)
 137 | 
 138 |   ||| Emits the first `n` elements of a `Pull`, returning the remainder.
 139 |   export %inline
 140 |   take : Nat -> Pull f c es r -> Pull f c es ()
 141 |   take 0 = const $ pure ()
 142 |   take n = ignore . newScope . Chunk.splitAt n
 143 | 
 144 |   ||| Like `take` but limits the number of emitted values.
 145 |   |||
 146 |   ||| This fails with the given error in case the limit is exceeded.
 147 |   export %inline
 148 |   limit : Has e es => Lazy e -> Nat -> Pull f c es r -> Pull f c es r
 149 |   limit err n p = do
 150 |     q      <- Chunk.splitAt n p
 151 |     Left v <- peekRes q | Right _ => throw err
 152 |     pure v
 153 | 
 154 |   ||| Drops the first `n` elements of a `Pull`, returning the
 155 |   ||| remainder.
 156 |   export %inline
 157 |   drop : Nat -> Pull f c es r -> Pull f c es r
 158 |   drop k p = join $ drain (Chunk.splitAt k p)
 159 | 
 160 |   ||| Emits the first element of a `Pull`, returning the remainder.
 161 |   export %inline
 162 |   head : Pull f c es r -> Pull f c es ()
 163 |   head = Chunk.take 1
 164 | 
 165 |   ||| Discards the first element of a `Pull`.
 166 |   export %inline
 167 |   tail : Pull f c es r -> Pull f c es r
 168 |   tail = Chunk.drop 1
 169 | 
 170 |   ||| Breaks a pull as soon as the given predicate returns `True` for
 171 |   ||| an emitted element.
 172 |   |||
 173 |   ||| `orElse` determines what to do if the pull is exhausted before any
 174 |   ||| splitting of output occurred.
 175 |   |||
 176 |   ||| The `BreakInstruction` dictates, if the value, for which the
 177 |   ||| predicate held, should be emitted as part of the prefix or the
 178 |   ||| suffix, or if it should be discarded.
 179 |   export
 180 |   breakFull :
 181 |        (orElse : r -> Pull f c es r)
 182 |     -> BreakInstruction
 183 |     -> (o -> Bool)
 184 |     -> Pull f c es r
 185 |     -> Pull f c es (Pull f c es r)
 186 |   breakFull orElse bi pred = breakPull orElse (breakChunk bi pred)
 187 | 
 188 |   ||| Like `breakFull` but fails with an error if the `Pull` is
 189 |   ||| exhausted before the prediate returns `True`.
 190 |   export %inline
 191 |   forceBreakFull :
 192 |        {auto has : Has e es}
 193 |     -> Lazy e
 194 |     -> BreakInstruction
 195 |     -> (o -> Bool)
 196 |     -> Pull f c es r
 197 |     -> Pull f c es (Pull f c es r)
 198 |   forceBreakFull err = breakFull (const $ throw err)
 199 | 
 200 |   ||| Emits values until the given predicate returns `True`.
 201 |   |||
 202 |   ||| The `BreakInstruction` dictates, if the value, for which the
 203 |   ||| predicate held, should be emitted as part of the prefix or not.
 204 |   export
 205 |   takeUntil : BreakInstruction -> (o -> Bool) -> Pull f c es r -> Stream f es c
 206 |   takeUntil tf pred = ignore . newScope . Chunk.breakFull pure tf pred
 207 | 
 208 |   ||| Emits values until the given predicate returns `False`,
 209 |   ||| returning the remainder of the `Pull`.
 210 |   export %inline
 211 |   takeWhile : (o -> Bool) -> Pull f c es r -> Stream f es c
 212 |   takeWhile pred = Chunk.takeUntil DropHit (not . pred)
 213 | 
 214 |   ||| Like `takeWhile` but also includes the first failure.
 215 |   export %inline
 216 |   takeThrough : (o -> Bool) -> Pull f c es r -> Stream f es c
 217 |   takeThrough pred = Chunk.takeUntil TakeHit (not . pred)
 218 | 
 219 |   ||| Discards values until the given predicate returns `True`.
 220 |   |||
 221 |   ||| The `BreakInstruction` dictates, if the value, for which the
 222 |   ||| predicate held, should be emitted as part of the remainder or not.
 223 |   export
 224 |   dropUntil : BreakInstruction -> (o -> Bool) -> Pull f c es r -> Pull f c es r
 225 |   dropUntil tf pred p = drain (Chunk.breakFull pure tf pred p) >>= id
 226 | 
 227 |   ||| Drops values from a stream while the given predicate returns `True`,
 228 |   ||| returning the remainder of the stream.
 229 |   export %inline
 230 |   dropWhile : (o -> Bool) -> Pull f c es r -> Pull f c es r
 231 |   dropWhile pred = Chunk.dropUntil PostHit (not . pred)
 232 | 
 233 |   ||| Like `dropWhile` but also drops the first value where
 234 |   ||| the predicate returns `False`.
 235 |   export %inline
 236 |   dropThrough : (o -> Bool) -> Pull f c es r -> Pull f c es r
 237 |   dropThrough pred = Chunk.dropUntil DropHit (not . pred)
 238 | 
 239 |   ||| Splits a stream of chunks whenever an element fulfills the given
 240 |   ||| predicate.
 241 |   export
 242 |   split : (o -> Bool) -> Pull f c es r -> Pull f (List c)  es r
 243 |   split pred = scanFull neutral impl (map pure . nonEmpty)
 244 |     where
 245 |       loop : SnocList c -> Maybe c -> (Maybe $ List c, c)
 246 |       loop sc Nothing  = (Just $ sc <>> [], neutral)
 247 |       loop sc (Just x) =
 248 |         assert_total $ case breakChunk DropHit pred x of
 249 |           Broken x post => loop (sc :< fromMaybe neutral x) post
 250 |           Keep x        => (Just $ sc <>> [], x)
 251 | 
 252 |       impl : c -> c -> (Maybe $ List c, c)
 253 |       impl pre cur =
 254 |         case breakChunk DropHit pred cur of
 255 |           Broken x post => loop [<pre <+> fromMaybe neutral x] post
 256 |           Keep x        => (Nothing, pre <+> x)
 257 | 
 258 | --------------------------------------------------------------------------------
 259 | -- Maps and Filters
 260 | --------------------------------------------------------------------------------
 261 | 
 262 | nel : List a -> Maybe (List a)
 263 | nel [] = Nothing
 264 | nel xs = Just xs
 265 | 
 266 | ||| Maps elements of output via a partial function.
 267 | export
 268 | mapMaybe : (o -> Maybe p) -> Pull f (List o) es r -> Pull f (List p) es r
 269 | mapMaybe f = P.mapMaybe (nel . mapMaybe f)
 270 | 
 271 | ||| Element-wise filtering of a stream of chunks.
 272 | export %inline
 273 | filter : Chunk c o => (o -> Bool) -> Pull f c es r -> Pull f c es r
 274 | filter = P.mapMaybe . filterChunk
 275 | 
 276 | ||| Element-wise filtering of a stream of chunks.
 277 | export %inline
 278 | filterNot : Chunk c o => (o -> Bool) -> Pull f c es r -> Pull f c es r
 279 | filterNot pred = Chunk.filter (not . pred)
 280 | 
 281 | ||| Maps a function over all elements emitted by a pull.
 282 | export %inline
 283 | mapOutput : Functor t => (o -> p) -> Pull f (t o) es r -> Pull f (t p) es r
 284 | mapOutput = P.mapOutput . map
 285 | 
 286 | --------------------------------------------------------------------------------
 287 | -- Folds
 288 | --------------------------------------------------------------------------------
 289 | 
 290 | parameters {auto fld : Foldable t}
 291 | 
 292 |   export %inline
 293 |   fold : (p -> o -> p) -> p -> Pull f (t o) es r -> Pull f p es r
 294 |   fold g = P.fold (foldl g)
 295 | 
 296 |   ||| Like `fold` but instead of emitting the result as a single
 297 |   ||| value of output, it is paired with the `Pull`s result.
 298 |   export %inline
 299 |   foldPair : (p -> o -> p) -> p -> Pull f (t o) es r -> Pull f q es (p,r)
 300 |   foldPair g = P.foldPair (foldl g)
 301 | 
 302 |   ||| Convenience version of `foldPair` for working on streams.
 303 |   export %inline
 304 |   foldGet : (p -> o -> p) -> p -> Stream f es (t o) -> Pull f q es p
 305 |   foldGet g = P.foldGet (foldl g)
 306 | 
 307 |   ||| Like `foldC` but will not emit a value in case of an empty pull.
 308 |   export
 309 |   fold1 : Chunk (t o) o => (o -> o -> o) -> Pull f (t o) es r -> Pull f o es r
 310 |   fold1 g s =
 311 |     Chunk.uncons s >>= \case
 312 |       Left r      => pure r
 313 |       Right (v,q) => Chunk.fold g v q
 314 | 
 315 |   ||| Returns `True` if all emitted values of the given stream fulfill
 316 |   ||| the given predicate
 317 |   export %inline
 318 |   all : (o -> Bool) -> Pull f (t o) es r -> Stream f es Bool
 319 |   all pred = P.all (all pred)
 320 | 
 321 |   ||| Returns `True` if any of the emitted values of the given stream fulfills
 322 |   ||| the given predicate
 323 |   export %inline
 324 |   any : (o -> Bool) -> Pull f (t o) es r -> Stream f es Bool
 325 |   any pred = P.any (any pred)
 326 | 
 327 |   ||| Emits the sum over all elements emitted by a `Pull`.
 328 |   export %inline
 329 |   sum : Num o => Pull f (t o) es r -> Pull f o es r
 330 |   sum = Chunk.fold (+) 0
 331 | 
 332 |   ||| Emits the number of elements emitted by a `Pull`.
 333 |   export %inline
 334 |   count : Pull f (t o) es r -> Pull f Nat es r
 335 |   count = Chunk.fold (const . S) 0
 336 | 
 337 |   ||| Emits the largest output encountered.
 338 |   export %inline
 339 |   maximum : Chunk (t o) o => Ord o => Pull f (t o) es r -> Pull f o es r
 340 |   maximum = Chunk.fold1 max
 341 | 
 342 |   ||| Emits the smallest output encountered.
 343 |   export %inline
 344 |   minimum : Chunk (t o) o => Ord o => Pull f (t o) es r -> Pull f o es r
 345 |   minimum = Chunk.fold1 min
 346 | 
 347 |   ||| Emits the smallest output encountered.
 348 |   export %inline
 349 |   mappend : Chunk (t o) o => Semigroup o => Pull f (t o) es r -> Pull f o es r
 350 |   mappend = Chunk.fold1 (<+>)
 351 | 
 352 |   ||| Accumulates the emitted values over a monoid.
 353 |   |||
 354 |   ||| Note: This corresponds to a left fold, so it will
 355 |   |||       run in quadratic time for monoids that are
 356 |   |||       naturally accumulated from the right (such as List)
 357 |   export %inline
 358 |   foldMap : Monoid m => (o -> m) -> Pull f (t o) es r -> Pull f m es r
 359 |   foldMap f = Chunk.fold (\v,el => v <+> f el) neutral
 360 | 
 361 | --------------------------------------------------------------------------------
 362 | -- Scans
 363 | --------------------------------------------------------------------------------
 364 | 
 365 | public export
 366 | interface Functor f => Scan f where
 367 |   scanChunk : (s -> o -> (p,s)) -> s -> f o -> (f p, s)
 368 | 
 369 |   escanChunk : (s -> o -> Either e (p,s)) -> s -> f o -> Either e (f p, s)
 370 | 
 371 | parameters {auto sca : Scan t}
 372 | 
 373 |   ||| Computes a stateful running total over all elements emitted by a
 374 |   ||| pull.
 375 |   export %inline
 376 |   scan : s -> (s -> o -> (p,s)) -> Pull f (t o) es r -> Pull f (t p) es r
 377 |   scan ini f = P.scan ini (scanChunk f)
 378 | 
 379 |   ||| Like `scan` but returns the final state as the pull's result
 380 |   export %inline
 381 |   scanReturn : s -> (s -> o -> (p,s)) -> Stream f es (t o) -> Pull f (t p) es s
 382 |   scanReturn ini f = P.scanReturn ini (scanChunk f)
 383 | 
 384 |   ||| Like `scan` but returns the final state as the pull's result
 385 |   export %inline
 386 |   escanReturn :
 387 |        s
 388 |     -> (s -> o -> Result es (p,s))
 389 |     -> Stream f es (t o)
 390 |     -> Pull f (t p) es s
 391 |   escanReturn ini f = P.escanReturn ini (escanChunk f)
 392 | 
 393 |   ||| Zips the input with a running total according to `s`, up to but
 394 |   ||| not including the current element. Thus the initial
 395 |   ||| `vp` value is the first emitted to the output:
 396 |   export
 397 |   zipWithScan : p -> (p -> o -> p) -> Pull f (t o) es r -> Pull f (t (o,p)) es r
 398 |   zipWithScan vp fun =
 399 |     Chunk.scan vp $ \vp1,vo => let vp2 := fun vp1 vo in ((vo, vp1),vp2)
 400 | 
 401 |   ||| Like `zipWithScan` but the running total is including the current element.
 402 |   export
 403 |   zipWithScan1 : p -> (p -> o -> p) -> Pull f (t o) es r -> Pull f (t (o,p)) es r
 404 |   zipWithScan1 vp fun =
 405 |     Chunk.scan vp $ \vp1,vo => let vp2 := fun vp1 vo in ((vo, vp2),vp2)
 406 | 
 407 |   ||| Pairs each element in the stream with its 0-based index.
 408 |   export %inline
 409 |   zipWithIndex : Pull f (t o) es r -> Pull f (t (o,Nat)) es r
 410 |   zipWithIndex = Chunk.zipWithScan 0 (\n,_ => S n)
 411 | 
 412 |   ||| Pairs each element in the stream with its 1-based count.
 413 |   export %inline
 414 |   zipWithCount : Pull f (t o) es r -> Pull f (t (o,Nat)) es r
 415 |   zipWithCount = Chunk.zipWithScan 1 (\n,_ => S n)
 416 | 
 417 |   ||| Emits the count of each element.
 418 |   export %inline
 419 |   runningCount : Pull f (t o) es r -> Pull f (t Nat) es r
 420 |   runningCount = Chunk.scan 1 (\n,_ => (n, S n))
 421 | 
 422 | --------------------------------------------------------------------------------
 423 | -- List Implementation
 424 | --------------------------------------------------------------------------------
 425 | 
 426 | %inline
 427 | len : SnocList a -> Maybe (List a)
 428 | len = nel . (<>> [])
 429 | 
 430 | broken : SnocList a -> List a -> BreakRes (List a)
 431 | broken sx xs = Broken (len sx) (nel xs)
 432 | 
 433 | unfoldList :
 434 |      SnocList o
 435 |   -> Nat
 436 |   -> (s -> Either r (o,s))
 437 |   -> s
 438 |   -> UnfoldRes r s (List o)
 439 | unfoldList sx 0     f x = More (sx <>> []) x
 440 | unfoldList sx (S k) f x =
 441 |   case f x of
 442 |     Right (v,x2) => unfoldList (sx:<v) k f x2
 443 |     Left res     => Last res (sx <>> [])
 444 | 
 445 | splitAtList : SnocList o -> Nat -> List o -> SplitRes (List o)
 446 | splitAtList sx (S k) (h::t) = splitAtList (sx :< h) k t
 447 | splitAtList sx n     []     = All n
 448 | splitAtList sx 0     xs     = Middle (sx <>> []) xs
 449 | 
 450 | breakList :
 451 |      SnocList a
 452 |   -> BreakInstruction
 453 |   -> (a -> Bool)
 454 |   -> List a
 455 |   -> BreakRes (List a)
 456 | breakList sx b f []        = Keep (sx <>> [])
 457 | breakList sx b f (x :: xs) =
 458 |   case f x of
 459 |     True => case b of
 460 |       TakeHit => broken (sx :< x) xs
 461 |       PostHit => broken sx (x::xs)
 462 |       DropHit => broken sx xs
 463 |     False => breakList (sx :< x) b f xs
 464 | 
 465 | export
 466 | Chunk (List a) a where
 467 |   unfoldChunk @{CS (S n)} f x =
 468 |     case f x of
 469 |       Left res     => Done res
 470 |       Right (v,x2) => unfoldList [<v] n f x2
 471 | 
 472 |   replicateChunk @{CS n} = List.replicate n
 473 | 
 474 |   isEmpty [] = True
 475 |   isEmpty _  = False
 476 | 
 477 |   unconsChunk []     = Nothing
 478 |   unconsChunk (h::t) = Just (h, nel t)
 479 | 
 480 |   splitChunkAt = splitAtList [<]
 481 | 
 482 |   breakChunk = breakList [<]
 483 | 
 484 |   filterChunk pred = nel . filter pred
 485 | 
 486 | scanListImpl : SnocList p -> (s -> o -> (p,s)) -> s -> List o -> (List p,s)
 487 | scanListImpl sx f v []        = (sx <>> [], v)
 488 | scanListImpl sx f v (x :: xs) =
 489 |  let (vp,v2) := f v x
 490 |   in scanListImpl (sx :< vp) f v2 xs
 491 | 
 492 | escanListImpl :
 493 |      SnocList p
 494 |   -> (s -> o -> Either e (p,s))
 495 |   -> s
 496 |   -> List o
 497 |   -> Either e (List p,s)
 498 | escanListImpl sx f v []        = Right (sx <>> [], v)
 499 | escanListImpl sx f v (x :: xs) =
 500 |  let Right (vp,v2) := f v x | Left x => Left x
 501 |   in escanListImpl (sx :< vp) f v2 xs
 502 | 
 503 | export %inline
 504 | Scan List where
 505 |   scanChunk = scanListImpl [<]
 506 |   escanChunk = escanListImpl [<]
 507 | 
 508 | --------------------------------------------------------------------------------
 509 | -- Zipping
 510 | --------------------------------------------------------------------------------
 511 | 
 512 | public export
 513 | data ZipRes : (a,b,c : Type) -> Type where
 514 |   ZB : List c -> ZipRes a b c
 515 |   ZL : List a -> List c -> ZipRes a b c
 516 |   ZR : List b -> List c -> ZipRes a b c
 517 | 
 518 | zipImpl : SnocList c -> (a -> b -> c) -> List a -> List b -> ZipRes a b c
 519 | zipImpl sx f (x::xs) (y::ys) = zipImpl (sx :< f x y) f xs ys
 520 | zipImpl sx f [] [] = ZB (sx <>> [])
 521 | zipImpl sx f xs [] = ZL xs (sx <>> [])
 522 | zipImpl sx f [] ys = ZR ys (sx <>> [])
 523 | 
 524 | zipWith_ :
 525 |      (this : Stream f es (List o1))
 526 |   -> (that : Stream f es (List o2))
 527 |   -> (k1   : ZipWithLeft f es (List o1) (List o3))
 528 |   -> (k2   : ZipWithLeft f es (List o2) (List o3))
 529 |   -> (k3   : Stream f es (List o2) -> Stream f es (List o3))
 530 |   -> (fun  : o1 -> o2 -> o3)
 531 |   -> Stream f es (List o3)
 532 | zipWith_ this that k1 k2 k3 fun = do
 533 |   Just l1 <- stepLeg this | Nothing => k3 that
 534 |   Just l2 <- stepLeg that | Nothing => k1 l1.out l1.pull
 535 |   go l1 l2
 536 | 
 537 |   where
 538 |     go : StepLeg f es (List o1) -> StepLeg f es (List o2) -> Stream f es (List o3)
 539 |     go l1 l2 =
 540 |       case zipImpl [<] fun l1.out l2.out of
 541 |         ZB cs     => do
 542 |           emit cs
 543 |           Just l12 <- step l1 | Nothing => k3 l2.pull
 544 |           Just l22 <- step l2 | Nothing => k1 l12.out l12.pull
 545 |           assert_total $ go l12 l22
 546 |         ZL as cs => do
 547 |           emit cs
 548 |           Just l22 <- step l2 | Nothing => k1 as l1.pull
 549 |           assert_total $ go ({out := as} l1) l22
 550 |         ZR bs cs => do
 551 |           emit cs
 552 |           Just l12 <- step l1 | Nothing => k2 bs l2.pull
 553 |           assert_total $ go l12 ({out := bs} l2)
 554 | 
 555 | ||| Determinsitically zips elements with the specified function, terminating
 556 | ||| when the ends of both branches are reached naturally, padding the left
 557 | ||| branch with `pad1` and padding the right branch with `pad2` as necessary.
 558 | export
 559 | zipAllWith :
 560 |      (pad1 : o1)
 561 |   -> (pad2 : o2)
 562 |   -> (o1 -> o2 -> o3)
 563 |   -> (this : Stream f es (List o1))
 564 |   -> (that : Stream f es (List o2))
 565 |   -> Stream f es (List o3)
 566 | zipAllWith pad1 pad2 fun this that =
 567 |  let kL := Chunk.mapOutput (`fun` pad2)
 568 |      kR := Chunk.mapOutput (fun pad1)
 569 |      k1 := \x,y => emit (map (`fun` pad2) x) >> kL y
 570 |      k2 := \x,y => emit (map (fun pad1) x) >> kR y
 571 |   in zipWith_ this that k1 k2 kR fun
 572 | 
 573 | ||| `zipAllWith` specialized to returning a pair of values
 574 | export %inline
 575 | zipAll :
 576 |      (pad1 : o1)
 577 |   -> (pad2 : o2)
 578 |   -> (this : Stream f es (List o1))
 579 |   -> (that : Stream f es (List o2))
 580 |   -> Stream f es (List (o1,o2))
 581 | zipAll pad1 pad2 = zipAllWith pad1 pad2 MkPair
 582 | 
 583 | ||| Deterministically zips elements, terminating when the end
 584 | ||| of either branch is reached naturally.
 585 | export %inline
 586 | zipWith :
 587 |      (o1 -> o2 -> o3)
 588 |   -> (this : Stream f es (List o1))
 589 |   -> (that : Stream f es (List o2))
 590 |   -> Stream f es (List o3)
 591 | zipWith fun this that =
 592 |   zipWith_ this that (\_,_ => pure ()) (\_,_ => pure ()) (\_ => pure ()) fun
 593 | 
 594 | ||| `zipAll` specialized to returning a pair of values
 595 | export %inline
 596 | zip :
 597 |      (this : Stream f es (List o1))
 598 |   -> (that : Stream f es (List o2))
 599 |   -> Stream f es (List (o1,o2))
 600 | zip = zipWith MkPair
 601 | 
 602 | export %inline
 603 | zipRight :
 604 |      (this : Stream f es (List o1))
 605 |   -> (that : Stream f es (List o2))
 606 |   -> Stream f es (List o2)
 607 | zipRight = Chunk.zipWith (\_ => id)
 608 | 
 609 | export %inline
 610 | zipLeft :
 611 |      (this : Stream f es (List o1))
 612 |   -> (that : Stream f es (List o2))
 613 |   -> Stream f es (List o1)
 614 | zipLeft = Chunk.zipWith const
 615 |