module THF.ProveIsabelle ( isaProver, nitpickProver,
refuteProver, sledgehammerProver ) where
import THF.SZSProver
import Interfaces.GenericATPState
import Data.List (isPrefixOf, stripPrefix)
import Data.Maybe (fromMaybe)
pfun :: String -> ProverFuncs
pfun :: String -> ProverFuncs
pfun tool :: String
tool = ProverFuncs :: (GenericConfig ProofTree -> Int)
-> (Int
-> String -> GenericConfig ProofTree -> IO (String, [String]))
-> (String -> String -> String -> String)
-> (String -> Maybe Int)
-> ProverFuncs
ProverFuncs {
cfgTimeout :: GenericConfig ProofTree -> Int
cfgTimeout = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 20 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 10) (Maybe Int -> Int)
-> (GenericConfig ProofTree -> Maybe Int)
-> GenericConfig ProofTree
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit,
proverCommand :: Int -> String -> GenericConfig ProofTree -> IO (String, [String])
proverCommand = \ tout :: Int
tout tmpFile :: String
tmpFile _ ->
(String, [String]) -> IO (String, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ("time", ["isabelle", String
tool, Int -> String
forall a. Show a => a -> String
show (Int
tout Int -> Int -> Int
forall a. Num a => a -> a -> a
- 10), String
tmpFile]),
getMessage :: String -> String -> String -> String
getMessage = \ res' :: String
res' pout :: String
pout _ ->
if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
res' then [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "*** ") (String -> [String]
lines String
pout)
else String
res',
getTimeUsed :: String -> Maybe Int
getTimeUsed = \ line :: String
line -> case String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "real\t" String
line of
[] -> Maybe Int
forall a. Maybe a
Nothing
s :: String
s -> let sp :: (Char -> Bool) -> String -> [String]
sp p :: Char -> Bool
p str :: String
str = case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
p String
str of
"" -> []
s' :: String
s' -> String
w String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Char -> Bool) -> String -> [String]
sp Char -> Bool
p String
s''
where (w :: String
w, s'' :: String
s'') = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
p String
s'
(m :: String
m : secs :: String
secs : _) = (Char -> Bool) -> String -> [String]
sp (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== 'm') String
s
in Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
m Int -> Int -> Int
forall a. Num a => a -> a -> a
* 60 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
forall a. Read a => String -> a
read String
secs }
createIsaSZSProver :: String -> String -> ProverFuncs -> ProverType
createIsaSZSProver :: String -> String -> ProverFuncs -> ProverType
createIsaSZSProver = String -> String -> String -> ProverFuncs -> ProverType
createSZSProver "isabelle"
isaProver :: ProverType
isaProver :: ProverType
isaProver = String -> String -> ProverFuncs -> ProverType
createIsaSZSProver "Isabelle (automated)"
"Automated Isabelle calling all tools available"
(ProverFuncs -> ProverType) -> ProverFuncs -> ProverType
forall a b. (a -> b) -> a -> b
$ String -> ProverFuncs
pfun "tptp_isabelle_demo"
nitpickProver :: ProverType
nitpickProver :: ProverType
nitpickProver = String -> String -> ProverFuncs -> ProverType
createIsaSZSProver "Isabelle (nitpick)"
"Nitpick for TPTP problems"
(ProverFuncs -> ProverType) -> ProverFuncs -> ProverType
forall a b. (a -> b) -> a -> b
$ String -> ProverFuncs
pfun "tptp_nitpick"
refuteProver :: ProverType
refuteProver :: ProverType
refuteProver = String -> String -> ProverFuncs -> ProverType
createIsaSZSProver "Isabelle (refute)"
"refute for TPTP problems"
(ProverFuncs -> ProverType) -> ProverFuncs -> ProverType
forall a b. (a -> b) -> a -> b
$ String -> ProverFuncs
pfun "tptp_refute"
sledgehammerProver :: ProverType
sledgehammerProver :: ProverType
sledgehammerProver = String -> String -> ProverFuncs -> ProverType
createIsaSZSProver "Isabelle (sledgehammer)"
"sledgehammer for TPTP problems"
(ProverFuncs -> ProverType) -> ProverFuncs -> ProverType
forall a b. (a -> b) -> a -> b
$ String -> ProverFuncs
pfun "tptp_sledgehammer"