{-# LANGUAGE MultilineStrings #-}

{- |
Module      : FOLTest
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (GHC extensions)

HUnit tests for FOL t'Proof's.

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 t'Proof' is valid, i.e.
everything is parsed correctly and every t'RuleApplication' can be verified.
* __Invalid rules__ (@tests\/InvalidRules\/@) — tests that the file contains
a wrongful t'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.
-}
module FOLTest where

import App.Model
import App.Update
import Fitch.Proof
import Fitch.Verification (verifyProof)
import Miso.Router (URI (..))
import Parser.Formula (parseFormula)
import Parser.Proof (parseProof)
import Specification.FOL
import System.Directory (listDirectory)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit

import Miso.Lens ((^.))

------------------------------------------------------------------------------------------

-- * IO Helpers

{- | Returns the full paths of every entry inside the given directory.

Each filename returned by 'listDirectory' is prefixed with the supplied
directory path @fp@.
-}
pathsInDir :: FilePath -> IO [FilePath]
pathsInDir :: FilePath -> IO [FilePath]
pathsInDir FilePath
fp = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath
fp FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<>) ([FilePath] -> [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO [FilePath]
listDirectory FilePath
fp

{- | Reads, parses, and fully verifies a FOL t'Proof' from a file on disk.

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

Returns the checked t'Proof' or fails with a parse failure.
-}
readProof :: String -> IO Proof
readProof :: FilePath -> IO Proof
readProof FilePath
filePath = do
  contents <- FilePath -> IO ByteString
forall (m :: * -> *). MonadIO m => FilePath -> m ByteString
readFileBS FilePath
filePath
  case parseProof operatorsFOL infixPredsFOL quantifiersFOL (decodeUtf8 contents) of
    Left Text
err ->
      FilePath -> IO Proof
forall a. HasCallStack => FilePath -> IO a
assertFailure (FilePath -> IO Proof) -> (Text -> FilePath) -> Text -> IO Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
forall a. ToString a => a -> FilePath
toString (Text -> IO Proof) -> Text -> IO Proof
forall a b. (a -> b) -> a -> b
$
        Text
"Could not parse file " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err
    Right Proof
p ->
      Proof -> IO Proof
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> IO Proof) -> (Model -> Proof) -> Model -> IO Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Model -> Lens Model Proof -> Proof
forall record field. record -> Lens record field -> field
^. Lens Model Proof
proof) (Model -> IO Proof) -> Model -> IO Proof
forall a b. (a -> b) -> a -> b
$
        State Model () -> Model -> Model
forall s a. State s a -> s -> s
execState
          State Model ()
forall (m :: * -> *). MonadState Model m => m ()
checkProof
          (URI -> Maybe Proof -> Maybe Bool -> Bool -> Model
initialModelFOL (Text -> Text -> Map Text (Maybe Text) -> URI
URI Text
"" Text
"" Map Text (Maybe Text)
forall a. Monoid a => a
mempty) (Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p) Maybe Bool
forall a. Maybe a
Nothing Bool
False)

------------------------------------------------------------------------------------------

-- * Assertion Helpers

-- | Asserts that a t'Wrapper' value is semantically valid.
assertValid :: Wrapper a -> Assertion
assertValid :: forall a. Wrapper a -> Assertion
assertValid (Unparsed Text
_ Text
err) =
  FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure (FilePath -> Assertion) -> (Text -> FilePath) -> Text -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
forall a. ToString a => a -> FilePath
toString (Text -> Assertion) -> Text -> Assertion
forall a b. (a -> b) -> a -> b
$
    Text
"Parse error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err
assertValid (ParsedInvalid Text
_ Text
err a
_) =
  FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure (FilePath -> Assertion) -> (Text -> FilePath) -> Text -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
forall a. ToString a => a -> FilePath
toString (Text -> Assertion) -> Text -> Assertion
forall a b. (a -> b) -> a -> b
$
    Text
"Error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err
assertValid Wrapper a
_ = Assertion
forall (f :: * -> *). Applicative f => f ()
pass

-- | Asserts that a t'Wrapper' value is semantically invalid.
assertInvalid :: Wrapper a -> Assertion
assertInvalid :: forall a. Wrapper a -> Assertion
assertInvalid (Unparsed Text
_ Text
err) =
  FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure (FilePath -> Assertion) -> (Text -> FilePath) -> Text -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
forall a. ToString a => a -> FilePath
toString (Text -> Assertion) -> Text -> Assertion
forall a b. (a -> b) -> a -> b
$
    Text
"Parse error: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err
assertInvalid f :: Wrapper a
f@(ParsedValid Text
txt a
_) =
  FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure (FilePath -> Assertion) -> (Text -> FilePath) -> Text -> Assertion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
forall a. ToString a => a -> FilePath
toString (Text -> Assertion) -> Text -> Assertion
forall a b. (a -> b) -> a -> b
$
    Text
"Expected invalid, but found valid: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
txt
assertInvalid Wrapper a
_ = Assertion
forall (f :: * -> *). Applicative f => f ()
pass

------------------------------------------------------------------------------------------

-- * Proof Expectations

{- | Traverses every line of a t'Proof' and asserts that each formula and
rule application is 'ParsedValid'.

Uses 'pFoldLinesM' to fold over assumptions and derivations in order:
-}
expectValidProof :: Proof -> Assertion
expectValidProof :: Proof -> Assertion
expectValidProof =
  (() -> Assumption -> Assertion)
-> (() -> Derivation -> Assertion) -> () -> Proof -> Assertion
forall (m :: * -> *) a.
Monad m =>
(a -> Assumption -> m a)
-> (a -> Derivation -> m a) -> a -> Proof -> m a
pFoldLinesM
    (\()
_ (Wrapper RawAssumption
a, Wrapper RuleApplication
_) -> Wrapper RawAssumption -> Assertion
forall a. Wrapper a -> Assertion
assertValid Wrapper RawAssumption
a)
    (\()
_ (Derivation Formula
f Wrapper RuleApplication
r) -> Formula -> Assertion
forall a. Wrapper a -> Assertion
assertValid Formula
f Assertion -> Assertion -> Assertion
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Wrapper RuleApplication -> Assertion
forall a. Wrapper a -> Assertion
assertValid Wrapper RuleApplication
r)
    ()

{- | Asserts that the t'RuleApplication' at line @n@ of a t'Proof' is
'ParsedInvalid'.
-}
expectInvalidRuleAt :: Int -> Proof -> Assertion
expectInvalidRuleAt :: Int -> Proof -> Assertion
expectInvalidRuleAt Int
n Proof
p = case Int -> Proof -> Maybe (Either Assumption Derivation)
pIndex Int
n Proof
p of
  Just (Right (Derivation Formula
_ Wrapper RuleApplication
r)) -> Wrapper RuleApplication -> Assertion
forall a. Wrapper a -> Assertion
assertInvalid Wrapper RuleApplication
r
  Maybe (Either Assumption Derivation)
_ -> FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure FilePath
"expectInvalidRuleAt: pIndex failed or found unexpected assumption!"

{- | Asserts that the t'Formula' at line @n@ of a
t'Proof' is 'ParsedInvalid'.
-}
expectInvalidFormulaAt :: Int -> Proof -> Assertion
expectInvalidFormulaAt :: Int -> Proof -> Assertion
expectInvalidFormulaAt Int
n Proof
p = case Int -> Proof -> Maybe (Either Assumption Derivation)
pIndex Int
n Proof
p of
  Just (Right (Derivation Formula
f Wrapper RuleApplication
_)) -> Formula -> Assertion
forall a. Wrapper a -> Assertion
assertInvalid Formula
f
  Just (Left (Wrapper RawAssumption
a, Wrapper RuleApplication
_)) -> Wrapper RawAssumption -> Assertion
forall a. Wrapper a -> Assertion
assertInvalid Wrapper RawAssumption
a
  Maybe (Either Assumption Derivation)
_ -> FilePath -> Assertion
forall a. HasCallStack => FilePath -> IO a
assertFailure FilePath
"expectInvalidFormulaAt: internal error, pIndex failed!"

------------------------------------------------------------------------------------------

-- * Tests

{- | Reads every proof file in @tests\/ValidProofs\/@ and asserts that the
entire t'Proof' is valid using 'expectValidProof.
-}
testValidProofs :: TestTree
testValidProofs :: TestTree
testValidProofs =
  FilePath -> ((FilePath -> Assertion) -> Assertion) -> TestTree
testCaseSteps FilePath
"Testing valid proofs" (((FilePath -> Assertion) -> Assertion) -> TestTree)
-> ((FilePath -> Assertion) -> Assertion) -> TestTree
forall a b. (a -> b) -> a -> b
$ \FilePath -> Assertion
step ->
    (FilePath -> Assertion) -> [FilePath] -> Assertion
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
      ( (\FilePath
str -> FilePath -> Assertion
step FilePath
str Assertion -> IO FilePath -> IO FilePath
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
str)
          (FilePath -> IO FilePath)
-> (FilePath -> Assertion) -> FilePath -> Assertion
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> FilePath -> IO Proof
readProof
          (FilePath -> IO Proof)
-> (Proof -> Assertion) -> FilePath -> Assertion
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Proof -> Assertion
expectValidProof
      )
      ([FilePath] -> Assertion) -> IO [FilePath] -> Assertion
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO [FilePath]
pathsInDir FilePath
"tests/ValidProofs/"

{- | Reads every proof file in @tests\/InvalidRules\/@ and asserts that the
  t'RuleApplication' at the line number encoded in the filename is v'ParsedInvalid'
using 'expectInvalidRuleAt'.
-}
testInvalidRules :: TestTree
testInvalidRules :: TestTree
testInvalidRules =
  FilePath -> ((FilePath -> Assertion) -> Assertion) -> TestTree
testCaseSteps FilePath
"Testing invalid proofs" (((FilePath -> Assertion) -> Assertion) -> TestTree)
-> ((FilePath -> Assertion) -> Assertion) -> TestTree
forall a b. (a -> b) -> a -> b
$ \FilePath -> Assertion
step ->
    (FilePath -> Assertion) -> [FilePath] -> Assertion
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
      ( \FilePath
str ->
          do
            let rem :: FilePath
rem = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') FilePath
str
                lineNo :: FilePath
lineNo = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') FilePath
rem
            FilePath -> Assertion
step (FilePath
str FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" at line " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
lineNo) Assertion -> IO (FilePath, FilePath) -> IO (FilePath, FilePath)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (FilePath, FilePath) -> IO (FilePath, FilePath)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath
str, FilePath
lineNo)
            p <- FilePath -> IO Proof
readProof FilePath
str
            no :: Int <- case reads lineNo of
              [] -> FilePath -> IO Int
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO Int) -> FilePath -> IO Int
forall a b. (a -> b) -> a -> b
$ FilePath
"'reads' failed extracting a number from lineNo=" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
lineNo
              (Int
n, FilePath
_) : [(Int, FilePath)]
_ -> Int -> IO Int
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n
            expectInvalidRuleAt no p
      )
      ([FilePath] -> Assertion) -> IO [FilePath] -> Assertion
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO [FilePath]
pathsInDir FilePath
"tests/InvalidRules/"

{- | Reads every proof file in @tests\/InvalidFormulae\/@ and asserts that the
t'Formula' at the line number encoded in the filename is v'ParsedInvalid'
using 'expectInvalidFormulaAt'.
-}
testInvalidFormulae :: TestTree
testInvalidFormulae :: TestTree
testInvalidFormulae =
  FilePath -> ((FilePath -> Assertion) -> Assertion) -> TestTree
testCaseSteps FilePath
"Testing invalid proofs" (((FilePath -> Assertion) -> Assertion) -> TestTree)
-> ((FilePath -> Assertion) -> Assertion) -> TestTree
forall a b. (a -> b) -> a -> b
$ \FilePath -> Assertion
step ->
    (FilePath -> Assertion) -> [FilePath] -> Assertion
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
      ( \FilePath
str ->
          do
            let rem :: FilePath
rem = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') FilePath
str
                lineNo :: FilePath
lineNo = (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') FilePath
rem
            FilePath -> Assertion
step (FilePath
str FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
" at line " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
lineNo) Assertion -> IO (FilePath, FilePath) -> IO (FilePath, FilePath)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (FilePath, FilePath) -> IO (FilePath, FilePath)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath
str, FilePath
lineNo)
            p <- FilePath -> IO Proof
readProof FilePath
str
            no :: Int <- case reads lineNo of
              [] -> FilePath -> IO Int
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO Int) -> FilePath -> IO Int
forall a b. (a -> b) -> a -> b
$ FilePath
"'reads' failed extracting a number from lineNo=" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
lineNo
              (Int
n, FilePath
_) : [(Int, FilePath)]
_ -> Int -> IO Int
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
n
            expectInvalidFormulaAt no p
      )
      ([FilePath] -> Assertion) -> IO [FilePath] -> Assertion
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO [FilePath]
pathsInDir FilePath
"tests/InvalidFormulae/"

-- | t'TestTree' for all tests related to "Fitch.Verification"
verificationTests :: TestTree
verificationTests :: TestTree
verificationTests =
  FilePath -> [TestTree] -> TestTree
testGroup
    FilePath
"Testing proof verification"
    [TestTree
testValidProofs, TestTree
testInvalidFormulae, TestTree
testInvalidRules]