| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
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
- parseApplication :: List2 Expr -> ScopeM Expr
- parseArguments :: Expr -> [Expr] -> ScopeM [NamedArg Expr]
- parseLHS :: DisplayLHS -> QName -> Pattern -> ScopeM LHSCore
- parsePattern :: Pattern -> ScopeM Pattern
- parsePatternSyn :: Pattern -> ScopeM Pattern
Documentation
parseApplication :: List2 Expr -> ScopeM Expr Source #
Parse a list of expressions (typically from a RawApp) into an application.
Parse the arguments of a raw application with known head.
Arguments
| :: DisplayLHS | Are we parsing a |
| -> QName | Name of the definition. |
| -> Pattern | Full left hand side. |
| -> ScopeM LHSCore |
Parses a left-hand side, and makes sure that it defined the expected name.