ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Concrete.Operators.Parser

3 types
1 class
11 values

PackageAgda-2.7.0.1
Exports16
LanguageHaskell2010
LicenceMIT
SourceParser.hs

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

valuemaybePlaceholder

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

datadata 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

Instances1HasRange

IsExpr e => HasRange (ExprView e)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser

classclass HasRange e => IsExpr e where

Methods

exprView :: e -> ExprView e
unExprView :: ExprView e -> e
patternView :: e -> Maybe Pattern

Instances2IsExpr

IsExpr ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser
IsExpr PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser

datadata ParseSections

Should sections be parsed?

ParseSections DoNotParseSections

Instances2Eq, Show

Eq ParseSectionsDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser
Show ParseSectionsDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser

valueparse :: 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

9 declarations

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

Parse a specific identifier as a NamePart

valueatLeastTwoParts :: 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.

valuepatternBinder :: IsExpr e => Parser e Binder

Parses a potentially pattern-matching binder

familytype family OperatorType (k :: NotationKind) e

Used to define the return type of opP.

Instances4OperatorType

type OperatorType 'InfixNotation e = MaybePlaceholder e -> MaybePlaceholder e -> eDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser
type OperatorType 'NonfixNotation e = eDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser
type OperatorType 'PostfixNotation e = MaybePlaceholder e -> eDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser
type OperatorType 'PrefixNotation e = MaybePlaceholder e -> eDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser

datadata NK (k :: NotationKind) where

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

Constructors

valueopP

:: 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.

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

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

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