  | 
 Module       :   ./TPTP / Prover / SPASS.hs 
 Description :   Interface for the SPASS theorem prover . 
 Copyright    :   ( c )    of Magdeburg 2017 
 License      :   GPLv2 or higher , see LICENSE.txt 

 Maintainer   :     <  > 
 Stability    :   provisional 
 Portability :   non - portable ( imports Logic ) 

Module      :  ./TPTP/Prover/SPASS.hs
Description :  Interface for the SPASS theorem prover.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <>
Stability   :  provisional
Portability :  non-portable (imports Logic)
-}

module TPTP.Prover.SPASS (spass) where

import TPTP.Prover.Common
import TPTP.Prover.SPASS.ProofParser
import TPTP.Prover.ProverState
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic

import Common.AS_Annotation
import Common.ProofTree
import Interfaces.GenericATPState hiding (proverState)
import Logic.Prover hiding (proofLines)

import Data.List

spass :: Prover Sign Sentence Morphism Sublogic ProofTree
spass = mkProver binary_name prover_name sublogics runTheProver

binary_name :: String
binary_name = "SPASS"

prover_name :: String
prover_name = "SPASS"

sublogics :: Sublogic
sublogics = FOF


runTheProver :: ProverState
                {- ^ logical part containing the input Sign and axioms and possibly
                goals that have been proved earlier as additional axioms -}
             -> GenericConfig ProofTree -- ^ configuration to use
             -> Bool -- ^ True means save TPTP file
  ^ name of the theory in the DevGraph
             -> Named Sentence -- ^ goal to prove
             -> IO (ATPRetval, GenericConfig ProofTree)
                -- ^ (retval, configuration with proof status and complete output)
runTheProver proverState cfg saveTPTPFile theoryName namedGoal = do
  let proverTimeLimitS = show $ getTimeLimit cfg
      allOptions = [ "-TPTP"
                   , "-DocProof"
                   , "-TimeLimit=" ++ proverTimeLimitS
                   ]

  problemFileName <-
    prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name

  (_, out, _) <-
    executeTheProver binary_name (allOptions ++ [problemFileName])

  let (mResult, axiomsUsed, outputExists, resultedTimeUsed) =
        parseOutput namedGoal out
  let (defaultProofStatus, provedStatus, disprovedStatus) =
        proofStatuses cfg namedGoal resultedTimeUsed axiomsUsed prover_name
  let (atpRetval, resultedProofStatus) = case mResult of
        Nothing -> (ATPError $ errorMessage outputExists, defaultProofStatus)
        Just result
          | isInfixOf "Proof found." result -> (ATPSuccess, provedStatus)
          | isInfixOf "Completion found." result -> (ATPSuccess, disprovedStatus)
          | isInfixOf "Ran out of time." result ->
              (ATPTLimitExceeded, defaultProofStatus)
        _ -> (ATPSuccess, defaultProofStatus)
  return (atpRetval, cfg { proofStatus = resultedProofStatus
                         , resultOutput = out
                         , timeUsed = resultedTimeUsed })
  where
    errorMessage :: Bool -> String
    errorMessage outputExists =
      "No " ++
        (if outputExists then "result" else "output") ++
        " of " ++ prover_name ++ " found."

 ^ logical part containing the input Sign and axioms and possibly
                goals that have been proved earlier as additional axioms 
 ^ configuration to use
 ^ True means save TPTP file
 ^ goal to prove
 ^ (retval, configuration with proof status and complete output)
  | 
 Module       :   ./TPTP / Prover / SPASS.hs 
 Description :   Interface for the SPASS theorem prover . 
 Copyright    :   ( c )    of Magdeburg 2017 
 License      :   GPLv2 or higher , see LICENSE.txt 

 Maintainer   :     <  > 
 Stability    :   provisional 
 Portability :   non - portable ( imports Logic ) 

Module      :  ./TPTP/Prover/SPASS.hs
Description :  Interface for the SPASS theorem prover.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <>
Stability   :  provisional
Portability :  non-portable (imports Logic)
-}

module TPTP.Prover.SPASS (spass) where

import TPTP.Prover.Common
import TPTP.Prover.SPASS.ProofParser
import TPTP.Prover.ProverState
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic

import Common.AS_Annotation
import Common.ProofTree
import Interfaces.GenericATPState hiding (proverState)
import Logic.Prover hiding (proofLines)

import Data.List

spass :: Prover Sign Sentence Morphism Sublogic ProofTree
spass = mkProver binary_name prover_name sublogics runTheProver

binary_name :: String
binary_name = "SPASS"

prover_name :: String
prover_name = "SPASS"

sublogics :: Sublogic
sublogics = FOF


runTheProver :: ProverState
  ^ name of the theory in the DevGraph
             -> IO (ATPRetval, GenericConfig ProofTree)
runTheProver proverState cfg saveTPTPFile theoryName namedGoal = do
  let proverTimeLimitS = show $ getTimeLimit cfg
      allOptions = [ "-TPTP"
                   , "-DocProof"
                   , "-TimeLimit=" ++ proverTimeLimitS
                   ]

  problemFileName <-
    prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name

  (_, out, _) <-
    executeTheProver binary_name (allOptions ++ [problemFileName])

  let (mResult, axiomsUsed, outputExists, resultedTimeUsed) =
        parseOutput namedGoal out
  let (defaultProofStatus, provedStatus, disprovedStatus) =
        proofStatuses cfg namedGoal resultedTimeUsed axiomsUsed prover_name
  let (atpRetval, resultedProofStatus) = case mResult of
        Nothing -> (ATPError $ errorMessage outputExists, defaultProofStatus)
        Just result
          | isInfixOf "Proof found." result -> (ATPSuccess, provedStatus)
          | isInfixOf "Completion found." result -> (ATPSuccess, disprovedStatus)
          | isInfixOf "Ran out of time." result ->
              (ATPTLimitExceeded, defaultProofStatus)
        _ -> (ATPSuccess, defaultProofStatus)
  return (atpRetval, cfg { proofStatus = resultedProofStatus
                         , resultOutput = out
                         , timeUsed = resultedTimeUsed })
  where
    errorMessage :: Bool -> String
    errorMessage outputExists =
      "No " ++
        (if outputExists then "result" else "output") ++
        " of " ++ prover_name ++ " found."
