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"
_ | 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
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) =
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)