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.Formula

Contents

Parser state
Term parsers
Formula parsers
Assumption parsers
Entry points

Description

This module defines parsers for RawFormulas, Terms and RawAssumptions.

Synopsis

data FormulaParserState = FormulaParserState {
- operators :: [(Text, Text, Int)]
- infixPreds :: [(Text, Text)]
- quantifiers :: [(Text, Text)]
}
type FormulaParser (m :: Type -> Type) = (MonadParsec Void Text m, MonadState FormulaParserState m)
pFun :: FormulaParser m => m Term
pVar :: FormulaParser m => m Term
pTerm :: FormulaParser m => m Term
pPredicate :: FormulaParser m => m RawFormula
pQuantifierName :: FormulaParser m => m Name
pConstant :: FormulaParser m => m RawFormula
pQuantifier :: FormulaParser m => m RawFormula
pInfixPredName :: FormulaParser m => m Name
pInfixPred :: FormulaParser m => m RawFormula
pFormulaAtomic :: FormulaParser m => m RawFormula
pRawFormula :: FormulaParser m => m RawFormula
pFreshVariable :: FormulaParser m => m RawAssumption
pRawAssumption :: FormulaParser m => m RawAssumption
initialParserState :: Int -> Text -> State Text e
parseFormula :: FormulaParserState -> Int -> Text -> Either Text RawFormula
parseAssumption :: FormulaParserState -> Int -> Text -> Either Text RawAssumption

Parser state

data FormulaParserState Source #

State for a Formula parser.

Constructors

FormulaParserState
Fields operators :: [(Text, Text, Int)] List of operators as (alias, operator, arity). infixPreds :: [(Text, Text)] List of infix predicates as (alias, predicate). quantifiers :: [(Text, Text)] List of quantifiers as (alias, quantifier).

type FormulaParser (m :: Type -> Type) = (MonadParsec Void Text m, MonadState FormulaParserState m) Source #

Constraint alias combining a Parser with a MonadState over FormulaParserState.

Term parsers

pFun :: FormulaParser m => m Term Source #

Parses a function application: a lowercase name followed by a parenthesised, comma-separated argument list, e.g. f(x, y).

Note: the parser cannot distinguish between function constants and variables. This does not matter for this application — constants are treated as variables.

pVar :: FormulaParser m => m Term Source #

Parses a variable: a single lowercase name.

pTerm :: FormulaParser m => m Term Source #

Parses a Term: tries pFun first, then falls back to pVar.

Formula parsers

pPredicate :: FormulaParser m => m RawFormula Source #

Parses a predicate: an uppercase name followed by an optional parenthesised argument list. Thus also capturing propositional atoms.

pQuantifierName :: FormulaParser m => m Name Source #

Parses a quantifier name from the current FormulaParserState, accepting both the actual symbol and the alias.

pConstant :: FormulaParser m => m RawFormula Source #

Parses a constant, i.e. a nullary Opr like ⊥ from the current FormulaParserState.

pQuantifier :: FormulaParser m => m RawFormula Source #

Parses a quantified RawFormula of the form quantifier variable . formula.

pInfixPredName :: FormulaParser m => m Name Source #

Parses an infix predicate name from the current FormulaParserState, accepting both the actual symbol and the alias.

pInfixPred :: FormulaParser m => m RawFormula Source #

Parses an infix predicate of the form term predicate term, e.g. x = y.

pFormulaAtomic :: FormulaParser m => m RawFormula Source #

Parses an atomic RawFormula: a quantifier, infix predicate, parenthesised formula, constant, or predicate.

pRawFormula :: FormulaParser m => m RawFormula Source #

Parses a full RawFormula, using makeExprParser to handle operator precedence and associativity.

Assumption parsers

pFreshVariable :: FormulaParser m => m RawAssumption Source #

Parses a fresh-variable marker: a lowercase name enclosed in square brackets, e.g. [x].

pRawAssumption :: FormulaParser m => m RawAssumption Source #

Parses a RawAssumption: either a fresh-variable marker or a plain RawFormula.

Entry points

initialParserState Source #

Arguments

:: Int	Line number at which parsing begins.
-> Text	Input `Text` to parse.
-> State Text e

Constructs an initial Megaparsec State positioned at the given line number, so that parse errors report the correct source location.

parseFormula Source #

Arguments

:: FormulaParserState	Initial parser state.
-> Int	Line number.
-> Text	Input `Text` to parse.
-> Either Text RawFormula

Parses a RawFormula from a Text. Returns Left with a human-readable error message on failure, or Right with the parsed RawFormula on success.

parseAssumption Source #

Arguments

:: FormulaParserState	Initial parser state.
-> Int	Line number.
-> Text	Input `Text` to parse.
-> Either Text RawAssumption

Parses a RawAssumption from a Text. Returns Left with a human-readable error message on failure, or Right with the parsed RawAssumption on success.