Text.Parser.Core

Reexports

import public Control.Delayed
import public Text.Bounded

Definitions

data Grammar : Type -> Type -> Bool -> Type -> Type

  Description of a language's grammar. The `tok` parameter is the type
  of tokens, and the `consumes` flag is True if the language is guaranteed
  to be non-empty - that is, successfully parsing the language is guaranteed
  to consume some input.

Totality: total
Visibility: export
Constructors:

Empty : ty -> Grammar state tok False ty
Terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
NextIs : String -> (tok -> Bool) -> Grammar state tok False tok
EOF : Grammar state tok False ()
Fail : Maybe Bounds -> Bool -> String -> Grammar state tok c ty
Try : Grammar state tok c ty -> Grammar state tok c ty
Commit : Grammar state tok False ()
MustWork : Grammar state tok c a -> Grammar state tok c a
SeqEat : Grammar state tok True a -> Inf (a -> Grammar state tok c2 b) -> Grammar state tok True b
SeqEmpty : Grammar state tok c1 a -> (a -> Grammar state tok c2 b) -> Grammar state tok (c1 || Delay c2) b
ThenEat : Grammar state tok True () -> Inf (Grammar state tok c2 a) -> Grammar state tok True a
ThenEmpty : Grammar state tok c1 () -> Grammar state tok c2 a -> Grammar state tok (c1 || Delay c2) a
Alt : Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) -> Grammar state tok (c1 && Delay c2) ty
Bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
Position : Grammar state tok False Bounds
Act : state -> Grammar state tok False ()

Hint:

Functor (Grammar state tok c)

(>>=) : Grammar state tok c1 a -> inf c1 (a -> Grammar state tok c2 b) -> Grammar state tok (c1 || Delay c2) b

  Sequence two grammars. If either consumes some input, the sequence is
  guaranteed to consume some input. If the first one consumes input, the
  second is allowed to be recursive (because it means some input has been
  consumed and therefore the input is smaller)

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 1

(>>) : Grammar state tok c1 () -> inf c1 (Grammar state tok c2 a) -> Grammar state tok (c1 || Delay c2) a

  Sequence two grammars. If either consumes some input, the sequence is
  guaranteed to consume some input. If the first one consumes input, the
  second is allowed to be recursive (because it means some input has been
  consumed and therefore the input is smaller)

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 1

seq : Grammar state tok c1 a -> (a -> Grammar state tok c2 b) -> Grammar state tok (c1 || Delay c2) b

  Sequence two grammars. If either consumes some input, the sequence is
  guaranteed to consume input. This is an explicitly non-infinite version
  of `>>=`.

Totality: total
Visibility: export

join : Grammar state tok c1 (Grammar state tok c2 a) -> Grammar state tok (c1 || Delay c2) a

  Sequence a grammar followed by the grammar it returns.

Totality: total
Visibility: export

(<|>) : Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) -> Grammar state tok (c1 && Delay c2) ty

  Give two alternative grammars. If both consume, the combination is
  guaranteed to consume.

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

(<||>) : Grammar state tok c1 a -> Lazy (Grammar state tok c2 b) -> Grammar state tok (c1 && Delay c2) (Either a b)

  Take the tagged disjunction of two grammars. If both consume, the
  combination is guaranteed to consume.

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

(<*>) : Grammar state tok c1 (a -> b) -> Grammar state tok c2 a -> Grammar state tok (c1 || Delay c2) b

  Sequence a grammar with value type `a -> b` and a grammar
  with value type `a`. If both succeed, apply the function
  from the first grammar to the value from the second grammar.
  Guaranteed to consume if either grammar consumes.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 3

(<*) : Grammar state tok c1 a -> Grammar state tok c2 b -> Grammar state tok (c1 || Delay c2) a

  Sequence two grammars. If both succeed, use the value of the first one.
  Guaranteed to consume if either grammar consumes.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 3

(*>) : Grammar state tok c1 a -> Grammar state tok c2 b -> Grammar state tok (c1 || Delay c2) b

  Sequence two grammars. If both succeed, use the value of the second one.
  Guaranteed to consume if either grammar consumes.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 3

act : state -> Grammar state tok False ()

Totality: total
Visibility: export

mapToken : (a -> b) -> Grammar state b c ty -> Grammar state a c ty

  Produce a grammar that can parse a different type of token by providing a
  function converting the new token type into the original one.

Totality: total
Visibility: export

pure : ty -> Grammar state tok False ty

  Always succeed with the given value.

Totality: total
Visibility: export

nextIs : String -> (tok -> Bool) -> Grammar state tok False tok

  Check whether the next token satisfies a predicate

Totality: total
Visibility: export

peek : Grammar state tok False tok

  Look at the next token in the input

Totality: total
Visibility: export

terminal : String -> (tok -> Maybe a) -> Grammar state tok True a

  Succeeds if running the predicate on the next token returns Just x,
  returning x. Otherwise fails.

Totality: total
Visibility: export

fail : String -> Grammar state tok c ty

  Always fail with a message

Totality: total
Visibility: export

failLoc : Bounds -> String -> Grammar state tok c ty

  Always fail with a message and a location

Totality: total
Visibility: export

fatalError : String -> Grammar state tok c ty

  Fail with no possibility for recovery (i.e.
  no alternative parsing can succeed).

Totality: total
Visibility: export

fatalLoc : Bounds -> String -> Grammar state tok c ty

  Fail with no possibility for recovery (i.e.
  no alternative parsing can succeed).

Totality: total
Visibility: export

try : Grammar state tok c ty -> Grammar state tok c ty

  Catch a fatal error

Totality: total
Visibility: export

eof : Grammar state tok False ()

  Succeed if the input is empty

Totality: total
Visibility: export

commit : Grammar state tok False ()

  Commit to an alternative; if the current branch of an alternative
  fails to parse, no more branches will be tried

Totality: total
Visibility: export

mustWork : Grammar state tok c ty -> Grammar state tok c ty

  If the parser fails, treat it as a fatal error

Totality: total
Visibility: export

bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)

Totality: total
Visibility: export

position : Grammar state tok False Bounds

Totality: total
Visibility: export

data ParsingError : Type -> Type

Totality: total
Visibility: public export
Constructor:

Error : String -> Maybe Bounds -> ParsingError tok

Hint:

Show tok => Show (ParsingError tok)

parse : Grammar () tok c ty -> List (WithBounds tok) -> Either (List1 (ParsingError tok)) (ty, List (WithBounds tok))

  Parse a list of tokens according to the given grammar. If successful,
  returns a pair of the parse result and the unparsed tokens (the remaining
  input).

Totality: total
Visibility: export

parseWith : Monoid state => Grammar state tok c ty -> List (WithBounds tok) -> Either (List1 (ParsingError tok)) (state, (ty, List (WithBounds tok)))

Totality: total
Visibility: export