842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Interface for the MathServe broker.
842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Rene Wagner, Klaus Luettich, Rainer Grabbe,
842ae4bd224140319ae7feec1872b93dfd491143fielding Uni Bremen 2005-2006
842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : GPLv2 or higher, see LICENSE.txt
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzMaintainer : Christian.Maeder@dfki.de
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzStability : provisional
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzPortability : needs POSIX
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzInterface for the MathServe broker which calls different ATP systems,
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz - check why an internal error during batch mode running does not invoke
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz an error window. Also the proving won't stop.
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz ( mathServBroker
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz , mathServBrokerCMDLautomaticBatch
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzimport qualified Common.AS_Annotation as AS_Anno
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzimport qualified Common.Result as Result
4bceff39f96a979b76e1dbef0d2e004ca0546f43rpluemimport qualified Control.Concurrent as Concurrent
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzimport qualified Control.Exception as Exception
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz-- * Prover implementation
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz The Prover implementation. First runs the batch prover (with graphical
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz feedback), then starts the GUI prover.
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzmathServBroker :: Prover Sign Sentence SoftFOLMorphism () ProofTree
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantzmathServBroker = (mkProverTemplate brokerName () mathServBrokerGUI)
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz { proveCMDLautomaticBatch = Just mathServBrokerCMDLautomaticBatch }
36ef8f77bffe75d1aa327882be1b5bdbe2ff567asfmathServHelpText :: String
36ef8f77bffe75d1aa327882be1b5bdbe2ff567asfmathServHelpText =
94e21bbbd0f0f960317594da47734c4b7f5d3ec4rpluem "No help for MathServ available.\n"
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin-- * Main prover functions
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz-- ** Utility functions
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin Record for prover specific functions. This is used by both GUI and command
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin line interface.
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinatpFun :: String -- ^ theory name
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinatpFun thName = ATPFunctions
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin { initialProverState = spassProverState,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin atpTransSenName = transSenName,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin atpInsertSentence = insertSentenceGen,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin goalOutput = showTPTPProblem thName,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin proverHelpText = mathServHelpText,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
0f19881eb155511972cec25a0b554ae0182c6ba1covener fileExtensions = FileExtensions {problemOutput = ".tptp",
ba1858598da91e42b574eee1b69ab485fbd0d1d5ylavic proverOutput = ".spass",
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz theoryConfiguration = ".spcf"},
56ab8639aed4d3b2f031d9c1160c5f40af01bdebjerenkrantz runProver = runMSBroker,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin createProverOptions = extraOpts}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin Invokes the generic prover GUI. SoftFOL specific functions are omitted by
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin data type ATPFunctions.
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinmathServBrokerGUI :: String -- ^ theory name
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> Theory Sign Sentence ProofTree
836587f1b2cd2cc99ee7dfb0c0f872f03ce8632drpluem {- ^ theory consisting of a SoftFOL.Sign.Sign
b1cf8b6c70a42f499ea03b61997bb8667810d285minfrin and a list of Named SoftFOL.Sign.Sentence -}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> [FreeDefMorphism SPTerm SoftFOLMorphism]
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -- ^ freeness constraints
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> IO [ProofStatus ProofTree]
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -- ^ proof status for each goal
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinmathServBrokerGUI thName th freedefs =
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin genericATPgui (atpFun thName) False (proverName mathServBroker) thName th
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin freedefs emptyProofTree
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin-- ** command line function
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
dcdce2058e8e657eb3b2f653461cbef0e89d9173niq automatic command line interface to the MathServe Broker.
470c2663449af7b1ba64f9e67c3709371f6825acrpluem MathServ specific functions are omitted by data type ATPFunctions.
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinmathServBrokerCMDLautomaticBatch ::
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin Bool -- ^ True means include proved theorems
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> Bool -- ^ True means save problem file
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -- ^ used to store the result of the batch run
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> String -- ^ theory name
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> TacticScript -- ^ default tactic script
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> Theory Sign Sentence ProofTree {- ^ theory consisting of a
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence' -}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin {- ^ fst: identifier of the batch thread for killing it
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin snd: MVar to wait for the end of the thread -}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinmathServBrokerCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin thName defTS th freedefs =
470c2663449af7b1ba64f9e67c3709371f6825acrpluem genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin resultMVar (proverName mathServBroker) thName
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
836587f1b2cd2cc99ee7dfb0c0f872f03ce8632drpluem Runs the MathServ broker and returns GUI proof status and prover
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin configuration with proof status and complete prover output.
836587f1b2cd2cc99ee7dfb0c0f872f03ce8632drpluemrunMSBroker :: SoftFOLProverState
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin {- ^ logical part containing the input Sign and axioms and possibly
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin goals that have been proved earlier as additional axioms -}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> GenericConfig ProofTree -- ^ configuration to use
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> Bool -- ^ True means save TPTP file
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> String -- ^ name of the theory in the DevGraph
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> AS_Anno.Named SPTerm -- ^ goal to prove
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -> IO (ATPRetval, GenericConfig ProofTree)
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin -- ^ (retval, configuration with proof status and complete output)
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrinrunMSBroker sps cfg saveTPTP thName nGoal =
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin prob <- showTPTPProblem thName sps nGoal $ extraOpts cfg
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin ++ ['[' : brokerName ++ "]"]
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin when saveTPTP
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin (writeFile (thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp") prob)
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin mathServOut <- callMathServ
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin MathServCall {mathServService = Broker,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin mathServOperation = ProblemOpt,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin problem = prob,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin proverTimeLimit = configTimeLimit cfg,
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin extraOptions = Nothing}
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin msResponse <- parseMathServOut mathServOut
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin return (mapMathServResponse (getAxioms sps) msResponse cfg nGoal $
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin proverName mathServBroker))
74e7f6c55fd67b10cb400b3f6d1dc718a303d944minfrin $ excepToATPResult (proverName mathServBroker) $ AS_Anno.senAttr nGoal