import Common (TestProof)
import Data.Logic.Instances.Test (V, Formula, SkAtom, SkTerm)
import System.Exit
import Test.HUnit
import qualified Logic
import qualified Chiou0 as Chiou0
--import qualified Data.Logic.Tests.TPTP as TPTP
import qualified Data
main :: IO ()
main =
runTestTT (TestList [Logic.tests,
Chiou0.tests,
-- TPTP.tests, -- This has a problem in the rendering code - it loops
Data.tests formulas proofs]) >>=
doCounts
where
doCounts counts' = exitWith (if errors counts' /= 0 || failures counts' /= 0 then ExitFailure 1 else ExitSuccess)
-- Generate the test data with a particular instantiation of FirstOrderFormula.
formulas = Data.allFormulas
proofs = (Data.proofs :: [TestProof Formula SkAtom SkTerm V])