Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 whereSource
Methods
exprView :: e -> ExprView eSource
unExprView :: ExprView e -> eSource
Parser combinators
recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok aSource
Combining a hierarchy of parsers.
chainr1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t aSource
Variant of chainr1
chainl1' :: ReadP t a -> ReadP t (a -> a -> ReadP t a) -> ReadP t aSource
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 eSource
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 LamBindingSource
($$$) :: (e -> ReadP a e) -> ReadP a e -> ReadP a eSource
infixrP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource
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 eSource
postfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource
prefixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource
nonfixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource
infixP :: IsExpr e => ReadP e (NewNotation, Range, [e]) -> ReadP e e -> ReadP e eSource
appP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e eSource
atomP :: IsExpr e => (Name -> Bool) -> ReadP e eSource
Produced by Haddock version 2.6.1