Agda.Syntax.Concrete.Operators.Parser

Contents

Parser combinators

Synopsis

data ExprView e

= LocalV Name

| OtherV e

| AppV e (NamedArg e)

| OpAppV Name [e]

| HiddenArgV (Named String e)

| LamV [LamBinding] e

| ParenV e

class HasRange e => IsExpr e where

exprView :: e -> ExprView e

unExprView :: ExprView e -> e

recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok a

chainr1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t a

chainl1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t a

partP :: IsExpr e => String -> ReadP e (Range, NamePart)

binop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> e -> ReadP a e)

postop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)

preop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)

opP :: IsExpr e => ReadP e e -> NewNotation -> ReadP e (NewNotation, Range, [e])

rebuild :: forall a e. IsExpr e => NewNotation -> Range -> [e] -> ReadP a e

rebuildBinding :: ExprView e -> ReadP a LamBinding

($$$) :: (e -> ReadP a e) -> ReadP a e -> ReadP a e

infixrP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

infixlP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

postfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

prefixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

nonfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

infixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

appP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e

atomP :: IsExpr e => (Name -> Bool) -> ReadP e e

Documentation

data ExprView e

Source

Constructors

LocalV Name
OtherV e
AppV e (NamedArg e)
OpAppV Name [e]
HiddenArgV (Named String e)
LamV [LamBinding] e
ParenV e

class HasRange e => IsExpr e where

Source

Methods

exprView :: e -> ExprView e

Source

unExprView :: ExprView e -> e

Source

Parser combinators

recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok a

Source

Combining a hierarchy of parsers.

chainr1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t a

Source

Variant of chainr1

chainl1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t a

Source

Variant of chainl1

partP :: IsExpr e => String -> ReadP e (Range, NamePart)

Source

Parse a specific identifier as a NamePart

binop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> e -> ReadP a e)

Source

postop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)

Source

preop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)

Source

opP :: IsExpr e => ReadP e e -> NewNotation -> ReadP e (NewNotation, Range, [e])

Source

Parse the operator part of the given syntax. holes at beginning and end are IGNORED.

rebuild :: forall a e. IsExpr e => NewNotation -> Range -> [e] -> ReadP a e

Source

Given a name with a syntax spec, and a list of parsed expressions fitting it, rebuild the expression. Note that this function must not parse any input (as guaranteed by the type)

rebuildBinding :: ExprView e -> ReadP a LamBinding

Source

($$$) :: (e -> ReadP a e) -> ReadP a e -> ReadP a e

Source

infixrP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

Parse using the appropriate fixity, given a parser parsing the operator part, the name of the operator, and a parser of subexpressions.

infixlP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

postfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

prefixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

nonfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

infixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e

Source

appP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e

Source

atomP :: IsExpr e => (Name -> Bool) -> ReadP e e

Source

Produced by Haddock version 2.6.1