f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederDescription : Interface to the Isabelle theorem prover.
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
421def3c7b0b9ca7762f809a2c57c6ee74495ffaJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
421def3c7b0b9ca7762f809a2c57c6ee74495ffaJonathan von SchroederStability : provisional
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederPortability : non-portable
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederIsabelle theorem prover for THF0
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroedermodule THF.ProveIsabelle ( isaProver, nitpickProver,
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder refuteProver, sledgehammerProver ) where
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Data.List (isPrefixOf, stripPrefix)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Data.Maybe (fromMaybe)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederpfun :: String -> ProverFuncs
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederpfun tool = ProverFuncs {
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder cfgTimeout = maybe 20 (+ 10) . timeLimit,
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder proverCommand = \ tout tmpFile _ ->
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder return ("time", ["isabelle", tool, show (tout - 10), tmpFile]),
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder getMessage = \ res' pout _ ->
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder if null res' then concat $ filter (isPrefixOf "*** ") (lines pout)
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder s -> let sp p str = case dropWhile p str of
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder s' -> w : sp p s''
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder where (w, s'') = break p s'
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder (m : secs : _) = sp (== 'm') s
87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder in Just $ read m * 60 + read secs }
e24ad3f655daa60ddabe690e4b11de3187996c16cmaedercreateIsaSZSProver :: String -> String -> ProverFuncs -> ProverType
e24ad3f655daa60ddabe690e4b11de3187996c16cmaedercreateIsaSZSProver = createSZSProver "isabelle"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederisaProver :: ProverType
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederisaProver = createIsaSZSProver "Isabelle (automated)"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder "Automated Isabelle calling all tools available"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder $ pfun "tptp_isabelle_demo"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroedernitpickProver :: ProverType
e24ad3f655daa60ddabe690e4b11de3187996c16cmaedernitpickProver = createIsaSZSProver "Isabelle (nitpick)"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder "Nitpick for TPTP problems"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder $ pfun "tptp_nitpick"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederrefuteProver :: ProverType
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederrefuteProver = createIsaSZSProver "Isabelle (refute)"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder "refute for TPTP problems"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder $ pfun "tptp_refute"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroedersledgehammerProver :: ProverType
e24ad3f655daa60ddabe690e4b11de3187996c16cmaedersledgehammerProver = createIsaSZSProver "Isabelle (sledgehammer)"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder "sledgehammer for TPTP problems"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder $ pfun "tptp_sledgehammer"