Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (GHC extensions)
Safe Haskell	None
Language	GHC2024

FOLTest

Contents

IO Helpers
Assertion Helpers
Proof Expectations
Tests

Description

HUnit tests for FOL Proofs.

Each HUnit test is a proof written in a .fitch file and then checked for (in-)correctness. There are three kinds of tests, each contained in their own folder:

Valid proofs (tests/ValidProofs/) — tests that the whole Proof is valid, i.e. everything is parsed correctly and every RuleApplication can be verified.
Invalid rules (tests/InvalidRules/) — tests that the file contains a wrongful RuleApplication. The offending line number is encoded into the filename via a %, e.g.:

tests/InvalidRules/eqE1%3.fitch

Invalid formulae (tests/InvalidFormulae/) — same as invalid rules, but checks that a formulae is invalid. This can either verify parse errors or freshness violations.

Synopsis

pathsInDir :: FilePath -> IO [FilePath]
readProof :: String -> IO Proof
assertValid :: Wrapper a -> Assertion
assertInvalid :: Wrapper a -> Assertion
expectValidProof :: Proof -> Assertion
expectInvalidRuleAt :: Int -> Proof -> Assertion
expectInvalidFormulaAt :: Int -> Proof -> Assertion
testValidProofs :: TestTree
testInvalidRules :: TestTree
testInvalidFormulae :: TestTree
verificationTests :: TestTree

IO Helpers

pathsInDir :: FilePath -> IO [FilePath] Source #

Returns the full paths of every entry inside the given directory.

Each filename returned by listDirectory is prefixed with the supplied directory path fp.

readProof :: String -> IO Proof Source #

Reads, parses, and fully verifies a FOL Proof from a file on disk.

The file is read as a ByteString and decoded as UTF-8.
The contents are parsed with parseProof.
The parsed Proof is checked with checkProof using a dummy initialModelFOL

Returns the checked Proof or fails with a parse failure.

Assertion Helpers

assertValid :: Wrapper a -> Assertion Source #

Asserts that a Wrapper value is semantically valid.

assertInvalid :: Wrapper a -> Assertion Source #

Asserts that a Wrapper value is semantically invalid.

Proof Expectations

expectValidProof :: Proof -> Assertion Source #

Traverses every line of a Proof and asserts that each formula and rule application is ParsedValid.

Uses pFoldLinesM to fold over assumptions and derivations in order:

expectInvalidRuleAt :: Int -> Proof -> Assertion Source #

Asserts that the RuleApplication at line n of a Proof is ParsedInvalid.

expectInvalidFormulaAt :: Int -> Proof -> Assertion Source #

Asserts that the Formula at line n of a tProof is ParsedInvalid.

Tests

testValidProofs :: TestTree Source #

Reads every proof file in tests/ValidProofs/ and asserts that the entire Proof is valid using 'expectValidProof.

testInvalidRules :: TestTree Source #

Reads every proof file in tests/InvalidRules/ and asserts that the RuleApplication at the line number encoded in the filename is ParsedInvalid using expectInvalidRuleAt.

testInvalidFormulae :: TestTree Source #

Reads every proof file in tests/InvalidFormulae/ and asserts that the tFormula at the line number encoded in the filename is ParsedInvalid using expectInvalidFormulaAt.

verificationTests :: TestTree Source #

TestTree for all tests related to Fitch.Verification