content: {- |
  Module      :  ./TPTP/ProveHyper.hs
  Description :  Interface to the theorem prover e-krhyper in CASC-mode.
  Copyright   :  (c) Otto-von-Guericke University of Magdeburg, 2020
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  mscodescu@gmail.com
  Stability   :  provisional
  Portability :  needs POSIX
  
  Check out
  http://www.uni-koblenz.de/~bpelzer/ekrhyper/
  for details. For the ease of maintenance we are using e-krhyper in
  its CASC-mode, aka tptp-input. It works for single input files and
  fof-style.
  -}
  
  module TPTP.ProveHyper (hyperS, hyperProver, hyperConsChecker)
      where
  
  import Logic.Prover
  
  import Common.ProofTree
  import qualified Common.Result as Result
  import Common.AS_Annotation as AS_Anno
  import Common.SZSOntology
  import Common.Timing
  import Common.Utils
  
  import TPTP.Sign
  import TPTP.Morphism
  import TPTP.Translate
  import TPTP.Prover.ProverState
  import TPTP.Sublogic
  
  import GUI.GenericATP
  import Proofs.BatchProcessing
  import Interfaces.GenericATPState
  
  import System.Directory
  
  import Control.Monad (when)
  import qualified Control.Concurrent as Concurrent
  
  import Data.Char
  import Data.List
  import Data.Maybe
  
  import Data.Time.LocalTime (TimeOfDay, midnight)
  
  -- Prover
  
  hyperS :: String
  hyperS = "ekrh"
  
  sublogics :: Sublogic
  sublogics = FOF
  
  -- | The Prover implementation.
  hyperProver :: Prover Sign Sentence Morphism Sublogic ProofTree
  hyperProver =
    mkAutomaticProver hyperS hyperS sublogics hyperGUI hyperCMDLautomaticBatch
  
  {- |
    Record for prover specific functions. This is used by both GUI and command
    line interface.
  -}
  atpFun :: String -- ^ theory name
    -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
  atpFun thName = ATPFunctions
    { initialProverState = tptpProverState
    , atpTransSenName = transSenName
    , atpInsertSentence = insertSentenceIntoProverState
    , goalOutput = ioShowTPTPProblem thName
    , proverHelpText = "for more information visit " ++
                       "http://www.uni-koblenz.de/~bpelzer/ekrhyper/"
    , batchTimeEnv = "HETS_HYPER_BATCH_TIME_LIMIT"
    , fileExtensions = FileExtensions
        { problemOutput = ".tptp"
        , proverOutput = ".hyper"
        , theoryConfiguration = ".hypcf" }
    , runProver = runHyper
    , createProverOptions = extraOpts }
  
  {- |
    Invokes the generic prover GUI.
  -}
  hyperGUI :: String -- ^ theory name
             -> Theory Sign Sentence ProofTree
             -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
             -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
  hyperGUI thName th freedefs =
      genericATPgui (atpFun thName) True hyperS thName th
                    freedefs emptyProofTree
  
  {- |
    Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
    automatic command line interface to the prover.
  -}
  hyperCMDLautomaticBatch ::
             Bool -- ^ True means include proved theorems
          -> Bool -- ^ True means save problem file
          -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
             -- ^ used to store the result of the batch run
          -> String -- ^ theory name
          -> TacticScript -- ^ default tactic script
          -> Theory Sign Sentence ProofTree -- ^ input theory
          -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
          -> IO (Concurrent.ThreadId, Concurrent.MVar ())
             {- ^ fst: identifier of the batch thread for killing it
             snd: MVar to wait for the end of the thread -}
  hyperCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
                          thName defTS th freedefs =
      genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
          resultMVar hyperS thName
          (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
  
  prelTxt :: String -> String
  prelTxt t =
      "% only print essential output\n" ++
      "#(set_verbosity(2)).\n\n" ++
      "% assume all input to be in tptp-syntax\n" ++
      "#(set_parameter(input_type, 2)).\n\n" ++
      "% To prevent blowing up my memory\n" ++
      "#(set_memory_limit(500)).\n\n" ++
      "% produce SZS results\n" ++
      "#(set_flag(szs_output_flag, true)).\n\n" ++
      "% do not use special evaluable symbols\n" ++
      "#(clear_builtins).\n\n" ++
      "% initial term weight bound, 3 recommended for TPTP-problems\n" ++
      "#(set_parameter(max_weight_initial, 3)).\n\n" ++
      "% Terminate if out of memory\n" ++
      "#(set_parameter(limit_termination_method,0)).\n\n" ++
      "% Terminate if out of time\n" ++
      "#(set_parameter(timeout_termination_method,0)).\n\n" ++
      "% Start timer\n" ++
      "#(start_wallclock_timer(" ++ t ++ ".0)).\n"
  
  checkOption :: String -> Bool
  checkOption a = isPrefixOf "#(" a && isSuffixOf ")." a
  
  uniteOptions :: [String] -> [String]
  uniteOptions opts =
      case opts of
        a : b : cs ->
            if checkOption a
             then
                 a : uniteOptions (b : cs)
             else
                 (a ++ b) : uniteOptions cs
        _ -> opts
  
  runTxt :: String
  runTxt =
      "% start derivation with the input received so far\n" ++
      "#(run).\n\n" ++
      "% print normal E-KRHyper proof\n" ++
      "%#(print_proof).\n\n" ++
      "% print result and proof using SZS terminology;\n" ++
      "% requires postprocessing with post_szs script for proper legibility\n" ++
      "#(print_szs_proof).\n"
  
  runHyper :: 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
             -> AS_Anno.Named Sentence -- ^ goal to prove
             -> IO (ATPRetval, GenericConfig ProofTree)
             -- ^ (retval, configuration with proof status and complete output)
  runHyper sps cfg saveTPTP thName nGoal =
      let
          saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp"
          simpleOptions = uniteOptions $ extraOpts cfg
          tl = configTimeLimit cfg
          tScript = TacticScript $ show ATPTacticScript
            { tsTimeLimit = tl
            , tsExtraOpts = filter (isPrefixOf "#")
                $ lines $ prelTxt (show tl) ++ runTxt }
          defProofStat = (openProofStatus
            (senAttr nGoal)
            hyperS
            emptyProofTree) { tacticScript = tScript }
      in
          if all checkOption simpleOptions
           then
             do
               prob <- ioShowTPTPProblem thName sps nGoal []
               when saveTPTP (writeFile saveFile prob)
               (stdoutC, stderrC, t_u) <- runHyperProcess prob saveFile (show tl)
                 ('\n' : unlines simpleOptions) runTxt
               let (pStat, ret) = examineProof sps stdoutC stderrC
                     defProofStat { usedTime = t_u }
               return (pStat, cfg
                                { proofStatus = ret
                                , resultOutput = lines (stdoutC ++ stderrC)
                                , timeUsed = usedTime ret })
           else return
                      (ATPError "Syntax error in options"
                      , cfg
                       { proofStatus = defProofStat
                       , resultOutput = ["Parse Error"]
                       , timeUsed = midnight
                       })
  
  -- | call ekrh
  runHyperProcess
    :: String -- ^ problem
    -> String -- ^ file name template
    -> String -- ^ time limit
    -> String -- ^ extra options
    -> String -- ^ run text
    -> IO (String, String, TimeOfDay) -- ^ out, err, diff time
  runHyperProcess prob saveFile tl opts runTxtA = do
    stpTmpFile <- getTempFile prob saveFile
    let stpPrelFile = stpTmpFile ++ ".prelude.tme"
        stpRunFile = stpTmpFile ++ ".run.tme"
    writeFile stpPrelFile $ prelTxt tl ++ opts
    writeFile stpRunFile runTxtA
    t_start <- getHetsTime
    (_, stdoutC, stderrC) <- executeProcess hyperS
      [stpPrelFile, stpTmpFile, stpRunFile] ""
    t_end <- getHetsTime
    removeFile stpPrelFile
    removeFile stpRunFile
    removeFile stpTmpFile
    return (stdoutC, stderrC, diffHetsTime t_end t_start)
  
  -- | Mapping type from SZS to Hets
  data HyperResult = HProved | HDisproved | HTimeout | HError | HMemout
  
  getHyperResult :: [String] -> HyperResult
  getHyperResult out = case map (takeWhile isAlpha . dropWhile isSpace)
      $ mapMaybe (stripPrefix "% SZS status ") out of
    [s] | szsProved s -> HProved
      | szsDisproved s -> HDisproved
      | szsTimeout s -> HTimeout
      | szsMemoryOut s -> HMemout
    _ -> HError
  
  -- | examine SZS output
  examineProof :: ProverState
               -> String
               -> String
               -> ProofStatus ProofTree
               -> (ATPRetval, ProofStatus ProofTree)
  examineProof sps stdoutC stderrC defStatus =
      let outText = "\nOutput was:\n\n" ++ stdoutC ++ stderrC
          provenStat = defStatus
            { usedAxioms = getAxioms sps
            , proofTree = ProofTree stdoutC }
       in case getHyperResult $ lines stdoutC of
                 HProved -> (ATPSuccess, provenStat { goalStatus = Proved True })
                 HTimeout -> (ATPTLimitExceeded, defStatus)
                 HDisproved -> (ATPSuccess, provenStat { goalStatus = Disproved })
                 HMemout -> (ATPError ("Out of Memory." ++ outText), defStatus)
                 HError -> ( ATPError ("Internal Error in ekrhyper." ++ outText)
                           , defStatus)
  
  -- Consistency Checker
  
  hyperConsChecker :: ConsChecker Sign Sentence Sublogic Morphism ProofTree
  hyperConsChecker = (mkUsableConsChecker hyperS hyperS sublogics consCheck)
    { ccNeedsTimer = False }
  
  {- |
    Runs the krhyper cons-chcker. The tactic script only contains a string for the
    time limit.
  -}
  
  runTxtC :: String
  runTxtC =
      "% start derivation with the input received so far\n" ++
      "#(run).\n\n" ++
      "% print Hyper proof\n" ++
      "%#(print_proof).\n\n" ++
      "% print result and proof using SZS terminology;\n" ++
      "% requires postprocessing with post_szs script for proper legibility\n" ++
      "%#(print_szs_proof).\n\n" ++
      "% Show the model\n" ++
      "#(print_model).\n"
  
  consCheck :: String
            -> TacticScript
            -> TheoryMorphism Sign Sentence Morphism ProofTree
            -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
            -> IO (CCStatus ProofTree)
  consCheck thName (TacticScript tl) tm freedefs =
      case tTarget tm of
        Theory sig nSens -> do
            let proverStateI = tptpProverState sig (toNamedList nSens) freedefs
                saveFile = basename thName ++ ".tptp"
            prob <- showTPTPProblemM thName proverStateI []
            (stdoutC, stderrC, t_u) <-
              runHyperProcess prob saveFile tl "" runTxtC
            return CCStatus
              { ccResult = case getHyperResult $ lines stdoutC of
                  HProved -> Just True
                  HDisproved -> Just False
                  _ -> Nothing
              , ccProofTree = ProofTree $ stdoutC ++ stderrC
              , ccUsedTime = t_u }
  