Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

Parser.Util

Contents

Description

This module provides shared utility parsers used across all other Parser.* modules.

Synopsis

type Parser = MonadParsec Void Text
sc :: MonadParsec Void Text m => m ()
lexeme :: Parser m => m a -> m a
symbol :: Parser m => Text -> m Text
matchNoSpaces :: Parser m => m a -> m (Text, a)
pUpperName :: Parser m => m Text
pLowerName :: Parser m => m Text
pSymbolicName :: Parser m => m Text
pText :: Parser m => m Text
comma :: Parser m => m Text
minus :: Parser m => m Text
parens :: Parser m => m a -> m a
brackets :: Parser m => m a -> m a
binary :: forall (m :: Type -> Type) a. Parser m => Text -> (a -> a -> a) -> Operator m a
prefix :: forall (m :: Type -> Type) a. Parser m => Text -> (a -> a) -> Operator m a

Types

Constraint alias for a Megaparsec parser over a Text stream with no custom error type.

Lexer

Space consumer that only skips whitespace

lexeme :: Parser m => m a -> m a Source #

Wraps a parser so that it consumes trailing whitespace via sc.

Parses the exact given Text token and consumes any trailing whitespace.

Runs a Parser via match but strips whitespace from the resulting Text.

Parses a name that starts with one or more uppercase letters, followed by zero or more letters. Used for predicate symbols.

Parses a name that starts with one or more lowercase letters, followed by zero or more letters. Used for function symbols and variables.

Parses a symbolic name, i.e. any non-empty sequence of characters that are neither ( nor ). Used for parsing rule applications.

Parses arbitrary characters, excluding the control characters \28, \29, \30, and \31 that are used as separators in tIncompleteProof.

Parses a comma ,.

Parses a minus sign -.

parens :: Parser m => m a -> m a Source #

Wraps a parser between ( and ).

brackets :: Parser m => m a -> m a Source #

Wraps a parser between [ and ].

binary :: forall (m :: Type -> Type) a. Parser m => Text -> (a -> a -> a) -> Operator m a Source #

Creates a left-associative infix operator for use with makeExprParser.

prefix :: forall (m :: Type -> Type) a. Parser m => Text -> (a -> a) -> Operator m a Source #

Creates a prefix operator for use with makeExprParser. Defined specifically so that multiple prefix symbols can get parsed without parentheses.