{- |
Module      :  ./SoftFOL/ProveSPASS.hs
Description :  Interface for the SPASS theorem prover.
Copyright   :  (c) Rene Wagner, Klaus Luettich, Rainer Grabbe,
                   Uni Bremen 2005-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Interface for the SPASS theorem prover, uses GUI.GenericATP.
See <http://spass.mpi-sb.mpg.de/> for details on SPASS.

-}

{-
      - check if the theorem is used in the proof;
        if not, the theory is inconsistent;
        mark goal as proved and emmit a warning...

      - Implement a consistency checker based on GUI
-}

module SoftFOL.ProveSPASS (spassProver, spassProveCMDLautomaticBatch) where

import Logic.Prover

import SoftFOL.Sign
import SoftFOL.Translate
import SoftFOL.ProverState

import GUI.GenericATP
import Interfaces.GenericATPState
import Proofs.BatchProcessing

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result
import Common.ProofTree
import Common.Utils

import Control.Monad (when)
import qualified Control.Concurrent as Concurrent

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

-- * Prover implementation

{- |
  The Prover implementation.

  Implemented are: a prover GUI, and both commandline prover interfaces.
-}

spassName :: String
spassName :: String
spassName = "SPASS_SoftFOL"

spassProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
spassProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
spassProver = String
-> String
-> ()
-> (String
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence SoftFOLMorphism () ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver String
spassName String
spassName () String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
spassProveGUI
  Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
spassProveCMDLautomaticBatch

-- * Main prover functions

-- ** Utility functions

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ theory name
  -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun :: String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> TransSenName
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
    { initialProverState :: InitialProverState Sign Sentence SoftFOLMorphism SoftFOLProverState
initialProverState = InitialProverState Sign Sentence SoftFOLMorphism SoftFOLProverState
spassProverState
    , atpTransSenName :: TransSenName
atpTransSenName = TransSenName
transSenName
    , atpInsertSentence :: SoftFOLProverState -> Named Sentence -> SoftFOLProverState
atpInsertSentence = SoftFOLProverState -> Named Sentence -> SoftFOLProverState
insertSentenceGen
    , goalOutput :: SoftFOLProverState -> Named Sentence -> [String] -> IO String
goalOutput = String
-> SoftFOLProverState -> Named Sentence -> [String] -> IO String
showDFGProblem String
thName
    , proverHelpText :: String
proverHelpText = "http://www.spass-prover.org/\n"
    , batchTimeEnv :: String
batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT"
    , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
        { problemOutput :: String
problemOutput = ".dfg"
        , proverOutput :: String
proverOutput = ".spass"
        , theoryConfiguration :: String
theoryConfiguration = ".spcf"}
    , runProver :: RunProver Sentence ProofTree SoftFOLProverState
runProver = RunProver Sentence ProofTree SoftFOLProverState
runSpass
    , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
createSpassOptions }

{- |
  Parses a given default tactic script into a
  'Interfaces.GenericATPState.ATPTacticScript' if possible. Otherwise a default
  SPASS tactic script is returned.
-}
parseSpassTacticScript :: TacticScript
                        -> ATPTacticScript
parseSpassTacticScript :: TacticScript -> ATPTacticScript
parseSpassTacticScript =
    Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit ["-Stdin", "-DocProof"]

-- ** GUI

{- |
  Invokes the generic prover GUI. SPASS specific functions are omitted by
  data type ATPFunctions.
-}
spassProveGUI :: String -- ^ theory name
          -> Theory Sign Sentence ProofTree {- ^ theory consisting of a
             'SPASS.Sign.Sign' and a list of Named 'SPASS.Sign.Sentence' -}
          -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
          -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
spassProveGUI :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
spassProveGUI thName :: String
thName th :: Theory Sign Sentence ProofTree
th freedefs :: [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs =
    ATPFunctions
  Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
-> Bool
-> String
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun String
thName) Bool
True String
spassName String
thName Theory Sign Sentence ProofTree
th
                  [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
emptyProofTree

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the SPASS prover.
  SPASS specific functions are omitted by data type ATPFunctions.
-}
spassProveCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory Sign Sentence ProofTree {- ^ theory consisting of a
           'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence' -}
        -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
        -> IO (Concurrent.ThreadId, Concurrent.MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
spassProveCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
spassProveCMDLautomaticBatch inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory Sign Sentence ProofTree
th freedefs :: [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs =
    ATPFunctions
  Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch (String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar String
spassName String
thName
        (TacticScript -> ATPTacticScript
parseSpassTacticScript TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
emptyProofTree


-- * SPASS Interfacing Code

{- |
  Reads and parses the output of SPASS.
-}
parseSpassOutput :: [String] -- ^ the SPASS process output
                 -> (Maybe String, [String], Bool, TimeOfDay)
                    -- ^ (result, used axioms, complete output, used time)
parseSpassOutput :: [String] -> (Maybe String, [String], Bool, TimeOfDay)
parseSpassOutput = ((Maybe String, [String], Bool, TimeOfDay)
 -> String -> (Maybe String, [String], Bool, TimeOfDay))
-> (Maybe String, [String], Bool, TimeOfDay)
-> [String]
-> (Maybe String, [String], Bool, TimeOfDay)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Maybe String, [String], Bool, TimeOfDay)
-> String -> (Maybe String, [String], Bool, TimeOfDay)
parseIt (Maybe String
forall a. Maybe a
Nothing, [], Bool
False, TimeOfDay
midnight)
  where
    parseIt :: (Maybe String, [String], Bool, TimeOfDay)
-> String -> (Maybe String, [String], Bool, TimeOfDay)
parseIt (res :: Maybe String
res, usedAxs :: [String]
usedAxs, startFound :: Bool
startFound, tUsed :: TimeOfDay
tUsed) 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
startFound -> Maybe String
r
             _ -> Maybe String
res
          , 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 -> [String]
words String
s
             Nothing -> [String]
usedAxs
          , Bool
startFound 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) -> TransSenName
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 ".:")
                        TransSenName -> TransSenName
forall a b. (a -> b) -> a -> b
$ TransSenName
trimLeft String
s
              _ -> TimeOfDay
tUsed)

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

{- |
  Runs SPASS. SPASS is assumed to reside in PATH.
-}
runSpass :: SoftFOLProverState {- ^ logical part containing the input Sign and
                     axioms and possibly goals that have been proved
                     earlier as additional axioms -}
         -> GenericConfig ProofTree -- ^ configuration to use
         -> Bool -- ^ True means save DFG file
         -> String -- ^ name of the theory in the DevGraph
         -> AS_Anno.Named SPTerm -- ^ goal to prove
         -> IO (ATPRetval, GenericConfig ProofTree)
             -- ^ (retval, configuration with proof status and complete output)
runSpass :: RunProver Sentence ProofTree SoftFOLProverState
runSpass sps :: SoftFOLProverState
sps cfg :: GenericConfig ProofTree
cfg saveDFG :: Bool
saveDFG thName :: String
thName nGoal :: Named Sentence
nGoal = do
  let allOptions :: [String]
allOptions = "-Stdin" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: GenericConfig ProofTree -> [String]
createSpassOptions GenericConfig ProofTree
cfg
      extraOptions :: [String]
extraOptions = "-DocProof" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: GenericConfig ProofTree -> [String]
cleanOptions GenericConfig ProofTree
cfg
  String
prob <- String
-> SoftFOLProverState -> Named Sentence -> [String] -> IO String
showDFGProblem String
thName SoftFOLProverState
sps Named Sentence
nGoal (GenericConfig ProofTree -> [String]
createSpassOptions GenericConfig ProofTree
cfg)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveDFG
    (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile (TransSenName
basename String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ '_' Char -> TransSenName
forall a. a -> [a] -> [a]
: Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".dfg") String
prob
  (_, pout :: String
pout, _) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
spassName [String]
allOptions String
prob
  -- SPASS 3.7 does not properly stop, but fails with an exit code
  let out :: [String]
out = String -> [String]
lines String
pout
      (res :: Maybe String
res, usedAxs :: [String]
usedAxs, startFound :: Bool
startFound, tUsed :: TimeOfDay
tUsed) = [String] -> (Maybe String, [String], Bool, TimeOfDay)
parseSpassOutput [String]
out
      defaultProofStatus :: ProofStatus ProofTree
defaultProofStatus =
        (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus (Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal) String
spassName
                           ProofTree
emptyProofTree)
        {tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
          {tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg,
           tsExtraOpts :: [String]
tsExtraOpts = [String]
extraOptions} }
      (err :: ATPRetval
err, retval :: ProofStatus ProofTree
retval) = case Maybe String
res of
        Nothing -> (String -> ATPRetval
ATPError (String -> ATPRetval) -> String -> ATPRetval
forall a b. (a -> b) -> a -> b
$ "Found no SPASS "
          String -> TransSenName
forall a. [a] -> [a] -> [a]
++ if Bool
startFound then "result" else "output"
          , ProofStatus ProofTree
defaultProofStatus)
        Just str :: String
str
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Proof found." String
str ->
            (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultProofStatus
             { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved (Bool -> GoalStatus) -> Bool -> GoalStatus
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal) [String]
usedAxs
             , usedAxioms :: [String]
usedAxioms = (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
AS_Anno.senAttr Named Sentence
nGoal) [String]
usedAxs
             , proofTree :: ProofTree
proofTree = String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
spassProof [String]
out })
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Completion found." String
str ->
            (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultProofStatus
             { goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved } )
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Ran out of time." String
str ->
            (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultProofStatus)
        _ -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultProofStatus)
  (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
err, GenericConfig ProofTree
cfg
    { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
retval
    , resultOutput :: [String]
resultOutput = [String]
out
    , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
tUsed })

{- |
  Creates a list of all options the SPASS prover runs with.
  That includes the defaults -DocProof and -Timelimit.
-}
createSpassOptions :: GenericConfig ProofTree -> [String]
createSpassOptions :: GenericConfig ProofTree -> [String]
createSpassOptions cfg :: GenericConfig ProofTree
cfg =
    GenericConfig ProofTree -> [String]
cleanOptions GenericConfig ProofTree
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["-DocProof", "-TimeLimit="
                             String -> TransSenName
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg)]

{- |
  Filters extra options and just returns the non standard options.
-}
cleanOptions :: GenericConfig ProofTree -> [String]
cleanOptions :: GenericConfig ProofTree -> [String]
cleanOptions cfg :: GenericConfig ProofTree
cfg =
    (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ opt :: String
opt -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
opt) [String]
filterOptions)
           (GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg)
    where
      filterOptions :: [String]
filterOptions = ["-DocProof", "-Stdin", "-TimeLimit"]

{- |
  Extract proof tree from SPASS output. This will be the String between
  "Here is a proof" and "Formulae used in the proof"
-}
spassProof :: [String] -- ^ SPASS output containing proof tree
           -> String -- ^ extracted proof tree
spassProof :: [String] -> String
spassProof =
        [String] -> String
unlines ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Formulae used in the proof")
             ([String] -> [String])
-> ([String] -> [String]) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ l :: [String]
l -> if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
l then [String]
l else [String] -> [String]
forall a. [a] -> [a]
tail [String]
l)
             ([String] -> [String])
-> ([String] -> [String]) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Here is a proof with depth")