Agda-2.4.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone

Agda.Syntax.Concrete.Operators

Description

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.

Synopsis

Documentation

parseApplication :: [Expr] -> ScopeM ExprSource

Parse a list of expressions into an application.

parseModuleApplication :: Expr -> ScopeM (QName, [NamedArg Expr])Source

Parse an expression into a module application (an identifier plus a list of arguments).

parseLHS :: Name -> Pattern -> ScopeM LHSCoreSource

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 PatternSource

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.

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

mparen :: Bool -> Expr -> ExprSource

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

Helper function for parseLHS and parsePattern.

patternAppView :: Pattern -> [NamedArg Pattern]Source

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 -> eSource

buildParsers :: forall e. IsExpr e => Range -> FlatScope -> UseBoundNames -> ScopeM (Parsers e)Source

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

For backwards compatibility. Returns the pTop from buildParsers.

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

Returns the list of possible parses.

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

Compute all unqualified defined names in scope and their fixities.

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

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

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