ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Concrete.Operators.Parser
Contents
Synopsis
- value placeholder
- value maybePlaceholder
- value satNoPlaceholder
- data ExprView
- class IsExpr
- data ParseSections
- value parse
- value partP
- value atLeastTwoParts
- value patternBinder
- family OperatorType
- data NK
- value opP
- value argsP
- value appP
- value atomP
- PackageAgda-2.8.0.2
- Exports16
- LanguageHaskell2010
- LicenceMIT
- SourceParser.hs
Constructors
LocalV QNameWildV eOtherV eAppV e (NamedArg e)OpAppV QName (Set1 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) eParenV e
Methods
exprView :: e -> ExprView eunExprView :: ExprView e -> epatternView :: e -> Maybe Pattern
Should sections be parsed?
Instances2Eq, Show
Eq ParseSectionsDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.ParserShow ParseSectionsDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parser
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
Parse a specific identifier as a NamePart
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.
Parses a potentially pattern-matching binder
Used to define the return type of opP.
Instances4OperatorType
type OperatorType 'InfixNotation e = MaybePlaceholder e -> MaybePlaceholder e -> eDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parsertype OperatorType 'NonfixNotation e = eDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parsertype OperatorType 'PostfixNotation e = MaybePlaceholder e -> eDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parsertype OperatorType 'PrefixNotation e = MaybePlaceholder e -> eDefined in Agda-2.8.0.2 · Agda.Syntax.Concrete.Operators.Parser
A singleton type for NotationKind (except for the constructor NoNotation).
Constructors
In :: NK 'InfixNotationPre :: NK 'PrefixNotationPost :: NK 'PostfixNotationNon :: NK 'NonfixNotation
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.