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

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.

parseArguments Source #

Arguments

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

Parse the arguments of a raw application with known head.

parseLHS Source #

Arguments

:: 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.

parsePattern :: Pattern -> ScopeM Pattern Source #

Parses a pattern.

parsePatternSyn :: Pattern -> ScopeM Pattern Source #