A wrapper around Proof that replaces the derived Show with PrettyPrint.

Unwraps a PrettyProof back to the underlying Proof.

Constructs a trivial Formula consisting of an Int.

Constructs a trivial Assumption consisting of an Int.

Constructs a trivial RuleApplication consisting of an Int.

Constructs a trivial Derivation using formula and rule.

Used for specifying which kind of NodeAddrs arbitraryNodeAddrFor should produce.

Constructor for setting _assumptionKind

Constructor for setting _lineKind

Constructor for setting _conclusionKind

Constructor for setting _afterConclusionKind

Constructor for setting all AddrKinds.

Constructor for setting all AddrKinds that are inside of the Proof, i.e. excluding afterConclusionKind.

Generates a valid NodeAddr of the specified AddrKind for the given Proof.

Generates a valid ProofAddr for the given Proof.

Generates a valid (start, end) line-number range within the given tProof.

Removing a lineKind or assumptionKind decreases pLength by exactly 1.

pLength <$> naRemove a p  ===  Just (pLength p - 1)

After removing the Derivation at address a, the entry that was immediately after a (at incrementNodeAddr a) is now reachable at address a.

naLookup a <$> naRemove a p === Just ((`naLookup` p) =<< incrementNodeAddr a)

After removing the Assumption at address a, the entry that was immediately after a (at incrementNodeAddr a) is now reachable at address a.

naLookup a <$> naRemove a p === Just ((`naLookup` p) =<< incrementNodeAddr a)

A wrapper around naInsertBefore that discards the returned NodeAddr and returns only the modified Proof.

Inserting an Assumption before an anyInsideKind address increases pLength by exactly 1.

pLength <$> naInsertBefore' (Left (assumption 0)) a p  ===  Just (pLength p + 1)

Inserting a Derivation before an anyInsideKind address increases pLength by exactly 1.

pLength <$> naInsertBefore' (Right (derivation 0)) a p  ===  Just (pLength p + 1)

After inserting assumption 0 before an assumptionKind address, naLookup returns assumption 0.

naLookup a <$> naInsertBefore' (Left (assumption 0)) a p ===  Just (Just (Left (assumption 0)))

After inserting derivation 0 before a lineKind address, naLookup returns derivation 0.

naLookup a <$> naInsertBefore' (Right (derivation 0)) a p ===  Just (Just (Right (derivation 0)))

Inserting an element and then removing it should return the original proof.

Moving a Proof to a new position with paMoveBeforeRaw preserves its content, i.e. looking up the source address in the original Proof yields the same Proof as looking up the destination address in the modified t'Proof.

paLookup paTarget' p'  ===  paLookup paSource p

fromLineNo followed by fromNodeAddr is the identity on valid line numbers.

(fromNodeAddr addr p =<< fromLineNo n p)  ===  Just (Just n)

fromNodeAddr followed by fromLineNo is the identity on valid tNodeAddr values.

(fromLineNo n p =<< fromNodeAddr a p)  ===  Just (Just a)

The Ord instance for NodeAddr is consistent with line-number ordering: for any two addresses a and b,

compare a b  ===  compare (fromNodeAddr a p) (fromNodeAddr b p)

lineRangeFromProofAddr followed by fromLineRange is the identity on valid ProofAddr values.

(fromLineRange s e p =<< lineRangeFromProofAddr pa p)  ===  Just pa

fromLineRange followed by lineRangeFromProofAddr is the identity on valid (start, end) line ranges.

(lineRangeFromProofAddr pa p =<< fromLineRange start end p) ===  Just (start, end)

Tests for naRemove

Tests for naInsertBefore

Tests for paMoveBefore

Tests regarding the conversion of line numbers and NodeAddrs.

Tests for compare instances of address types like NodeAddr and t'ProofAddr.

Tests regarding the conversion of line ranges and ProofAddrs.

Groups all tests in this module.