
   0 | module Text.ILex.Interfaces
   1 | 
   2 | import Data.Buffer
   3 | import Data.Linear.Ref1
   4 | import Data.String
   5 | import Syntax.T1
   6 | import Text.ByteBounds
   7 | import Text.ILex.Char.UTF8
   8 | import Text.ILex.Parser
   9 | import Text.ILex.Util
  10 | import Text.ParseError
  11 | 
  12 | %hide Prelude.(>>)
  13 | %hide Prelude.(<*)
  14 | %hide Prelude.pure
  15 | 
  16 | %default total
  17 | 
  18 | --------------------------------------------------------------------------------
  19 | -- Interfaces
  20 | --------------------------------------------------------------------------------
  21 | 
  22 | ||| An interface for mutable parser stacks `s` that allow us to
  23 | ||| register custom errors, which will then be raised during parsing.
  24 | public export
  25 | interface HasBBErr (0 s : Type -> Type) (0 e : Type) | s where
  26 |   constructor MkBE
  27 |   error     : s q -> Ref q (Maybe $ BBErr e)
  28 | 
  29 | ||| An interface for mutable parser stacks `s` that facilitates
  30 | ||| parsing string tokens containing escape sequences.
  31 | public export
  32 | interface HasStringLits (0 s : Type -> Type) where
  33 |   constructor MkHSL
  34 |   strings   : s q -> Ref q (SnocList String)
  35 | 
  36 | ||| An interface for mutable parser stacks `s` that facilitates
  37 | ||| parsing string tokens containing escape sequences.
  38 | public export
  39 | interface HasStack (0 s : Type -> Type) (0 a : Type) | s where
  40 |   constructor MkHS
  41 |   stack     : s q -> Ref q a
  42 | 
  43 | --------------------------------------------------------------------------------
  44 | -- General Utilities
  45 | --------------------------------------------------------------------------------
  46 | 
  47 | export %inline
  48 | go : a -> (s q => F1 q (Index r)) -> (a,Step q r s)
  49 | go x f = (x, Run $ \(E x t) => f t)
  50 | 
  51 | export %inline
  52 | ign : a -> (s q => F1 q ()) -> (a,Step q r s)
  53 | ign x f = (x, Ign $ \(E x t) => f t)
  54 | 
  55 | export %inline
  56 | goBS : HasBytes s => a -> (s q => ByteString -> F1 q (Index r)) -> (a,Step q r s)
  57 | goBS x f = (x, Run $ \(E x t) => let bs # t := getBytes t in f bs t)
  58 | 
  59 | export %inline
  60 | goStr : HasBytes s => a -> (s q => String -> F1 q (Index r)) -> (a,Step q r s)
  61 | goStr x f = (x, Run $ \(E x t) => let bs # t := getBytes t in f (toString bs) t)
  62 | 
  63 | ||| Writes a mutable reference and returns the given result.
  64 | export %inline
  65 | writeAs : Ref q a -> a -> r -> F1 q r
  66 | writeAs ref v res = write1 ref v >> pure res
  67 | 
  68 | ||| Appends a value to mutable reference of a snoclist.
  69 | export %inline
  70 | push1 : Ref q (SnocList a) -> a -> F1' q
  71 | push1 ref v = T1.do
  72 |  ss <- read1 ref
  73 |  write1 ref (ss:<v)
  74 | 
  75 | ||| Drops and discards a the last entry from a snoclist
  76 | ||| stored in a mutable reference.
  77 | export %inline
  78 | pop1 : Ref q (SnocList a) -> F1' q
  79 | pop1 ref =
  80 |   read1 ref >>= \case
  81 |     sv:<_ => write1 ref sv
  82 |     _     => pure ()
  83 | 
  84 | ||| Returns the value stored in a mutable reference and
  85 | ||| overwrites it with the given replacement.
  86 | export %inline
  87 | replace1 : Ref q a -> a -> F1 q a
  88 | replace1 ref v = T1.do
  89 |   s <- read1 ref
  90 |   write1 ref v
  91 |   pure s
  92 | 
  93 | ||| Empties a mutable reference holding a snoclist and returns
  94 | ||| the corresponding list.
  95 | export %inline
  96 | getList : Ref q (SnocList a) -> F1 q (List a)
  97 | getList ref = T1.do
  98 |   sv <- replace1 ref [<]
  99 |   pure (sv <>> [])
 100 | 
 101 | ||| Returns the content of some mutable state implementing
 102 | ||| `HasStack`.
 103 | export %inline
 104 | getStack : HasStack s a => (sk : s q) => F1 q a
 105 | getStack = read1 (stack sk)
 106 | 
 107 | ||| Overwrites the content of some mutable state implementing
 108 | ||| `HasStack`.
 109 | export %inline
 110 | putStack : HasStack s a => (sk : s q) => a -> F1' q
 111 | putStack = write1 (stack sk)
 112 | 
 113 | ||| Like `putStack` but returns the given result.
 114 | export %inline
 115 | putStackAs : HasStack s a => (sk : s q) => a -> v -> F1 q v
 116 | putStackAs = writeAs (stack sk)
 117 | 
 118 | ||| Like `putStack` but returns the given result.
 119 | export %inline
 120 | putStackAsC : Cast b v => HasStack s a => (sk : s q) => a -> b -> F1 q v
 121 | putStackAsC res = putStackAs res . cast
 122 | 
 123 | ||| Reads and updates the stack.
 124 | export %inline
 125 | modStackAs : (0 s : _) -> HasStack s a => (sk : s q) => (a -> a) -> v -> F1 q v
 126 | modStackAs _ f v = getStack >>= \x => putStackAs (f x) v
 127 | 
 128 | ||| Appends a value to some mutable state implementing `HasStack`.
 129 | export %inline
 130 | pushStack : HasStack s (SnocList a) => (sk : s q) => a -> F1' q
 131 | pushStack = push1 (stack sk)
 132 | 
 133 | ||| Like `pushStack` but returns the given result.
 134 | export %inline
 135 | pushStackAs : HasStack s (SnocList a) => (sk : s q) => a -> v -> F1 q v
 136 | pushStackAs v res = pushStack v >> pure res
 137 | 
 138 | ||| A small utility for counting down a parser and returning one
 139 | ||| of two possible outcomes.
 140 | export %inline
 141 | countdown : Ref q Nat -> (ifSucc, ifZero : a) -> F1 q a
 142 | countdown ref s z t =
 143 |  let S k # t := read1 ref t | Z # t => z # t
 144 |   in writeAs ref k s t
 145 | 
 146 | ||| A small utility for counting down a parser and returning one
 147 | ||| of two possible actions.
 148 | export %inline
 149 | countdownAct : Ref q Nat -> (ifSucc, ifZero : F1 q a) -> F1 q a
 150 | countdownAct ref s z t =
 151 |  let S k # t := read1 ref t | Z # t => z t
 152 |      _   # t := write1 ref k t
 153 |   in s t
 154 | 
 155 | --------------------------------------------------------------------------------
 156 | -- String Literals
 157 | --------------------------------------------------------------------------------
 158 | 
 159 | parameters {auto sk  : s q}
 160 |            {auto pos : HasStringLits s}
 161 | 
 162 |   ||| Empties the `strings` field of some mutable state implementing
 163 |   ||| `HasStringLits` and returns the concatenated string literal.
 164 |   export %inline
 165 |   getStr : F1 q String
 166 |   getStr = T1.do
 167 |     sv <- replace1 (strings sk) [<]
 168 |     pure $ snocPack sv
 169 | 
 170 |   ||| Appends the given string to the `strings` field of some mutable
 171 |   ||| state implementing `HasStringLits`.
 172 |   export %inline
 173 |   pushStr' : String -> F1' q
 174 |   pushStr' str = push1 (strings sk) str
 175 | 
 176 |   ||| Appends the given string to the `strings` field of some mutable
 177 |   ||| state implementing `HasStringLits` and returns the given result.
 178 |   export %inline
 179 |   pushStr : Cast t (Index r) => t -> String -> F1 q (Index r)
 180 |   pushStr res str = T1.do
 181 |     push1 (strings sk) str
 182 |     pure (cast res)
 183 | 
 184 |   ||| Appends the given character to the `strings` field of some mutable
 185 |   ||| state implementing `HasStringLits` and returns the given result.
 186 |   export %inline
 187 |   pushChar : Cast t (Index r) => t -> Char -> F1 q (Index r)
 188 |   pushChar res = pushStr res . singleton
 189 | 
 190 |   ||| Appends the given unicode code point to the `strings` field of some mutable
 191 |   ||| state implementing `HasStringLits` and returns the given result.
 192 |   export %inline
 193 |   pushBits32 : Cast t (Index r) => t -> Bits32 -> F1 q (Index r)
 194 |   pushBits32 res = pushChar res . cast
 195 | 
 196 | --------------------------------------------------------------------------------
 197 | -- Bounds and Position
 198 | --------------------------------------------------------------------------------
 199 | 
 200 | parameters {auto sk   : s q}
 201 |            {auto hb   : HasBytes s}
 202 | 
 203 |   ||| Gets the absolute position of the
 204 |   ||| first byte of the current token.
 205 |   export %inline
 206 |   startPos : F1 q BytePos
 207 |   startPos = T1.do
 208 |     o <- read1 (offset sk)
 209 |     r <- read1 (relpos sk)
 210 |     pure (BP $ cast (cast o + r))
 211 | 
 212 |   ||| Gets the absolute position of the last byte of the current token.
 213 |   export %inline
 214 |   endPos : F1 q BytePos
 215 |   endPos = T1.do
 216 |     o <- startPos
 217 |     l <- read1 (len sk)
 218 |     pure (incLen l o)
 219 | 
 220 |   ||| Gets the bounds of the current token.
 221 |   export %inline
 222 |   bounds : F1 q ByteBounds
 223 |   bounds = T1.do
 224 |     s <- startPos
 225 |     l <- read1 (len sk)
 226 |     pure $ BB s (incLen l s)
 227 | 
 228 |   ||| Computes the given value and pairs it with the token bounds.
 229 |   export %inline
 230 |   bounded : F1 q a -> F1 q (ByteBounded a)
 231 |   bounded f t =
 232 |    let bs # t := Interfaces.bounds t
 233 |        v  # t := f t
 234 |     in B v bs # t
 235 | 
 236 |   ||| Pairs the given value with the token bounds.
 237 |   export %inline
 238 |   bounded' : a -> F1 q (ByteBounded a)
 239 |   bounded' v t =
 240 |    let bs # t := Interfaces.bounds t
 241 |     in B v bs # t
 242 | 
 243 |   ||| Pushes the current byte position onto the position stack.
 244 |   |||
 245 |   ||| This is often used when ecountering some "opening token"
 246 |   ||| (such as an opening quote or parenthesis) for which we later
 247 |   ||| expect a suitable closing token. If no closing token is encountered,
 248 |   ||| we typically want to fail with an error that lists the position
 249 |   ||| of the unclosed token.
 250 |   export %inline
 251 |   pushPosition : F1' q
 252 |   pushPosition = startPos >>= push1 (positions sk)
 253 | 
 254 |   ||| Discards the latest entry from the positions stack.
 255 |   export %inline
 256 |   popPosition : F1' q
 257 |   popPosition = pop1 (positions sk)
 258 | 
 259 |   popAndGetBounds : Nat -> F1 q ByteBounds
 260 |   popAndGetBounds n =
 261 |     read1 (positions sk) >>= \case
 262 |       sb:<b => writeAs (positions sk) sb (BB b $ incLen n b)
 263 |       [<]   => pure NoBB
 264 | 
 265 |   ||| Returns the bounds from start to end of some "enclosed" or
 266 |   ||| quoted region of text such as an expression in parantheses
 267 |   ||| or some text in quotes.
 268 |   export %inline
 269 |   closeBounds : F1 q ByteBounds
 270 |   closeBounds = T1.do
 271 |     pe <- endPos
 272 |     read1 (positions sk) >>= \case
 273 |       sb:<b => writeAs (positions sk) sb (BB b pe)
 274 |       [<]   => pure NoBB
 275 | 
 276 | --------------------------------------------------------------------------------
 277 | -- Error Handling
 278 | --------------------------------------------------------------------------------
 279 | 
 280 | parameters {auto hae : HasBBErr s e}
 281 | 
 282 |   ||| Writes the given exception to the `error` field of some
 283 |   ||| mutable state and returns the given result.
 284 |   export %inline
 285 |   failWith : (sk : s q) => BBErr e -> v -> F1 q v
 286 |   failWith = writeAs (error sk) . Just
 287 | 
 288 |   ||| Like `failWith`, but generates the bounds of the error from the
 289 |   ||| current position and the bytes read until the error occurred.
 290 |   export %inline
 291 |   failHere : HasBytes s => (sk : s q) => InnerError e -> v -> F1 q v
 292 |   failHere x res = T1.do
 293 |     bs <- bounds
 294 |     failWith (B x bs) res
 295 | 
 296 | --------------------------------------------------------------------------------
 297 | -- Terminals
 298 | --------------------------------------------------------------------------------
 299 | 
 300 | parameters {auto hbp : HasBytes s}
 301 |            (x        : a)
 302 | 
 303 |   export %inline
 304 |   ignore : (s q => F1 q ()) -> (a,Step q r s)
 305 |   ignore = ign x
 306 | 
 307 |   export %inline
 308 |   ignore' : (a,Step q r s)
 309 |   ignore' = ign x (() #)
 310 | 
 311 |   export %inline
 312 |   step : (s q => F1 q (Index r)) -> (a,Step q r s)
 313 |   step = go x
 314 | 
 315 |   export %inline
 316 |   step' : Cast t (Index r) => t -> (a,Step q r s)
 317 |   step' x = step (pure $ cast x)
 318 | 
 319 |   export %inline
 320 |   bytes : (s q => ByteString -> F1 q (Index r)) -> (a,Step q r s)
 321 |   bytes f = goBS x f
 322 | 
 323 |   export %inline
 324 |   string : (s q => String -> F1 q (Index r)) -> (a,Step q r s)
 325 |   string f = goStr x f
 326 | 
 327 |   ||| Recognizes the given character(s)
 328 |   ||| and uses it to update the parser state
 329 |   ||| as specified by `f`.
 330 |   |||
 331 |   ||| The current column is increased by one, and a new entry is pushed onto
 332 |   ||| the stack of bounds.
 333 |   export %inline
 334 |   opn : (s q => F1 q (Index r)) -> (a, Step q r s)
 335 |   opn f = step $ pushPosition >> f
 336 | 
 337 |   ||| Convenience alias for `copen . pure`.
 338 |   export %inline
 339 |   opn' : Cast t (Index r) => t -> (a, Step q r s)
 340 |   opn' v = opn $ pure (cast v)
 341 | 
 342 |   ||| Recognizes the given character(s) and uses it to update the parser state
 343 |   ||| as specified by `f`.
 344 |   |||
 345 |   ||| The current column is increased by `n`, and one `Position` entry
 346 |   ||| is popped from the stack.
 347 |   export %inline
 348 |   close : (s q => F1 q (Index r)) -> (a, Step q r s)
 349 |   close f = step $ popPosition >> f
 350 | 
 351 |   ||| Recognizes the given character(s) and uses it to
 352 |   ||| finalize and assemble a string literal.
 353 |   |||
 354 |   ||| The current column is increased by `n`, and one `Position` entry
 355 |   ||| is popped from the stack.
 356 |   export %inline
 357 |   closeStr :
 358 |        {auto hap : HasStringLits s}
 359 |     -> (s q => String -> F1 q (Index r))
 360 |     -> (a, Step q r s)
 361 |   closeStr f = close $ getStr >>= f
 362 | 
 363 |   ||| Recognizes the given character(s) and uses it to update the parser state
 364 |   ||| as specified by `f`.
 365 |   |||
 366 |   ||| The current column is increased by one, and on `Bounds` entry
 367 |   ||| is popped from the stack.
 368 |   export %inline
 369 |   closeWithBounds : (s q => ByteBounds -> F1 q (Index r)) -> (a, Step q r s)
 370 |   closeWithBounds f = step $ closeBounds >>= f
 371 | 
 372 |   ||| Recognizes the given character(s) and uses it to
 373 |   ||| finalize and assemble a string literal.
 374 |   |||
 375 |   ||| The current column is increased by `n`, and one `Position` entry
 376 |   ||| is popped from the stack.
 377 |   export %inline
 378 |   closeBoundedStr :
 379 |        {auto hap : HasStringLits s}
 380 |     -> (s q => ByteBounded String -> F1 q (Index r))
 381 |     -> (a, Step q r s)
 382 |   closeBoundedStr f = closeWithBounds $ \bs => getStr >>= \s => f (B s bs)
 383 | 
 384 | parameters {auto hbp : HasBytes s}
 385 | 
 386 |   ||| Lexes a single value based on its printed form. Returns
 387 |   ||| `Nothing` in case `display` returns the empty string.
 388 |   |||
 389 |   ||| For instance, `val show soSomething True` would recognice
 390 |   ||| the token `"True"` and invoke act with `True`.
 391 |   export
 392 |   val :
 393 |        (display : a -> String)
 394 |     -> (act     : a -> Step1 q r s)
 395 |     -> (value   : a)
 396 |     -> Maybe (RExp True, Step q r s)
 397 |   val display act v =
 398 |    let f := act v
 399 |     in case unpack (display v) of
 400 |          cs@(_::_) => Just $ step (chars cs) (f %search)
 401 |          []        => Nothing
 402 | 
 403 |   ||| Like `val` but for a value that can be displayed in
 404 |   ||| different ways.
 405 |   export
 406 |   valN :
 407 |        (displays : a -> List String)
 408 |     -> (act      : a -> Step1 q r s)
 409 |     -> (value    : a)
 410 |     -> List (RExp True, Step q r s)
 411 |   valN displays act v =
 412 |    let f := act v
 413 |     in mapMaybe (exp f . unpack) (displays v)
 414 |   where
 415 |     exp : Step1 q r s -> List Char -> Maybe (RExp True, Step q r s)
 416 |     exp f cs@(_::_)= Just $ step (chars cs) (f %search)
 417 |     exp f [] = Nothing
 418 | 
 419 |   ||| Specialized version of `val` that writes the lexed value
 420 |   ||| to a predefined mutable field of the parser stack.
 421 |   export %inline
 422 |   writeVal :
 423 |        (display : a -> String)
 424 |     -> (field   : s q -> Ref q a)
 425 |     -> Index r
 426 |     -> (value   : a)
 427 |     -> Maybe (RExp True, Step q r s)
 428 |   writeVal display field res =
 429 |     val display (\v,x => writeAs (field x) v res)
 430 | 
 431 |   ||| Specialized version of `valN` that writes the lexed value
 432 |   ||| to a predefined mutable field of the parser stack.
 433 |   export %inline
 434 |   writeValN :
 435 |        (displays : a -> List String)
 436 |     -> (field    : s q -> Ref q a)
 437 |     -> Index r
 438 |     -> (value    : a)
 439 |     -> List (RExp True, Step q r s)
 440 |   writeValN displays field res =
 441 |     valN displays (\v,x => writeAs (field x) v res)
 442 | 
 443 |   ||| Applies `val` to a list of values.
 444 |   |||
 445 |   ||| Highly useful in combination with the `Finite` interface from
 446 |   ||| the idris2-finite library.
 447 |   export %inline
 448 |   vals :
 449 |        (display : a -> String)
 450 |     -> (act     : a -> Step1 q r s)
 451 |     -> List a
 452 |     -> List (RExp True, Step q r s)
 453 |   vals display = mapMaybe . val display
 454 | 
 455 |   ||| Like `vals` but for values that can be displayed in
 456 |   ||| several ways.
 457 |   |||
 458 |   ||| Highly useful in combination with the `Finite` interface from
 459 |   ||| the idris2-finite library.
 460 |   export %inline
 461 |   valsN :
 462 |        (displays : a -> List String)
 463 |     -> (act      : a -> Step1 q r s)
 464 |     -> List a
 465 |     -> List (RExp True, Step q r s)
 466 |   valsN displays act vs = vs >>= valN displays act
 467 | 
 468 |   ||| Specialized version of `vals` that writes the lexed value
 469 |   ||| to a predefined mutable field of the parser stack.
 470 |   export %inline
 471 |   writeVals :
 472 |        (display : a -> String)
 473 |     -> (field   : s q -> Ref q a)
 474 |     -> (res     : Index r)
 475 |     -> List a
 476 |     -> List (RExp True, Step q r s)
 477 |   writeVals display field = mapMaybe . writeVal display field
 478 | 
 479 |   ||| Specialized version of `valsN` that writes the lexed value
 480 |   ||| to a predefined mutable field of the parser stack.
 481 |   export %inline
 482 |   writeValsN :
 483 |        (displays : a -> List String)
 484 |     -> (field    : s q -> Ref q a)
 485 |     -> (res      : Index r)
 486 |     -> List a
 487 |     -> List (RExp True, Step q r s)
 488 |   writeValsN displays field res vs = vs >>= writeValN displays field res
 489 | 
 490 | export
 491 | jsonSpace : RExp True
 492 | jsonSpace = oneof [' ','\t','\n','\r']
 493 | 
 494 | export %inline
 495 | jsonSpaces : RExp True
 496 | jsonSpaces = plus jsonSpace
 497 | 
 498 | export %inline
 499 | jsonSpaced : HasBytes s => Steps q r s -> Steps q r s
 500 | jsonSpaced xs = ignore' jsonSpaces :: xs
 501 | 
 502 | --------------------------------------------------------------------------------
 503 | -- Error handling
 504 | --------------------------------------------------------------------------------
 505 | 
 506 | parameters {auto he  : HasBBErr s e}
 507 |            {auto pos : HasBytes s}
 508 | 
 509 |   export
 510 |   raise : InnerError e -> Nat -> s q => v -> F1 q v
 511 |   raise err n res = T1.do
 512 |     ps <- startPos
 513 |     failWith (B err $ BB ps (incLen n ps)) res
 514 | 
 515 |   export
 516 |   unexpected : List String -> s q -> F1 q (BBErr e)
 517 |   unexpected strs sk =
 518 |     read1 (error sk) >>= \case
 519 |       Just x  => pure x
 520 |       Nothing => T1.do
 521 |        bb <- bounds
 522 |        bs <- getBytes
 523 |        case bs of
 524 |          BS 0 _  => pure (B EOI bb)
 525 |          BS 1 bv =>
 526 |           let b := bv `at` 0
 527 |               s := String.singleton (cast b)
 528 |            in case isAscii b of
 529 |                 True  => pure (B (Expected strs s) bb)
 530 |                 False => pure (B (InvalidByte b) bb)
 531 |          _ => pure (B (Expected strs (toString bs)) bb)
 532 | 
 533 |   export
 534 |   unclosed : String -> s q -> F1 q (BBErr e)
 535 |   unclosed str sk = T1.do
 536 |     bnds <- popAndGetBounds (length str)
 537 |     pure $ B (Unclosed str) bnds
 538 | 
 539 |   ||| Fails with `unclosed` if this is the end of input, otherwise
 540 |   ||| invokes `unexpected`.
 541 |   export
 542 |   unclosedIfEOI : String -> List String -> s q -> F1 q (BBErr e)
 543 |   unclosedIfEOI s ss sk =
 544 |     getBytes >>= \case
 545 |       BS 0 _ => unclosed s sk
 546 |       bs     => unexpected ss sk
 547 | 
 548 |   ||| Fails with `unclosed` if this is the end of input or
 549 |   ||| a linefeed character (`\n`, byte `0x0a`) was encountered,
 550 |   ||| otherwise, invokes `unexpected`.
 551 |   export
 552 |   unclosedIfNLorEOI : String -> List String -> s q -> F1 q (BBErr e)
 553 |   unclosedIfNLorEOI s ss sk =
 554 |     getBytes >>= \case
 555 |       BS 0 _ => unclosed s sk
 556 |       bs     => if elem 0x0a bs then unclosed s sk else unexpected ss sk
 557 | 
 558 |   export %inline
 559 |   errs :
 560 |        {n : _}
 561 |     -> List (Entry n $ s q -> F1 q (BBErr e))
 562 |     -> Arr32 n (s q -> F1 q (BBErr e))
 563 |   errs = arr32 n (unexpected [])
 564 | 
 565 | --------------------------------------------------------------------------------
 566 | -- Streaming
 567 | --------------------------------------------------------------------------------
 568 | 
 569 | ||| Never emits a chunk of values during streaming.
 570 | |||
 571 | ||| This is for parsers that produce a single value after consuming the
 572 | ||| whole input. Such a parser can still be used with the facilities
 573 | ||| from ilex-streams but will only emit a single value at the end of input.
 574 | ||| In general, such a parser consumes a linear amount of memory and can
 575 | ||| typically not be used to process very large amounts of data.
 576 | export
 577 | noChunk : s -> F1 q (Maybe a)
 578 | noChunk _ t = (Nothing # t)
 579 | 
 580 | ||| Extracts the values parsed so far from the parser stack
 581 | ||| and emits them during streaming.
 582 | export
 583 | snocChunk : HasStack s (SnocList a) => s q -> F1 q (Maybe $ List a)
 584 | snocChunk sk = T1.do
 585 |   ss <- replace1 (stack sk) [<]
 586 |   pure (maybeList ss)
 587 |