Text.ParseError

(source)

Definitions

data DigitType : Type

Totality: total
Visibility: public export
Constructors:

Bin : DigitType
Oct : DigitType
Dec : DigitType
Hex : DigitType

Hints:

Eq DigitType
Interpolation DigitType
Ord DigitType
Show DigitType

data CharClass : Type

Totality: total
Visibility: public export
Constructors:

Space : CharClass

  A whitespace character

Digit : DigitType -> CharClass

  A digit

Upper : CharClass

  An upper-case letter

Lower : CharClass

  A lower-case letter

Alpha : CharClass

  An upper- or lower-case letter

AlphaNum : CharClass

  An upper- or lower-case letter or a decimal digit

Hints:

Eq CharClass
Interpolation CharClass
Ord CharClass
Show CharClass

data InnerError : Type -> Type

Totality: total
Visibility: public export
Constructors:

Custom : e -> InnerError e

  A custom error for the current parsing topic

EOI : InnerError e

  Unexpected end of input

Expected : List String -> String -> InnerError e

  Expected one of the given tokens but got something else.

ExpectedChar : CharClass -> InnerError e

  Expected the given type of character

ExpectedEOI : InnerError e

  Got more input that we expected

InvalidControl : Char -> InnerError e

  Got an invalid control character

InvalidEscape : InnerError e

  Got an invalid character escape sequence

OutOfBounds : String -> InnerError e

  Got a (usually numeric) value that was out of bounds

Unclosed : String -> InnerError e

  An unclosed opening token

Unknown : String -> InnerError e

  Got an unknown or invalid token

InvalidByte : Bits8 -> InnerError e

  An unexpected non-ascii byte, either from an unexpected
  mutli-byte codepoint or from altogether invalid unicode
  input.

Hints:

Cast a e => Cast a (InnerError e)
Eq err => Eq (InnerError err)
FailParse (Either (Bounded (InnerError e))) e
Functor InnerError
Interpolation e => Interpolation (InnerError e)
Show err => Show (InnerError err)

0 BoundedErr : Type -> Type

  Convenience alias for `Bounded . InnerError`

Totality: total
Visibility: public export

hexChar : Bits8 -> Char

  Converts a value in the range `[0..15]` to a hexadecimal
  lower-case character.
  
  For simplicity, this function assumes the range has been checked.
  Therefore, values `>= 15` will return `'f'`.

Totality: total
Visibility: public export

toHex : Bits8 -> String

  Pretty prints a byte as two hexadecimal digits.
  
  Example: `toHex 110 === "6e"`.

Totality: total
Visibility: export

interface FailParse : (Type -> Type) -> Type -> Type

Parameters: m, e
Methods:

parseFail : Bounds -> InnerError e -> m a

Implementation:

FailParse (Either (Bounded (InnerError e))) e

parseFail : FailParse m e => Bounds -> InnerError e -> m a

Totality: total
Visibility: public export

custom : FailParse m e => Bounds -> e -> m a

Totality: total
Visibility: public export

expected : Interpolation t => FailParse m e => Bounds -> t -> String -> m a

Totality: total
Visibility: public export

unclosed : Interpolation t => FailParse m e => Bounds -> t -> m a

Totality: total
Visibility: public export

unexpected : Interpolation t => FailParse m e => Bounded t -> m a

Totality: total
Visibility: public export

eoi : FailParse m e => m a

Totality: total
Visibility: public export

expectedEOI : FailParse m e => Bounds -> m a

Totality: total
Visibility: public export

fromVoid : InnerError Void -> InnerError e

Totality: total
Visibility: public export

record FCErr : Type -> Type

  Pairs a parsing error with a text's origin, the error's bound, and
  the text itself.

Totality: total
Visibility: public export
Constructor:

PE : Origin -> Bounds -> Bounds -> Maybe String -> e -> FCErr e

Projections:

.bounds : FCErr e -> Bounds

  Absolute bounds where the error occurred.

.content : FCErr e -> Maybe String

  Relevant part of the text that was parsed.

.error : FCErr e -> e

  The actual error that occurred.

.origin : FCErr e -> Origin

  Origin of the byte sequence that was parsed.

.relBounds : FCErr e -> Bounds

  Bounds where the error occurred relative to the string stored
  in `content`. See also the docs of `Text.ILex.FC.printFC` for an
  explanation why the distinction between relative and absolute bounds
  is necessary.

Hints:

Eq e => Eq (FCErr e)
Interpolation e => Interpolation (FCErr e)
Show e => Show (FCErr e)

.origin : FCErr e -> Origin

  Origin of the byte sequence that was parsed.

Totality: total
Visibility: public export

origin : FCErr e -> Origin

  Origin of the byte sequence that was parsed.

Totality: total
Visibility: public export

.bounds : FCErr e -> Bounds

  Absolute bounds where the error occurred.

Totality: total
Visibility: public export

bounds : FCErr e -> Bounds

  Absolute bounds where the error occurred.

Totality: total
Visibility: public export

.relBounds : FCErr e -> Bounds

  Bounds where the error occurred relative to the string stored
  in `content`. See also the docs of `Text.ILex.FC.printFC` for an
  explanation why the distinction between relative and absolute bounds
  is necessary.

Totality: total
Visibility: public export

relBounds : FCErr e -> Bounds

  Bounds where the error occurred relative to the string stored
  in `content`. See also the docs of `Text.ILex.FC.printFC` for an
  explanation why the distinction between relative and absolute bounds
  is necessary.

Totality: total
Visibility: public export

.content : FCErr e -> Maybe String

  Relevant part of the text that was parsed.

Totality: total
Visibility: public export

content : FCErr e -> Maybe String

  Relevant part of the text that was parsed.

Totality: total
Visibility: public export

.error : FCErr e -> e

  The actual error that occurred.

Totality: total
Visibility: public export

error : FCErr e -> e

  The actual error that occurred.

Totality: total
Visibility: public export

0 ParseError : Type -> Type

Totality: total
Visibility: public export

toParseError : Origin -> String -> Bounded e -> FCErr e

  Converts a bounded error to a `ParseError` by pairing it with
  an origin and the parsed string.

Totality: total
Visibility: export

leftErr : Origin -> String -> Either (Bounded e) a -> Either (FCErr e) a

Totality: total
Visibility: export