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

Contents

Serialization
Parsers
Entry point

Description

This module defines a compact serialization format for Proofs using ASCII control characters, and a corresponding parser for deserialization. This format is used for encoding Proofs in URLs via tURLDecoder.

In contrast to Parser.Proof this can also parse incomplete Proofs, i.e. ones with parse errors.

Synopsis

safeParsePrint :: Proof -> Text
pIncompleteDerivation :: Parser m => m Derivation
pIncompleteAssumption :: Parser m => m Assumption
pIncompleteProof :: Parser m => m Proof
parseIncompleteProof :: Text -> Maybe Proof

Serialization

safeParsePrint :: Proof -> Text Source #

Serializes a Proof to a compact Text representation using ASCII control characters as delimiters, suitable for later re-parsing with parseIncompleteProof.

Legend of control characters:

\31 separates a Formula from its RuleApplication
\30 separates individual lines from each other
\29 encloses groups: the Assumption list, the Derivation or Proof list, and the conclusion
\28 encloses an entire Proof

Parsers

pIncompleteDerivation :: Parser m => m Derivation Source #

Parses a single Derivation from the serialization format produced by safeParsePrint. The Formula and RuleApplication fields are left as Unparsed wrappers and are re-parsed later by the application.

pIncompleteAssumption :: Parser m => m Assumption Source #

Parses a single Assumption from the serialization format produced by safeParsePrint. Both the Formula and RuleApplication fields are left as Unparsed wrappers and are re-parsed later by the application.

pIncompleteProof :: Parser m => m Proof Source #

Parses a full Proof from the serialization format produced by safeParsePrint.

Entry point

parseIncompleteProof :: Text -> Maybe Proof Source #

Deserializes a Proof from a Text produced by safeParsePrint. Returns Nothing if parsing fails.