Agda.Syntax.Concrete.Operators.Parser

Contents

• Parser combinators

Synopsis

• data MemoKey
  • = NodeK (Either Integer Integer)
  • | PostLeftsK (Either Integer Integer)
  • | TopK
  • | AppK
  • | NonfixK
• type Parser tok a = Parser MemoKey tok (MaybePlaceholder tok) a
• placeholder :: Placeholder -> Parser e (MaybePlaceholder e)
• maybePlaceholder :: Maybe Placeholder -> Parser e e -> Parser e (MaybePlaceholder e)
• notPlaceholder :: Parser e e
• sat' :: (e -> Bool) -> Parser e e
• data ExprView e
  • = LocalV QName
  • | WildV e
  • | OtherV e
  • | AppV e (NamedArg e)
  • | OpAppV QName (Set Name) [NamedArg (MaybePlaceholder (OpApp e))]
  • | HiddenArgV (Named_ e)
  • | InstanceArgV (Named_ e)
  • | LamV [LamBinding] e
  • | ParenV e
• class HasRange e => IsExpr e where
  • exprView :: e -> ExprView e
  • unExprView :: ExprView e -> e
• data ParseSections
  • = ParseSections
  • | DoNotParseSections
• parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a]
• partP :: IsExpr e => [Name] -> RawName -> Parser e Range
• type family OperatorType k e :: *
• data NK k :: * where
  • In :: NK InfixNotation
  • Pre :: NK PrefixNotation
  • Post :: NK PostfixNotation
  • Non :: NK NonfixNotation
• opP :: forall e k. IsExpr e => ParseSections -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e)
• argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e]
• appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e
• atomP :: IsExpr e => (QName -> Bool) -> Parser e e

Documentation

Parser combinators