{- |
Module      :  ./THF/ProveIsabelle.hs
Description :  Interface to the Isabelle theorem prover.
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable

Isabelle theorem prover for THF0
-}

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"