Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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.

It also contains the function that puts parenthesis back given the precedence of the context.

Synopsis
parseApplication :: [Expr] -> ScopeM Expr
parseLHS :: Maybe Name -> Pattern -> ScopeM Pattern
paren :: Monad m => (Name -> m Fixity) -> Expr -> m (Precedence -> Expr)
mparen :: Bool -> Expr -> Expr
Documentation
parseApplication :: [Expr] -> ScopeM ExprSource
parseLHS :: Maybe Name -> Pattern -> ScopeM PatternSource
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.
paren :: Monad m => (Name -> m Fixity) -> Expr -> m (Precedence -> Expr)Source
mparen :: Bool -> Expr -> ExprSource
Produced by Haddock version 2.6.0