{-# LANGUAGE ScopedTypeVariables #-}

{- |

test module similar to GUI_tests, but tests CMDL functions

-}

module Main where

import Interfaces.GenericATPState

import qualified Logic.Prover as LProver

import SoftFOL.Sign

import SoftFOL.ProveSPASS

import SoftFOL.ProveVampire

import SoftFOL.ProveMathServ

import SoftFOL.ProveDarwin

import System.IO (stdout, hSetBuffering, BufferMode (NoBuffering))

import System.Environment (getArgs)

import System.Exit

import Common.AS_Annotation

import Common.Id

import Common.ProofTree

import Common.Result

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.Maybe

import qualified Control.Concurrent as Concurrent

import Control.Monad

-- * Definitions of test theories

sign1 :: SoftFOL.Sign.Sign

sign1 = emptySign

{ sortMap = Map.insert (mkSimpleId "s") Nothing Map.empty

, predMap = Map.fromList (map (\ (x, y) ->

(mkSimpleId x, Set.singleton $ map mkSimpleId y))

[("p", ["s"]), ("q", ["s"]), ("r", ["s"]), ("a", ["s"])])}

term_x :: SPTerm

term_x = simpTerm (mkSPCustomSymbol "X")

axiom1 :: Named SPTerm

axiom1 = makeNamed "ax" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPEquiv [SPComplexTerm (mkSPCustomSymbol "p") [term_x], SPComplexTerm (mkSPCustomSymbol "q") [term_x]]))

axiom2 :: Named SPTerm

axiom2 = makeNamed "ax2" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x], SPComplexTerm (mkSPCustomSymbol "r") [term_x]]))

axiom3 :: Named SPTerm

axiom3 = makeNamed "b$$-3" (SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x], SPComplexTerm (mkSPCustomSymbol "a") [term_x]]))

goal1 :: Named SPTerm

goal1 = (makeNamed "go" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "q") [term_x], SPComplexTerm (mkSPCustomSymbol "p") [term_x] ])) { isAxiom = False }

goal2 :: Named SPTerm

goal2 = (makeNamed "go2" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "p") [term_x], SPComplexTerm (mkSPCustomSymbol "r") [term_x] ])) { isAxiom = False }

goal3 :: Named SPTerm

goal3 = (makeNamed "go3" $ SPQuantTerm SPForall [term_x] (SPComplexTerm SPImplies [SPComplexTerm (mkSPCustomSymbol "p") [term_x], SPComplexTerm (mkSPCustomSymbol "a") [term_x] ])) { isAxiom = False }

theory1 :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theory1 = LProver.Theory sign1 $ LProver.toThSens [axiom1, -- axiom2,

goal1, goal2]

theory2 :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theory2 = LProver.Theory sign1 $ LProver.toThSens [axiom1, axiom2, axiom3,

goal1, goal2, goal3]

-- A more complicated theory including ExtPartialOrder from Basic/RelationsAndOrders.casl

signExt :: SoftFOL.Sign.Sign

signExt = emptySign {sortMap = {- Map.insert "Elem" Nothing -} Map.empty,

funcMap = Map.fromList (map (\ (x, (y, z)) -> (mkSimpleId x,

Set.singleton (map mkSimpleId y, mkSimpleId z)))

[("gn_bottom", ([], "Elem")),

("inf", (["Elem", "Elem"], "Elem")),

("sup", (["Elem", "Elem"], "Elem"))]),

predMap = Map.fromList (map (\ (x, y) -> (mkSimpleId x,

Set.singleton $ map mkSimpleId y))

[ ("gn_defined", ["Elem"]),

("p__LtEq__", ["Elem", "Elem"])] )}

ga_nonEmpty :: Named SPTerm

ga_nonEmpty = makeNamed "ga_nonEmpty" SPQuantTerm {quantSym = SPExists, variableList = [simpTerm (mkSPCustomSymbol "X")], qFormula = SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}}

ga_notDefBottom :: Named SPTerm

ga_notDefBottom = makeNamed "ga_notDefBottom" SPComplexTerm {symbol = SPNot, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_bottom", arguments = []}]}]}

ga_strictness :: Named SPTerm

ga_strictness = makeNamed "ga_strictness" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")]}]}, SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

ga_strictness_one :: Named SPTerm

ga_strictness_one = makeNamed "ga_strictness_one" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")]}]}, SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

ga_predicate_strictness :: Named SPTerm

ga_predicate_strictness = makeNamed "ga_predicate_strictness" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X_one"), simpTerm (mkSPCustomSymbol "X_two")]}, SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_one")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X_two")]}]}]}}

antisym :: Named SPTerm

antisym = makeNamed "antisym" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "X")]}]}, SPComplexTerm {symbol = SPEqual, arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}]}]}}

trans :: Named SPTerm

trans = makeNamed "trans" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]}, SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "Z")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Z")]}]}]}}

refl :: Named SPTerm

refl = makeNamed "refl" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "X")]}]}}

inf_def_ExtPartialOrder :: Named SPTerm

inf_def_ExtPartialOrder = makeNamed "inf_def_ExtPartialOrder" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]}, SPComplexTerm {symbol = SPEquiv, arguments = [SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, simpTerm (mkSPCustomSymbol "Z")]}, SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"), simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"), simpTerm (mkSPCustomSymbol "Y")]}]}, SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "T")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "T")]}, SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"), simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"), simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "T"), simpTerm (mkSPCustomSymbol "Z")]}]}]}}]}]}]}}

sup_def_ExtPartialOrder :: Named SPTerm

sup_def_ExtPartialOrder = makeNamed "sup_def_ExtPartialOrder" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "Z")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Z")]}]}, SPComplexTerm {symbol = SPEquiv, arguments = [SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, simpTerm (mkSPCustomSymbol "Z")]}, SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Z")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "Z")]}]}, SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "T")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "T")]}, SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "T")]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "T")]}]}, SPComplexTerm {symbol = mkSPCustomSymbol "p__LtEq__", arguments = [simpTerm (mkSPCustomSymbol "Z"), simpTerm (mkSPCustomSymbol "T")]}]}]}}]}]}]}}

ga_comm_sup :: Named SPTerm

ga_comm_sup = (makeNamed "ga_comm_sup" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, SPComplexTerm {symbol = mkSPCustomSymbol "sup", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "X")]}]}]}}) { isAxiom = False }

ga_comm_inf :: Named SPTerm

ga_comm_inf = (makeNamed "ga_comm_inf" SPQuantTerm {quantSym = SPForall, variableList = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")], qFormula = SPComplexTerm {symbol = SPImplies, arguments = [SPComplexTerm {symbol = SPAnd, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "X")]}, SPComplexTerm {symbol = mkSPCustomSymbol "gn_defined", arguments = [simpTerm (mkSPCustomSymbol "Y")]}]}, SPComplexTerm {symbol = SPEqual, arguments = [SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "X"), simpTerm (mkSPCustomSymbol "Y")]}, SPComplexTerm {symbol = mkSPCustomSymbol "inf", arguments = [simpTerm (mkSPCustomSymbol "Y"), simpTerm (mkSPCustomSymbol "X")]}]}]}}) { isAxiom = False }

gone :: Named SPTerm

gone = (makeNamed "gone" $ simpTerm SPTrue) { isAxiom = False }

theoryExt :: LProver.Theory SoftFOL.Sign.Sign SPTerm ProofTree

theoryExt = LProver.Theory signExt $ LProver.toThSens [ga_nonEmpty, ga_notDefBottom, ga_strictness, ga_strictness_one, ga_predicate_strictness, antisym, trans, refl, inf_def_ExtPartialOrder, sup_def_ExtPartialOrder, gone, ga_comm_sup, ga_comm_inf]

-- * Testing functions

main :: IO ()

main = do

args <- getArgs

hSetBuffering stdout NoBuffering

if null args

then runAllTests

else runBatchTests

exitOnBool :: Bool -> IO ()

exitOnBool b = exitWith $ if b then ExitSuccess else ExitFailure 9

runBatchTests :: IO ()

runBatchTests =

let go23 = zip ["go", "go2", "go3"] $ repeat $ LProver.Proved True

in sequence

[runTestBatch2 True Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo2" theory2 go23

, runTestBatch2 True Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo2" theory2 go23

, runTestBatch2 True Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo2" theory2 go23

, runTestBatch2 True (Just 12) spassProveCMDLautomaticBatch "SPASS"

"[Test]ExtPartialOrder" theoryExt

(("gone", LProver.Proved True)

: zip ["ga_comm_inf", "ga_comm_sup"]

(repeat LProver.openGoalStatus))

, runTestBatch2 True (Just 12) darwinCMDLautomaticBatch "Darwin"

"[Test]ExtPartialOrder" theoryExt

[("gone", LProver.Proved True),

("ga_comm_sup", LProver.openGoalStatus)]

, runTestBatch2 True (Just 20) vampireCMDLautomaticBatch "Vampire"

"[Test]ExtPartialOrder" theoryExt

(zip ["gone", "ga_comm_sup"] (repeat LProver.openGoalStatus))

] >>= (exitOnBool . and)

{- |

Main function doing all tests (combinations of theory and prover) in a row.

Outputs status lines with information whether test passed or failed.

-}

runAllTests :: IO ()

runAllTests = do

let goRes = [("go", LProver.Proved True)]

goneR = [("gone", LProver.Proved True)]

go2 = goRes ++ [("go2", LProver.Disproved)]

go23 = zip ["go", "go2", "go3"] $ repeat $ LProver.Proved True

goneComm = goneR

++ zip ["ga_comm_inf", "ga_comm_sup"] (repeat LProver.openGoalStatus)

sequence

[runTestBatch Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo1" theory1 go2

, runTestBatch Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo1" theory1 go2

, runTestBatch Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo1" theory1 go2

, runTestBatch Nothing mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]Foo1" theory1 go2

, runTestBatch Nothing spassProveCMDLautomaticBatch "SPASS"

"[Test]Foo2" theory2 go23

, runTestBatch Nothing darwinCMDLautomaticBatch "Darwin"

"[Test]Foo2" theory2 go23

, runTestBatch Nothing vampireCMDLautomaticBatch "Vampire"

"[Test]Foo2" theory2 go23

, runTestBatch Nothing mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]Foo2" theory2 go23

, runTestBatch (Just 30) spassProveCMDLautomaticBatch "SPASS"

"[Test]ExtPartialOrder" theoryExt goneComm

, runTestBatch (Just 30) darwinCMDLautomaticBatch "Darwin"

"[Test]ExtPartialOrder" theoryExt goneComm

, runTestBatch (Just 35) vampireCMDLautomaticBatch "Vampire"

"[Test]ExtPartialOrder" theoryExt

(zip ["gone", "ga_comm_sup", "ga_comm_inf"]

(repeat LProver.openGoalStatus))

, runTestBatch (Just 30) mathServBrokerCMDLautomaticBatch "MathServ"

"[Test]ExtPartialOrder" theoryExt goneComm

] >>= (exitOnBool . and)

{- |

Runs a CMDL automatic function (given as parameter) over a given theory.

The result will be output as status message.

-}

runTest :: (String

-> LProver.TacticScript

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Result [LProver.ProofStatus ProofTree])

)

-> String -- ^ prover name for proof status in case of error

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String, LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTest runCMDLProver prName thName th expStatus = do

putStrLn $ "Trying " ++ thName ++ "(automatic) with prover " ++ prName

++ " ... "

print ATPTacticScript { tsTimeLimit = 20, tsExtraOpts = [] }

m_result <- runCMDLProver

thName

(LProver.TacticScript (show ATPTacticScript {

tsTimeLimit = 20, tsExtraOpts = [] }))

th []

stResult <- maybe (return [LProver.openProofStatus ""

prName (ProofTree "")])

return (maybeResult m_result)

putStrLn $ if succeeded stResult expStatus

then "passed"

else unlines $ "failed" : map show (diags m_result)

return (succeeded stResult expStatus)

{- |

Runs a CMDL automatic batch function (given as parameter) over a given

theory. The result will be output as status message.

-}

runTestBatch :: Maybe Int -- ^ seconds to pass before thread will be killed

-> (Bool

-> Bool

-> Concurrent.MVar

(Result [LProver.ProofStatus ProofTree])

-> String

-> LProver.TacticScript

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Concurrent.ThreadId, Concurrent.MVar ())

)

-> String -- ^ prover name

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String, LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTestBatch = runTestBatch2 False

{- |

Runs a CMDL automatic batch function (given as parameter) over a given

theory. The result will be output as status message.

-}

runTestBatch2 :: Bool -- ^ True means try to read intermediate results

-> Maybe Int -- ^ seconds to pass before thread will be killed

-> (Bool

-> Bool

-> Concurrent.MVar

(Result [LProver.ProofStatus ProofTree])

-> String

-> LProver.TacticScript

-> LProver.Theory Sign Sentence ProofTree

-> [LProver.FreeDefMorphism Sentence SoftFOLMorphism]

-> IO (Concurrent.ThreadId, Concurrent.MVar ())

)

-> String -- ^ prover name

-> String -- ^ theory name

-> LProver.Theory Sign Sentence ProofTree

-> [(String, LProver.GoalStatus)] -- ^ list of expected results

-> IO Bool

runTestBatch2 intermRes waitsec runCMDLProver prName thName th expStatus = do

putStr $ "Trying " ++ thName ++ "(automaticBatch" ++

(if intermRes then " reading intermediate results" else "") ++

") with prover " ++ prName ++ " ... "

resultMVar <- if intermRes

then Concurrent.newEmptyMVar

else Concurrent.newMVar (return [])

(threadID, mvar) <- runCMDLProver

False False resultMVar thName

(LProver.TacticScript (show ATPTacticScript {

tsTimeLimit = 10, tsExtraOpts = [] }))

th []

maybe (return ()) (\ ws -> do

Concurrent.threadDelay (ws * 1000000)

Concurrent.killThread threadID) waitsec

(stResult, diaStr) :: ([LProver.ProofStatus ProofTree], String)

<- if intermRes

then do -- reading intermediate results

iResMV <- Concurrent.newMVar []

putStrLn ""

let isReady =

Concurrent.tryTakeMVar mvar >>=

maybe (return True)

(const $ Concurrent.putMVar mvar () >> return False)

waitForEachResult = do

-- Concurrent.yield

mRes <- Concurrent.takeMVar resultMVar

oldRes <- Concurrent.takeMVar iResMV

putStrLn (unlines $ map show $ diags mRes)

newRes <- maybe (return [])

(mapM (\ res -> do

putStrLn $ "Proof status of goal \"" ++

LProver.goalName res ++ "\": " ++

show (LProver.goalStatus res)

return res))

(maybeResult mRes)

Concurrent.putMVar iResMV (oldRes ++ newRes)

isReady

-- external reader thread

Concurrent.forkIO (

foldM_ (\ run ac ->

if run then ac

else return False) True $

map (const waitForEachResult) expStatus)

-- wait for prover to complete

Concurrent.takeMVar mvar

mmRes <- Concurrent.tryTakeMVar resultMVar

mRes <- maybe (return $ return [])

(\ mR -> do

putStrLn (unlines $ map show $ diags mR)

return mR)

mmRes

res <- Concurrent.takeMVar iResMV

putStr "... "

return (res ++ fromMaybe [] (maybeResult mRes), "")

else do -- only read at the end of a batch run

Concurrent.takeMVar mvar

m_result <- Concurrent.takeMVar resultMVar

return ( fromMaybe [] (maybeResult m_result)

, unlines (map show $ diags m_result) ++ "\n" ++ show m_result)

putStrLn $ if succeeded stResult expStatus

then "passed"

else "failed\n" ++ diaStr

return (succeeded stResult expStatus)

{- |

Checks if a prover run's result matches expected result.

-}

succeeded :: [LProver.ProofStatus ProofTree]

-> [(String, LProver.GoalStatus)]

-> Bool

succeeded stResult expStatus =

length stResult == length expStatus

&& foldl (\ b givenRes -> maybe False (== LProver.goalStatus givenRes)

(lookup (LProver.goalName givenRes)

expStatus)

&& b)

True stResult