
   0 | module Text.Lex.Manual
   1 | 
   2 | import Data.List.Quantifiers
   3 | import public Text.Bounds
   4 | import public Text.ParseError
   5 | import public Data.List.Suffix
   6 | import public Data.List.Suffix.Result
   7 | 
   8 | %default total
   9 | 
  10 | ||| Result of running a (strict) tokenizer.
  11 | public export
  12 | 0 LexRes : (b : Bool) -> List Char -> (e,a : Type) -> Type
  13 | LexRes b ts e a = Result b Char ts (InnerError e) a
  14 | 
  15 | --------------------------------------------------------------------------------
  16 | --          Bounds
  17 | --------------------------------------------------------------------------------
  18 | 
  19 | ||| Shift the position by a number of columns represented by
  20 | ||| a `Suffix` value. This assumes, that no line break was "shifted".
  21 | public export %inline
  22 | move : Position -> Suffix b xs ys -> Position
  23 | move p s = addCol (toNat s) p
  24 | 
  25 | calcEnd : (line,col : Nat) -> (cs : List Char) -> Suffix b ys cs -> Position
  26 | calcEnd l c ys          Same       = P l c
  27 | calcEnd l c ('\n' :: t) (Uncons x) = calcEnd (S l) 0 t (unconsBoth x)
  28 | calcEnd l c (_    :: t) (Uncons x) = calcEnd l (S c) t (unconsBoth x)
  29 | calcEnd l c []          (Uncons x) = absurd x
  30 | 
  31 | ||| Calculates the new position from a `Suffix` by reinspecting
  32 | ||| the original list of characters.
  33 | ||| 
  34 | ||| Use this, if the consumed prefix might have contained line breaks.
  35 | ||| Otherwise, consider using `move`, which runs in O(1) instead of O(n).
  36 | export %inline
  37 | endPos :
  38 |      {cs : List Char}
  39 |   -> (pos : Position)
  40 |   -> Suffix b ys cs
  41 |   -> Position
  42 | endPos pos = calcEnd pos.line pos.col cs
  43 | 
  44 | export
  45 | boundedErr :
  46 |      {0 e : Type}
  47 |   -> {ts,errStart : List Char}
  48 |   -> Position
  49 |   -> (start : Suffix False errStart ts)
  50 |   -> (0 errEnd : List Char)
  51 |   -> {auto end : Suffix False errEnd errStart}
  52 |   -> (err : e)
  53 |   -> Bounded e
  54 | boundedErr pos start errEnd err =
  55 |   let ps := endPos pos start
  56 |       pe := endPos ps end
  57 |    in bounded err ps pe
  58 | 
  59 | --------------------------------------------------------------------------------
  60 | --          Combinators
  61 | --------------------------------------------------------------------------------
  62 | 
  63 | public export
  64 | (<|>) :
  65 |      Result b t ts r a
  66 |   -> Lazy (Result b t ts r a)
  67 |   -> Result b t ts r a
  68 | s@(Succ {}) <|> _ = s
  69 | _           <|> r = r
  70 | 
  71 | --------------------------------------------------------------------------------
  72 | --         Character Utilities
  73 | --------------------------------------------------------------------------------
  74 | 
  75 | ||| Returns true if the character is a space (`' '`) character.
  76 | public export %inline
  77 | isSpaceChar : Char -> Bool
  78 | isSpaceChar ' ' = True
  79 | isSpaceChar _   = False
  80 | 
  81 | ||| Returns true if the character is a line feed (`'\n'`) character.
  82 | public export %inline
  83 | isLineFeed : Char -> Bool
  84 | isLineFeed '\n' = True
  85 | isLineFeed _    = False
  86 | 
  87 | public export %inline
  88 | Cast (SnocList Char) String where
  89 |   cast = pack . (<>> [])
  90 | 
  91 | ||| Converts a character to an octal digit. This works under the
  92 | ||| assumption that the character has already been verified to be
  93 | ||| an octal digit.
  94 | public export
  95 | octDigit : Char -> Nat
  96 | octDigit '0' = 0
  97 | octDigit '1' = 1
  98 | octDigit '2' = 2
  99 | octDigit '3' = 3
 100 | octDigit '4' = 4
 101 | octDigit '5' = 5
 102 | octDigit '6' = 6
 103 | octDigit _   = 7
 104 | 
 105 | ||| Converts a character to a decimal digit. This works under the
 106 | ||| assumption that the character has already been verified to be
 107 | ||| a decimal digit.
 108 | public export
 109 | digit : Char -> Nat
 110 | digit '8' = 8
 111 | digit '9' = 9
 112 | digit c   = octDigit c
 113 | 
 114 | ||| Converts a character to a hexadecimal digit. This works under the
 115 | ||| assumption that the character has already been verified to be
 116 | ||| a hexadecimal digit.
 117 | public export
 118 | hexDigit : Char -> Nat
 119 | hexDigit c = case toLower c of
 120 |   'a' => 10
 121 |   'b' => 11
 122 |   'c' => 12
 123 |   'd' => 13
 124 |   'e' => 14
 125 |   'f' => 15
 126 |   c   => digit c
 127 | 
 128 | ||| True if the given character is a binary digit.
 129 | public export
 130 | isBinDigit : Char -> Bool
 131 | isBinDigit '0' = True
 132 | isBinDigit '1' = True
 133 | isBinDigit _   = False
 134 | 
 135 | ||| Converts a character to a binary digit. This works under the
 136 | ||| assumption that the character has already been verified to be
 137 | ||| a binary digit.
 138 | public export
 139 | binDigit : Char -> Nat
 140 | binDigit '0' = 0
 141 | binDigit _   = 1
 142 | 
 143 | --------------------------------------------------------------------------------
 144 | --          Tokenizers
 145 | --------------------------------------------------------------------------------
 146 | 
 147 | ||| A tokenizing function, which will consume a strict
 148 | ||| prefix of the input list or fail with a stop reason.
 149 | public export
 150 | 0 Tok : (b : Bool) -> (e,a : Type) -> Type
 151 | Tok b e a = (cs : List Char) -> LexRes b cs e a
 152 | 
 153 | ||| A tokenizing function, which will consume additional characters
 154 | ||| from the input string. This can only be used if already some
 155 | ||| have been consumed.
 156 | public export
 157 | 0 AutoTok : (e,a : Type) -> Type
 158 | AutoTok e a =
 159 |      {orig     : List Char}
 160 |   -> (cs       : List Char)
 161 |   -> {auto   p : Suffix True cs orig}
 162 |   -> LexRes True orig e a
 163 | 
 164 | ||| A tokenizing function that cannot fail.
 165 | public export
 166 | 0 SafeTok : (a : Type) -> Type
 167 | SafeTok a =
 168 |      {0 e      : Type}
 169 |   -> {orig     : List Char}
 170 |   -> (cs       : List Char)
 171 |   -> {auto   p : Suffix True cs orig}
 172 |   -> LexRes True orig e a
 173 | 
 174 | ||| A tokenizing function, which will consume additional characters
 175 | ||| from the input string.
 176 | public export
 177 | 0 StrictTok : (e,a : Type) -> Type
 178 | StrictTok e a =
 179 |      {orig     : List Char}
 180 |   -> (cs       : List Char)
 181 |   -> {auto   p : Suffix False cs orig}
 182 |   -> LexRes True orig e a
 183 | 
 184 | public export %inline
 185 | tok : StrictTok e a -> Tok True e a
 186 | tok f ts = f ts
 187 | 
 188 | public export %inline
 189 | autoTok : StrictTok e a -> AutoTok e a
 190 | autoTok f ts @{p} = weakens $ f ts @{weaken p}
 191 | 
 192 | public export %inline
 193 | safeTok : SafeTok a -> AutoTok e a
 194 | safeTok f ts = f ts
 195 | 
 196 | public export %inline
 197 | range :
 198 |      {0 b, bres : Bool}
 199 |   -> {orig      : List Char}
 200 |   -> {errBegin  : List Char}
 201 |   -> (err       : InnerError e)
 202 |   -> (suffixCur : Suffix b errBegin orig)
 203 |   -> (0 errEnd  : List Char)
 204 |   -> {auto sr   : Suffix False errEnd errBegin}
 205 |   -> LexRes bres orig e a
 206 | range err sc errEnd = Fail (weaken sc) errEnd err
 207 | 
 208 | public export %inline
 209 | invalidEscape :
 210 |      {0 b, bres : Bool}
 211 |   -> {orig      : List Char}
 212 |   -> {errBegin  : List Char}
 213 |   -> (suffixCur : Suffix b errBegin orig)
 214 |   -> (0 errEnd  : List Char)
 215 |   -> {auto sr   : Suffix False errEnd errBegin}
 216 |   -> LexRes bres orig e a
 217 | invalidEscape = range InvalidEscape
 218 | 
 219 | public export %inline
 220 | unknownRange :
 221 |      {0 b, bres : Bool}
 222 |   -> {orig      : List Char}
 223 |   -> {errBegin  : List Char}
 224 |   -> (suffixCur : Suffix b errBegin orig)
 225 |   -> (0 errEnd  : List Char)
 226 |   -> {auto sr   : Suffix False errEnd errBegin}
 227 |   -> LexRes bres orig e a
 228 | unknownRange sc ee = range (Unknown $ packPrefix sr) sc ee
 229 | 
 230 | public export %inline
 231 | single :
 232 |      {0 bres        : Bool}
 233 |   -> {c             : Char}
 234 |   -> {orig,errEnd   : List Char}
 235 |   -> (err           : InnerError e)
 236 |   -> (suffixCur     : Suffix b (c::errEnd) orig)
 237 |   -> LexRes bres orig e a
 238 | single r p = range r p errEnd
 239 | 
 240 | public export %inline
 241 | unknown :
 242 |      {0 bres        : Bool}
 243 |   -> {c             : Char}
 244 |   -> {orig,errEnd   : List Char}
 245 |   -> (suffixCur     : Suffix b (c::errEnd) orig)
 246 |   -> LexRes bres orig e a
 247 | unknown sc = unknownRange sc errEnd
 248 | 
 249 | public export %inline
 250 | eoiAt :
 251 |      {0 b, bres  : Bool}
 252 |   -> {orig       : List Char}
 253 |   -> (suffixCur  : Suffix b [] orig)
 254 |   -> LexRes bres orig e a
 255 | eoiAt sc = range EOI sc []
 256 | 
 257 | public export %inline
 258 | failCharClass :
 259 |      {0 bres        : Bool}
 260 |   -> {c             : Char}
 261 |   -> {orig,errEnd   : List Char}
 262 |   -> (class         : CharClass)
 263 |   -> (suffixCur     : Suffix b (c::errEnd) orig)
 264 |   -> LexRes bres orig e a
 265 | failCharClass cc = single (ExpectedChar cc)
 266 | 
 267 | public export %inline
 268 | failDigit :
 269 |      {0 bres        : Bool}
 270 |   -> {c             : Char}
 271 |   -> {orig,errEnd   : List Char}
 272 |   -> (tpe           : DigitType)
 273 |   -> (suffixCur     : Suffix b (c::errEnd) orig)
 274 |   -> LexRes bres orig e a
 275 | failDigit = failCharClass . Digit
 276 | 
 277 | public export %inline
 278 | fail :
 279 |      {0 b, bres : Bool}
 280 |   -> {errBegin  : List Char}
 281 |   -> {orig      : List Char}
 282 |   -> (suffixCur : Suffix b errBegin orig)
 283 |   -> LexRes bres orig e a
 284 | fail {errBegin = x::xs} p = unknown p
 285 | fail {errBegin = []}    p = eoiAt p
 286 | 
 287 | --------------------------------------------------------------------------------
 288 | --          Natural Numbers
 289 | --------------------------------------------------------------------------------
 290 | 
 291 | ||| Tries to read additional decimal digits onto a growing natural number.
 292 | public export
 293 | dec1 : (n : Nat) -> SafeTok Nat
 294 | dec1 n (x::xs) = if isDigit x then dec1 (n*10 + digit x) xs else succ n p
 295 | dec1 n []      = succ n p
 296 | 
 297 | ||| Tries to read a natural number. Fails, if this does not contain at least
 298 | ||| one digit.
 299 | public export
 300 | dec : StrictTok e Nat
 301 | dec (x::xs) = if isDigit x then dec1 (digit x) xs else failDigit Dec p
 302 | dec []      = eoiAt p
 303 | 
 304 | ||| Tries to read more decimal digits onto a growing natural number.
 305 | ||| Supports underscores as separators for better readability.
 306 | public export
 307 | dec_1 : (n : Nat) -> AutoTok e Nat
 308 | dec_1 n ('_'::x::xs) =
 309 |   if isDigit x then dec_1 (n*10 + digit x) xs else failDigit Dec (uncons p)
 310 | dec_1 n (x::xs)      = if isDigit x then dec_1 (n*10 + digit x) xs else succ n p
 311 | dec_1 n []           = Succ n []
 312 | 
 313 | ||| Tries to read a natural number.
 314 | ||| Supports underscores as separators for better readability.
 315 | public export
 316 | decSep : StrictTok e Nat
 317 | decSep (x::xs) = if isDigit x then dec_1 (digit x) xs else failDigit Dec p
 318 | decSep []      = eoiAt p
 319 | 
 320 | ||| Tries to read more binary digits onto a growing natural number.
 321 | public export
 322 | bin1 : (n : Nat) -> SafeTok Nat
 323 | bin1 n (x :: xs) = if isBinDigit x then bin1 (n*2 + binDigit x) xs else succ n p
 324 | bin1 n []        = succ n p
 325 | 
 326 | ||| Tries to read a binary natural number.
 327 | ||| Fails, if this does not contain at least one digit.
 328 | public export
 329 | bin : StrictTok e Nat
 330 | bin (x::xs) = if isBinDigit x then bin1 (binDigit x) xs else failDigit Bin p
 331 | bin []      = eoiAt p
 332 | 
 333 | ||| Tries to read more binary digits onto a growing natural number.
 334 | ||| Supports underscores as separators for better readability.
 335 | public export
 336 | bin_1 : (n : Nat) -> AutoTok e Nat
 337 | bin_1 n ('_' :: x :: xs) =
 338 |   if isBinDigit x then bin_1 (n*2 + binDigit x) xs else failDigit Bin (uncons p)
 339 | bin_1 n (x :: xs) =
 340 |   if isBinDigit x then bin_1 (n*2 + binDigit x) xs else succ n p
 341 | bin_1 n []        = succ n p
 342 | 
 343 | ||| Tries to read a binary natural number.
 344 | ||| Fails, if this does not contain at least one digit.
 345 | ||| Supports underscores as separators for better readability.
 346 | public export
 347 | binSep : StrictTok e Nat
 348 | binSep (x::xs) = if isBinDigit x then bin_1 (binDigit x) xs else failDigit Bin p
 349 | binSep []      = eoiAt p
 350 | 
 351 | ||| Tries to read more octal digits onto a growing natural number.
 352 | public export
 353 | oct1 : (n : Nat) -> SafeTok Nat
 354 | oct1 n (x :: xs) = if isOctDigit x then oct1 (n*8 + octDigit x) xs else succ n p
 355 | oct1 n []        = succ n p
 356 | 
 357 | ||| Tries to read a octal natural number.
 358 | ||| Fails, if this does not contain at least one digit.
 359 | public export
 360 | oct : StrictTok e Nat
 361 | oct (x::xs) = if isOctDigit x then oct1 (octDigit x) xs else failDigit Oct p
 362 | oct []      = eoiAt p
 363 | 
 364 | ||| Tries to read more octal digits onto a growing natural number.
 365 | ||| Supports underscores as separators for better readability.
 366 | public export
 367 | oct_1 : (n : Nat) -> AutoTok e Nat
 368 | oct_1 n ('_' :: x :: xs) =
 369 |   if isOctDigit x then oct_1 (n*8 + octDigit x) xs else failDigit Oct (uncons p)
 370 | oct_1 n (x :: xs) =
 371 |   if isOctDigit x then oct_1 (n*8 + octDigit x) xs else succ n p
 372 | oct_1 n []        = succ n p
 373 | 
 374 | ||| Tries to read a octal natural number.
 375 | ||| Fails, if this does not contain at least one digit.
 376 | ||| Supports underscores as separators for better readability.
 377 | public export
 378 | octSep : StrictTok e Nat
 379 | octSep (x::xs) = if isOctDigit x then oct_1 (octDigit x) xs else failDigit Oct p
 380 | octSep []      = eoiAt p
 381 | 
 382 | ||| Tries to read more hexadecimal digits onto a growing natural number.
 383 | public export
 384 | hex1 : (n : Nat) -> SafeTok Nat
 385 | hex1 n (x :: xs) = if isHexDigit x then hex1 (n*16 + hexDigit x) xs else succ n p
 386 | hex1 n []        = succ n p
 387 | 
 388 | ||| Tries to read a hexadecimal natural number.
 389 | ||| Fails, if this does not contain at least one digit.
 390 | public export
 391 | hex : StrictTok e Nat
 392 | hex (x::xs) = if isHexDigit x then hex1 (hexDigit x) xs else failDigit Hex p
 393 | hex []      = eoiAt p
 394 | 
 395 | ||| Tries to read more hexadecimal digits onto a growing natural number.
 396 | ||| Supports underscores as separators for better readability.
 397 | public export
 398 | hex_1 : (n : Nat) -> AutoTok e Nat
 399 | hex_1 n ('_' :: x :: xs) =
 400 |   if isHexDigit x then hex_1 (n*16 + hexDigit x) xs else failDigit Hex (uncons p)
 401 | hex_1 n (x :: xs) =
 402 |   if isHexDigit x then hex_1 (n*16 + hexDigit x) xs else succ n p
 403 | hex_1 n []        = succ n p
 404 | 
 405 | ||| Tries to read a hexadecimal natural number.
 406 | ||| Fails, if this does not contain at least one digit.
 407 | ||| Supports underscores as separators for better readability.
 408 | public export
 409 | hexSep : StrictTok e Nat
 410 | hexSep (x::xs) = if isHexDigit x then hex_1 (hexDigit x) xs else failDigit Hex p
 411 | hexSep []      = eoiAt p
 412 | 
 413 | --------------------------------------------------------------------------------
 414 | --          Integer Literals
 415 | -----------------------------------------------------------------------------
 416 | 
 417 | ||| A shifter that takes moves an integer prefix
 418 | public export
 419 | int : StrictTok e Integer
 420 | int ('-' :: xs) = negate . cast <$> dec xs
 421 | int xs          = cast <$> dec xs
 422 | 
 423 | ||| Like `int` but also allows an optional leading `'+'` character.
 424 | public export
 425 | intPlus : StrictTok e Integer
 426 | intPlus ('+'::xs) = cast <$> dec xs
 427 | intPlus xs        = int xs
 428 | 
 429 | --------------------------------------------------------------------------------
 430 | --          Other Convertions
 431 | -----------------------------------------------------------------------------
 432 | 
 433 | public export
 434 | takeJustOnto : SnocList y -> (Char -> Maybe y) -> SafeTok (SnocList y)
 435 | takeJustOnto sx f (x :: xs) = case f x of
 436 |   Just vb => takeJustOnto (sx :< vb) f xs
 437 |   Nothing => Succ sx (x::xs)
 438 | takeJustOnto sx f []        = Succ sx []
 439 | 
 440 | ||| Consumes and converts a list prefix until the given
 441 | ||| function returns `Nothing`.
 442 | public export %inline
 443 | takeJust : (Char -> Maybe y) -> SafeTok (SnocList y)
 444 | takeJust f = takeJustOnto [<] f
 445 | 
 446 | ||| Consumes and converts a strict list prefix until the given
 447 | ||| function returns `Nothing`.
 448 | public export %inline
 449 | takeJust1 : (Char -> Maybe y) -> StrictTok e (SnocList y)
 450 | takeJust1 f (x::xs) = case f x of
 451 |   Just vb => takeJustOnto [<vb] f xs
 452 |   Nothing => unknown p
 453 | takeJust1 _ [] = eoiAt p
 454 | 
 455 | --------------------------------------------------------------------------------
 456 | --          Running Tokenizers
 457 | -----------------------------------------------------------------------------
 458 | 
 459 | ||| Repeatedly consumes a strict prefix of a list of characters
 460 | ||| until the whole list is consumed. Drops all white space
 461 | ||| it encounters (unsing `Prelude.isSpace` to determine, what is
 462 | ||| a whitespace character).
 463 | |||
 464 | ||| This assumes that every token is on a single line. Therefore, it is
 465 | ||| more efficient than `multilineDropSpaces`, because it does not have
 466 | ||| to traverse the consumed characters to find line breaks.
 467 | |||
 468 | ||| This is provably total, due to the strictness of the consuming
 469 | ||| function.
 470 | public export
 471 | singleLineDropSpaces :
 472 |      Tok True e a
 473 |   -> String
 474 |   -> Either (Bounded $ InnerError e) (List $ Bounded a)
 475 | singleLineDropSpaces f s = go begin [<] (unpack s) suffixAcc
 476 | 
 477 |   where
 478 |     go : Position
 479 |       -> SnocList (Bounded a)
 480 |       -> (ts : List Char)
 481 |       -> (0 acc : SuffixAcc ts)
 482 |       -> Either (Bounded $ InnerError e) (List $ Bounded a)
 483 |     go p1 sx []       _        = Right $ sx <>> []
 484 |     go p1 sx ('\n'::cs) (SA r) = go (incLine p1) sx cs r
 485 |     go p1 sx (c::cs)    (SA r) =
 486 |       if isSpace c then go (incCol p1) sx cs r
 487 |       else case f (c::cs) of
 488 |         Succ v xs2 @{p}     =>
 489 |           let p2 := move p1 p
 490 |            in go p2 (sx :< bounded v p1 p2) xs2 r
 491 |         Fail s e r => Left $ boundedErr p1 s e r
 492 | 
 493 | ||| Like `singleLineDropSpaces`, but consumed tokens might be
 494 | ||| spread across several lines.
 495 | |||
 496 | ||| This is provably total, due to the strictness of the consuming
 497 | ||| function.
 498 | public export
 499 | multiLineDropSpaces :
 500 |      Tok True e a
 501 |   -> String
 502 |   -> Either (Bounded $ InnerError e) (List $ Bounded a)
 503 | multiLineDropSpaces f s = go begin [<] (unpack s) suffixAcc
 504 | 
 505 |   where
 506 |     go : Position
 507 |       -> SnocList (Bounded a)
 508 |       -> (ts : List Char)
 509 |       -> (0 acc : SuffixAcc ts)
 510 |       -> Either (Bounded $ InnerError e) (List $ Bounded a)
 511 |     go p1 sx []       _        = Right $ sx <>> []
 512 |     go p1 sx ('\n'::cs) (SA r) = go (incLine p1) sx cs r
 513 |     go p1 sx (c::cs)    (SA r) =
 514 |       if isSpace c then go (incCol p1) sx cs r
 515 |       else case f (c::cs) of
 516 |         Succ v xs2 @{p}     =>
 517 |           let p2 := endPos p1 p
 518 |            in go p2 (sx :< bounded v p1 p2) xs2 r
 519 |         Fail s e r => Left $ boundedErr p1 s e r
 520 | 
 521 | ||| Repeatedly consumes a strict prefix of a list of characters
 522 | ||| until the whole list is consumed. It uses the amount of characters
 523 | ||| consumed to determine the bounds of the consumed lexemes.
 524 | |||
 525 | ||| This is provably total, due to the strictness of the consuming
 526 | ||| function.
 527 | public export
 528 | lexManual :
 529 |      Tok True e a
 530 |   -> String
 531 |   -> Either (Bounded $ InnerError e) (List $ Bounded a)
 532 | lexManual f s = go begin [<] (unpack s) suffixAcc
 533 | 
 534 |   where
 535 |     go : Position
 536 |       -> SnocList (Bounded a)
 537 |       -> (ts : List Char)
 538 |       -> (0 acc : SuffixAcc ts)
 539 |       -> Either (Bounded $ InnerError e) (List $ Bounded a)
 540 |     go p1 sx [] _      = Right $ sx <>> []
 541 |     go p1 sx cs (SA r) = case f cs of
 542 |       Succ v xs2 @{p}     =>
 543 |         let p2 := endPos p1 p
 544 |          in go p2 (sx :< bounded v p1 p2) xs2 r
 545 |       Fail s e r => Left $ boundedErr p1 s e r
 546 |