TPTP/Prover/ProofParser.hs

{- |
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)