Type class for pretty printing as Text.

Wraps data with parsing and semantic information.

Returns whether a Wrapper represents a parse failure.

Returns whether a Wrapper represents a semantically valid parse.

Extract data from a wrapper, returns Nothing if no data is present.

Extract text value from a wrapper, always succeeds.

Renders a short preview of a Proof as assumptions followed by its conclusion.

Type of symbolic names such as variables, predicates, rules, and operators.

A term in first-order logics consists either of a variable or a function applied to terms.

Returns whether a Term is a function application.

A formula of first-order logic. It can also represent propositional formulae by using Pred without any Terms.

A reference to either a single line or a whole subproof.

A formula with parsing and semantic information.

The raw content of an Assumption.

A wrapped assumption together with its attached RuleApplication for easily converting between Assumption and Derivation.

Constructs an Assumption with the default rule (⊤I).

Converts a Derivation into an Assumption by wrapping its formula as a RawAssumption.

Converts an Assumption into a Derivation. Fresh-variable assumptions cannot be converted to formulas and are therefore turned into Unparsed.

Application of a rule.

A derivation inside a Proof.

A datatype for representing Fitch-style proofs.

pFoldLines af df s p folds the proof p line-wise to a value of type a with starting value s.

The pLength of a Proof is its total number of lines.

Monadic variant of pFoldLines.

Serializes a Proof by mapping Assumptions, Derivations, Proofs, and conclusions. Nested proofs are first serialized recursively and then combined with the given proof function.

pSerializeLines af df p serializes the Proof p line-by-line, applying af to each Assumption and df to each Derivation, and collecting the results into a flat list.

Like pSerializeLines but also passes the current NodeAddr to each mapping function.

pMapLines af df p maps each line of the Proof p, applying af to every Assumption and df to every Derivation.

Like pMapLines, but threads an accumulator from left to right.

Like pMapLines, but also passes the current line number to the mapping functions.

Like pMapLines, but also passes the current NodeAddr to the mapping functions.

Like pMapLines but lifted to monadic results.

Like pMapLinesM but threads an accumulator from left to right.

Maps every Reference in a Proof, optionally removing references by returning Nothing.

This type is used for indexing lines in a proof. Its recursive structure makes defining functions that manipulate proofs more convenient

A NodeAddr may either be a reference to

• a single Assumption: NAAssumption n,
• the conclusion: NAConclusion of the Proof
• the spot after the conclusion: NAAfterConclusion
• a single Derivation inside the proof NALine n
• a reference to a nested element inside the Proof NAProof n (Just a)

Returns whether a NodeAddr points to an assumption of the current proof level.

Returns whether a NodeAddr points to a possibly nested Assumption.

Returns whether a NodeAddr points to a possibly nested Assumption.

Returns whether two NodeAddrs are on the same level in the same Proof.

Returns whether two ProofAddrs are on the same level in the same Proof.

Returns whether a NodeAddr is the first line in a Proof. This could be because:

• it is the first assumption;
• there are no assumptions and it is the first line;
• there are no assumptions and it is the first line of the first subproof;
• there are no assumptions, no lines, no subproofs and it is the conclusion.

Address of a Proof within a Proof.

Moves the given ProofAddr one level higher, returning a function that can be used to build ProofAddrs on the current level.

Returns the ProofAddr that contains the NodeAddr.

Takes a line number and returns the corresponding NodeAddr for a given Proof. Returns Nothing on error.

Note: NodeAddr indices start at 0, but line numbers start at 1.

Takes a NodeAddr and returns the corresponding line number for a given Proof.

Note: NodeAddr indices start at 0, but line numbers start at 1.

Like fromNodeAddr, but falls back to line number 999 if the NodeAddr is invalid.

Returns the ProofAddr of the Proof spanning from the given start line to the given end line, or Nothing if no such Proof exists.

Returns the start and end line numbers of the Proof addressed by a ProofAddr. Returns Nothing if the ProofAddr is invalid.

Increments a NodeAddr index by 1, keeping the nesting structure unchanged. Returns Nothing for addresses without a numeric index (e.g. NAConclusion).

Converts a NodeAddr to a ProofAddr, by

• Converting NALine n to PAProof n
• Converting v'NAConclusion n' to PAProof (length ps)@
• Converting NAProof n to PANested n and recursing.

For other NodeAddrs, returns Nothing.

Turns a ProofAddr into a function for building a NodeAddr that is contained in the ProofAddr.

Returns a function that lifts a nested NodeAddr by one proof level, if possible.

Counts the number of parse or validation errors occurring in a Proof.

Returns whether the element at the given index exists and satisfies a predicate.

Returns whether the element at the given NodeAddr exists and satisfies a predicate.

Returns whether the NodeAddr is a valid address for the given Proof. (Valid in the sense that naLookup would return a valid result.)

Returns the line at a given NodeAddr. Returns Nothing if the NodeAddr does not correspond to any line in the Proof.

Returns the Proof at a given ProofAddr if it exists.

Returns the Assumption or Derivation at the given line number if it exists.

Returns the Proof spanning the given start and end line numbers if it exists.

Returns whether the second NodeAddr is relevant when checking freshness for the first NodeAddr.

I.e., whether the second NodeAddr appears before the first one, or appears on the same level.

Collects all lines relevant for freshness checking of the given NodeAddr.

naUpdateFormula f addr proof replaces the Assumption or tFormula at addr in proof using f. Pass Left to update an Assumption, or Right to update the Formula of a Derivation. Returns Nothing if the address does not exist or is incompatible with the chosen update function.

naUpdateRule f addr proof updates the RuleApplication at addr in proof using f. Returns Nothing if the address does not exist or points to an Assumption (which has no editable RuleApplication).

naRemoveRaw addr proof removes the element at a valid addr from proof without updating any References.

For the NAConclusion case: if the last element of ps is a Derivation, it is promoted to become the new conclusion. Otherwise Nothing is returned.

Note: Use naRemove if references must stay consistent.

Removes the Proof at a valid ProofAddr without updating references.

Note: Use paRemove if references must stay consistent.

Removes the line at a valid NodeAddr and updates all affected references.

Removes the Proof at a valid ProofAddr and updates all affected references.

Inserts a line before the given NodeAddr in the Proof, without updating References.

• naInsertBeforeRaw (Left a) addr proof inserts the Assumption a before addr.
• naInsertBeforeRaw (Right d) addr proof inserts the Derivation d before addr.

Returns the NodeAddr of the inserted line together with the updated Proof. Returns Nothing if line could not be inserted.

Note: Use naInsertBefore if references must stay consistent.

Like naInsertBeforeRaw, but also updates references affected by the insertion.

Returns the NodeAddr of the inserted line together with the updated Proof.

Inserts a Proof before the Proof at the given ProofAddr without updating references. Returns Nothing if Proof could not be inserted.

Note: Use paInsertBefore if references must stay consistent.

Like paInsertBeforeRaw, but also updates references affected by the insertion. Returns the ProofAddr of the inserted Proof together with the updated Proof.

Moves the line at source before the line at target in Proof p, without updating any References. Returns the updated target NodeAddr together with the modified Proof or Nothing on failure.

Note: Use naMoveBefore if references must stay consistent.

Returns whether lineNo falls within the given line range, accounting for same-proof boundary rules.

Moves the line at source before the line at target in Proof p, and updates all References affected by the move. Returns Nothing if the move is rejected by naCanMoveBefore.

Returns whether a NodeAddr is contained in the Proof designated by a ProofAddr.

Note: does not check if the NodeAddr is valid!

Returns whether a ProofAddr is contained in another ProofAddr.

Note: does not check if either ProofAddr is valid!

Returns whether the target address is identical to, or immediately after, the source.

Returns whether the target address is identical to, or immediately after, the source.

Helper for deciding whether a NodeAddr may be moved to the target position defaulting to True and only does a real check for NAConclusion where it checks whether the conclusion has a Derivation that can take its place, when it moves.

Returns whether a NodeAddr can be moved before the given target NodeAddr.

Returns whether a ProofAddr can be moved before the given target ProofAddr.

Moves a Proof before another Proof without updating references.

Note: Use paMoveBefore if references must stay consistent.

Moves a Proof before another Proof and updates all affected references.