content: {- |
  Module      :  ./TPTP/Prover/Vampire/ProofParser.hs
  Description :  Parses a Vampire proof.
  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.Vampire.ProofParser ( parseStatus
                                         , parseTimeUsed
                                         , filterProofLines
                                         ) where
  
  import Common.Utils
  
  import Data.Char
  import Data.List hiding (lines)
  import Data.Maybe
  import Data.Time (TimeOfDay (..), midnight)
  import Prelude hiding (lines)
  
  parseStatus :: [String] -> String
  parseStatus = fromMaybe "Unknown" . foldr parseStatusIfStatusline Nothing
    where
      parseStatusIfStatusline :: String -> Maybe String -> Maybe String
      parseStatusIfStatusline line mStatus = case mStatus of
        Nothing -> case () of
          _ | isInfixOf "Termination reason: Time limit" line -> Just "Timeout"
          _ | isInfixOf "Termination reason: Memory limit" line -> Just "MemoryOut"
          _ | isInfixOf "Termination reason: Refutation not found" line -> Just "GaveUp"
          _ | isInfixOf "Termination reason: Refutation" line -> Just "Theorem"
          _ | isInfixOf "Termination reason: Satisfiable" line -> Just "CounterSatisfiable" -- this is a model
          _ | isInfixOf "Termination reason: Unknown" line -> Just "Unknown"
          _ -> mStatus
        _ -> mStatus
  
  parseTimeUsed :: [String] -> TimeOfDay
  parseTimeUsed = fromMaybe midnight . foldr parseTimeUsedIfTimeLine Nothing
    where
      parseTimeUsedIfTimeLine :: String -> Maybe TimeOfDay -> Maybe TimeOfDay
      parseTimeUsedIfTimeLine line mTime = case mTime of
        Just _ -> mTime
        Nothing -> case stripPrefix "Time elapsed: " line of
          Just s -> Just $ parseTimeOfDay $
            takeWhile (\ c -> isDigit c || c == '.') $ trimLeft s
          Nothing -> mTime
  
      parseTimeOfDay :: String -> TimeOfDay
      parseTimeOfDay s = TimeOfDay
          { todHour = 0
          , todMin = 0
          , todSec = realToFrac (read s :: Double) }
  
  data FilterState = Version | Separator | Proof deriving Show
  
  -- filters the lines of the proof
  -- The first line does not belong to the proof. The next lines before the
  -- "------------------------------" belong to the proof.
  -- Right after that separator, the version indicator appears.
  filterProofLines :: [String] -> [String]
  filterProofLines lines = fst $ foldr addIfInProof ([], Version) $ tail lines
    where
      addIfInProof :: String -> ([String], FilterState) -> ([String], FilterState)
      addIfInProof line (addedLines, state) =
        -- @state@ tells if the line is between "SZS output start/end".
        -- Since the lines are in reverse order (by foldr), we need to parse after
        -- the separator ("------------------------------").
        case state of
          Version ->
            if isPrefixOf "Version: " line
            then (addedLines, Separator)
            else (addedLines, state)
          Separator ->
            if isPrefixOf "------------------------------" line
            then (addedLines, Proof)
            else (addedLines, state)
          Proof -> (line : addedLines, state)
  