Agda.Syntax.Concrete.Operators.Parser

Documentation

placeholder :: PositionInName -> Parser e (MaybePlaceholder e)

maybePlaceholder :: Maybe PositionInName -> Parser e e -> Parser e (MaybePlaceholder e)

satNoPlaceholder :: (e -> Maybe a) -> Parser e a

data ExprView e

Constructors

LocalV QName

WildV e

OtherV e

AppV e (NamedArg e)

OpAppV QName (Set Name) (OpAppArgs' 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 (List1 LamBinding) e

ParenV e

Instances

IsExpr e => HasRange (ExprView e)

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

getRange :: ExprView e -> Range

class HasRange e => IsExpr e where

Methods

exprView :: e -> ExprView e

unExprView :: ExprView e -> e

patternView :: e -> Maybe Pattern

Instances

IsExpr Expr

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Expr -> ExprView Expr

unExprView :: ExprView Expr -> Expr

patternView :: Expr -> Maybe Pattern

IsExpr Pattern

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

exprView :: Pattern -> ExprView Pattern

unExprView :: ExprView Pattern -> Pattern

patternView :: Pattern -> Maybe Pattern

data ParseSections

Should sections be parsed?

Constructors

ParseSections

DoNotParseSections

Instances

Show ParseSections

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

showsPrec :: Int -> ParseSections -> ShowS

show :: ParseSections -> String

showList :: [ParseSections] -> ShowS

Eq ParseSections

Defined in Agda.Syntax.Concrete.Operators.Parser

Methods

(==) :: ParseSections -> ParseSections -> Bool

(/=) :: ParseSections -> ParseSections -> Bool

parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]

Runs a parser. If sections should be parsed, then identifiers with at least two name parts are split up into multiple tokens, using PositionInName to record the tokens' original positions within their respective identifiers.

Parser combinators

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

Parse a specific identifier as a NamePart

atLeastTwoParts :: IsExpr e => Parser e Name

Parses a split-up, unqualified name consisting of at least two name parts.

The parser does not check that underscores and other name parts alternate. The range of the resulting name is the range of the first name part that is not an underscore.

patternBinder :: IsExpr e => Parser e Binder

Parses a potentially pattern-matching binder

type family OperatorType (k :: NotationKind) (e :: Type) :: Type

Used to define the return type of opP.

Instances

type OperatorType 'InfixNotation e

Defined in Agda.Syntax.Concrete.Operators.Parser

type OperatorType 'InfixNotation e = MaybePlaceholder e -> MaybePlaceholder e -> e

type OperatorType 'NonfixNotation e

Defined in Agda.Syntax.Concrete.Operators.Parser

type OperatorType 'NonfixNotation e = e

type OperatorType 'PostfixNotation e

Defined in Agda.Syntax.Concrete.Operators.Parser

type OperatorType 'PostfixNotation e = MaybePlaceholder e -> e

type OperatorType 'PrefixNotation e

Defined in Agda.Syntax.Concrete.Operators.Parser

type OperatorType 'PrefixNotation e = MaybePlaceholder e -> e

data NK (k :: NotationKind) :: Type where

A singleton type for NotationKind (except for the constructor NoNotation).

Constructors

In :: NK 'InfixNotation

Pre :: NK 'PrefixNotation

Post :: NK 'PostfixNotation

Non :: NK 'NonfixNotation

opP :: forall e k. IsExpr e => ParseSections -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)

Parse the "operator part" of the given notation.

Normal holes (but not binders) at the beginning and end are ignored.

If the notation does not contain any binders, then a section notation is allowed.

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

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

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