content: {- |
  Module      :  ./TPTP/Prover/EProver.hs
  Description :  Interface for the E Theorem Prover.
  Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
  Stability   :  provisional
  Portability :  non-portable (imports Logic)
  -}
  
  module TPTP.Prover.Common where
  
  import TPTP.Prover.ProverState
  import TPTP.Morphism
  import TPTP.Sign
  import TPTP.Sublogic
  
  import Common.AS_Annotation
  import Common.ProofTree
  import Common.Result
  import Common.SZSOntology
  import Common.Timing
  import Common.Utils
  import GUI.GenericATP
  import Interfaces.GenericATPState hiding (proverState, timeUsed)
  import Logic.Prover
  import Proofs.BatchProcessing
  
  import qualified Control.Concurrent as Concurrent
  import Control.Monad
  import Data.Char (toUpper)
  import Data.Maybe
  import Data.Time.LocalTime
  import System.Directory
  import System.Exit
  
  type AtpFunType =
    String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
  
  type RunTheProverType =
       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
    -> String -- ^ name of the theory in the DevGraph
    -> Named Sentence -- ^ goal to prove
    -> IO (ATPRetval, GenericConfig ProofTree)
       -- ^ (retval, configuration with proof status and complete output)
  
  mkProver :: String
           -> String
           -> Sublogic
           -> RunTheProverType
           -> Prover Sign Sentence Morphism Sublogic ProofTree
  mkProver binary_name prover_name sublogics runTheProver =
    mkAutomaticProver binary_name prover_name sublogics proverGUI proverCLI
    where
      atpFun :: String
             -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
      atpFun theoryName = ATPFunctions
        { initialProverState = tptpProverState,
          atpTransSenName = id,
          atpInsertSentence = insertSentenceIntoProverState,
          goalOutput = ioShowTPTPProblem theoryName,
          proverHelpText = helpText,
          batchTimeEnv = "HETS_" ++ map toUpper prover_name ++ "_BATCH_TIME_LIMIT",
          fileExtensions =
            FileExtensions { problemOutput = ".tptp"
                           , proverOutput = "."++ prover_name ++ ".out"
                           , theoryConfiguration = "." ++ prover_name ++ ".conf"
                           },
          runProver = runTheProver,
          createProverOptions = extraOpts}
  
      helpText :: String
      helpText =
        "No help yet available.\n" ++
        "Email hets-devel@informatik.uni-bremen.de " ++
        "for more information.\n"
  
      proverGUI :: String
                -> Theory Sign Sentence ProofTree
                -> [FreeDefMorphism Sentence Morphism]
                -> IO [ProofStatus ProofTree]
      proverGUI theoryName theory freenessConstraints =
        genericATPgui
          (atpFun theoryName)
          True
          prover_name
          theoryName
          theory
          freenessConstraints
          emptyProofTree
  
      proverCLI :: Bool
                -> Bool
                -> Concurrent.MVar (Result [ProofStatus ProofTree])
                -> String
                -> TacticScript
                -> Theory Sign Sentence ProofTree
                -> [FreeDefMorphism Sentence Morphism]
                -> IO (Concurrent.ThreadId, Concurrent.MVar ())
      proverCLI includeProvedTheorems saveProblemFile batchResultStore theoryName
                  defaultTacticScript theory freenessConstraints =
        genericCMDLautomaticBatch
          (atpFun theoryName)
          includeProvedTheorems
          saveProblemFile
          batchResultStore
          prover_name
          theoryName
          (parseProverTacticScript defaultTacticScript)
          theory
          freenessConstraints
          emptyProofTree
  
      parseProverTacticScript :: TacticScript -> ATPTacticScript
      parseProverTacticScript = parseTacticScript batchTimeLimit []
  
  
  mkTheoryFileName :: String -> Named Sentence -> String
  mkTheoryFileName theoryName namedGoal =
    basename (theoryName ++ '_' : senAttr namedGoal ++ ".tptp")
  
  getTimeLimit :: GenericConfig ProofTree -> Int
  getTimeLimit cfg = fromMaybe 100 $ timeLimit cfg
  
  hardTimeLimit :: GenericConfig ProofTree -> Int
  hardTimeLimit cfg =
    let configuredTimeLimit = getTimeLimit cfg
    in minimum [ configuredTimeLimit + 30
               , round ((1.5 :: Double) * fromIntegral configuredTimeLimit)
               ]
  
  gnuTimeout :: IO String
  gnuTimeout = do
    path <- findExecutable "gtimeout"
    return $ if isJust path then "gtimeout" else "timeout"
  
  
  prepareProverInput :: ProverState
                     -> GenericConfig ProofTree
                     -> Bool
                     -> String
                     -> Named Sentence
                     -> String
                     -> IO String
  prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name =
    do
      let theoryFileName = mkTheoryFileName theoryName namedGoal
      tptpProblemString <- getProblemString
      problemFileName <- getTempFile tptpProblemString theoryFileName
      saveProblemFileIfNeeded theoryFileName tptpProblemString
      return problemFileName
    where
      getProblemString :: IO String
      getProblemString = ioShowTPTPProblem theoryName proverState namedGoal $
          extraOpts cfg ++ ["Requested prover: " ++ prover_name]
  
      saveProblemFileIfNeeded :: String -> String -> IO ()
      saveProblemFileIfNeeded theoryFileName tptpProblemString =
        when saveTPTPFile $ writeFile theoryFileName tptpProblemString
  
  executeTheProver :: String -> [String] -> IO (ExitCode, [String], TimeOfDay)
  executeTheProver binary_name options = do
    startTime <- getHetsTime
    (exitCode, pout, perr) <- executeProcess binary_name options ""
    endTime <- return exitCode >> getHetsTime
    let wallTimeUsed = diffHetsTime endTime startTime
    let out = lines (perr ++ pout)
    return (exitCode, out, wallTimeUsed)
  
  atpRetValAndProofStatus :: GenericConfig ProofTree
                          -> Named Sentence
                          -> TimeOfDay
                          -> [String]
                          -> String
                          -> String
                          -> (ATPRetval, ProofStatus ProofTree)
  atpRetValAndProofStatus cfg namedGoal = atpRetValAndProofStatus' cfg $ senAttr namedGoal
  
  atpRetValAndProofStatus' :: GenericConfig ProofTree
                          -> String
                          -> TimeOfDay
                          -> [String]
                          -> String
                          -> String
                          -> (ATPRetval, ProofStatus ProofTree)
  atpRetValAndProofStatus' cfg nameOfGoal timeUsed axiomsUsed szsStatusLine prover_name =
    let statuses = proofStatuses' cfg nameOfGoal timeUsed axiomsUsed prover_name
    in selectRetValAndProofStatus statuses szsStatusLine
  
  selectRetValAndProofStatus :: (ProofStatus ProofTree,
                                 ProofStatus ProofTree,
                                 ProofStatus ProofTree)
                             -> String
                             -> (ATPRetval, ProofStatus ProofTree)
  selectRetValAndProofStatus (defaultPS, proved, disproved) szsStatusLine =
    case () of
      _ | szsProved szsStatusLine    -> (ATPSuccess, proved)
      _ | szsDisproved szsStatusLine -> (ATPSuccess, disproved)
      _ | szsTimeout szsStatusLine   -> (ATPTLimitExceeded, defaultPS)
      _ | szsStopped szsStatusLine   -> (ATPBatchStopped, defaultPS)
      _                              -> (ATPError szsStatusLine, defaultPS)
  
  proofStatuses :: GenericConfig ProofTree
                -> Named Sentence
                -> TimeOfDay
                -> [String]
                -> String
                -> (ProofStatus ProofTree,
                    ProofStatus ProofTree,
                    ProofStatus ProofTree)
  proofStatuses cfg namedGoal =
    proofStatuses' cfg (senAttr namedGoal)
  
  proofStatuses' :: GenericConfig ProofTree
                -> String
                -> TimeOfDay
                -> [String]
                -> String
                -> (ProofStatus ProofTree,
                    ProofStatus ProofTree,
                    ProofStatus ProofTree)
  proofStatuses' cfg nameOfGoal timeUsed axiomsUsed prover_name =
    let defaultPS =
          (openProofStatus nameOfGoal prover_name emptyProofTree)
            { usedTime = timeUsed
            , tacticScript = TacticScript $ show ATPTacticScript
               { tsTimeLimit = configTimeLimit cfg
               , tsExtraOpts = extraOpts cfg } }
        disproved = defaultPS { goalStatus = Disproved }
        proved = defaultPS
          { goalStatus = Proved True
          , usedAxioms = axiomsUsed
          , usedProver = prover_name
          , usedTime = timeUsed
          }
    in  (defaultPS, proved, disproved)
  