Agda.Syntax.Concrete.Operators

The parser doesn't know about operators and parses everything as normal function application. This module contains the functions that parses the operators properly. For a stand-alone implementation of this see src/prototyping/mixfix/old.

It also contains the function that puts parenthesis back given the precedence of the context.

Documentation

parseApplication :: [Expr] -> ScopeM Expr

Parse a list of expressions into an application.

parseLHS :: Name -> Pattern -> ScopeM LHSCore

Parses a left-hand side, and makes sure that it defined the expected name. TODO: check the arities of constructors. There is a possible ambiguity with postfix constructors: Assume _ * is a constructor. Then 'true *' can be parsed as either the intended _* applied to true, or as true applied to a variable *. If we check arities this problem won't appear.

parsePattern :: Pattern -> ScopeM Pattern

Parses a pattern. TODO: check the arities of constructors. There is a possible ambiguity with postfix constructors: Assume _ * is a constructor. Then 'true *' can be parsed as either the intended _* applied to true, or as true applied to a variable *. If we check arities this problem won't appear.

parsePatternSyn :: Pattern -> ScopeM Pattern

paren :: Monad m => (QName -> m Fixity) -> Expr -> m (Precedence -> Expr)

mparen :: Bool -> Expr -> Expr

validConPattern :: [QName] -> Pattern -> Bool

Helper function for parseLHS and parsePattern.

patternAppView :: Pattern -> [NamedArg Pattern]

View a pattern p as a list p0 .. pn where p0 is the identifier (in most cases a constructor).

Pattern needs to be parsed already (operators resolved).

fullParen :: IsExpr e => e -> e

buildParser :: forall e. IsExpr e => Range -> FlatScope -> UseBoundNames -> ScopeM (ReadP e e)

parsePat :: ReadP Pattern Pattern -> Pattern -> [Pattern]

Returns the list of possible parses.

getDefinedNames :: [KindOfName] -> FlatScope -> [(QName, Fixity')]

Compute all unqualified defined names in scope and their fixities.

data UseBoundNames

Constructors

UseBoundNames

DontUseBoundNames

qualifierModules :: [QName] -> [[Name]]

Return all qualifiers occuring in a list of QNames. Each qualifier is returned as a list of names, e.g. for Data.Nat._+_ we return the list [Data,Nat].

patternQNames :: Pattern -> [QName]

Collect all names in a pattern into a list of qualified names.