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

Safe Haskell | None

Agda.Syntax.Concrete.Operators.Parser

Contents

- Parser combinators

Synopsis

- data ExprView e
  - = LocalV QName
  - | WildV e
  - | OtherV e
  - | AppV e (NamedArg e)
  - | OpAppV QName [OpApp e]
  - | HiddenArgV (Named String e)
  - | InstanceArgV (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 => [Name] -> String -> ReadP e Range
- binop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> e -> ReadP a e)
- preop :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e (e -> ReadP a e)
- postop :: 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 symbol e. IsExpr e => NewNotation -> Range -> [e] -> ReadP symbol e
- rebuildBinding :: ExprView e -> ReadP a LamBinding
- ($$$) :: (e -> ReadP a e) -> ReadP a e -> ReadP a e
- infixP :: 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
- prefixP :: 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
- infixlP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e e
- infixrP :: 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 => (QName -> Bool) -> ReadP e e

# Documentation

data ExprView e

Constructors

LocalV QName |
WildV e |
OtherV e |
AppV e (NamedArg e) |
OpAppV QName [OpApp e] |
HiddenArgV (Named String e) |
InstanceArgV (Named String e) |
LamV [LamBinding] e |
ParenV e |

class HasRange e => IsExpr e where

Methods

exprView :: e -> ExprView e

unExprView :: ExprView e -> e

Instances

IsExpr Pattern |
IsExpr Expr |

# Parser combinators

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

Combining a hierarchy of parsers.

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

Variant of chainr1

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

Variant of chainl1

partP :: IsExpr e => [Name] -> String -> ReadP e Range

Parse a specific identifier as a NamePart

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

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

postop :: 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])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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