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)
  • | 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
• partP :: IsExpr e => String -> ReadP e (Range, NamePart)
• binop :: IsExpr e => ReadP e e -> ReadP e (e -> e -> e)
• preop :: IsExpr e => ReadP e e -> ReadP e (e -> e)
• postop :: IsExpr e => ReadP e e -> ReadP e (e -> e)
• opP :: IsExpr e => ReadP e e -> Name -> ReadP e e
• prefixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
• postfixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
• infixrP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
• infixlP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
• infixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
• nonfixP :: IsExpr e => ReadP e 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

Parser combinators