Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 :: List2 Expr -> ScopeM Expr Source #

Parse a list of expressions (typically from a RawApp) 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 :: QName -> Pattern -> ScopeM LHSCore Source #

Parses a left-hand side, and makes sure that it defined the expected name.

parsePattern :: Pattern -> ScopeM Pattern Source #

Parses a pattern.