ModuleAgda-2.8.0.2Haskell2010

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.

5 values

PackageAgda-2.8.0.2
Exports5
LanguageHaskell2010
LicenceMIT
SourceOperators.hs

valueparseApplication :: List2 Expr -> ScopeM Expr

Parse a list of expressions (typically from a RawApp) into an application.

valueparseArguments

:: Expr
Head
-> [Expr]
Raw arguments
-> ScopeM [NamedArg Expr]
Operator-parsed arguments

Parse the arguments of a raw application with known head.

valueparseLHS

:: DisplayLHS
Are we parsing a DisplayPragma?
-> 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.

valueparsePattern :: Pattern -> ScopeM Pattern

Parses a pattern.

valueparsePatternSyn :: Pattern -> ScopeM Pattern