| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Expr | Source

parseLHS :: Maybe Name -> Pattern -> ScopeM Pattern | Source

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 -> Expr | Source

Produced by Haddock version 2.4.2