Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Concrete.Operators.Parser

Contents

Parser combinators

Synopsis

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
- = LocalV QName
- | WildV e
- | OtherV e
- | AppV e (NamedArg e)
- | OpAppV QName (Set Name) (OpAppArgs' e)
- | HiddenArgV (Named_ e)
- | InstanceArgV (Named_ e)
- | LamV (List1 LamBinding) e
- | ParenV e
class HasRange e => IsExpr e where
- exprView :: e -> ExprView e
- unExprView :: ExprView e -> e
- patternView :: e -> Maybe Pattern
data ParseSections
- = ParseSections
- | DoNotParseSections
parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
partP :: IsExpr e => [Name] -> RawName -> Parser e Range
atLeastTwoParts :: IsExpr e => Parser e Name
patternBinder :: IsExpr e => Parser e Binder
type family OperatorType (k :: NotationKind) e
data NK (k :: NotationKind) where
- In :: NK 'InfixNotation
- Pre :: NK 'PrefixNotation
- Post :: NK 'PostfixNotation
- Non :: NK 'NonfixNotation
opP :: forall e (k :: NotationKind). IsExpr e => ParseSections -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
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

Documentation

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

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

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

data ExprView e Source #

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

Instances details

IsExpr e => HasRange (ExprView e) Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods getRange :: ExprView e -> Range Source #

class HasRange e => IsExpr e where Source #

Methods

exprView :: e -> ExprView e Source #

unExprView :: ExprView e -> e Source #

patternView :: e -> Maybe Pattern Source #

Instances

Instances details

IsExpr Expr Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Expr -> ExprView Expr Source # unExprView :: ExprView Expr -> Expr Source # patternView :: Expr -> Maybe Pattern Source #
IsExpr Pattern Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods exprView :: Pattern -> ExprView Pattern Source # unExprView :: ExprView Pattern -> Pattern Source # patternView :: Pattern -> Maybe Pattern Source #

data ParseSections Source #

Should sections be parsed?

Constructors

ParseSections
DoNotParseSections

Instances

Instances details

Show ParseSections Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods showsPrec :: Int -> ParseSections -> ShowS show :: ParseSections -> String showList :: [ParseSections] -> ShowS
Eq ParseSections Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser Methods (==) :: ParseSections -> ParseSections -> Bool (/=) :: ParseSections -> ParseSections -> Bool

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

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 Source #

Parse a specific identifier as a NamePart

atLeastTwoParts :: IsExpr e => Parser e Name Source #

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 Source #

Parses a potentially pattern-matching binder

type family OperatorType (k :: NotationKind) e Source #

Used to define the return type of opP.

Instances

Instances details

type OperatorType 'InfixNotation e Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser type OperatorType 'InfixNotation e = MaybePlaceholder e -> MaybePlaceholder e -> e
type OperatorType 'NonfixNotation e Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser type OperatorType 'NonfixNotation e = e
type OperatorType 'PostfixNotation e Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser type OperatorType 'PostfixNotation e = MaybePlaceholder e -> e
type OperatorType 'PrefixNotation e Source #
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser type OperatorType 'PrefixNotation e = MaybePlaceholder e -> e

data NK (k :: NotationKind) where Source #

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 :: NotationKind). IsExpr e => ParseSections -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e) Source #

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] Source #

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

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