{- |
Module      :  ./THF/ProveSatallax.hs
Description :  Interface to the Satallax 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

Satallax theorem prover for THF0
-}

module THF.ProveSatallax ( satallaxProver ) where

import THF.SZSProver
import Interfaces.GenericATPState
import Data.List (stripPrefix)
import Data.Maybe (fromMaybe)

pfun :: ProverFuncs
pfun :: ProverFuncs
pfun = 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 10 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (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", ["satallax", "-t", Int -> String
forall a. Show a => a -> String
show Int
tout, String
tmpFile]),
 getMessage :: String -> String -> String -> String
getMessage = \ res' :: String
res' _ _ -> 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 }

satallaxProver :: ProverType
satallaxProver :: ProverType
satallaxProver = String -> String -> String -> ProverFuncs -> ProverType
createSZSProver "satallax" "Satallax"
 ("Satallax is an automated theorem prover for higher-order logic."
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " The particular form of higher-order logic supported by Satallax"
 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is Church's simple type theory with extensionality and choice operators.")
 ProverFuncs
pfun