Agda.Syntax.Concrete.Operators.Parser

Documentation

data ExprView e

Constructors

LocalV QName

WildV e

OtherV e

AppV e (NamedArg e)

OpAppV QName (Set Name) [NamedArg (OpApp e)]

The QName is possibly ambiguous, but it must correspond to one of the names in the set.

HiddenArgV (Named_ e)

InstanceArgV (Named_ e)

LamV [LamBinding] e

ParenV e

Instances

IsExpr e => HasRange (ExprView e)

class HasRange e => IsExpr e where

Methods

exprView :: e -> ExprView e

unExprView :: ExprView e -> e

Parser combinators

partP :: IsExpr e => [Name] -> RawName -> ReadP e Range

Parse a specific identifier as a NamePart

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

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

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

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

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

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

Given a name with a syntax spec, and a list of parsed expressions fitting it, rebuild the expression.

rebuildBinding :: IsExpr e => ExprView e -> LamBinding

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

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

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

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

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

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

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

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

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

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

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

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

argsP :: IsExpr e => ReadP e e -> ReadP e [NamedArg e]

appP :: IsExpr e => ReadP e e -> ReadP e [NamedArg e] -> ReadP e e

atomP :: IsExpr e => (QName -> Bool) -> ReadP e e