{- |
Module      :  ./TPTP/Prover/EProver.hs
Description :  Interface for the E Theorem Prover.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017, Tom Kranz 2021-2022
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.SPASS.ProofParser (parseOutput) where

import TPTP.Sign

import Common.AS_Annotation
import Common.ProofTree (ProofGraphNode)
import Common.Utils

import Data.Char
import Data.List
import Data.Maybe
import Data.Time (TimeOfDay (..), midnight)

import Text.ParserCombinators.Parsec

parseOutput :: Named Sentence -- ^ the proof goal
            -> [String] -- ^ the SPASS process output
            -> (Maybe String, [String], Bool, TimeOfDay, Bool, [(Int, ProofGraphNode)], [(Int,Int,Int)])
               -- ^ (result, used axioms, output exists, used time, proof exists, proof clauses/inferences, clause/inference relations)
parseOutput :: Named Sentence
-> [String]
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
parseOutput namedGoal :: Named Sentence
namedGoal = ((Maybe String, [String], Bool, TimeOfDay, Bool,
  [(Int, ProofGraphNode)], [(Int, Int, Int)])
 -> String
 -> (Maybe String, [String], Bool, TimeOfDay, Bool,
     [(Int, ProofGraphNode)], [(Int, Int, Int)]))
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
-> [String]
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Maybe String, [String], Bool, TimeOfDay, Bool,
 [(Int, ProofGraphNode)], [(Int, Int, Int)])
-> String
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
parseIt (Maybe String
forall a. Maybe a
Nothing, [], Bool
False, TimeOfDay
midnight, Bool
False, [], [])
  where
    parseIt :: (Maybe String, [String], Bool, TimeOfDay, Bool, [(Int, ProofGraphNode)], [(Int,Int,Int)])
            -> String
            -> (Maybe String, [String], Bool, TimeOfDay, Bool, [(Int, ProofGraphNode)], [(Int,Int,Int)])
    parseIt :: (Maybe String, [String], Bool, TimeOfDay, Bool,
 [(Int, ProofGraphNode)], [(Int, Int, Int)])
-> String
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
parseIt (result :: Maybe String
result, axiomsUsed :: [String]
axiomsUsed, spass_start_passed :: Bool
spass_start_passed, timeUsed :: TimeOfDay
timeUsed, spass_proof_passed :: Bool
spass_proof_passed, clNodes :: [(Int, ProofGraphNode)]
clNodes, clEdges :: [(Int, Int, Int)]
clEdges) line :: String
line =
          ( case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SPASS beiseite: " String
line of
             r :: Maybe String
r@(Just _) | Bool
spass_start_passed -> Maybe String
r
             _ -> Maybe String
result
          , case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "Formulae used in the proof :" String
line of
             Just s :: String
s -> (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr Named Sentence
namedGoal) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
s
             Nothing -> [String]
axiomsUsed
          , Bool
spass_start_passed Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "SPASS-START" String
line
          , case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SPASS spent" String
line of
              Just s :: String
s | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "on the problem." String
line ->
                TimeOfDay -> Maybe TimeOfDay -> TimeOfDay
forall a. a -> Maybe a -> a
fromMaybe TimeOfDay
midnight (Maybe TimeOfDay -> TimeOfDay) -> Maybe TimeOfDay -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ String -> Maybe TimeOfDay
parseTimeOfDay (String -> Maybe TimeOfDay) -> String -> Maybe 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 -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c ".:") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
trimLeft String
s
              _ -> TimeOfDay
timeUsed
          , Bool
spass_proof_passed Bool -> Bool -> Bool
||  ("Here is a proof " String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
line)
          , case (Bool
spass_proof_passed, Either ParseError (Int, String, [Int], String)
parsedProofLine) of
              (True, Right (clId :: Int
clId, rule :: String
rule, _, clSntc :: String
clSntc)) -> [(Int
clId, (String, String) -> ProofGraphNode
forall a b. b -> Either a b
Right (Int -> String
forall a. Show a => a -> String
show Int
clId,String
clSntc)),(-Int
clIdInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,String -> ProofGraphNode
forall a b. a -> Either a b
Left String
rule)][(Int, ProofGraphNode)]
-> [(Int, ProofGraphNode)] -> [(Int, ProofGraphNode)]
forall a. [a] -> [a] -> [a]
++[(Int, ProofGraphNode)]
clNodes
              _ -> [(Int, ProofGraphNode)]
clNodes
          , case (Bool
spass_proof_passed, Either ParseError (Int, String, [Int], String)
parsedProofLine) of
              (True, Right (clId :: Int
clId, _, parents :: [Int]
parents, _)) -> [(Int
p, -Int
clIdInt -> Int -> Int
forall a. Num a => a -> a -> a
-1, Int
i) | (i :: Int
i,p :: Int
p) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Int]
parents] [(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++ (-Int
clIdInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Int
clId,-1)(Int, Int, Int) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. a -> [a] -> [a]
:[(Int, Int, Int)]
clEdges
              _ -> [(Int, Int, Int)]
clEdges
          ) where parsedProofLine :: Either ParseError (Int, String, [Int], String)
parsedProofLine = GenParser Char () (Int, String, [Int], String)
-> ()
-> String
-> String
-> Either ParseError (Int, String, [Int], String)
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser GenParser Char () (Int, String, [Int], String)
proofLine () "" String
line


proofLine :: Parser (Int, String, [Int], String)
proofLine :: GenParser Char () (Int, String, [Int], String)
proofLine = do
 Int
clauseId <- Parser Int
decimal
 Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '['
 Parser Int
decimal -- What's this?
 Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':'
 String
rule <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum
 ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ':')
 [Int]
parents <- (Parser Int
decimal Parser Int -> (Int -> Parser Int) -> Parser Int
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\d :: Int
d-> (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.') ParsecT String () Identity Char -> Parser Int -> Parser Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Int
decimal Parser Int -> Parser Int -> Parser Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> Parser Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
d)) Parser Int
-> ParsecT String () Identity Char
-> ParsecT String () Identity [Int]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
`sepBy` (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ',')
 String -> ParsecT String () Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "] "
 String
clSentence <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
 (Int, String, [Int], String)
-> GenParser Char () (Int, String, [Int], String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
clauseId, String
rule, [Int]
parents, String
clSentence) where
   decimal :: Parser Int
   decimal :: Parser Int
decimal = do
    String
n <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
    Int -> Parser Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Parser Int) -> Int -> Parser Int
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
n

parseTimeOfDay :: String -> Maybe TimeOfDay
parseTimeOfDay :: String -> Maybe TimeOfDay
parseTimeOfDay str :: String
str =
    case Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ':' String
str of
      [h :: String
h, m :: String
m, s :: String
s] -> TimeOfDay -> Maybe TimeOfDay
forall a. a -> Maybe a
Just TimeOfDay :: Int -> Int -> Pico -> TimeOfDay
TimeOfDay
        { todHour :: Int
todHour = String -> Int
forall a. Read a => String -> a
read String
h
        , todMin :: Int
todMin = String -> Int
forall a. Read a => String -> a
read String
m
        , 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) }
      _ -> Maybe TimeOfDay
forall a. Maybe a
Nothing