ProveIsabelle.hs revision e24ad3f655daa60ddabe690e4b11de3187996c16
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyDescription : Interface to the Isabelle theorem prover.
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyStability : provisional
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyPortability : non-portable
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyIsabelle theorem prover for THF0
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillymodule THF.ProveIsabelle ( isaProver, nitpickProver,
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly refuteProver, sledgehammerProver ) where
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport Data.List (isPrefixOf, stripPrefix)
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reillyimport Data.Maybe (fromMaybe)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reillypfun :: String -> ProverFuncs
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reillypfun tool = ProverFuncs {
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly cfgTimeout = maybe 20 (+ 10) . timeLimit,
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly proverCommand = \ tout tmpFile _ ->
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly return ("time", ["isabelle", tool, show (tout - 10), tmpFile]),
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly getMessage = \ res' pout _ ->
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly if null res' then concat $ filter (isPrefixOf "*** ") (lines pout)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly [] -> Nothing
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly s -> let sp p str = case dropWhile p str of
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly s' -> w : sp p s''
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly where (w, s'') = break p s'
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly (m : secs : _) = sp (== 'm') s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in Just $ read m * 60 + read secs }
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'ReillycreateIsaSZSProver :: String -> String -> ProverFuncs -> ProverType
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'ReillycreateIsaSZSProver = createSZSProver "isabelle"
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'ReillyisaProver :: ProverType
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'ReillyisaProver = createIsaSZSProver "Isabelle (automated)"
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly "Automated Isabelle calling all tools available"
1b2195930f52ad43e6bb64b1df0cf6718bfd84c0Liam O'Reilly $ pfun "tptp_isabelle_demo"
9738b4e358f960105062839c835bb9eff3e44588Liam O'ReillynitpickProver :: ProverType
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillynitpickProver = createIsaSZSProver "Isabelle (nitpick)"
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly "Nitpick for TPTP problems"
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly $ pfun "tptp_nitpick"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrefuteProver :: ProverType
9738b4e358f960105062839c835bb9eff3e44588Liam O'ReillyrefuteProver = createIsaSZSProver "Isabelle (refute)"
9738b4e358f960105062839c835bb9eff3e44588Liam O'Reilly "refute for TPTP problems"
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly $ pfun "tptp_refute"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillysledgehammerProver :: ProverType
c3efd4f435e954846981cf46bca64e0485266634Liam O'ReillysledgehammerProver = createIsaSZSProver "Isabelle (sledgehammer)"
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly "sledgehammer for TPTP problems"
c3efd4f435e954846981cf46bca64e0485266634Liam O'Reilly $ pfun "tptp_sledgehammer"