{- |
Module      :  ./CASL/Zipperposition.hs
Description :  Zipperposition prover for CASL
Copyright   :  (c) Tom Kranz 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :
Stability   :  experimentatl
Portability :  non-portable (via GUI imports)

provides higher-order and first-order+induction prover for CASL

The FO+induction prover only works if all sort-generation constraints are
  introduced via free-datatype declarations. Higher-order mode can deal with
  anything by receiving any sort-generation constraints as second-order
  induction axioms.
  Currently limited by an inability to parse simultaneous (interdependent) data
  type declarations and annotations (e.g. axiom names).
-}
module CASL.Zipperposition (zipperpositionFreeFolProver, zipperpositionCFolProver) where

import CASL.Sublogic
import CASL.Sign
import CASL.Morphism
import CASL.AS_Basic_CASL
import CASL.ToTIP
import qualified TIP.AbsTIP as T
import TIP.Prover.Common
import TIP.Utils
import Logic.Prover
import Common.AS_Annotation
import Common.ProofTree
import qualified Common.Result as Result
import Interfaces.GenericATPState
import TPTP.Prover.ProofParser
import TPTP.Prover.Common (executeTheProver,atpRetValAndProofStatus')
import GUI.GenericATP
import Common.SZSOntology
import Control.Concurrent
import Data.List (foldl',break,stripPrefix)
import Data.Maybe (mapMaybe)
import Data.Time (timeToTimeOfDay,picosecondsToDiffTime)
import qualified Data.Set as Set
import qualified Data.IntMap.Strict as IM
import Text.Read (readMaybe)
import Proofs.BatchProcessing

data ZipperpositionMode = ZPMode
  { ZipperpositionMode -> String
name :: String
  , ZipperpositionMode -> CASL_Sublogics
sublogic :: CASL_Sublogics
  , ZipperpositionMode -> String
mode :: String
  , ZipperpositionMode -> [String]
options :: [String]
  }

zpFreeFOL :: ZipperpositionMode
zpFreeFOL :: ZipperpositionMode
zpFreeFOL = 
  String
-> CASL_Sublogics -> String -> [String] -> ZipperpositionMode
ZPMode 
    "Zipperposition (FOL+Induction)"
    (CASL_Sublogics
forall a. Lattice a => CASL_SL a
fol { cons_features :: SortGenerationFeatures
cons_features = Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
False Bool
False SortGenTotality
OnlyFree })
    "fo-complete-basic"
    ["--induction"]
zpCFOL :: ZipperpositionMode
zpCFOL :: ZipperpositionMode
zpCFOL =
  String
-> CASL_Sublogics -> String -> [String] -> ZipperpositionMode
ZPMode
    "Zipperposition (HOL)"
    CASL_Sublogics
forall a. Lattice a => CASL_SL a
cFol
    "best"
    []

zpQuirks :: TIPQuirks
zpQuirks :: TIPQuirks
zpQuirks = TIPQuirks
noTIPQuirks { noAnnotations :: Bool
noAnnotations = Bool
True, noPluralDatatype :: Bool
noPluralDatatype = Bool
True }

zipperpositionFreeFolProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionFreeFolProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionFreeFolProver = ZipperpositionMode
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionProver ZipperpositionMode
zpFreeFOL
zipperpositionCFolProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionCFolProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionCFolProver = ZipperpositionMode
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionProver ZipperpositionMode
zpCFOL

zipperpositionProver :: ZipperpositionMode -> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionProver :: ZipperpositionMode
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
zipperpositionProver md :: ZipperpositionMode
md =
  (String
-> CASL_Sublogics
-> (String
    -> Theory CASLSign CASLFORMULA ProofTree
    -> [FreeDefMorphism CASLFORMULA CASLMor]
    -> IO [ProofStatus ProofTree])
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate (ZipperpositionMode -> String
name ZipperpositionMode
md) (ZipperpositionMode -> CASL_Sublogics
sublogic ZipperpositionMode
md) ((String
  -> Theory CASLSign CASLFORMULA ProofTree
  -> [FreeDefMorphism CASLFORMULA CASLMor]
  -> IO [ProofStatus ProofTree])
 -> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree)
-> (String
    -> Theory CASLSign CASLFORMULA ProofTree
    -> [FreeDefMorphism CASLFORMULA CASLMor]
    -> IO [ProofStatus ProofTree])
-> Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
forall a b. (a -> b) -> a -> b
$ ZipperpositionMode
-> String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO [ProofStatus ProofTree]
zipperpositionGUI ZipperpositionMode
md)
    { proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus ProofTree])
   -> String
   -> TacticScript
   -> Theory CASLSign CASLFORMULA ProofTree
   -> [FreeDefMorphism CASLFORMULA CASLMor]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = (Bool
 -> Bool
 -> MVar (Result [ProofStatus ProofTree])
 -> String
 -> TacticScript
 -> Theory CASLSign CASLFORMULA ProofTree
 -> [FreeDefMorphism CASLFORMULA CASLMor]
 -> IO (ThreadId, MVar ()))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus ProofTree])
      -> String
      -> TacticScript
      -> Theory CASLSign CASLFORMULA ProofTree
      -> [FreeDefMorphism CASLFORMULA CASLMor]
      -> IO (ThreadId, MVar ()))
forall a. a -> Maybe a
Just ((Bool
  -> Bool
  -> MVar (Result [ProofStatus ProofTree])
  -> String
  -> TacticScript
  -> Theory CASLSign CASLFORMULA ProofTree
  -> [FreeDefMorphism CASLFORMULA CASLMor]
  -> IO (ThreadId, MVar ()))
 -> Maybe
      (Bool
       -> Bool
       -> MVar (Result [ProofStatus ProofTree])
       -> String
       -> TacticScript
       -> Theory CASLSign CASLFORMULA ProofTree
       -> [FreeDefMorphism CASLFORMULA CASLMor]
       -> IO (ThreadId, MVar ())))
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory CASLSign CASLFORMULA ProofTree
    -> [FreeDefMorphism CASLFORMULA CASLMor]
    -> IO (ThreadId, MVar ()))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus ProofTree])
      -> String
      -> TacticScript
      -> Theory CASLSign CASLFORMULA ProofTree
      -> [FreeDefMorphism CASLFORMULA CASLMor]
      -> IO (ThreadId, MVar ()))
forall a b. (a -> b) -> a -> b
$ ZipperpositionMode
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO (ThreadId, MVar ())
zipperpositionCMDLautomaticBatch ZipperpositionMode
md }

atpFun :: ZipperpositionMode
  -> String
  -> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [T.Decl]
atpFun :: ZipperpositionMode
-> String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
atpFun md :: ZipperpositionMode
md _thryName :: String
_thryName = 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 CASLSign CASLFORMULA CASLMor [Decl]
initialProverState = \ sig :: CASLSign
sig s :: [Named CASLFORMULA]
s _ -> (CASLSign, [Named CASLFORMULA]) -> [Decl]
tipSign (CASLSign
sig, [Named CASLFORMULA]
s) [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ (Named CASLFORMULA -> Decl) -> [Named CASLFORMULA] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Named CASLFORMULA -> Decl
tipAxiom ((Named CASLFORMULA -> Bool)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter Named CASLFORMULA -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named CASLFORMULA]
s),
      atpTransSenName :: TransSenName
atpTransSenName = TransSenName
forall a. a -> a
id,
      atpInsertSentence :: [Decl] -> Named CASLFORMULA -> [Decl]
atpInsertSentence = \ thry :: [Decl]
thry s :: Named CASLFORMULA
s -> [Decl]
thry [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA -> Decl
tipAxiom Named CASLFORMULA
s],
      goalOutput :: [Decl] -> Named CASLFORMULA -> [String] -> IO String
goalOutput = \ thry :: [Decl]
thry nGoal :: Named CASLFORMULA
nGoal _ -> do
            let tipTheory :: Start
tipTheory = [Decl] -> Start
T.Start [Decl]
thry
            let (tipProblem :: Start
tipProblem,_) = TIPQuirks -> Start -> Maybe Decl -> (Start, IntMap Int)
generateProblem TIPQuirks
noTIPQuirks Start
tipTheory (Maybe Decl -> (Start, IntMap Int))
-> Maybe Decl -> (Start, IntMap Int)
forall a b. (a -> b) -> a -> b
$ Decl -> Maybe Decl
forall a. a -> Maybe a
Just (Decl -> Maybe Decl) -> Decl -> Maybe Decl
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> Decl
tipAxiom Named CASLFORMULA
nGoal
            let tipProblemString :: String
tipProblemString = Start -> String
printTIP Start
tipProblem
            String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
tipProblemString,
      proverHelpText :: String
proverHelpText = "" ,
      batchTimeEnv :: String
batchTimeEnv = "HETS_ZIPPERPOSITION_BATCH_TIME_LIMIT",
      fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions {problemOutput :: String
problemOutput = ".smt2",
                                      proverOutput :: String
proverOutput = ".tptp",
                                      theoryConfiguration :: String
theoryConfiguration = ".none3"},
      runProver :: RunProver CASLFORMULA ProofTree [Decl]
runProver = ZipperpositionMode -> RunProver CASLFORMULA ProofTree [Decl]
runZipperposition ZipperpositionMode
md,
      createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = \cfg :: GenericConfig ProofTree
cfg ->
        [ "--input=tip"
        , "--output=tptp"
        , "--timeout=" 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)
        , "--mode=" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ZipperpositionMode -> String
mode ZipperpositionMode
md
        ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ZipperpositionMode -> [String]
options ZipperpositionMode
md [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg }

zipperpositionCMDLautomaticBatch :: ZipperpositionMode
        -> Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory CASLSign CASLFORMULA ProofTree {- ^ theory consisting of a
           signature and a list of named sentences -}
        -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
        -> IO (ThreadId, MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
zipperpositionCMDLautomaticBatch :: ZipperpositionMode
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO (ThreadId, MVar ())
zipperpositionCMDLautomaticBatch md :: ZipperpositionMode
md inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory CASLSign CASLFORMULA ProofTree
th freedefs :: [FreeDefMorphism CASLFORMULA CASLMor]
freedefs =
    ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> 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 (ZipperpositionMode
-> String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
atpFun ZipperpositionMode
md String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (ZipperpositionMode -> String
name ZipperpositionMode
md) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory CASLSign CASLFORMULA ProofTree
th [FreeDefMorphism CASLFORMULA CASLMor]
freedefs ProofTree
emptyProofTree

zipperpositionGUI :: ZipperpositionMode
  -> String -- ^ theory name
  -> Theory CASLSign CASLFORMULA ProofTree
  {- ^ theory consisting of a signature
  and a list of named sentences -}
  -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
  -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
zipperpositionGUI :: ZipperpositionMode
-> String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> IO [ProofStatus ProofTree]
zipperpositionGUI md :: ZipperpositionMode
md thName :: String
thName th :: Theory CASLSign CASLFORMULA ProofTree
th freedefs :: [FreeDefMorphism CASLFORMULA CASLMor]
freedefs =
  ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
-> Bool
-> String
-> String
-> Theory CASLSign CASLFORMULA ProofTree
-> [FreeDefMorphism CASLFORMULA CASLMor]
-> 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 (ZipperpositionMode
-> String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
atpFun ZipperpositionMode
md String
thName) Bool
True (ZipperpositionMode -> String
name ZipperpositionMode
md) String
thName Theory CASLSign CASLFORMULA ProofTree
th [FreeDefMorphism CASLFORMULA CASLMor]
freedefs ProofTree
emptyProofTree

runZipperposition :: ZipperpositionMode
  -> [T.Decl]
  {- ^ 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 theory file
  -> String -- ^ name of the theory in the DevGraph
  -> Named CASLFORMULA -- ^ goal to prove
  -> IO (ATPRetval, GenericConfig ProofTree)
runZipperposition :: ZipperpositionMode -> RunProver CASLFORMULA ProofTree [Decl]
runZipperposition md :: ZipperpositionMode
md state :: [Decl]
state cfg :: GenericConfig ProofTree
cfg saveFile :: Bool
saveFile thName :: String
thName nGoal :: Named CASLFORMULA
nGoal = do
  (problemFileName :: String
problemFileName,blame :: IntMap Int
blame) <-
    Start
-> GenericConfig ProofTree
-> Bool
-> String
-> Decl
-> TIPQuirks
-> String
-> IO (String, IntMap Int)
prepareProverInput ([Decl] -> Start
T.Start [Decl]
state) GenericConfig ProofTree
cfg Bool
saveFile String
thName (Named CASLFORMULA -> Decl
tipAxiom Named CASLFORMULA
nGoal) TIPQuirks
zpQuirks (ZipperpositionMode -> String
name ZipperpositionMode
md)
  let allOptions :: [String]
allOptions = ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
-> GenericConfig ProofTree -> [String]
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> GenericConfig proof_tree -> [String]
createProverOptions (ZipperpositionMode
-> String
-> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree [Decl]
atpFun ZipperpositionMode
md String
thName) GenericConfig ProofTree
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
problemFileName]
  (_, out :: [String]
out, wallTimeUsed :: TimeOfDay
wallTimeUsed) <-
    String -> [String] -> IO (ExitCode, [String], TimeOfDay)
executeTheProver "zipperposition" [String]
allOptions
  let szsStatusLine :: String
szsStatusLine = [String] -> String
findSZS [String]
out
  let reportedTimeUsed :: Integer
reportedTimeUsed = [String] -> Integer
parseTimeUsed [String]
out
  let resultedTimeUsed :: TimeOfDay
resultedTimeUsed =
        if Integer
reportedTimeUsed Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -1
        then TimeOfDay
wallTimeUsed
        else DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
picosecondsToDiffTime Integer
reportedTimeUsed
  let proofOut :: [String]
proofOut = [String] -> [String]
filterProofLines [String]
out
  let allAxiomNames :: Set String
allAxiomNames = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$ (Decl -> Maybe String) -> [Decl] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Decl -> Maybe String
getFormulaName [Decl]
state
  [String]
axiomsUsed <- if String -> Bool
szsProved String
szsStatusLine Bool -> Bool -> Bool
|| String -> Bool
szsDisproved String
szsStatusLine
                then case [String] -> ([String], [String])
axiomsFromProofObject [String]
proofOut of
                  (axiomNames :: [String]
axiomNames, []) -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$
                    (String -> Maybe String) -> [String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Set String -> [Decl] -> IntMap Int -> String -> Maybe String
mapAxiomName Set String
allAxiomNames [Decl]
state IntMap Int
blame) [String]
axiomNames
                  (_, errs :: [String]
errs) -> do
                    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
errs
                    [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ Set String -> [String]
forall a. Set a -> [a]
Set.toList Set String
allAxiomNames
                else [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ Set String -> [String]
forall a. Set a -> [a]
Set.toList Set String
allAxiomNames
  let proofGraph :: ProofTree
proofGraph = if String -> Bool
szsProved String
szsStatusLine Bool -> Bool -> Bool
|| String -> Bool
szsDisproved String
szsStatusLine
                then [String] -> ProofTree
graphFromProofObject [String]
proofOut
                else ProofStatus ProofTree -> ProofTree
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree (GenericConfig ProofTree -> ProofStatus ProofTree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig ProofTree
cfg)
  let (atpRetval :: ATPRetval
atpRetval, resultedProofStatus :: ProofStatus ProofTree
resultedProofStatus) =
        GenericConfig ProofTree
-> String
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus' GenericConfig ProofTree
cfg (Named CASLFORMULA -> String
forall s a. SenAttr s a -> a
senAttr Named CASLFORMULA
nGoal)
          TimeOfDay
resultedTimeUsed [String]
axiomsUsed
          String
szsStatusLine (ZipperpositionMode -> String
name ZipperpositionMode
md)
  (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
atpRetval, GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
resultedProofStatus { proofTree :: ProofTree
proofTree = ProofTree
proofGraph }
                         , resultOutput :: [String]
resultOutput = [String]
out
                         , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
resultedTimeUsed })

parseTimeUsed :: [String] -> Integer
parseTimeUsed :: [String] -> Integer
parseTimeUsed = (Integer, Bool) -> Integer
forall a b. (a, b) -> a
fst ((Integer, Bool) -> Integer)
-> ([String] -> (Integer, Bool)) -> [String] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Integer, Bool) -> String -> (Integer, Bool))
-> (Integer, Bool) -> [String] -> (Integer, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Integer, Bool) -> String -> (Integer, Bool)
checkLine (-1, Bool
False)
  where
    checkLine :: (Integer, Bool) -> String -> (Integer, Bool)
    checkLine :: (Integer, Bool) -> String -> (Integer, Bool)
checkLine unchanged :: (Integer, Bool)
unchanged@(_time :: Integer
_time, found :: Bool
found) line :: String
line
      | Bool
found
      = (Integer, Bool)
unchanged
      | ["%", "done", _iterations :: String
_iterations, "iterations", "in", secs :: String
secs] <- String -> [String]
words String
line
      , (sec :: String
sec, msecs :: String
msecs) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
=='.') String
secs
      , Just s :: Integer
s <- String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
sec
      , '.' : msec :: String
msec <- Int -> TransSenName
forall a. Int -> [a] -> [a]
take 4 String
msecs
      , Just ms :: Integer
ms <- String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
msec
      = (Integer
s Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* 10Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(12 :: Integer) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
ms Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* 10Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(9 :: Integer), Bool
True)
      | Bool
otherwise
      = (Integer, Bool)
unchanged

mapAxiomName :: Set.Set String -> [T.Decl] -> IM.IntMap Int -> String -> Maybe String
mapAxiomName :: Set String -> [Decl] -> IntMap Int -> String -> Maybe String
mapAxiomName allAx :: Set String
allAx thry :: [Decl]
thry blame :: IntMap Int
blame ax :: String
ax
  | String
ax String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
allAx
  = String -> Maybe String
forall a. a -> Maybe a
Just String
ax
  | Just n :: String
n <- String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "zf_stmt_" String
ax
  , Just lineN :: Int
lineN <- String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
n
  , Just originalLineN :: Int
originalLineN <- Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
lineN IntMap Int
blame
  , [Decl] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Decl]
thry Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
originalLineN
  = Decl -> Maybe String
getFormulaName ([Decl]
thry [Decl] -> Int -> Decl
forall a. [a] -> Int -> a
!! Int
lineN)
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing