
   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.Bounds
   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 allows us to keep
  23 | ||| track of the current position (line and column) in the currently
  24 | ||| parsed string.
  25 | public export
  26 | interface HasPosition (0 s : Type -> Type) where
  27 |   constructor MkHP
  28 |   line      : s q -> Ref q Nat
  29 |   col       : s q -> Ref q Nat
  30 |   positions : s q -> Ref q (SnocList Position)
  31 | 
  32 | ||| An interface for mutable parser stacks `s` that allow us to
  33 | ||| register custom errors, which will then be raised during parsing.
  34 | public export
  35 | interface HasError (0 s : Type -> Type) (0 e : Type) | s where
  36 |   constructor MkHE
  37 |   error     : s q -> Ref q (Maybe $ BoundedErr e)
  38 | 
  39 | ||| An interface for mutable parser stacks `s` that facilitates
  40 | ||| parsing string tokens containing escape sequences.
  41 | public export
  42 | interface HasStringLits (0 s : Type -> Type) where
  43 |   constructor MkHSL
  44 |   strings   : s q -> Ref q (SnocList String)
  45 | 
  46 | ||| An interface for mutable parser stacks `s` that facilitates
  47 | ||| parsing string tokens containing escape sequences.
  48 | public export
  49 | interface HasStack (0 s : Type -> Type) (0 a : Type) | s where
  50 |   constructor MkHS
  51 |   stack     : s q -> Ref q a
  52 | 
  53 | --------------------------------------------------------------------------------
  54 | -- General Utilities
  55 | --------------------------------------------------------------------------------
  56 | 
  57 | export %inline
  58 | go : a -> (s q => F1 q (Index r)) -> (a,Step q r s)
  59 | go x f = (x,Go $ \(x # t) => f t)
  60 | 
  61 | export %inline
  62 | goBS : HasBytes s => a -> (s q => ByteString -> F1 q (Index r)) -> (a,Step q r s)
  63 | goBS x f = (x, Rd $ \(x # t) => let bs # t := read1 (bytes x) t in f bs t)
  64 | 
  65 | export %inline
  66 | goStr : HasBytes s => a -> (s q => String -> F1 q (Index r)) -> (a,Step q r s)
  67 | goStr x f =
  68 |   ( x
  69 |   , Rd $ \(x # t) =>
  70 |      let bs # t := read1 (bytes x) t
  71 |          s      := toString bs
  72 |       in f s t
  73 |   )
  74 | 
  75 | ||| Writes a mutable reference and returns the given result.
  76 | export %inline
  77 | writeAs : Ref q a -> a -> r -> F1 q r
  78 | writeAs ref v res = write1 ref v >> pure res
  79 | 
  80 | ||| Appends a value to mutable reference of a snoclist.
  81 | export %inline
  82 | push1 : Ref q (SnocList a) -> a -> F1' q
  83 | push1 ref v = T1.do
  84 |  ss <- read1 ref
  85 |  write1 ref (ss:<v)
  86 | 
  87 | ||| Drops and discards a the last entry from a snoclist
  88 | ||| stored in a mutable reference.
  89 | export %inline
  90 | pop1 : Ref q (SnocList a) -> F1' q
  91 | pop1 ref =
  92 |   read1 ref >>= \case
  93 |     sv:<_ => write1 ref sv
  94 |     _     => pure ()
  95 | 
  96 | ||| Returns the value stored in a mutable reference and
  97 | ||| overwrites it with the given replacement.
  98 | export %inline
  99 | replace1 : Ref q a -> a -> F1 q a
 100 | replace1 ref v = T1.do
 101 |   s <- read1 ref
 102 |   write1 ref v
 103 |   pure s
 104 | 
 105 | ||| Empties a mutable reference holding a snoclist and returns
 106 | ||| the corresponding list.
 107 | export %inline
 108 | getList : Ref q (SnocList a) -> F1 q (List a)
 109 | getList ref = T1.do
 110 |   sv <- replace1 ref [<]
 111 |   pure (sv <>> [])
 112 | 
 113 | ||| Returns the content of some mutable state implementing
 114 | ||| `HasStack`.
 115 | export %inline
 116 | getStack : HasStack s a => (sk : s q) => F1 q a
 117 | getStack = read1 (stack sk)
 118 | 
 119 | ||| Overwrites the content of some mutable state implementing
 120 | ||| `HasStack`.
 121 | export %inline
 122 | putStack : HasStack s a => (sk : s q) => a -> F1' q
 123 | putStack = write1 (stack sk)
 124 | 
 125 | ||| Like `putStack` but returns the given result.
 126 | export %inline
 127 | putStackAs : HasStack s a => (sk : s q) => a -> v -> F1 q v
 128 | putStackAs = writeAs (stack sk)
 129 | 
 130 | ||| Like `putStack` but returns the given result.
 131 | export %inline
 132 | putStackAsC : Cast b v => HasStack s a => (sk : s q) => a -> b -> F1 q v
 133 | putStackAsC res = putStackAs res . cast
 134 | 
 135 | ||| Reads and updates the stack.
 136 | export %inline
 137 | modStackAs : (0 s : _) -> HasStack s a => (sk : s q) => (a -> a) -> v -> F1 q v
 138 | modStackAs _ f v = getStack >>= \x => putStackAs (f x) v
 139 | 
 140 | ||| Appends a value to some mutable state implementing `HasStack`.
 141 | export %inline
 142 | pushStack : HasStack s (SnocList a) => (sk : s q) => a -> F1' q
 143 | pushStack = push1 (stack sk)
 144 | 
 145 | ||| Like `pushStack` but returns the given result.
 146 | export %inline
 147 | pushStackAs : HasStack s (SnocList a) => (sk : s q) => a -> v -> F1 q v
 148 | pushStackAs v res = pushStack v >> pure res
 149 | 
 150 | ||| A small utility for counting down a parser and returning one
 151 | ||| of two possible outcomes.
 152 | export %inline
 153 | countdown : Ref q Nat -> (ifSucc, ifZero : a) -> F1 q a
 154 | countdown ref s z t =
 155 |  let S k # t := read1 ref t | Z # t => z # t
 156 |   in writeAs ref k s t
 157 | 
 158 | ||| A small utility for counting down a parser and returning one
 159 | ||| of two possible actions.
 160 | export %inline
 161 | countdownAct : Ref q Nat -> (ifSucc, ifZero : F1 q a) -> F1 q a
 162 | countdownAct ref s z t =
 163 |  let S k # t := read1 ref t | Z # t => z t
 164 |      _   # t := write1 ref k t
 165 |   in s t
 166 | 
 167 | --------------------------------------------------------------------------------
 168 | -- String Literals
 169 | --------------------------------------------------------------------------------
 170 | 
 171 | parameters {auto sk  : s q}
 172 |            {auto pos : HasStringLits s}
 173 | 
 174 |   ||| Empties the `strings` field of some mutable state implementing
 175 |   ||| `HasStringLits` and returns the concatenated string literal.
 176 |   export %inline
 177 |   getStr : F1 q String
 178 |   getStr = T1.do
 179 |     sv <- replace1 (strings sk) [<]
 180 |     pure $ snocPack sv
 181 | 
 182 |   ||| Appends the given string to the `strings` field of some mutable
 183 |   ||| state implementing `HasStringLits`.
 184 |   export %inline
 185 |   pushStr' : String -> F1' q
 186 |   pushStr' str = push1 (strings sk) str
 187 | 
 188 |   ||| Appends the given string to the `strings` field of some mutable
 189 |   ||| state implementing `HasStringLits` and returns the given result.
 190 |   export %inline
 191 |   pushStr : Cast t (Index r) => t -> String -> F1 q (Index r)
 192 |   pushStr res str = T1.do
 193 |     push1 (strings sk) str
 194 |     pure (cast res)
 195 | 
 196 |   ||| Appends the given character to the `strings` field of some mutable
 197 |   ||| state implementing `HasStringLits` and returns the given result.
 198 |   export %inline
 199 |   pushChar : Cast t (Index r) => t -> Char -> F1 q (Index r)
 200 |   pushChar res = pushStr res . singleton
 201 | 
 202 |   ||| Appends the given unicode code point to the `strings` field of some mutable
 203 |   ||| state implementing `HasStringLits` and returns the given result.
 204 |   export %inline
 205 |   pushBits32 : Cast t (Index r) => t -> Bits32 -> F1 q (Index r)
 206 |   pushBits32 res = pushChar res . cast
 207 | 
 208 | --------------------------------------------------------------------------------
 209 | -- Bounds and Position
 210 | --------------------------------------------------------------------------------
 211 | 
 212 | parameters {auto sk  : s q}
 213 |            {auto pos : HasPosition s}
 214 | 
 215 |   ||| Gets the current text position (line and column) from some
 216 |   ||| mutable state implementing `HasPosition`.
 217 |   export %inline
 218 |   getPosition : F1 q Position
 219 |   getPosition = T1.do
 220 |     l <- read1 (line sk)
 221 |     c <- read1 (col sk)
 222 |     pure $ P l c
 223 | 
 224 |   ||| Increases the text column of some mutable state implementing
 225 |   ||| `HasPosition` by the given amount.
 226 |   export %inline
 227 |   inccol : Nat -> F1 q ()
 228 |   inccol n = let c := col sk in read1 c >>= write1 c . (n+)
 229 | 
 230 |   ||| Increases the text column of some mutable state implementing
 231 |   ||| `HasPosition` by the given amount.
 232 |   export %inline
 233 |   setcol : Nat -> F1 q ()
 234 |   setcol n = write1 (col sk) n
 235 | 
 236 |   ||| Increases the line of some mutable state implementing
 237 |   ||| `HasPosition` by the given amount. The column field is
 238 |   ||| reset to zero.
 239 |   export %inline
 240 |   incline : Nat -> F1 q ()
 241 |   incline n = T1.do
 242 |     l <- read1 (line sk)
 243 |     write1 (line sk) (n + l)
 244 |     write1 (col sk) 0
 245 | 
 246 |   ||| Increases the current text position according to the characters
 247 |   ||| encountered in the given byte string.
 248 |   |||
 249 |   ||| See also `Text.ILex.Bounds.inBytes`.
 250 |   export %inline
 251 |   incML : ByteString -> F1 q ()
 252 |   incML bs = T1.do
 253 |     p <- getPosition
 254 |     let P l c := incBytes bs p
 255 |     write1 (line sk) l
 256 |     write1 (col sk) c
 257 | 
 258 |   ||| Gets the current token bounds from some
 259 |   ||| mutable state implementing `HasPosition` after
 260 |   ||| increasing the column by `n` characters.
 261 |   export %inline
 262 |   tokenBounds : Nat -> F1 q Bounds
 263 |   tokenBounds n = T1.do
 264 |     sp <- getPosition
 265 |     inccol n
 266 |     ep <- getPosition
 267 |     pure (BS sp ep)
 268 | 
 269 |   ||| Pushes the current text position onto the position stack.
 270 |   |||
 271 |   ||| This is often used when ecountering some "opening token"
 272 |   ||| (such as an opening quote or parenthesis) for which we later
 273 |   ||| expect a suitable closing token. If no closing token is encountered,
 274 |   ||| we typically want to fail with an error that lists the position
 275 |   ||| of the unclosed token.
 276 |   export %inline
 277 |   pushPosition : F1' q
 278 |   pushPosition = getPosition >>= push1 (positions sk)
 279 | 
 280 |   ||| Discards the latest entry from the positions stack.
 281 |   export %inline
 282 |   popPosition : F1' q
 283 |   popPosition = pop1 (positions sk)
 284 | 
 285 |   popAndGetBounds : Nat -> F1 q Bounds
 286 |   popAndGetBounds n =
 287 |     read1 (positions sk) >>= \case
 288 |       sb:<b => writeAs (positions sk) sb (BS b $ addCol n b)
 289 |       [<]   => pure NoBounds
 290 | 
 291 |   ||| Returns the bounds from start to end of some "enclosed" or
 292 |   ||| quoted region of text such as an expression in parantheses
 293 |   ||| or some text in quotes.
 294 |   export %inline
 295 |   closeBounds : F1 q Bounds
 296 |   closeBounds = T1.do
 297 |     pe <- getPosition
 298 |     read1 (positions sk) >>= \case
 299 |       sb:<b => writeAs (positions sk) sb (BS b pe)
 300 |       [<]   => pure NoBounds
 301 | 
 302 | parameters {auto pos : HasPosition s}
 303 | 
 304 |   ||| Recognizes the given expression and invokes `incline` before
 305 |   ||| returning the given result.
 306 |   export %inline
 307 |   newline : RExpOf True b -> (v : s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)
 308 |   newline x f = go x $ f <* incline 1
 309 | 
 310 |   ||| Convenience alias for `newline x (pure v)`.
 311 |   export %inline
 312 |   newline' : Cast t (Index r) => RExpOf True b -> t -> (RExpOf True b, Step q r s)
 313 |   newline' x v = go x $ incline 1 >> pure (cast v)
 314 | 
 315 |   ||| Recognizes the given expression and invokes `incline n` before
 316 |   ||| returning the given result.
 317 |   export %inline
 318 |   newlines :
 319 |        Nat
 320 |     -> RExpOf True b
 321 |     -> (v : s q => F1 q (Index r))
 322 |     -> (RExpOf True b, Step q r s)
 323 |   newlines n x f = go x $ f <* incline n
 324 | 
 325 |   ||| Convenience alias for `newlines n x (pure v)`.
 326 |   export %inline
 327 |   newlines' : Nat -> RExpOf True b -> (v : Index r) -> (RExpOf True b, Step q r s)
 328 |   newlines' n x v = go x $ incline n >> pure v
 329 | 
 330 |   ||| Recognizes the given expression, increasing the line count by the given
 331 |   ||| number and setting the current column to the given value *after* invoming
 332 |   ||| the given action.
 333 |   export
 334 |   linecol :
 335 |        (line,col : Nat)
 336 |     -> RExpOf True b
 337 |     -> (v : s q => F1 q (Index r))
 338 |     -> (RExpOf True b, Step q r s)
 339 |   linecol l c x f = go x $ f <* incline l <* setcol c
 340 | 
 341 |   ||| Convenience alias for `linecol line col x (pure v)`.
 342 |   export
 343 |   linecol' : (line,col : Nat) -> RExpOf True b -> Index r -> (RExpOf True b, Step q r s)
 344 |   linecol' l c x v = go x $ incline l >> setcol c >> pure v
 345 | 
 346 | parameters {auto hae : HasError s e}
 347 | 
 348 |   ||| Writes the given exception to the `error` field of some
 349 |   ||| mutable state and returns the given result.
 350 |   export %inline
 351 |   failWith : (sk : s q) => BoundedErr e -> v -> F1 q v
 352 |   failWith = writeAs (error sk) . Just
 353 | 
 354 |   ||| Like `failWith`, but generates the bounds of the error from the
 355 |   ||| current position and the bytes read until the error occurred.
 356 |   export %inline
 357 |   failHere : HasBytes s => HasPosition s => (sk : s q) => InnerError e -> v -> F1 q v
 358 |   failHere x res = T1.do
 359 |     p  <- getPosition
 360 |     bs <- read1 (bytes sk)
 361 |     failWith (B x $ BS p (incBytes bs p)) res
 362 | 
 363 | --------------------------------------------------------------------------------
 364 | -- Constant-Size Terminals
 365 | --------------------------------------------------------------------------------
 366 | 
 367 | parameters (x          : RExpOf True b)
 368 |            {n          : Nat}
 369 |            {auto 0 prf : ConstSize n x}
 370 |            {auto   pos : HasPosition s}
 371 | 
 372 |   ||| Recognizes the given character and uses it to update the parser state
 373 |   ||| as specified by `f`.
 374 |   |||
 375 |   ||| The current column is increased by `n` *before* invoking `f`.
 376 |   export %inline
 377 |   cexpr : (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)
 378 |   cexpr f = go x $ inccol n >> f
 379 | 
 380 |   ||| Convenience alias for `cexpr . pure`.
 381 |   export %inline
 382 |   cexpr' : Cast t (Index r) => t -> (RExpOf True b, Step q r s)
 383 |   cexpr' v = cexpr $ pure (cast v)
 384 | 
 385 |   ||| Recognizes the given character(s)
 386 |   ||| and uses it to update the parser state
 387 |   ||| as specified by `f`.
 388 |   |||
 389 |   ||| The current column is increased by one, and a new entry is pushed onto
 390 |   ||| the stack of bounds.
 391 |   export %inline
 392 |   copen : (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)
 393 |   copen f = go x $ pushPosition >> inccol n >> f
 394 | 
 395 |   ||| Convenience alias for `copen . pure`.
 396 |   export %inline
 397 |   copen' : Cast t (Index r) => t -> (RExpOf True b, Step q r s)
 398 |   copen' v = copen $ pure (cast v)
 399 | 
 400 |   ||| Recognizes the given character(s) and uses it to update the parser state
 401 |   ||| as specified by `f`.
 402 |   |||
 403 |   ||| The current column is increased by `n`, and one `Position` entry
 404 |   ||| is popped from the stack.
 405 |   export %inline
 406 |   cclose : (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)
 407 |   cclose f = go x $ inccol n >> popPosition >> f
 408 | 
 409 |   ||| Recognizes the given character(s) and uses it to
 410 |   ||| finalize and assemble a string literal.
 411 |   |||
 412 |   ||| The current column is increased by `n`, and one `Position` entry
 413 |   ||| is popped from the stack.
 414 |   export %inline
 415 |   ccloseStr :
 416 |        {auto hap : HasStringLits s}
 417 |     -> (s q => String -> F1 q (Index r))
 418 |     -> (RExpOf True b, Step q r s)
 419 |   ccloseStr f = cclose $ getStr >>= f
 420 | 
 421 |   ||| Recognizes the given character(s) and uses it to update the parser state
 422 |   ||| as specified by `f`.
 423 |   |||
 424 |   ||| The current column is increased by one, and on `Bounds` entry
 425 |   ||| is popped from the stack.
 426 |   export %inline
 427 |   ccloseWithBounds : (s q => Bounds -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 428 |   ccloseWithBounds f = go x $ inccol {q} n >> closeBounds >>= f
 429 | 
 430 |   ||| Recognizes the given character(s) and uses it to
 431 |   ||| finalize and assemble a string literal.
 432 |   |||
 433 |   ||| The current column is increased by `n`, and one `Position` entry
 434 |   ||| is popped from the stack.
 435 |   export %inline
 436 |   ccloseBoundedStr :
 437 |        {auto hap : HasStringLits s}
 438 |     -> (s q => Bounded String -> F1 q (Index r))
 439 |     -> (RExpOf True b, Step q r s)
 440 |   ccloseBoundedStr f = ccloseWithBounds $ \bs => getStr >>= \s => f (B s bs)
 441 | 
 442 | parameters {auto pos : HasPosition s}
 443 | 
 444 |   ||| Lexes a single value based on its printed form. Returns
 445 |   ||| `Nothing` in case `display` returns the empty string.
 446 |   |||
 447 |   ||| For instance, `val show soSomething True` would recognice
 448 |   ||| the token `"True"` and invoke act with `True`.
 449 |   export
 450 |   val :
 451 |        (display : a -> String)
 452 |     -> (act     : a -> Step1 q r s)
 453 |     -> (value   : a)
 454 |     -> Maybe (RExp True, Step q r s)
 455 |   val display act v =
 456 |    let f := act v
 457 |     in case unpack (display v) of
 458 |          cs@(_::_) =>
 459 |           let 0 prf := charsConstSize cs
 460 |            in Just $ cexpr (chars cs) (\t => f (%search # t))
 461 |          []        => Nothing
 462 | 
 463 |   ||| Like `val` but for a value that can be displayed in
 464 |   ||| different ways.
 465 |   export
 466 |   valN :
 467 |        (displays : a -> List String)
 468 |     -> (act      : a -> Step1 q r s)
 469 |     -> (value    : a)
 470 |     -> List (RExp True, Step q r s)
 471 |   valN displays act v =
 472 |    let f := act v
 473 |     in mapMaybe (exp f . unpack) (displays v)
 474 |   where
 475 |     exp : Step1 q r s -> List Char -> Maybe (RExp True, Step q r s)
 476 |     exp f cs@(_::_)=
 477 |      let 0 prf := charsConstSize cs
 478 |       in Just $ cexpr (chars cs) (\t => f (%search # t))
 479 |     exp f [] = Nothing
 480 | 
 481 |   ||| Specialized version of `val` that writes the lexed value
 482 |   ||| to a predefined mutable field of the parser stack.
 483 |   export %inline
 484 |   writeVal :
 485 |        (display : a -> String)
 486 |     -> (field   : s q -> Ref q a)
 487 |     -> Index r
 488 |     -> (value   : a)
 489 |     -> Maybe (RExp True, Step q r s)
 490 |   writeVal display field res =
 491 |     val display (\v => \(x # t) => writeAs (field x) v res t)
 492 | 
 493 |   ||| Specialized version of `valN` that writes the lexed value
 494 |   ||| to a predefined mutable field of the parser stack.
 495 |   export %inline
 496 |   writeValN :
 497 |        (displays : a -> List String)
 498 |     -> (field    : s q -> Ref q a)
 499 |     -> Index r
 500 |     -> (value    : a)
 501 |     -> List (RExp True, Step q r s)
 502 |   writeValN displays field res =
 503 |     valN displays (\v => \(x # t) => writeAs (field x) v res t)
 504 | 
 505 |   ||| Applies `val` to a list of values.
 506 |   |||
 507 |   ||| Highly useful in combination with the `Finite` interface from
 508 |   ||| the idris2-finite library.
 509 |   export %inline
 510 |   vals :
 511 |        (display : a -> String)
 512 |     -> (act     : a -> Step1 q r s)
 513 |     -> List a
 514 |     -> List (RExp True, Step q r s)
 515 |   vals display = mapMaybe . val display
 516 | 
 517 |   ||| Like `vals` but for values that can be displayed in
 518 |   ||| several ways.
 519 |   |||
 520 |   ||| Highly useful in combination with the `Finite` interface from
 521 |   ||| the idris2-finite library.
 522 |   export %inline
 523 |   valsN :
 524 |        (displays : a -> List String)
 525 |     -> (act      : a -> Step1 q r s)
 526 |     -> List a
 527 |     -> List (RExp True, Step q r s)
 528 |   valsN displays act vs = vs >>= valN displays act
 529 | 
 530 |   ||| Specialized version of `vals` that writes the lexed value
 531 |   ||| to a predefined mutable field of the parser stack.
 532 |   export %inline
 533 |   writeVals :
 534 |        (display : a -> String)
 535 |     -> (field   : s q -> Ref q a)
 536 |     -> (res     : Index r)
 537 |     -> List a
 538 |     -> List (RExp True, Step q r s)
 539 |   writeVals display field = mapMaybe . writeVal display field
 540 | 
 541 |   ||| Specialized version of `valsN` that writes the lexed value
 542 |   ||| to a predefined mutable field of the parser stack.
 543 |   export %inline
 544 |   writeValsN :
 545 |        (displays : a -> List String)
 546 |     -> (field    : s q -> Ref q a)
 547 |     -> (res      : Index r)
 548 |     -> List a
 549 |     -> List (RExp True, Step q r s)
 550 |   writeValsN displays field res vs = vs >>= writeValN displays field res
 551 | 
 552 | --------------------------------------------------------------------------------
 553 | -- String Terminals
 554 | --------------------------------------------------------------------------------
 555 | 
 556 | parameters (x        : RExpOf True b)
 557 |            {auto pos : HasPosition s}
 558 |            {auto pos : HasBytes s}
 559 | 
 560 |   ||| Converts the recognized token to a `String`, increases the
 561 |   ||| current column by its length and invokes the given state transformer.
 562 |   export %inline
 563 |   read : (s q => String -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 564 |   read f = goStr x $ \s => f s <* inccol (length s)
 565 | 
 566 |   ||| Increases the current line by one after invoking the given
 567 |   ||| state transformer.
 568 |   export %inline
 569 |   readline : (s q => String -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 570 |   readline f = goStr x $ \s => f s <* incline 1
 571 | 
 572 |   ||| Convenience alias for `read . pure`
 573 |   ||| current column by its length after invoking the given state transformer.
 574 |   export %inline
 575 |   read' : Cast t (Index r) => t -> (RExpOf True b, Step q r s)
 576 |   read' v =
 577 |     ( x
 578 |     , Rd $ \(sk # t) =>
 579 |       let bs # t := read1 (bytes sk) t
 580 |           _  # t := inccol (length $ toString bs) t
 581 |        in cast v # t
 582 |     )
 583 | 
 584 |   ||| Increases the current column by the length of the byte string
 585 |   ||| and invokes the given state transformer.
 586 |   export %inline
 587 |   conv : (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 588 |   conv f = goBS x $ \bs => f bs <* inccol (size bs)
 589 | 
 590 |   ||| Increases the current line by one after invoking the given
 591 |   ||| state transformer.
 592 |   export %inline
 593 |   convline : (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 594 |   convline f = goBS x $ \bs => f bs <* incline 1
 595 | 
 596 |   ||| Like `conv` but can handle byte sequence with an unknown number
 597 |   ||| of line feed characters.
 598 |   |||
 599 |   ||| Note: In performance critical parsers, this should be avoided whenever
 600 |   |||       possible. Advancing token bounds by inspecting every byte a second
 601 |   |||       time *can* have an impact. Whenever possible, try to separate your
 602 |   |||       lexems into those which consist of no line breaks and those which
 603 |   |||       consist of a predefine (typically only one) number of line breaks.
 604 |   export %inline
 605 |   multiline : (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)
 606 |   multiline f = goBS x $ \bs => f bs <* incML bs
 607 | 
 608 |   ||| Convenience alias for `conv . pure`.
 609 |   export %inline
 610 |   conv' : Cast t (Index r) => t -> (RExpOf True b, Step q r s)
 611 |   conv' v =
 612 |     ( x
 613 |     , Rd $ \(sk # t) =>
 614 |        let bs # t := read1 (bytes sk) t
 615 |            _  # t := inccol (size bs) t
 616 |         in cast v # t
 617 |     )
 618 | 
 619 |   ||| Convenience alias for `convML . pure`.
 620 |   |||
 621 |   ||| Please not, that the same performance considerations as for `convML`
 622 |   ||| apply.
 623 |   export %inline
 624 |   multiline' : Index r -> (RExpOf True b, Step q r s)
 625 |   multiline' v =
 626 |     ( x
 627 |     , Rd $ \(sk # t) =>
 628 |        let bs # t := read1 (bytes sk) t
 629 |            _  # t := incML bs t
 630 |         in v # t
 631 |     )
 632 | 
 633 | export %inline
 634 | jsonSpaced :
 635 |      {auto hp : HasPosition s}
 636 |   -> {auto hb : HasBytes s}
 637 |   -> {auto cs : Cast b (Index r)}
 638 |   -> b
 639 |   -> Steps q r s
 640 |   -> Steps q r s
 641 | jsonSpaced v xs =
 642 |   [ conv' (plus $ oneof [' ','\t']) v
 643 |   , newline' ('\n' <|> '\r' <|> "\r\n") v
 644 |   ] ++ xs
 645 | 
 646 | --------------------------------------------------------------------------------
 647 | -- Error handling
 648 | --------------------------------------------------------------------------------
 649 | 
 650 | parameters {auto he  : HasError s e}
 651 |            {auto pos : HasPosition s}
 652 |            {auto pos : HasBytes s}
 653 | 
 654 |   export
 655 |   raise : InnerError e -> Nat -> s q => v -> F1 q v
 656 |   raise err n res = T1.do
 657 |     ps <- getPosition
 658 |     let bs := BS ps (addCol n ps)
 659 |     failWith (B err bs) res
 660 | 
 661 |   export
 662 |   unexpected : List String -> s q -> F1 q (BoundedErr e)
 663 |   unexpected strs sk =
 664 |     read1 (error sk) >>= \case
 665 |       Just x  => pure x
 666 |       Nothing => T1.do
 667 |        bs <- read1 (bytes sk)
 668 |        ps <- getPosition
 669 |        let bnds1 := BS ps $ incCol ps
 670 |        case bs of
 671 |          BS 0 _  => pure (B EOI bnds1)
 672 |          BS 1 bv =>
 673 |           let b := bv `at` 0
 674 |               s := String.singleton (cast b)
 675 |            in case isAscii b of
 676 |                 True  => pure (B (Expected strs s) bnds1)
 677 |                 False => pure (B (InvalidByte b) bnds1)
 678 |          bs =>
 679 |           let str  := toString bs
 680 |               bnds := BS ps (incBytes bs ps)
 681 |            in pure (B (Expected strs str) bnds)
 682 | 
 683 |   export
 684 |   unclosed : String -> s q -> F1 q (BoundedErr e)
 685 |   unclosed str sk = T1.do
 686 |     bnds <- popAndGetBounds (length str)
 687 |     pure $ B (Unclosed str) bnds
 688 | 
 689 |   ||| Fails with `unclosed` if this is the end of input, otherwise
 690 |   ||| invokes `unexpected`.
 691 |   export
 692 |   unclosedIfEOI : String -> List String -> s q -> F1 q (BoundedErr e)
 693 |   unclosedIfEOI s ss sk =
 694 |     read1 (bytes sk) >>= \case
 695 |       BS 0 _ => unclosed s sk
 696 |       _      => unexpected ss sk
 697 | 
 698 |   ||| Fails with `unclosed` if this is the end of input or
 699 |   ||| a linefeed character (`\n`, byte `0x0a`) was encountered,
 700 |   ||| otherwise, invokes `unexpected`.
 701 |   export
 702 |   unclosedIfNLorEOI : String -> List String -> s q -> F1 q (BoundedErr e)
 703 |   unclosedIfNLorEOI s ss sk =
 704 |     read1 (bytes sk) >>= \case
 705 |       BS 0 _ => unclosed s sk
 706 |       bs     => if elem 0x0a bs then unclosed s sk else unexpected ss sk
 707 | 
 708 |   export %inline
 709 |   errs :
 710 |        {n : _}
 711 |     -> List (Entry n $ s q -> F1 q (BoundedErr e))
 712 |     -> Arr32 n (s q -> F1 q (BoundedErr e))
 713 |   errs = arr32 n (unexpected [])
 714 | 
 715 | --------------------------------------------------------------------------------
 716 | -- Streaming
 717 | --------------------------------------------------------------------------------
 718 | 
 719 | ||| Never emits a chunk of values during streaming.
 720 | |||
 721 | ||| This is for parsers that produce a single value after consuming the
 722 | ||| whole input. Such a parser can still be used with the facilities
 723 | ||| from ilex-streams but will only emit a single value at the end of input.
 724 | ||| In general, such a parser consumes a linear amount of memory and can
 725 | ||| typically not be used to process very large amounts of data.
 726 | export
 727 | noChunk : s -> F1 q (Maybe a)
 728 | noChunk _ t = (Nothing # t)
 729 | 
 730 | ||| Extracts the values parsed so far from the parser stack
 731 | ||| and emits them during streaming.
 732 | export
 733 | snocChunk : HasStack s (SnocList a) => s q -> F1 q (Maybe $ List a)
 734 | snocChunk sk = T1.do
 735 |   ss <- replace1 (stack sk) [<]
 736 |   pure (maybeList ss)
 737 |