2799N/A{- |

2799N/AModule : ./THF/ProveIsabelle.hs

2799N/ADescription : Interface to the Isabelle theorem prover.

2799N/ACopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012

2799N/ALicense : GPLv2 or higher, see LICENSE.txt

2799N/A

248N/AMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>

2799N/AStability : provisional

2799N/APortability : non-portable

2799N/A

248N/AIsabelle theorem prover for THF0

2799N/A-}

2799N/A

248N/Amodule THF.ProveIsabelle ( isaProver, nitpickProver,

2799N/A refuteProver, sledgehammerProver ) where

2799N/A

2799N/Aimport THF.SZSProver

2799N/Aimport Interfaces.GenericATPState

2799N/Aimport Data.List (isPrefixOf, stripPrefix)

2799N/Aimport Data.Maybe (fromMaybe)

248N/A

2799N/Apfun :: String -> ProverFuncs

2799N/Apfun tool = ProverFuncs {

2799N/A cfgTimeout = maybe 20 (+ 10) . timeLimit,

2799N/A proverCommand = \ tout tmpFile _ ->

2799N/A return ("time", ["isabelle", tool, show (tout - 10), tmpFile]),

2799N/A getMessage = \ res' pout _ ->

2799N/A if null res' then concat $ filter (isPrefixOf "*** ") (lines pout)

2799N/A else res',

2799N/A getTimeUsed = \ line -> case fromMaybe "" $ stripPrefix "real\t" line of

248N/A [] -> Nothing

2799N/A s -> let sp p str = case dropWhile p str of

2799N/A "" -> []

2799N/A s' -> w : sp p s''

2799N/A where (w, s'') = break p s'

2799N/A (m : secs : _) = sp (== 'm') s

2799N/A in Just $ read m * 60 + read secs }

248N/A

2799N/AcreateIsaSZSProver :: String -> String -> ProverFuncs -> ProverType

2799N/AcreateIsaSZSProver = createSZSProver "isabelle"

2799N/A

2799N/AisaProver :: ProverType

248N/AisaProver = createIsaSZSProver "Isabelle (automated)"

2799N/A "Automated Isabelle calling all tools available"

2799N/A $ pfun "tptp_isabelle_demo"

2799N/A

2799N/AnitpickProver :: ProverType

2799N/AnitpickProver = createIsaSZSProver "Isabelle (nitpick)"

248N/A "Nitpick for TPTP problems"

2799N/A $ pfun "tptp_nitpick"

2799N/A

2799N/ArefuteProver :: ProverType

2799N/ArefuteProver = createIsaSZSProver "Isabelle (refute)"

2799N/A "refute for TPTP problems"

2799N/A $ pfun "tptp_refute"

2799N/A

2799N/AsledgehammerProver :: ProverType

2799N/AsledgehammerProver = createIsaSZSProver "Isabelle (sledgehammer)"

2799N/A "sledgehammer for TPTP problems"

248N/A $ pfun "tptp_sledgehammer"

2799N/A