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

Contents

Line parsers
Proof structure parsers
Entry points

Description

This module defines parsers for Derivations and full Proofs.

Synopsis

pFormula :: FormulaParser m => m Formula
pAssumption :: FormulaParser m => m Assumption
pDerivation :: FormulaParser m => m Derivation
withIndent :: Parser m => Int -> m a -> m a
pFormulaSep :: Parser m => Int -> m ()
pProof :: FormulaParser m => Int -> m Proof
parseLine :: [(Text, Text, Int)] -> [(Text, Text)] -> [(Text, Text)] -> Text -> Either Text Derivation
parseProof :: [(Text, Text, Int)] -> [(Text, Text)] -> [(Text, Text)] -> Text -> Either Text Proof

Line parsers

pFormula :: FormulaParser m => m Formula Source #

Parses a Formula, capturing the source text and wrapping the result in ParsedValid.

pAssumption :: FormulaParser m => m Assumption Source #

Parses an Assumption, capturing the source text and wrapping the result in ParsedValid.

pDerivation :: FormulaParser m => m Derivation Source #

Parses a Derivation: a Formula followed by a RuleApplication.

Proof structure parsers

withIndent :: Parser m => Int -> m a -> m a Source #

Combinator that gates a parser behind n leading | symbols.

pFormulaSep :: Parser m => Int -> m () Source #

Parses the --- separator that divides Assumptions from Derivations in a Proof, respecting the current indentation depth.

pProof :: FormulaParser m => Int -> m Proof Source #

Parses a Proof at the given indentation depth.

The structure is:

Zero or more Assumptions, collected up to the --- separator.
One or more Derivations or nested SubProofs.
The final element must be a Derivation.

Entry points

parseLine Source #

Arguments

:: [(Text, Text, Int)]	List of operators as (alias, operator, arity).
-> [(Text, Text)]	List of infix predicates as (alias, predicate).
-> [(Text, Text)]	List of quantifiers as (alias, quantifier).
-> Text	Input `Text` to parse.
-> Either Text Derivation

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

parseProof Source #

Arguments

:: [(Text, Text, Int)]	List of operators as (alias, operator, arity).
-> [(Text, Text)]	List of infix predicates as (alias, predicate).
-> [(Text, Text)]	List of quantifiers as (alias, quantifier).
-> Text	Input `Text` to parse.
-> Either Text Proof

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