{- |

Module : ./TPTP/Prover/ProofParser.hs

Description : Parses a TPTP 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.ProofParser ( axiomsFromProofObject

, filterProofLines

, findSZS

) where

import TPTP.AS ( Annotated_formula

, Formula_role (..)

, Annotations (..)

, Source (..)

, External_source (..)

, File_source (..)

, formulaRole

, annotations )

import TPTP.Parser (annotated_formula)

import TPTP.Pretty ()

import Common.DocUtils

import Data.List

import Data.List.Split (splitOn)

import Data.Maybe

import Text.ParserCombinators.Parsec

axiomsFromProofObject :: [String] -> ([String], [String])

axiomsFromProofObject =

foldr addIfAxiom ([], []) . map parseFormulae . splitFormulae . unlines

where

splitFormulae :: String -> [String]

splitFormulae = init . map (\ s -> s ++ ").\n") . splitOn ").\n"

parseFormulae :: String -> Either String Annotated_formula

parseFormulae text = case runParser annotated_formula () "" text of

Right formula -> Right formula

Left err -> Left ("Warning: unable to parse proof:\n" ++

"Formula in the proof: " ++ text ++ "\n" ++

"Error: " ++ show err ++ "\n")

addIfAxiom :: Either String Annotated_formula

-> ([String], [String]) -> ([String], [String])

addIfAxiom formulaOrError (axiomNames, parserErrors) =

case formulaOrError of

Left err -> (axiomNames, err : parserErrors)

Right formula -> (getAxiomName formula ++ axiomNames, parserErrors)

getAxiomName :: Annotated_formula -> [String]

getAxiomName formula = case (formulaRole formula, annotations formula) of

(Axiom, (Annotations mAnnos)) -> case mAnnos of

Just (Source_external (ExtSrc_file (File_source _ (Just fileInfo))),_) ->

[show $ pretty fileInfo]

_ -> []

_ -> []

-- Find the SZS status line

findSZS :: [String] -> String

findSZS = fst . foldl' checkLine ("Could not determine SZS status", False)

where

checkLine :: (String, Bool) -> String -> (String, Bool)

checkLine (szsStatusLine, found) line =

if found

then (szsStatusLine, found)

else if isPrefixOf "Couldn't find " line

then (line, found)

else case getSZSStatusWord line of

Just szsStatus -> (szsStatus, True)

_ -> (szsStatusLine, found)

getSZSStatusWord :: String -> Maybe String

getSZSStatusWord line = case words $ fromMaybe "" $

stripPrefix "SZS status" $ dropWhile (`elem` "%# ") line of

[] -> Nothing

w : _ -> Just w

-- filters the lines of the proof

filterProofLines :: [String] -> [String]

filterProofLines = fst . foldr addIfInProof ([], False)

where

addIfInProof :: String -> ([String], Bool) -> ([String], Bool)

addIfInProof line (addedLines, insideProof) =

-- @insideProof@ tells if the line is between "SZS output start/end".

-- Since the lines are in reverse order (by foldr), we need to parse after

-- "SZS output end" and before "SZS output start".

if insideProof

then if isPrefixOf "SZS output start" $ dropWhile (`elem` "%# ") line

then (addedLines, False)

else (line : addedLines, insideProof)

else if isPrefixOf "SZS output end" $ dropWhile (`elem` "%# ") line

then (addedLines, True)

else (addedLines, insideProof)