{- |
Module      :  $Header$
Description :  Interface to the TPTP theorem prover via Darwin.
Copyright   :  (c) Heng Jiang, Uni Bremen 2004-2007
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Interface for the Darwin service, uses GUI.GenericATP.
See <http://spass.mpi-sb.mpg.de/> for details on SPASS, and
<http://combination.cs.uiowa.edu/Darwin/> for Darwin.
-}

module SoftFOL.ProveDarwin
  ( darwinProver
  , darwinCMDLautomaticBatch
  , darwinConsChecker
  , ProverBinary (..)
  , darwinExe
  , tptpProvers
  ) where

-- preliminary hacks for display of CASL models
import Logic.Prover

import SoftFOL.Sign
import SoftFOL.Translate
import SoftFOL.ProverState
import SoftFOL.EProver

import Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result
import Common.ProofTree
import Common.ProverTools
import Common.SZSOntology
import Common.Utils

import Data.Char (isDigit)
import Data.List
import Data.Maybe
import Data.Time (timeToTimeOfDay)
import Data.Time.Clock (secondsToDiffTime)

import Control.Monad (when)
import qualified Control.Concurrent as Concurrent

import System.Directory
import System.Process (waitForProcess, runInteractiveCommand,
                       runProcess, terminateProcess)
import System.IO (hGetContents, openFile, hClose, IOMode (WriteMode))

import Control.Exception as Exception

import GUI.GenericATP
import Interfaces.GenericATPState
import Proofs.BatchProcessing

import qualified Data.Map as Map
import qualified Data.Set as Set

-- * Prover implementation

data ProverBinary = Darwin | DarwinFD | EDarwin | EProver | Leo | IProver
  deriving (Enum, Bounded)

tptpProvers :: [ProverBinary]
tptpProvers = [minBound .. maxBound]

proverBinary :: ProverBinary -> String
proverBinary b = darwinExe b ++
  case b of
    Darwin -> "-non-fd"
    _ -> ""

darwinExe :: ProverBinary -> String
darwinExe b = case b of
  Darwin -> "darwin"
  DarwinFD -> "darwin"
  EDarwin -> "e-darwin"
  EProver -> "eprover"
  Leo -> "leo"
  IProver -> "iproveropt"

{- | The Prover implementation. First runs the batch prover (with
  graphical feedback), then starts the GUI prover. -}
darwinProver
  :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
darwinProver b = mkAutomaticProver (proverBinary b) () (darwinGUI b)
  $ darwinCMDLautomaticBatchAux b

darwinConsChecker
  :: ProverBinary -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
darwinConsChecker b = (mkConsChecker (proverBinary b) () $ consCheck b)
  { ccNeedsTimer = False }

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: ProverBinary  -- ^ the actual binary
  -> String -- ^ theory name
  -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun b thName = ATPFunctions
  { initialProverState = spassProverState
  , atpTransSenName = transSenName
  , atpInsertSentence = insertSentenceGen
  , goalOutput = showTPTPProblem thName
  , proverHelpText = "no help for darwin available"
  , batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT"
  , fileExtensions = FileExtensions
      { problemOutput = ".tptp"
      , proverOutput = ".spass"
      , theoryConfiguration = ".spcf" }
  , runProver = runDarwin b
  , createProverOptions = extraOpts }

-- ** GUI

{- |
  Invokes the generic prover GUI. SPASS specific functions are omitted by
  data type ATPFunctions.
-}
darwinGUI
  :: ProverBinary -- ^ the actual binary
  -> String -- ^ theory name
  -> Theory Sign Sentence ProofTree
  -- ^ theory consisting of a signature and sentences
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
  -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
darwinGUI b thName th freedefs =
    genericATPgui (atpFun b thName) True (proverBinary b) thName th
                  freedefs emptyProofTree

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the Darwin prover.
  Darwin specific functions are omitted by data type ATPFunctions.
-}
darwinCMDLautomaticBatch
  :: 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
  -- ^ theory consisting of a signature and sentences
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ 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 -}
darwinCMDLautomaticBatch = darwinCMDLautomaticBatchAux Darwin

darwinCMDLautomaticBatchAux
  :: ProverBinary -- ^ the actual binary
  -> 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
  -- ^ theory consisting of a signature and sentences
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ 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 -}
darwinCMDLautomaticBatchAux b inclProvedThs saveProblem_batch resultMVar
                        thName defTS th freedefs =
    genericCMDLautomaticBatch (atpFun b thName) inclProvedThs saveProblem_batch
        resultMVar (proverBinary b) thName
        (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

-- * Main prover functions

eproverOpts :: String -> String
eproverOpts verb = "-xAuto -tAuto --tptp3-format " ++ verb
  ++ " --memory-limit=2048 --soft-cpu-limit="

extras :: ProverBinary -> Bool -> String -> String
extras b cons tl = let
  tOut = " -to " ++ tl
  darOpt = "-pc false"
  fdOpt = darOpt ++ (if cons then " -pmtptp true" else "") ++ " -fd true"
  in case b of
    EProver -> eproverOpts (if cons then "-s" else "") ++ tl
    Leo -> "-t " ++ tl
    Darwin -> darOpt ++ tOut
    DarwinFD -> fdOpt ++ tOut
    EDarwin -> fdOpt ++ " -eq Axioms" ++ tOut
    IProver -> "--time_out_real " ++ tl ++ " --sat_mode true"

{- | Runs the Darwin service. The tactic script only contains a string for the
  time limit. -}
consCheck
  :: ProverBinary
  -> String
  -> TacticScript
  -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
  -> IO (CCStatus ProofTree)
consCheck b thName (TacticScript tl) tm freedefs = case tTarget tm of
    Theory sig nSens -> do
        let proverStateI = spassProverState sig (toNamedList nSens) freedefs
        prob <- showTPTPProblemM thName proverStateI []
        (exitCode, out, tUsed) <-
          runDarwinProcess (darwinExe b) False (extras b True tl) thName prob
        let outState = CCStatus
               { ccResult = Just True
               , ccProofTree = ProofTree $ unlines $ exitCode : out
               , ccUsedTime = timeToTimeOfDay $ secondsToDiffTime
                            $ toInteger tUsed }
        return $ if szsProved exitCode then outState else
                    outState
                    { ccResult = if szsDisproved exitCode then Just False
                                 else Nothing }

runDarwinProcess
  :: String -- ^ binary name
  -> Bool -- ^ save problem
  -> String -- ^ options
  -> String -- ^ filename without extension
  -> String -- ^ problem
  -> IO (String, [String], Int)
runDarwinProcess bin saveTPTP options tmpFileName prob = do
  let tmpFile = basename tmpFileName ++ ".tptp"
  when saveTPTP (writeFile tmpFile prob)
  noProg <- missingExecutableInPath bin
  if noProg then
    return (bin ++ " not found. Check your $PATH", [], -1)
    else do
    timeTmpFile <- getTempFile prob tmpFile
    (_, pout, perr) <-
      executeProcess bin (words options ++ [timeTmpFile]) ""
    let l = lines $ pout ++ perr
        (res, _, tUsed) = parseOutput l
    removeFile timeTmpFile
    return (res, l, tUsed)

mkGraph :: String -> IO ()
mkGraph f = do
 (_, cat, _) <- executeProcess "cat" [f] ""
 (_, tac, _) <- executeProcess "tac" [f] ""
 let ((p_set, (cs, axs)), res) =
      processProof (zipF proofInfo $ zipF conjectures axioms)
       (Set.empty, ([], [])) $ lines tac
     (aliases, _) = processProof alias Map.empty $ lines cat
     same_rank = intercalate "; " $ map (\ (_, n) -> 'v' : n) $
                 filter (\ (_, n) -> Set.member n p_set
                                && isNothing (Map.lookup n aliases)) $ cs ++ axs
 case res of
  Just s -> putStrLn s
  _ -> return ()
 writeFile "/tmp/graph.dot" $ unlines ["digraph {",
  "subgraph { rank = same; " ++ same_rank ++ " }",
  (\ (_, _, d, _) -> d) . fst $ processProof (digraph p_set aliases)
   (Set.empty, Set.empty, "", Map.empty) $ lines cat, "}"]

runEProverBuffered
  :: Bool -- ^ save problem
  -> Bool
  -> Bool
  -> String -- ^ options
  -> String -- ^ filename without extension
  -> String -- ^ problem
  -> IO (String, [String], Int)
runEProverBuffered saveTPTP graph fullgraph options tmpFileName prob = do
  s <- supportsProofObject
  let tmpFile = basename tmpFileName ++ ".tptp"
      useProofObject = s && not fullgraph
      bin = if useProofObject then "eprover"
            else "eproof"
  noProg <- missingExecutableInPath bin
  when saveTPTP (writeFile tmpFile prob)
  if noProg then return (bin ++ " not found. Check your $PATH", [], -1)
    else do
   (err, out) <-
      do
       timeTmpFile <- getTempFile prob tmpFile
       (_, out, err, _) <-
        if graph || fullgraph || not s then do
              bufferFile <- getTempFile "" "eprover-proof-buffer"
              buff <- openFile bufferFile WriteMode
              h <- runProcess bin (words options ++
                    ["--proof-object" | useProofObject] ++ [timeTmpFile])
                    Nothing Nothing Nothing (Just buff) (Just buff)
              (waitForProcess h >> removeFile timeTmpFile)
               `Exception.catch` (\ ThreadKilled -> terminateProcess h)
              hClose buff
              mkGraph bufferFile
              runInteractiveCommand $ unwords ["grep", "-e", "axiom",
               "-e", "SZS", bufferFile, "&&", "rm", "-f", bufferFile]
        else runInteractiveCommand $ unwords
             [bin, "--proof-object", options, timeTmpFile,
              "|", "grep", "-e", "axiom", "-e", "SZS",
               "&&", "rm", timeTmpFile]
       return (out, err)
   perr <- hGetContents err
   pout <- hGetContents out
   let l = lines $ perr ++ pout
       (res, _, tUsed) = parseOutput l
   return (res, l, tUsed)

runDarwin
  :: ProverBinary
  -> SoftFOLProverState
  {- ^ 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 SPTerm -- ^ goal to prove
  -> IO (ATPRetval, GenericConfig ProofTree)
     -- ^ (retval, configuration with proof status and complete output)
runDarwin b sps cfg saveTPTP thName nGoal = do
    let bin = darwinExe b
        (options, graph, fullgraph) = case b of
          EProver ->
           let w = extraOpts cfg
           in (filter (not . (\ e -> elem e ["--graph", "--full-graph"])) w,
               elem "--graph" w, elem "--full-graph" w)
          _ -> (extraOpts cfg, False, False)
        tl = maybe "10" show $ timeLimit cfg
        extraOptions = extras b False tl
        tmpFileName = thName ++ '_' : AS_Anno.senAttr nGoal
    prob <- showTPTPProblem thName sps nGoal
      $ options ++ ["Requested prover: " ++ bin]
    (exitCode, out, tUsed) <- case b of
      EProver -> runEProverBuffered saveTPTP graph fullgraph
                  extraOptions tmpFileName prob
      _ -> runDarwinProcess bin saveTPTP extraOptions tmpFileName prob
    axs <- case b of
            EProver | szsProved exitCode ||
                      szsDisproved exitCode ->
                         case processProof axioms [] out of
                          (l, Nothing) -> return $ map fst l
                          (_, Just err) -> do
                                            putStrLn err
                                            return $ getAxioms sps
            _ -> return $ getAxioms sps
    let ctime = timeToTimeOfDay $ secondsToDiffTime $ toInteger tUsed
        (err, retval) = case () of
          _ | szsProved exitCode -> (ATPSuccess, provedStatus)
          _ | szsDisproved exitCode -> (ATPSuccess, disProvedStatus)
          _ | szsTimeout exitCode ->
              (ATPTLimitExceeded, defaultProofStatus)
          _ | szsStopped exitCode ->
              (ATPBatchStopped, defaultProofStatus)
          _ -> (ATPError exitCode, defaultProofStatus)
        defaultProofStatus =
            (openProofStatus
            (AS_Anno.senAttr nGoal) bin emptyProofTree)
                       { usedTime = ctime
                       , tacticScript = TacticScript $ show ATPTacticScript
                        {tsTimeLimit = configTimeLimit cfg,
                         tsExtraOpts = options} }

        disProvedStatus = defaultProofStatus {goalStatus = Disproved}
        provedStatus = defaultProofStatus
          { goalName = AS_Anno.senAttr nGoal
          , goalStatus = Proved True
          , usedAxioms = axs
          , usedProver = bin
          , usedTime = timeToTimeOfDay $ secondsToDiffTime $ toInteger tUsed
          }
    return (err, cfg {proofStatus = retval,
                      resultOutput = case b of
                                      EProver -> reverse out
                                      _ -> out,
                      timeUsed = ctime })

getSZSStatusWord :: String -> Maybe String
getSZSStatusWord line = case words $ fromMaybe ""
    $ stripPrefix "SZS status" $ dropWhile (`elem` "%# ") line of
  [] -> Nothing
  w : _ -> Just w

parseOutput :: [String] -> (String, Bool, Int)
  -- ^ (exit code, status found, used time)
parseOutput = foldl' checkLine ("could not determine SZS status", False, -1)
  where checkLine (exCode, stateFound, to) line =
          if isPrefixOf "Couldn't find eprover" line
             || isInfixOf "darwin -h for further information" line
                -- error by running darwin.
            then (line, stateFound, to)
            else case getSZSStatusWord line of
                Just szsState | not stateFound ->
                  (szsState, True, to)
                _ -> if "CPU  Time" `isPrefixOf` line  -- get cpu time
                  then let time = case takeWhile isDigit $ last (words line) of
                             ds@(_ : _) -> read ds
                             _ -> to
                       in (exCode, stateFound, time)
                  else (exCode, stateFound, to)
