Text.Parse.Manual

(source)

This module provides utilities for writing parsers by hand (without
using the combinators from module `Text.Parse.Core`).

Typically, you get the best performance by using direct pattern matches
and explicit recursion. However, for those cases where performance is
not the main issue, this module provides some combinators for
certain reoccuring patterns.

It is strongly recommended to use a lexer and probably one or two
cleanup passes over the sequence of generated tokens before parsing,
as this can significantly simplify the parsers.

Example parsers can be found in sub-packages `parser-json` and
`parser-toml`.

Note: The raison d'etre of this module is that writing provably total
      parsers for (recursive) syntax trees is cumbersome or even impossible
      when using parser combinators. In such cases, you have to arrange
      things manually, using a `SuffixAcc` helper to proof termination.
      For everything else, the combinators in here can make your life
      easier.

Reexports

import public Data.Bool.Rewrite
import public Data.List1
import public Data.List.Shift
import public Data.List.Suffix
import public Data.List.Suffix.Result
import public Data.List.Suffix.Result0
import public Text.Bounds
import public Text.FC
import public Text.ParseError
import public Text.Lex.Manual
import public Text.Lex.Shift

Definitions

0 Res : Bool -> (t : Type) -> List (Bounded t) -> Type -> Type -> Type

Totality: total
Visibility: public export

0 Grammar : Bool -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export

0 AccGrammar : Bool -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export

acc : AccGrammar b t e a -> Grammar b t e a

  Converts a grammar requiring a proof of accessibility to a regular
  grammar.

Totality: total
Visibility: public export

swapOr : Grammar (x || Delay y) t e a -> Grammar (y || Delay x) t e a

Totality: total
Visibility: public export

orSame : Grammar (x || Delay x) t e a -> Grammar x t e a

Totality: total
Visibility: public export

orTrue : Grammar (x || Delay True) t e a -> Grammar True t e a

Totality: total
Visibility: public export

orFalse : Grammar (x || Delay False) t e a -> Grammar x t e a

Totality: total
Visibility: public export

swapAnd : Grammar (x && Delay y) t e a -> Grammar (y && Delay x) t e a

Totality: total
Visibility: public export

andSame : Grammar (x && Delay x) t e a -> Grammar x t e a

Totality: total
Visibility: public export

andTrue : Grammar (x && Delay True) t e a -> Grammar x t e a

Totality: total
Visibility: public export

andFalse : Grammar (x && Delay False) t e a -> Grammar False t e a

Totality: total
Visibility: public export

terminal : Interpolation t => (t -> Maybe a) -> Grammar True t e a

  Tries to convert the head of the list of tokens.
  Fails with appropriate errors if the list is empty or the conversion
  fails.

Totality: total
Visibility: public export

terminalE : (t -> Either e a) -> Grammar True t e a

  Like `terminal` but fails with a custom error if the conversion fails.

Totality: total
Visibility: public export

exact : Interpolation t => Eq t => t -> Grammar True t e ()

  Tries to drop the given token from the head of the list of tokens.
  Fails with appropriate errors if the list is empty or the token
  at the head does not match.

Totality: total
Visibility: public export

peek : Grammar False t e t

  Look at the next token without consuming any input.

Totality: total
Visibility: public export

nextIs : Interpolation t => (t -> Bool) -> Grammar False t e t

  Check whether the next token satisfies a predicate. Does not consume.

Totality: total
Visibility: public export

nextEquals : Interpolation t => Eq t => t -> Grammar False t e t

  Check whether the next token equals the given value. Does not consume.

Totality: total
Visibility: public export

testParse : Show a => Interpolation e => Interpolation t => (Origin -> String -> Either (ParseError e) a) -> String -> IO ()

  Utility for testing a parses and the error messages it produces
  at the REPL.

Totality: total
Visibility: export