TyRE.Text.Parser.Core

This is a slightly modified copy of the same module from `contrib` package.

Reexports

Definitions

data Grammar : 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: public export
Constructors:

Empty : ty -> Grammar tok False ty

Terminal : String -> (tok -> Maybe a) -> Grammar tok True a

NextIs : String -> (tok -> Bool) -> Grammar tok False tok

EOF : Grammar tok False ()

Fail : Bool -> String -> Grammar tok c ty

Commit : Grammar tok False ()

MustWork : Grammar tok c a -> Grammar tok c a

SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) -> Grammar tok True b

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

ThenEat : Grammar tok True () -> Inf (Grammar tok c2 b) -> Grammar tok True b

ThenEmpty : Grammar tok c1 () -> Grammar tok c2 b -> Grammar tok (c1 || Delay c2) b

Alt : Grammar tok c1 ty -> Grammar tok c2 ty -> Grammar tok (c1 && Delay c2) ty

Hint: 

Functor (Grammar tok c)

(>>=) : Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) -> Grammar 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)

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

(>>) : Grammar tok c1 () -> inf c1 (Grammar tok c2 a) -> Grammar 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)

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

seq : Grammar tok c1 a -> (a -> Grammar tok c2 b) -> Grammar 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 `>>=`.

Visibility: public export

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

  Sequence a grammar followed by the grammar it returns.

Visibility: public export

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

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

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

(<*>) : Grammar tok c1 (a -> b) -> Inf (Grammar tok c2 a) -> Grammar 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.

Visibility: public export
Fixity Declarations:
infixl operator, level 3
infixr operator, level 6

(<*) : Grammar tok c1 a -> Inf (Grammar tok c2 b) -> Grammar 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.

Visibility: public export
Fixity Declarations:
infixl operator, level 3
infixr operator, level 6

(*>) : Grammar tok c1 a -> Inf (Grammar tok c2 b) -> Grammar 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.

Visibility: public export
Fixity Declarations:
infixl operator, level 3
infixr operator, level 6

mapToken : (a -> b) -> Grammar b c ty -> Grammar 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.

Visibility: public export

pure : ty -> Grammar tok False ty

  Always succeed with the given value.

Visibility: public export

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

  Check whether the next token satisfies a predicate

Visibility: public export

peek : Grammar tok False tok

  Look at the next token in the input

Visibility: public export

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

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

Visibility: public export

fail : String -> Grammar tok c ty

  Always fail with a message

Visibility: public export

fatalError : String -> Grammar tok c ty

Visibility: public export

eof : Grammar tok False ()

  Succeed if the input is empty

Visibility: public export

commit : Grammar tok False ()

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

Visibility: public export

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

  If the parser fails, treat it as a fatal error

Visibility: public export

data ParseResult : List tok -> Bool -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Failure : Bool -> Bool -> String -> List tok -> ParseResult xs c ty

EmptyRes : Bool -> ty -> (more : List tok) -> ParseResult more False ty

NonEmptyRes : Bool -> ty -> (more : List tok) -> ParseResult (x :: (xs ++ more)) c ty

weakenRes : Bool -> ParseResult xs c ty -> ParseResult xs (whatever && Delay c) ty

Visibility: public export

doParse : Bool -> Grammar tok c ty -> (xs : List tok) -> ParseResult xs c ty

Visibility: public export

data ParseError : Type -> Type

Totality: total
Visibility: public export
Constructor: 

Error : String -> List tok -> ParseError tok

parse : Grammar tok c ty -> List tok -> Either (ParseError tok) (ty, List 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).

Visibility: public export