{- |
Module      :  ./TPTP/Prover/ProofParser.hs
Description :  Parses a TPTP proof.
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.ProofParser ( axiomsFromProofObject
                               , graphFromProofObject
                               , filterProofLines
                               , findSZS
                               ) where

import TPTP.AS ( Annotated_formula (..)
               , Formula_role (..)
               , Annotations (..)
               , Source (..)
               , DAG_source (..)
               , External_source (..)
               , File_source (..)
               , Inference_record (..)
               , Parent_info (..)
               , Name (..)
               , formulaRole
               , annotations
               , name )
import TPTP.Parser (annotated_formula)
import TPTP.Pretty ()

import Common.DocUtils
import Common.ProofTree
import Common.Id (Token (..))

import Data.Data (toConstr)
import Data.List
import Data.List.Split (splitOn)
import Data.Maybe
import Data.Graph.Inductive.Graph
import qualified Data.HashMap.Strict as Map
import Text.ParserCombinators.Parsec

axiomsFromProofObject :: [String] -> ([String], [String])
axiomsFromProofObject :: [String] -> ([String], [String])
axiomsFromProofObject =
  (Either String Annotated_formula
 -> ([String], [String]) -> ([String], [String]))
-> ([String], [String])
-> [Either String Annotated_formula]
-> ([String], [String])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Either String Annotated_formula
-> ([String], [String]) -> ([String], [String])
addIfAxiom ([], []) ([Either String Annotated_formula] -> ([String], [String]))
-> ([String] -> [Either String Annotated_formula])
-> [String]
-> ([String], [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Either String Annotated_formula)
-> [String] -> [Either String Annotated_formula]
forall a b. (a -> b) -> [a] -> [b]
map String -> Either String Annotated_formula
parseFormulae ([String] -> [Either String Annotated_formula])
-> ([String] -> [String])
-> [String]
-> [Either String Annotated_formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
splitFormulae (String -> [String])
-> ([String] -> String) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
  where
    addIfAxiom :: Either String Annotated_formula
               -> ([String], [String]) -> ([String], [String])
    addIfAxiom :: Either String Annotated_formula
-> ([String], [String]) -> ([String], [String])
addIfAxiom formulaOrError :: Either String Annotated_formula
formulaOrError (axiomNames :: [String]
axiomNames, parserErrors :: [String]
parserErrors) =
      case Either String Annotated_formula
formulaOrError of
        Left err :: String
err -> ([String]
axiomNames, String
err String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
parserErrors)
        Right formula :: Annotated_formula
formula -> (Annotated_formula -> [String]
getAxiomName Annotated_formula
formula [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
axiomNames, [String]
parserErrors)

    getAxiomName :: Annotated_formula -> [String]
    getAxiomName :: Annotated_formula -> [String]
getAxiomName formula :: Annotated_formula
formula
      | Formula_role
Axiom <- Annotated_formula -> Formula_role
formulaRole Annotated_formula
formula
      , Annotations (Just (Source_external (ExtSrc_file (File_source _ (Just fileInfo :: Name
fileInfo))),_)) <- Annotated_formula -> Annotations
annotations Annotated_formula
formula
      = [Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
fileInfo]
      | Formula_role
Axiom <- Annotated_formula -> Formula_role
formulaRole Annotated_formula
formula
      = [Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ Annotated_formula -> Name
name Annotated_formula
formula]
      | Bool
otherwise
      = []

splitFormulae :: String -> [String]
splitFormulae :: String -> [String]
splitFormulae = [String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: String
s -> String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ").\n") ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn ").\n"

parseFormulae :: String -> Either String Annotated_formula
parseFormulae :: String -> Either String Annotated_formula
parseFormulae text :: String
text = case GenParser Char () Annotated_formula
-> () -> String -> String -> Either ParseError Annotated_formula
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser GenParser Char () Annotated_formula
forall st. CharParser st Annotated_formula
annotated_formula () "" String
text of
  Right formula :: Annotated_formula
formula -> Annotated_formula -> Either String Annotated_formula
forall a b. b -> Either a b
Right Annotated_formula
formula
  Left err :: ParseError
err -> String -> Either String Annotated_formula
forall a b. a -> Either a b
Left ("Warning: unable to parse proof:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                    "Formula in the proof: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
text String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                    "Error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ParseError -> String
forall a. Show a => a -> String
show ParseError
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")

graphFromProofObject :: [String] -> ProofTree
graphFromProofObject :: [String] -> ProofTree
graphFromProofObject l :: [String]
l = case (((([(Int, ProofGraphNode)], [(Int, Int, Int)]),
  (Int, HashMap String Int, [String]))
 -> Either String Annotated_formula
 -> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
     (Int, HashMap String Int, [String])))
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
    (Int, HashMap String Int, [String]))
-> [Either String Annotated_formula]
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
    (Int, HashMap String Int, [String]))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
    (Int, HashMap String Int, [String]))
addNode (([], []), (0, HashMap String Int
forall k v. HashMap k v
Map.empty,[])) ([Either String Annotated_formula]
 -> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
     (Int, HashMap String Int, [String])))
-> ([String] -> [Either String Annotated_formula])
-> [String]
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
    (Int, HashMap String Int, [String]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Either String Annotated_formula)
-> [String] -> [Either String Annotated_formula]
forall a b. (a -> b) -> [a] -> [b]
map String -> Either String Annotated_formula
parseFormulae ([String] -> [Either String Annotated_formula])
-> ([String] -> [String])
-> [String]
-> [Either String Annotated_formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
splitFormulae (String -> [String])
-> ([String] -> String) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines) [String]
l of
  ((ns :: [(Int, ProofGraphNode)]
ns, es :: [(Int, Int, Int)]
es),(_,_,[])) -> Gr ProofGraphNode Int -> ProofTree
ProofGraph (Gr ProofGraphNode Int -> ProofTree)
-> Gr ProofGraphNode Int -> ProofTree
forall a b. (a -> b) -> a -> b
$ [(Int, ProofGraphNode)]
-> [(Int, Int, Int)] -> Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Int, ProofGraphNode)]
ns [(Int, Int, Int)]
es
  _ -> String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
l
  where
    strName :: Name -> String
    strName :: Name -> String
strName (NameString t :: Token
t ) = Token -> String
tokStr Token
t
    strName (NameInteger i :: Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i
    strSentence :: Annotated_formula -> String
    strSentence :: Annotated_formula -> String
strSentence = Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (Annotated_formula -> Doc) -> Annotated_formula -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotated_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
    addNode :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]), (Int, Map.HashMap String Int,[String]))
            -> Either String Annotated_formula
            -> (([(Int, ProofGraphNode)], [(Int, Int, Int)]), (Int, Map.HashMap String Int,[String]))
    addNode :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
    (Int, HashMap String Int, [String]))
addNode ((_,_),(_,_,errs :: [String]
errs)) (Left err :: String
err) = (([],[]),(0,HashMap String Int
forall k v. HashMap k v
Map.empty,String
errString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
errs))
    addNode args :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
args@((nodeList :: [(Int, ProofGraphNode)]
nodeList,edgeList :: [(Int, Int, Int)]
edgeList),(index :: Int
index,keyIdMap :: HashMap String Int
keyIdMap,[])) (Right formula :: Annotated_formula
formula) =
      let forName :: String
forName = Name -> String
strName (Annotated_formula -> Name
name Annotated_formula
formula)
          forSentence :: String
forSentence = Annotated_formula -> String
strSentence Annotated_formula
formula
          (anons :: Int
anons,infrs :: [(Int, String)]
infrs,newEdges :: [(Int, Int, Int)]
newEdges) = Annotations -> (Int, [(Int, String)], [(Int, Int, Int)])
extractParentEdges (Annotated_formula -> Annotations
annotations Annotated_formula
formula) in
          if String
forName String -> HashMap String Int -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`Map.member` HashMap String Int
keyIdMap then (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
args else
          -- every formula introduces one sentence node but *at least* one inference node, i.e. its own origin inference and potential anonymous intermediates' inferences
          ((((Int, String) -> (Int, ProofGraphNode))
-> [(Int, String)] -> [(Int, ProofGraphNode)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i,infr :: String
infr)->(Int
i,String -> ProofGraphNode
forall a b. a -> Either a b
Left String
infr)) [(Int, String)]
infrs [(Int, ProofGraphNode)]
-> [(Int, ProofGraphNode)] -> [(Int, ProofGraphNode)]
forall a. [a] -> [a] -> [a]
++ (Int
index, (String, String) -> ProofGraphNode
forall a b. b -> Either a b
Right (String
forName,String
forSentence)) (Int, ProofGraphNode)
-> [(Int, ProofGraphNode)] -> [(Int, ProofGraphNode)]
forall a. a -> [a] -> [a]
: [(Int, ProofGraphNode)]
nodeList
          -- the origin inference of a sentence with index i has index -i-1
          , [(Int, Int, Int)]
newEdges [(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++ (-Int
indexInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Int
index,-1)(Int, Int, Int) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. a -> [a] -> [a]
:[(Int, Int, Int)]
edgeList)
          -- the anonymous sentences don't appear as nodes but their respective origin inferences have indices that need to be skipped nonetheless
          ,(Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
anons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
          -- collecting formula names this way makes it necessary to fold left!
          , String -> Int -> HashMap String Int -> HashMap String Int
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert String
forName Int
index HashMap String Int
keyIdMap
          , [] ))
      where
        extractParentEdges :: Annotations -> (Int,[(Int,String)],[(Int, Int, Int)])
        -- Computes number of nameless ancestors, list of all inference nodes and list of all origin relations described in annotation's source record,…
        extractParentEdges :: Annotations -> (Int, [(Int, String)], [(Int, Int, Int)])
extractParentEdges (Annotations (Just (src :: Source
src, _))) = Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences Source
src Int
index Int
index Maybe Int
forall a. Maybe a
Nothing
        -- if it exists, else there is nothing to report.
        extractParentEdges _ = (0,[],[])
        walkInferences :: Source -> Int -> Int -> Maybe Int -> (Int,[(Int,String)],[(Int, Int, Int)])
        -- Treats a list of parents/inferences as arguments to an inference for child and marks them accordingly
        walkInferences :: Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences (Source_many srcs :: Sources
srcs) child :: Int
child start :: Int
start _ =
          ((Int, Source)
 -> (Int, [(Int, String)], [(Int, Int, Int)])
 -> (Int, [(Int, String)], [(Int, Int, Int)]))
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> [(Int, Source)]
-> (Int, [(Int, String)], [(Int, Int, Int)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int, Source)
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> (Int, [(Int, String)], [(Int, Int, Int)])
collectInferences (0,[],[]) ([Int] -> Sources -> [(Int, Source)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] Sources
srcs)
            where
              collectInferences :: (Int,Source) -> (Int,[(Int,String)],[(Int,Int,Int)]) -> (Int,[(Int,String)],[(Int,Int,Int)])
              -- Collect inferences for each source in the list while letting them know of their legacy (child is theirs), the index from which they may count new intermediate inferences and their place in the argument list
              collectInferences :: (Int, Source)
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> (Int, [(Int, String)], [(Int, Int, Int)])
collectInferences (i :: Int
i,s :: Source
s) (oAnons :: Int
oAnons,oInfr :: [(Int, String)]
oInfr,oEdges :: [(Int, Int, Int)]
oEdges) =
                let (nAnons :: Int
nAnons,nInfr :: [(Int, String)]
nInfr,nEdges :: [(Int, Int, Int)]
nEdges) = Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences Source
s Int
child (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
oAnons) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
                 in (Int
nAnonsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oAnons, [(Int, String)]
nInfr [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [(Int, String)]
oInfr, [(Int, Int, Int)]
nEdges [(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int, Int)]
oEdges)
        -- We've found the name of a parent!
        walkInferences (Source_DAG (DAGS_name sname :: Name
sname)) child :: Int
child _ infrArg :: Maybe Int
infrArg =
          -- Again, the default should never be returned and if it is, the resulting cycle should stick out in the DAG
          let parent :: Int
parent = Int -> String -> HashMap String Int -> Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.lookupDefault Int
child (Name -> String
strName Name
sname) HashMap String Int
keyIdMap
           in (0,[],[(Int
parent, -Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1, Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 Maybe Int
infrArg)])
        -- infrule is child's birthplace, so record who was there!
        walkInferences (Source_DAG (DAGS_record (Inference_record infrule :: Token
infrule _ parents :: Inference_parents
parents))) child :: Int
child start :: Int
start infrArg :: Maybe Int
infrArg =
          let (nextNode :: Int
nextNode, nextStart :: Int
nextStart, anon :: Int
anon, aEdge :: [(Int, Int, Int)]
aEdge) =
                case Maybe Int
infrArg of
                  -- If this record has no place in an inference's argument list, it must be at top level in the annotation, so no other ancestors to record
                  Nothing -> (Int
child,Int
start,0,[])
                  -- Otherwise we know that child comes from here and whatever we find next (start+1) must be the iArg'th argument to infrule
                  Just iArg :: Int
iArg -> (Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,1,[(-Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
-2,-Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Int
iArg)])
              (nAnons :: Int
nAnons, nInfr :: [(Int, String)]
nInfr, nEdges :: [(Int, Int, Int)]
nEdges) =
                -- Find nextNode's parents' origins while remembering what the nextStart-ing node index is
                Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences (Sources -> Source
Source_many (Sources -> Source) -> Sources -> Source
forall a b. (a -> b) -> a -> b
$ (Parent_info -> Source) -> Inference_parents -> Sources
forall a b. (a -> b) -> [a] -> [b]
map (\(Parent_info src :: Source
src _) -> Source
src) Inference_parents
parents) Int
nextNode Int
nextStart Maybe Int
forall a. Maybe a
Nothing
           in (Int
anonInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nAnons,(-Int
nextNodeInt -> Int -> Int
forall a. Num a => a -> a -> a
-1, Token -> String
tokStr Token
infrule)(Int, String) -> [(Int, String)] -> [(Int, String)]
forall a. a -> [a] -> [a]
:[(Int, String)]
nInfr,[(Int, Int, Int)]
aEdge[(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++[(Int, Int, Int)]
nEdges)
        -- If the source is of any other shape, simply record it as origin of child
        walkInferences src :: Source
src child :: Int
child _ _ = (0,[(-Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Constr -> String
forall a. Show a => a -> String
show (Source -> Constr
forall a. Data a => a -> Constr
toConstr Source
src))],[])
    addNode a :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
a _ = (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
 (Int, HashMap String Int, [String]))
a

-- Find the SZS status line
findSZS :: [String] -> String
findSZS :: [String] -> String
findSZS = (String, Bool) -> String
forall a b. (a, b) -> a
fst ((String, Bool) -> String)
-> ([String] -> (String, Bool)) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Bool) -> String -> (String, Bool))
-> (String, Bool) -> [String] -> (String, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (String, Bool) -> String -> (String, Bool)
checkLine ("Could not determine SZS status", Bool
False)
  where
    checkLine :: (String, Bool) -> String -> (String, Bool)
    checkLine :: (String, Bool) -> String -> (String, Bool)
checkLine (szsStatusLine :: String
szsStatusLine, found :: Bool
found) line :: String
line =
      if Bool
found
      then (String
szsStatusLine, Bool
found)
      else if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Couldn't find " String
line
           then (String
line, Bool
found)
           else case String -> Maybe String
getSZSStatusWord String
line of
             Just szsStatus :: String
szsStatus -> (String
szsStatus, Bool
True)
             _ -> (String
szsStatusLine, Bool
found)

    getSZSStatusWord :: String -> Maybe String
    getSZSStatusWord :: String -> Maybe String
getSZSStatusWord line :: String
line = case String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$
      String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SZS status" (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line of
        [] -> Maybe String
forall a. Maybe a
Nothing
        w :: String
w : _ -> String -> Maybe String
forall a. a -> Maybe a
Just String
w

-- filters the lines of the proof
filterProofLines :: [String] -> [String]
filterProofLines :: [String] -> [String]
filterProofLines = ([String], Bool) -> [String]
forall a b. (a, b) -> a
fst (([String], Bool) -> [String])
-> ([String] -> ([String], Bool)) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ([String], Bool) -> ([String], Bool))
-> ([String], Bool) -> [String] -> ([String], Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> ([String], Bool) -> ([String], Bool)
addIfInProof ([], Bool
False)
  where
    addIfInProof :: String -> ([String], Bool) -> ([String], Bool)
    addIfInProof :: String -> ([String], Bool) -> ([String], Bool)
addIfInProof line :: String
line (addedLines :: [String]
addedLines, insideProof :: Bool
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 Bool
insideProof
      then if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "SZS output start" (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line
           then ([String]
addedLines, Bool
False)
           else (String
line String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
addedLines, Bool
insideProof)
      else if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "SZS output end" (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line
           then ([String]
addedLines, Bool
True)
           else ([String]
addedLines, Bool
insideProof)