ProofParser.hs revision 7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Interface for the E Theorem Prover.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Eugen Kuksa University of Magdeburg 2017
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable (imports Logic)
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maedermodule TPTP.Prover.SPASS.ProofParser (parseOutput) where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederimport Data.Time (TimeOfDay (..), midnight)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichparseOutput :: Named Sentence -- ^ the proof goal
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> [String] -- ^ the SPASS process output
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> (Maybe String, [String], Bool, TimeOfDay)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder -- ^ (result, used axioms, output exists, used time)
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian MaederparseOutput namedGoal = foldl parseIt (Nothing, [], False, midnight)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder parseIt :: (Maybe String, [String], Bool, TimeOfDay)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> (Maybe String, [String], Bool, TimeOfDay)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder parseIt (result, axiomsUsed, spass_start_passed, timeUsed) line =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ( case stripPrefix "SPASS beiseite: " line of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder r@(Just _) | spass_start_passed -> r
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , case stripPrefix "Formulae used in the proof :" line of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Just s -> filter (/= senAttr namedGoal) $ words s
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Nothing -> axiomsUsed
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , spass_start_passed || isInfixOf "SPASS-START" line
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder , case stripPrefix "SPASS spent" line of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Just s | isInfixOf "on the problem." line ->
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder fromMaybe midnight $ parseTimeOfDay $
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder takeWhile (\ c -> isDigit c || elem c ".:") $ trimLeft s
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederparseTimeOfDay :: String -> Maybe TimeOfDay
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederparseTimeOfDay str =
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder case splitOn ':' str of
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder [h, m, s] -> Just TimeOfDay
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder { todHour = read h
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder , todMin = read m
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder , todSec = realToFrac (read s :: Double) }