
   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 -> (a,Step q r s)
  53 | ign x = (x, Ign)
  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 s # t := Parser.getString t in f s 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 | ||| Appends a value to some mutable state implementing `HasStack`.
 102 | export %inline
 103 | pushStack : HasStack s (SnocList a) => (sk : s q) => a -> F1' q
 104 | pushStack = push1 (stack sk)
 105 | 
 106 | ||| Like `pushStack` but returns the given result.
 107 | export %inline
 108 | pushStackAs : HasStack s (SnocList a) => (sk : s q) => a -> v -> F1 q v
 109 | pushStackAs v res = pushStack v >> pure res
 110 | 
 111 | ||| A small utility for counting down a parser and returning one
 112 | ||| of two possible outcomes.
 113 | export %inline
 114 | countdown : Ref q Nat -> (ifSucc, ifZero : a) -> F1 q a
 115 | countdown ref s z t =
 116 |  let S k # t := read1 ref t | Z # t => z # t
 117 |   in writeAs ref k s t
 118 | 
 119 | ||| A small utility for counting down a parser and returning one
 120 | ||| of two possible actions.
 121 | export %inline
 122 | countdownAct : Ref q Nat -> (ifSucc, ifZero : F1 q a) -> F1 q a
 123 | countdownAct ref s z t =
 124 |  let S k # t := read1 ref t | Z # t => z t
 125 |      _   # t := write1 ref k t
 126 |   in s t
 127 | 
 128 | --------------------------------------------------------------------------------
 129 | -- String Literals
 130 | --------------------------------------------------------------------------------
 131 | 
 132 | parameters {auto sk  : s q}
 133 |            {auto pos : HasStringLits s}
 134 | 
 135 |   ||| Empties the `strings` field of some mutable state implementing
 136 |   ||| `HasStringLits` and returns the concatenated string literal.
 137 |   export %inline
 138 |   getStr : F1 q String
 139 |   getStr = T1.do
 140 |     sv <- replace1 (strings sk) [<]
 141 |     pure $ snocPack sv
 142 | 
 143 |   ||| Appends the given string to the `strings` field of some mutable
 144 |   ||| state implementing `HasStringLits`.
 145 |   export %inline
 146 |   pushStr' : String -> F1' q
 147 |   pushStr' str = push1 (strings sk) str
 148 | 
 149 |   ||| Appends the given string to the `strings` field of some mutable
 150 |   ||| state implementing `HasStringLits` and returns the given result.
 151 |   export %inline
 152 |   pushStr : Cast t (Index r) => t -> String -> F1 q (Index r)
 153 |   pushStr res str = T1.do
 154 |     push1 (strings sk) str
 155 |     pure (cast res)
 156 | 
 157 |   ||| Appends the given character to the `strings` field of some mutable
 158 |   ||| state implementing `HasStringLits` and returns the given result.
 159 |   export %inline
 160 |   pushChar : Cast t (Index r) => t -> Char -> F1 q (Index r)
 161 |   pushChar res = pushStr res . singleton
 162 | 
 163 |   ||| Appends the given unicode code point to the `strings` field of some mutable
 164 |   ||| state implementing `HasStringLits` and returns the given result.
 165 |   export %inline
 166 |   pushBits32 : Cast t (Index r) => t -> Bits32 -> F1 q (Index r)
 167 |   pushBits32 res = pushChar res . cast
 168 | 
 169 | --------------------------------------------------------------------------------
 170 | -- Bounds and Position
 171 | --------------------------------------------------------------------------------
 172 | 
 173 | parameters {auto sk   : s q}
 174 |            {auto hb   : HasBytes s}
 175 | 
 176 |   ||| Gets the absolute position of the
 177 |   ||| first byte of the current token.
 178 |   export %inline
 179 |   startPos : F1 q BytePos
 180 |   startPos = T1.do
 181 |     LN f <- read1 (from sk)
 182 |     pure $ case f of
 183 |       0 => BP (prevOffset sk)
 184 |       _ => BP (curOffset sk + f)
 185 | 
 186 |   ||| Gets the absolute position of the last byte of the current token.
 187 |   export %inline
 188 |   endPos : F1 q BytePos
 189 |   endPos t =
 190 |     let LN rf # t := read1 (from sk) t
 191 |         LN rt # t := read1 (till sk) t
 192 |         coff         := curOffset sk
 193 |         till         := coff + rt
 194 |      in case rf of
 195 |           0 => let from := prevOffset sk in endPos from till # t
 196 |           _ => let from := coff + rf     in endPos from till # t
 197 | 
 198 |   ||| Gets the bounds of the current token.
 199 |   export %inline
 200 |   bounds : F1 q ByteBounds
 201 |   bounds t =
 202 |     let LN rf # t := read1 (from sk) t
 203 |         LN rt # t := read1 (till sk) t
 204 |         coff      := curOffset sk
 205 |         till      := coff + rt
 206 |      in case rf of
 207 |           0 => let from := prevOffset sk in BB (BP from) (endPos from till) # t
 208 |           _ => let from := coff + rf     in BB (BP from) (endPos from till) # t
 209 | 
 210 |   ||| Computes the given value and pairs it with the token bounds.
 211 |   export %inline
 212 |   bounded : F1 q a -> F1 q (ByteBounded a)
 213 |   bounded f t =
 214 |    let bs # t := Interfaces.bounds t
 215 |        v  # t := f t
 216 |     in B v bs # t
 217 | 
 218 |   ||| Pairs the given value with the token bounds.
 219 |   export %inline
 220 |   bounded' : a -> F1 q (ByteBounded a)
 221 |   bounded' v t =
 222 |    let bs # t := Interfaces.bounds t
 223 |     in B v bs # t
 224 | 
 225 |   ||| Pushes the current byte position onto the position stack.
 226 |   |||
 227 |   ||| This is often used when ecountering some "opening token"
 228 |   ||| (such as an opening quote or parenthesis) for which we later
 229 |   ||| expect a suitable closing token. If no closing token is encountered,
 230 |   ||| we typically want to fail with an error that lists the position
 231 |   ||| of the unclosed token.
 232 |   export %inline
 233 |   pushPosition : F1' q
 234 |   pushPosition = startPos >>= push1 (positions sk)
 235 | 
 236 |   ||| Discards the latest entry from the positions stack.
 237 |   export %inline
 238 |   popPosition : F1' q
 239 |   popPosition = pop1 (positions sk)
 240 | 
 241 |   popAndGetBounds : Nat -> F1 q ByteBounds
 242 |   popAndGetBounds n =
 243 |     read1 (positions sk) >>= \case
 244 |       sb:<b => writeAs (positions sk) sb (BB b $ incLen n b)
 245 |       [<]   => pure NoBB
 246 | 
 247 |   ||| Returns the bounds from start to end of some "enclosed" or
 248 |   ||| quoted region of text such as an expression in parantheses
 249 |   ||| or some text in quotes.
 250 |   export %inline
 251 |   closeBounds : F1 q ByteBounds
 252 |   closeBounds = T1.do
 253 |     pe <- endPos
 254 |     read1 (positions sk) >>= \case
 255 |       sb:<b => writeAs (positions sk) sb (BB b pe)
 256 |       [<]   => pure NoBB
 257 | 
 258 | --------------------------------------------------------------------------------
 259 | -- Parser Stack
 260 | --------------------------------------------------------------------------------
 261 | 
 262 | parameters {auto hs : HasStack s a}
 263 |            {auto sk : s q}
 264 |   ||| Returns the content of some mutable state implementing
 265 |   ||| `HasStack`.
 266 |   export %inline
 267 |   getStack : F1 q a
 268 |   getStack = read1 (stack sk)
 269 | 
 270 |   ||| Overwrites the content of some mutable state implementing
 271 |   ||| `HasStack`.
 272 |   export %inline
 273 |   putStack : a -> F1' q
 274 |   putStack = write1 (stack sk)
 275 | 
 276 |   ||| Like `putStack` but returns the given result.
 277 |   export %inline
 278 |   putStackAs : a -> v -> F1 q v
 279 |   putStackAs = writeAs (stack sk)
 280 | 
 281 |   ||| Like `putStack` but returns the given result.
 282 |   export %inline
 283 |   putStackAsC : Cast b v => a -> b -> F1 q v
 284 |   putStackAsC res = putStackAs res . cast
 285 | 
 286 |   export %inline
 287 |   withStack : (a -> F1 q b) -> F1 q b
 288 |   withStack f = getStack >>= f
 289 | 
 290 |   export %inline
 291 |   boundsWithStack : HasBytes s => (ByteBounds -> a -> F1 q b) -> F1 q b
 292 |   boundsWithStack f = bounds >>= withStack . f
 293 | 
 294 |   export %inline
 295 |   posWithStack : HasBytes s => (BytePos -> a -> F1 q b) -> F1 q b
 296 |   posWithStack f = startPos >>= withStack . f
 297 | 
 298 |   export %inline
 299 |   boundedWithStack : HasBytes s => (ByteBounded x -> a -> F1 q b) -> x -> F1 q b
 300 |   boundedWithStack f v = bounds >>= withStack . f . B v
 301 | 
 302 | 
 303 | ||| Reads and updates the stack.
 304 | export %inline
 305 | modStackAs : (0 s : _) -> HasStack s a => s q => (a -> a) -> v -> F1 q v
 306 | modStackAs _ f v = getStack >>= \x => putStackAs (f x) v
 307 | 
 308 | export %inline
 309 | posModStack :
 310 |      (0 s : _)
 311 |   -> {auto hb : HasBytes s}
 312 |   -> {auto hs : HasStack s a}
 313 |   -> {auto sk : s q}
 314 |   -> (a -> BytePos -> a)
 315 |   -> v
 316 |   -> F1 q v
 317 | posModStack s f v = T1.do
 318 |   p <- startPos
 319 |   x <- getStack
 320 |   putStackAs (f x p) v
 321 | 
 322 | --------------------------------------------------------------------------------
 323 | -- Error Handling
 324 | --------------------------------------------------------------------------------
 325 | 
 326 | parameters {auto hae : HasBBErr s e}
 327 |            {auto sk  : s q}
 328 | 
 329 |   export %inline
 330 |   ifNoErrorRaised : F1 q (BBErr e) -> F1 q (BBErr e)
 331 |   ifNoErrorRaised raise = read1 (error sk) >>= maybe raise pure
 332 | 
 333 |   export
 334 |   unexpectedErr : HasBytes s => List String -> F1 q (InnerError e)
 335 |   unexpectedErr ss = T1.do
 336 |     bs <- getBytes
 337 |     pure $ case bs of
 338 |       BS 0 _  => EOI
 339 |       BS 1 bv =>
 340 |        let b := bv `at` 0
 341 |            s := String.singleton (cast b)
 342 |         in case isAscii b of
 343 |              True  => Expected ss s
 344 |              False => InvalidByte b
 345 |       _ => Expected ss (toString bs)
 346 | 
 347 |   export
 348 |   unclosedErr : HasBytes s => String -> F1 q (BBErr e)
 349 |   unclosedErr str = T1.do
 350 |     bnds <- popAndGetBounds (length str)
 351 |     pure $ B (Unclosed str) bnds
 352 | 
 353 |   ||| Fails with `unclosed` if this is the end of input, otherwise
 354 |   ||| invokes `unexpected`.
 355 |   export
 356 |   unclosedIfEOIErr : HasBytes s => String -> List String -> F1 q (BBErr e)
 357 |   unclosedIfEOIErr s ss =
 358 |     getBytes >>= \case
 359 |       BS 0 _ => unclosedErr s
 360 |       bs     => bounded (unexpectedErr ss)
 361 | 
 362 |   ||| Fails with `unclosed` if this is the end of input or
 363 |   ||| a linefeed character (`\n`, byte `0x0a`) was encountered,
 364 |   ||| otherwise, invokes `unexpected`.
 365 |   export
 366 |   unclosedIfNLorEOIErr : HasBytes s => String -> List String -> F1 q (BBErr e)
 367 |   unclosedIfNLorEOIErr s ss =
 368 |     getBytes >>= \case
 369 |       BS 0 _ => unclosedErr s
 370 |       bs     =>
 371 |         if elem 0x0a bs then unclosedErr s else bounded (unexpectedErr ss)
 372 | 
 373 |   ||| Writes the given exception to the `error` field of some
 374 |   ||| mutable state and returns the given result.
 375 |   |||
 376 |   ||| If another error occurred already (the content of `error sk` is
 377 |   ||| not `Nothing`), the previous error will take precedence and will
 378 |   ||| not be replaced.
 379 |   export %inline
 380 |   failWith : BBErr e -> v -> F1 q v
 381 |   failWith x v =
 382 |     read1 (error sk) >>= \case
 383 |       Just _  => pure v
 384 |       Nothing => writeAs (error sk) (Just x) v
 385 | 
 386 |   ||| Like `failWith`, but generates the bounds of the error from the
 387 |   ||| current position and the bytes read until the error occurred.
 388 |   export %inline
 389 |   failHere : HasBytes s => InnerError e -> v -> F1 q v
 390 |   failHere x res = T1.do
 391 |     bs <- bounds
 392 |     failWith (B x bs) res
 393 | 
 394 |   export %inline
 395 |   failUnexpected : HasBytes s => List String -> v -> F1 q v
 396 |   failUnexpected vs v = unexpectedErr vs >>= flip failHere v
 397 | 
 398 |   export %inline
 399 |   failUnclosed : HasBytes s => String -> v -> F1 q v
 400 |   failUnclosed s v = unclosedErr s >>= flip failWith v
 401 | 
 402 |   export %inline
 403 |   failUnclosedIfEOI : HasBytes s => String -> List String -> v -> F1 q v
 404 |   failUnclosedIfEOI s ss v = unclosedIfEOIErr s ss >>= flip failWith v
 405 | 
 406 | --------------------------------------------------------------------------------
 407 | -- Terminals
 408 | --------------------------------------------------------------------------------
 409 | 
 410 | parameters {auto hbp : HasBytes s}
 411 |            (x        : a)
 412 | 
 413 |   export %inline
 414 |   ignore : (a,Step q r s)
 415 |   ignore = ign x
 416 | 
 417 |   export %inline
 418 |   step : (s q => F1 q (Index r)) -> (a,Step q r s)
 419 |   step = go x
 420 | 
 421 |   export %inline
 422 |   step' : Cast t (Index r) => t -> (a,Step q r s)
 423 |   step' x = step (pure $ cast x)
 424 | 
 425 |   export %inline
 426 |   bytes : (s q => ByteString -> F1 q (Index r)) -> (a,Step q r s)
 427 |   bytes f = goBS x f
 428 | 
 429 |   export %inline
 430 |   string : (s q => String -> F1 q (Index r)) -> (a,Step q r s)
 431 |   string f = goStr x f
 432 | 
 433 |   ||| Recognizes the given character(s)
 434 |   ||| and uses it to update the parser state
 435 |   ||| as specified by `f`.
 436 |   |||
 437 |   ||| The current column is increased by one, and a new entry is pushed onto
 438 |   ||| the stack of bounds.
 439 |   export %inline
 440 |   opn : (s q => F1 q (Index r)) -> (a, Step q r s)
 441 |   opn f = step $ pushPosition >> f
 442 | 
 443 |   ||| Convenience alias for `copen . pure`.
 444 |   export %inline
 445 |   opn' : Cast t (Index r) => t -> (a, Step q r s)
 446 |   opn' v = opn $ pure (cast v)
 447 | 
 448 |   ||| Recognizes the given character(s) and uses it to update the parser state
 449 |   ||| as specified by `f`.
 450 |   |||
 451 |   ||| The current column is increased by `n`, and one `Position` entry
 452 |   ||| is popped from the stack.
 453 |   export %inline
 454 |   close : (s q => F1 q (Index r)) -> (a, Step q r s)
 455 |   close f = step $ popPosition >> f
 456 | 
 457 |   ||| Recognizes the given character(s) and uses it to
 458 |   ||| finalize and assemble a string literal.
 459 |   |||
 460 |   ||| The current column is increased by `n`, and one `Position` entry
 461 |   ||| is popped from the stack.
 462 |   export %inline
 463 |   closeStr :
 464 |        {auto hap : HasStringLits s}
 465 |     -> (s q => String -> F1 q (Index r))
 466 |     -> (a, Step q r s)
 467 |   closeStr f = close $ getStr >>= f
 468 | 
 469 |   ||| Recognizes the given character(s) and uses it to update the parser state
 470 |   ||| as specified by `f`.
 471 |   |||
 472 |   ||| The current column is increased by one, and on `Bounds` entry
 473 |   ||| is popped from the stack.
 474 |   export %inline
 475 |   closeWithBounds : (s q => ByteBounds -> F1 q (Index r)) -> (a, Step q r s)
 476 |   closeWithBounds f = step $ closeBounds >>= f
 477 | 
 478 |   ||| Recognizes the given character(s) and uses it to
 479 |   ||| finalize and assemble a string literal.
 480 |   |||
 481 |   ||| The current column is increased by `n`, and one `Position` entry
 482 |   ||| is popped from the stack.
 483 |   export %inline
 484 |   closeBoundedStr :
 485 |        {auto hap : HasStringLits s}
 486 |     -> (s q => ByteBounded String -> F1 q (Index r))
 487 |     -> (a, Step q r s)
 488 |   closeBoundedStr f = closeWithBounds $ \bs => getStr >>= \s => f (B s bs)
 489 | 
 490 | parameters {auto hbp : HasBytes s}
 491 | 
 492 |   ||| Lexes a single value based on its printed form. Returns
 493 |   ||| `Nothing` in case `display` returns the empty string.
 494 |   |||
 495 |   ||| For instance, `val show soSomething True` would recognice
 496 |   ||| the token `"True"` and invoke act with `True`.
 497 |   export
 498 |   val :
 499 |        (display : a -> String)
 500 |     -> (act     : a -> Step1 q r s)
 501 |     -> (value   : a)
 502 |     -> Maybe (RExp True, Step q r s)
 503 |   val display act v =
 504 |    let f := act v
 505 |     in case unpack (display v) of
 506 |          cs@(_::_) => Just $ step (chars cs) (f %search)
 507 |          []        => Nothing
 508 | 
 509 |   ||| Like `val` but for a value that can be displayed in
 510 |   ||| different ways.
 511 |   export
 512 |   valN :
 513 |        (displays : a -> List String)
 514 |     -> (act      : a -> Step1 q r s)
 515 |     -> (value    : a)
 516 |     -> List (RExp True, Step q r s)
 517 |   valN displays act v =
 518 |    let f := act v
 519 |     in mapMaybe (exp f . unpack) (displays v)
 520 |   where
 521 |     exp : Step1 q r s -> List Char -> Maybe (RExp True, Step q r s)
 522 |     exp f cs@(_::_)= Just $ step (chars cs) (f %search)
 523 |     exp f [] = Nothing
 524 | 
 525 |   ||| Specialized version of `val` that writes the lexed value
 526 |   ||| to a predefined mutable field of the parser stack.
 527 |   export %inline
 528 |   writeVal :
 529 |        (display : a -> String)
 530 |     -> (field   : s q -> Ref q a)
 531 |     -> Index r
 532 |     -> (value   : a)
 533 |     -> Maybe (RExp True, Step q r s)
 534 |   writeVal display field res =
 535 |     val display (\v,x => writeAs (field x) v res)
 536 | 
 537 |   ||| Specialized version of `valN` that writes the lexed value
 538 |   ||| to a predefined mutable field of the parser stack.
 539 |   export %inline
 540 |   writeValN :
 541 |        (displays : a -> List String)
 542 |     -> (field    : s q -> Ref q a)
 543 |     -> Index r
 544 |     -> (value    : a)
 545 |     -> List (RExp True, Step q r s)
 546 |   writeValN displays field res =
 547 |     valN displays (\v,x => writeAs (field x) v res)
 548 | 
 549 |   ||| Applies `val` to a list of values.
 550 |   |||
 551 |   ||| Highly useful in combination with the `Finite` interface from
 552 |   ||| the idris2-finite library.
 553 |   export %inline
 554 |   vals :
 555 |        (display : a -> String)
 556 |     -> (act     : a -> Step1 q r s)
 557 |     -> List a
 558 |     -> List (RExp True, Step q r s)
 559 |   vals display = mapMaybe . val display
 560 | 
 561 |   ||| Like `vals` but for values that can be displayed in
 562 |   ||| several ways.
 563 |   |||
 564 |   ||| Highly useful in combination with the `Finite` interface from
 565 |   ||| the idris2-finite library.
 566 |   export %inline
 567 |   valsN :
 568 |        (displays : a -> List String)
 569 |     -> (act      : a -> Step1 q r s)
 570 |     -> List a
 571 |     -> List (RExp True, Step q r s)
 572 |   valsN displays act vs = vs >>= valN displays act
 573 | 
 574 |   ||| Specialized version of `vals` that writes the lexed value
 575 |   ||| to a predefined mutable field of the parser stack.
 576 |   export %inline
 577 |   writeVals :
 578 |        (display : a -> String)
 579 |     -> (field   : s q -> Ref q a)
 580 |     -> (res     : Index r)
 581 |     -> List a
 582 |     -> List (RExp True, Step q r s)
 583 |   writeVals display field = mapMaybe . writeVal display field
 584 | 
 585 |   ||| Specialized version of `valsN` that writes the lexed value
 586 |   ||| to a predefined mutable field of the parser stack.
 587 |   export %inline
 588 |   writeValsN :
 589 |        (displays : a -> List String)
 590 |     -> (field    : s q -> Ref q a)
 591 |     -> (res      : Index r)
 592 |     -> List a
 593 |     -> List (RExp True, Step q r s)
 594 |   writeValsN displays field res vs = vs >>= writeValN displays field res
 595 | 
 596 | export
 597 | jsonSpace : RExp True
 598 | jsonSpace = oneof [' ','\t','\n','\r']
 599 | 
 600 | export %inline
 601 | jsonSpaces : RExp True
 602 | jsonSpaces = plus jsonSpace
 603 | 
 604 | export %inline
 605 | jsonSpaced : HasBytes s => Steps q r s -> Steps q r s
 606 | jsonSpaced xs = ignore jsonSpaces :: xs
 607 | 
 608 | --------------------------------------------------------------------------------
 609 | -- Error handling
 610 | --------------------------------------------------------------------------------
 611 | 
 612 | parameters {auto he  : HasBBErr s e}
 613 |            {auto pos : HasBytes s}
 614 | 
 615 |   export
 616 |   raise : InnerError e -> Nat -> s q => v -> F1 q v
 617 |   raise err n res = T1.do
 618 |     ps <- startPos
 619 |     failWith (B err $ BB ps (incLen n ps)) res
 620 | 
 621 |   export %inline
 622 |   unexpected : List String -> s q -> F1 q (BBErr e)
 623 |   unexpected strs sk = ifNoErrorRaised (bounded $ unexpectedErr strs)
 624 | 
 625 |   export %inline
 626 |   unclosed : String -> s q -> F1 q (BBErr e)
 627 |   unclosed str sk = ifNoErrorRaised (unclosedErr str)
 628 | 
 629 |   ||| Fails with `unclosed` if this is the end of input, otherwise
 630 |   ||| invokes `unexpected`.
 631 |   export %inline
 632 |   unclosedIfEOI : String -> List String -> s q -> F1 q (BBErr e)
 633 |   unclosedIfEOI s ss sk = ifNoErrorRaised (unclosedIfEOIErr s ss)
 634 | 
 635 |   ||| Fails with `unclosed` if this is the end of input or
 636 |   ||| a linefeed character (`\n`, byte `0x0a`) was encountered,
 637 |   ||| otherwise, invokes `unexpected`.
 638 |   export %inline
 639 |   unclosedIfNLorEOI : String -> List String -> s q -> F1 q (BBErr e)
 640 |   unclosedIfNLorEOI s ss sk = ifNoErrorRaised (unclosedIfNLorEOIErr s ss)
 641 | 
 642 |   export %inline
 643 |   errs :
 644 |        {n : _}
 645 |     -> List (Entry n $ s q -> F1 q (BBErr e))
 646 |     -> Arr32 n (s q -> F1 q (BBErr e))
 647 |   errs = arr32 n (unexpected [])
 648 | 
 649 | --------------------------------------------------------------------------------
 650 | -- Streaming
 651 | --------------------------------------------------------------------------------
 652 | 
 653 | ||| Never emits a chunk of values during streaming.
 654 | |||
 655 | ||| This is for parsers that produce a single value after consuming the
 656 | ||| whole input. Such a parser can still be used with the facilities
 657 | ||| from ilex-streams but will only emit a single value at the end of input.
 658 | ||| In general, such a parser consumes a linear amount of memory and can
 659 | ||| typically not be used to process very large amounts of data.
 660 | export
 661 | noChunk : s -> F1 q (Maybe a)
 662 | noChunk _ t = (Nothing # t)
 663 | 
 664 | ||| Extracts the values parsed so far from the parser stack
 665 | ||| and emits them during streaming.
 666 | export
 667 | snocChunk : HasStack s (SnocList a) => s q -> F1 q (Maybe $ List a)
 668 | snocChunk sk = T1.do
 669 |   ss <- replace1 (stack sk) [<]
 670 |   pure (maybeList ss)
 671 |