{- |
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 :: [String] -> String
parseStatus = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "Unknown" (Maybe String -> String)
-> ([String] -> Maybe String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe String -> Maybe String)
-> Maybe String -> [String] -> Maybe String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Maybe String -> Maybe String
parseStatusIfStatusline Maybe String
forall a. Maybe a
Nothing
  where
    parseStatusIfStatusline :: String -> Maybe String -> Maybe String
    parseStatusIfStatusline :: String -> Maybe String -> Maybe String
parseStatusIfStatusline line :: String
line mStatus :: Maybe String
mStatus = case Maybe String
mStatus of
      Nothing -> case () of
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Time limit" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "Timeout"
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Memory limit" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "MemoryOut"
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Refutation not found" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "GaveUp"
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Refutation" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "Theorem"
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Satisfiable" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "CounterSatisfiable" -- this is a model
        _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Termination reason: Unknown" String
line -> String -> Maybe String
forall a. a -> Maybe a
Just "Unknown"
        _ -> Maybe String
mStatus
      _ -> Maybe String
mStatus

parseTimeUsed :: [String] -> TimeOfDay
parseTimeUsed :: [String] -> TimeOfDay
parseTimeUsed = TimeOfDay -> Maybe TimeOfDay -> TimeOfDay
forall a. a -> Maybe a -> a
fromMaybe TimeOfDay
midnight (Maybe TimeOfDay -> TimeOfDay)
-> ([String] -> Maybe TimeOfDay) -> [String] -> TimeOfDay
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe TimeOfDay -> Maybe TimeOfDay)
-> Maybe TimeOfDay -> [String] -> Maybe TimeOfDay
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Maybe TimeOfDay -> Maybe TimeOfDay
parseTimeUsedIfTimeLine Maybe TimeOfDay
forall a. Maybe a
Nothing
  where
    parseTimeUsedIfTimeLine :: String -> Maybe TimeOfDay -> Maybe TimeOfDay
    parseTimeUsedIfTimeLine :: String -> Maybe TimeOfDay -> Maybe TimeOfDay
parseTimeUsedIfTimeLine line :: String
line mTime :: Maybe TimeOfDay
mTime = case Maybe TimeOfDay
mTime of
      Just _ -> Maybe TimeOfDay
mTime
      Nothing -> case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Time elapsed: " String
line of
        Just s :: String
s -> TimeOfDay -> Maybe TimeOfDay
forall a. a -> Maybe a
Just (TimeOfDay -> Maybe TimeOfDay) -> TimeOfDay -> Maybe TimeOfDay
forall a b. (a -> b) -> a -> b
$ String -> TimeOfDay
parseTimeOfDay (String -> TimeOfDay) -> String -> TimeOfDay
forall a b. (a -> b) -> a -> b
$
          (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (\ c :: Char
c -> Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.') (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
trimLeft String
s
        Nothing -> Maybe TimeOfDay
mTime

    parseTimeOfDay :: String -> TimeOfDay
    parseTimeOfDay :: String -> TimeOfDay
parseTimeOfDay s :: String
s = TimeOfDay :: Int -> Int -> Pico -> TimeOfDay
TimeOfDay
        { todHour :: Int
todHour = 0
        , todMin :: Int
todMin = 0
        , todSec :: Pico
todSec = Double -> Pico
forall a b. (Real a, Fractional b) => a -> b
realToFrac (String -> Double
forall a. Read a => String -> a
read String
s :: Double) }

data FilterState = Version | Separator | Proof deriving Int -> FilterState -> String -> String
[FilterState] -> String -> String
FilterState -> String
(Int -> FilterState -> String -> String)
-> (FilterState -> String)
-> ([FilterState] -> String -> String)
-> Show FilterState
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FilterState] -> String -> String
$cshowList :: [FilterState] -> String -> String
show :: FilterState -> String
$cshow :: FilterState -> String
showsPrec :: Int -> FilterState -> String -> String
$cshowsPrec :: Int -> FilterState -> String -> String
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 :: [String] -> [String]
filterProofLines lines :: [String]
lines = ([String], FilterState) -> [String]
forall a b. (a, b) -> a
fst (([String], FilterState) -> [String])
-> ([String], FilterState) -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> ([String], FilterState) -> ([String], FilterState))
-> ([String], FilterState) -> [String] -> ([String], FilterState)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> ([String], FilterState) -> ([String], FilterState)
addIfInProof ([], FilterState
Version) ([String] -> ([String], FilterState))
-> [String] -> ([String], FilterState)
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
tail [String]
lines
  where
    addIfInProof :: String -> ([String], FilterState) -> ([String], FilterState)
    addIfInProof :: String -> ([String], FilterState) -> ([String], FilterState)
addIfInProof line :: String
line (addedLines :: [String]
addedLines, state :: FilterState
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 FilterState
state of
        Version ->
          if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Version: " String
line
          then ([String]
addedLines, FilterState
Separator)
          else ([String]
addedLines, FilterState
state)
        Separator ->
          if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "------------------------------" String
line
          then ([String]
addedLines, FilterState
Proof)
          else ([String]
addedLines, FilterState
state)
        Proof -> (String
line String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
addedLines, FilterState
state)