Text.Lex.Manual

Reexports

Definitions

0 LexRes : Bool -> List Char -> Type -> Type -> Type

  Result of running a (strict) tokenizer.

Totality: total
Visibility: public export

move : Position -> Suffix b xs ys -> Position

  Shift the position by a number of columns represented by
  a `Suffix` value. This assumes, that no line break was "shifted".

Totality: total
Visibility: public export

endPos : Position -> Suffix b ys cs -> Position

  Calculates the new position from a `Suffix` by reinspecting
  the original list of characters.
  
  Use this, if the consumed prefix might have contained line breaks.
  Otherwise, consider using `move`, which runs in O(1) instead of O(n).

Totality: total
Visibility: export

boundedErr : Position -> Suffix False errStart ts -> (0 errEnd : List Char) -> Suffix False errEnd errStart => e -> Bounded e

Totality: total
Visibility: export

(<|>) : Result b t ts r a -> Lazy (Result b t ts r a) -> Result b t ts r a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 2

isSpaceChar : Char -> Bool

  Returns true if the character is a space (`' '`) character.

Totality: total
Visibility: public export

isLineFeed : Char -> Bool

  Returns true if the character is a line feed (`'\n'`) character.

Totality: total
Visibility: public export

octDigit : Char -> Nat

  Converts a character to an octal digit. This works under the
  assumption that the character has already been verified to be
  an octal digit.

Totality: total
Visibility: public export

digit : Char -> Nat

  Converts a character to a decimal digit. This works under the
  assumption that the character has already been verified to be
  a decimal digit.

Totality: total
Visibility: public export

hexDigit : Char -> Nat

  Converts a character to a hexadecimal digit. This works under the
  assumption that the character has already been verified to be
  a hexadecimal digit.

Totality: total
Visibility: public export

isBinDigit : Char -> Bool

  True if the given character is a binary digit.

Totality: total
Visibility: public export

binDigit : Char -> Nat

  Converts a character to a binary digit. This works under the
  assumption that the character has already been verified to be
  a binary digit.

Totality: total
Visibility: public export

0 Tok : Bool -> Type -> Type -> Type

  A tokenizing function, which will consume a strict
  prefix of the input list or fail with a stop reason.

Totality: total
Visibility: public export

0 AutoTok : Type -> Type -> Type

  A tokenizing function, which will consume additional characters
  from the input string. This can only be used if already some
  have been consumed.

Totality: total
Visibility: public export

0 SafeTok : Type -> Type

  A tokenizing function that cannot fail.

Totality: total
Visibility: public export

0 StrictTok : Type -> Type -> Type

  A tokenizing function, which will consume additional characters
  from the input string.

Totality: total
Visibility: public export

tok : StrictTok e a -> Tok True e a

Totality: total
Visibility: public export

autoTok : StrictTok e a -> AutoTok e a

Totality: total
Visibility: public export

safeTok : SafeTok a -> AutoTok e a

Totality: total
Visibility: public export

range : InnerError e -> Suffix b errBegin orig -> (0 errEnd : List Char) -> Suffix False errEnd errBegin => LexRes bres orig e a

Totality: total
Visibility: public export

invalidEscape : Suffix b errBegin orig -> (0 errEnd : List Char) -> Suffix False errEnd errBegin => LexRes bres orig e a

Totality: total
Visibility: public export

unknownRange : Suffix b errBegin orig -> (0 errEnd : List Char) -> Suffix False errEnd errBegin => LexRes bres orig e a

Totality: total
Visibility: public export

single : InnerError e -> Suffix b (c :: errEnd) orig -> LexRes bres orig e a

Totality: total
Visibility: public export

unknown : Suffix b (c :: errEnd) orig -> LexRes bres orig e a

Totality: total
Visibility: public export

eoiAt : Suffix b [] orig -> LexRes bres orig e a

Totality: total
Visibility: public export

failCharClass : CharClass -> Suffix b (c :: errEnd) orig -> LexRes bres orig e a

Totality: total
Visibility: public export

failDigit : DigitType -> Suffix b (c :: errEnd) orig -> LexRes bres orig e a

Totality: total
Visibility: public export

fail : Suffix b errBegin orig -> LexRes bres orig e a

Totality: total
Visibility: public export

dec1 : Nat -> SafeTok Nat

  Tries to read additional decimal digits onto a growing natural number.

Totality: total
Visibility: public export

dec : StrictTok e Nat

  Tries to read a natural number. Fails, if this does not contain at least
  one digit.

Totality: total
Visibility: public export

dec_1 : Nat -> AutoTok e Nat

  Tries to read more decimal digits onto a growing natural number.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

decSep : StrictTok e Nat

  Tries to read a natural number.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

bin1 : Nat -> SafeTok Nat

  Tries to read more binary digits onto a growing natural number.

Totality: total
Visibility: public export

bin : StrictTok e Nat

  Tries to read a binary natural number.
  Fails, if this does not contain at least one digit.

Totality: total
Visibility: public export

bin_1 : Nat -> AutoTok e Nat

  Tries to read more binary digits onto a growing natural number.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

binSep : StrictTok e Nat

  Tries to read a binary natural number.
  Fails, if this does not contain at least one digit.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

oct1 : Nat -> SafeTok Nat

  Tries to read more octal digits onto a growing natural number.

Totality: total
Visibility: public export

oct : StrictTok e Nat

  Tries to read a octal natural number.
  Fails, if this does not contain at least one digit.

Totality: total
Visibility: public export

oct_1 : Nat -> AutoTok e Nat

  Tries to read more octal digits onto a growing natural number.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

octSep : StrictTok e Nat

  Tries to read a octal natural number.
  Fails, if this does not contain at least one digit.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

hex1 : Nat -> SafeTok Nat

  Tries to read more hexadecimal digits onto a growing natural number.

Totality: total
Visibility: public export

hex : StrictTok e Nat

  Tries to read a hexadecimal natural number.
  Fails, if this does not contain at least one digit.

Totality: total
Visibility: public export

hex_1 : Nat -> AutoTok e Nat

  Tries to read more hexadecimal digits onto a growing natural number.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

hexSep : StrictTok e Nat

  Tries to read a hexadecimal natural number.
  Fails, if this does not contain at least one digit.
  Supports underscores as separators for better readability.

Totality: total
Visibility: public export

int : StrictTok e Integer

  A shifter that takes moves an integer prefix

Totality: total
Visibility: public export

intPlus : StrictTok e Integer

  Like `int` but also allows an optional leading `'+'` character.

Totality: total
Visibility: public export

takeJustOnto : SnocList y -> (Char -> Maybe y) -> SafeTok (SnocList y)

Totality: total
Visibility: public export

takeJust : (Char -> Maybe y) -> SafeTok (SnocList y)

  Consumes and converts a list prefix until the given
  function returns `Nothing`.

Totality: total
Visibility: public export

takeJust1 : (Char -> Maybe y) -> StrictTok e (SnocList y)

  Consumes and converts a strict list prefix until the given
  function returns `Nothing`.

Totality: total
Visibility: public export

singleLineDropSpaces : Tok True e a -> String -> Either (Bounded (InnerError e)) (List (Bounded a))

  Repeatedly consumes a strict prefix of a list of characters
  until the whole list is consumed. Drops all white space
  it encounters (unsing `Prelude.isSpace` to determine, what is
  a whitespace character).
  
  This assumes that every token is on a single line. Therefore, it is
  more efficient than `multilineDropSpaces`, because it does not have
  to traverse the consumed characters to find line breaks.
  
  This is provably total, due to the strictness of the consuming
  function.

Totality: total
Visibility: public export

multiLineDropSpaces : Tok True e a -> String -> Either (Bounded (InnerError e)) (List (Bounded a))

  Like `singleLineDropSpaces`, but consumed tokens might be
  spread across several lines.
  
  This is provably total, due to the strictness of the consuming
  function.

Totality: total
Visibility: public export

lexManual : Tok True e a -> String -> Either (Bounded (InnerError e)) (List (Bounded a))

  Repeatedly consumes a strict prefix of a list of characters
  until the whole list is consumed. It uses the amount of characters
  consumed to determine the bounds of the consumed lexemes.
  
  This is provably total, due to the strictness of the consuming
  function.

Totality: total
Visibility: public export