Text.Parse.Syntax

Definitions

pure : a -> Grammar False t e a

Totality: total
Visibility: public export

(<*>) : Grammar b1 t e (a -> b) -> Grammar b2 t e a -> Grammar (b1 || Delay b2) t e b

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

(*>) : Grammar b1 t e () -> Grammar b2 t e a -> Grammar (b1 || Delay b2) t e a

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

seqt : Grammar b t e () -> Grammar True t e a -> Grammar True t e a

  Version of `(*>)` specialized for strict second grammars

Totality: total
Visibility: public export

(<*) : Grammar b1 t e a -> Grammar b2 t e () -> Grammar (b1 || Delay b2) t e a

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

before : Interpolation t => Eq t => Grammar b t e a -> t -> Grammar True t e a

  Drops the given token after parsing the given grammar

Totality: total
Visibility: public export

after : Interpolation t => Eq t => t -> Grammar b t e a -> Grammar True t e a

  Drops the given token before parsing the given grammar

Totality: total
Visibility: public export

between : Interpolation t => Eq t => t -> t -> Grammar b t e a -> Grammar True t e a

  Wrapps the given grammar between an opening and closing token.
  
  Note: This fails with an `Unclosed` exception if the end of
        input is reached without closing the opening token.

Totality: total
Visibility: public export

optional : Grammar b t e a -> Grammar False t e (Maybe a)

Totality: total
Visibility: public export

manyOnto : (InnerError e -> Bool) -> Grammar True t e a -> SnocList a -> AccGrammar False t e (List a)

Totality: total
Visibility: public export

manyF : (InnerError e -> Bool) -> Grammar True t e a -> Grammar False t e (List a)

  Runs the given parser zero or more times, accumulating the
  results in a list.
  
  Note: This will fail in case of a fatal error, which allows for
        more fine-grained control over whether a parser is successful
        or not.

Totality: total
Visibility: public export

many : Grammar True t e a -> Grammar False t e (List a)

  Runs the given parser zero or more times, accumulating the
  results in a list.
  
  Note: This will never fail, even if the given parser fails
        with an error that should be fatal. User `manyF` to
        have the ability to specify fatal errors.

Totality: total
Visibility: public export

someF : (InnerError e -> Bool) -> Grammar True t e a -> Grammar True t e (List1 a)

  Runs the given parser one or more times, accumulating the
  results in a non-empty list.
  
  Note: This will fail in case of a fatal error, even when parsing
        the tail of the list, which allows for
        more fine-grained control over whether a parser is successful
        or not.

Totality: total
Visibility: public export

some : Grammar True t e a -> Grammar True t e (List1 a)

  Runs the given parser one or more times, accumulating the
  results in a non-empty list.
  
  Note: User `manyF` for the ability to specify fatal errors.

Totality: total
Visibility: public export

sepByF1 : (InnerError e -> Bool) -> Grammar b t e () -> Grammar True t e a -> Grammar True t e (List1 a)

  Runs the given parser one or more times, separating occurences with
  the given separator.
  
  Note: This will fail in case of a fatal error, even when parsing
        the tail of the list, which allows for
        more fine-grained control over whether a parser is successful
        or not.
  
        Consider using `sepByExact1` for better error behavior,
        if the separator consists of a single, constant token.

Totality: total
Visibility: public export

sepByExact1 : Interpolation t => Eq t => Eq e => t -> Grammar True t e a -> Grammar True t e (List1 a)

  Like `sepBy1` but with better error behavior:
  If the separator was recognized, this fails instead of
  aborting with a partial list.

Totality: total
Visibility: public export