Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.Syntax.Concrete.Operators.Parser

Contents

Synopsis

Documentation

class HasRange e => IsExpr e whereSource

Parser combinators

recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok aSource

Combining a hierarchy of parsers.

chainr1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t aSource

Variant of chainr1

chainl1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t aSource

Variant of chainl1

partP :: IsExpr e => String -> ReadP e (Range, NamePart)Source

Parse a specific identifier as a NamePart

binop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> e -> ReadP a e)Source

preop, postop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)Source

opP :: IsExpr e => ReadP e e -> NewNotation -> ReadP e (NewNotation, Range, [e])Source

Parse the operator part of the given syntax. holes at beginning and end are IGNORED.

rebuild :: forall symbol e. IsExpr e => NewNotation -> Range -> [e] -> ReadP symbol eSource

Given a name with a syntax spec, and a list of parsed expressions fitting it, rebuild the expression. Note that this function must not parse any input (as guaranteed by the type)

($$$) :: (e -> ReadP a e) -> ReadP a e -> ReadP a eSource

infixP, nonfixP, prefixP, postfixP, infixlP, infixrP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource

Parse using the appropriate fixity, given a parser parsing the operator part, the name of the operator, and a parser of subexpressions.

appP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e eSource

atomP :: IsExpr e => (Name -> Bool) -> ReadP e eSource