{- |
Module      :  ./Proofs/BatchProcessing.hs
Description :  Batch processing functions.
Copyright   :  (c) Klaus Luettich, Rainer Grabbe 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Prover)

Functions for batch processing. Used by SoftFOL provers.
-}

module Proofs.BatchProcessing
  ( batchTimeLimit
  , isTimeLimitExceeded
  , adjustOrSetConfig
  , filterOpenGoals
  , checkGoal
  , goalProcessed
  , genericProveBatch
  , genericCMDLautomaticBatch
  ) where

import Logic.Prover

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import qualified Data.Map as Map
import Common.Result

import Data.List
import Data.Maybe

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

import Interfaces.GenericATPState

-- * Non-interactive Batch Prover

-- ** Constants

{- |
  Time limit used by the batch mode prover.
-}
batchTimeLimit :: Int
batchTimeLimit :: Int
batchTimeLimit = 20

-- ** Utility Functions

{- |
  Checks whether an ATPRetval indicates that the time limit was
  exceeded.
-}
isTimeLimitExceeded :: ATPRetval -> Bool
isTimeLimitExceeded :: ATPRetval -> Bool
isTimeLimitExceeded ATPTLimitExceeded = Bool
True
isTimeLimitExceeded _ = Bool
False


{- |
  Adjusts the configuration associated to a goal by applying the supplied
  function or inserts a new emptyConfig with the function applied if there's
  no configuration associated yet.

  Uses Map.member, Map.adjust, and Map.insert for the corresponding tasks
  internally.
-}
adjustOrSetConfig :: (Ord proof_tree) =>
                     (GenericConfig proof_tree -> GenericConfig proof_tree)
                     {- ^ function to be applied against the current
                     configuration or a new emptyConfig -}
                  -> String -- ^ name of the prover
                  -> ATPIdentifier -- ^ name of the goal
                  -> proof_tree -- ^ initial empty proof_tree
                  -> GenericConfigsMap proof_tree -- ^ current GenericConfigsMap
                  -> GenericConfigsMap proof_tree
                  -- ^ resulting GenericConfigsMap with the changes applied
adjustOrSetConfig :: (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
adjustOrSetConfig f :: GenericConfig proof_tree -> GenericConfig proof_tree
f prName :: String
prName k :: String
k pt :: proof_tree
pt m :: GenericConfigsMap proof_tree
m =
  if String -> GenericConfigsMap proof_tree -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
k GenericConfigsMap proof_tree
m then (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust GenericConfig proof_tree -> GenericConfig proof_tree
f String
k GenericConfigsMap proof_tree
m else
      String
-> GenericConfig proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k (GenericConfig proof_tree -> GenericConfig proof_tree
f (GenericConfig proof_tree -> GenericConfig proof_tree)
-> GenericConfig proof_tree -> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ String -> String -> proof_tree -> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig String
prName String
k proof_tree
pt) GenericConfigsMap proof_tree
m

filterOpenGoals :: GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
filterOpenGoals :: GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
filterOpenGoals = (GenericConfig proof_tree -> Bool)
-> GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((GenericConfig proof_tree -> Bool)
 -> GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree)
-> (GenericConfig proof_tree -> Bool)
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall a b. (a -> b) -> a -> b
$ GoalStatus -> Bool
isOpenGoal (GoalStatus -> Bool)
-> (GenericConfig proof_tree -> GoalStatus)
-> GenericConfig proof_tree
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus (ProofStatus proof_tree -> GoalStatus)
-> (GenericConfig proof_tree -> ProofStatus proof_tree)
-> GenericConfig proof_tree
-> GoalStatus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus

{- |
  Checks whether a goal in the results map is marked as proved.
-}
checkGoal :: GenericConfigsMap proof_tree -> ATPIdentifier -> Bool
checkGoal :: GenericConfigsMap proof_tree -> String -> Bool
checkGoal cfgMap :: GenericConfigsMap proof_tree
cfgMap goal :: String
goal =
  Bool
-> (GenericConfig proof_tree -> Bool)
-> Maybe (GenericConfig proof_tree)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat (ProofStatus proof_tree -> Bool)
-> (GenericConfig proof_tree -> ProofStatus proof_tree)
-> GenericConfig proof_tree
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus) (Maybe (GenericConfig proof_tree) -> Bool)
-> Maybe (GenericConfig proof_tree) -> Bool
forall a b. (a -> b) -> a -> b
$ String
-> GenericConfigsMap proof_tree -> Maybe (GenericConfig proof_tree)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
goal GenericConfigsMap proof_tree
cfgMap

-- ** Callbacks

{- |
  Called every time a goal has been processed in the batch mode.
-}

goalProcessed :: (Ord proof_tree) =>
                 Conc.MVar (GenericState sentence proof_tree pst)
                 -- ^ IORef pointing to the backing State data structure
              -> Int -- ^ batch time limit
              -> [String] -- ^ extra options
              -> Int -- class Unpair f where  Source^ total number of goals
              -> String -- ^ name of the prover
              -> Int -- ^ number of goals processed so far
              -> AS_Anno.Named sentence -- ^ goal that has just been processed
              -> Bool -- ^ wether to be verbose: print goal status (CMDL mode)
              -> (ATPRetval, GenericConfig proof_tree)
              -> IO Bool
goalProcessed :: MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
goalProcessed stateMVar :: MVar (GenericState sentence proof_tree pst)
stateMVar tLimit :: Int
tLimit extOpts :: [String]
extOpts numGoals :: Int
numGoals prName :: String
prName processedGoalsSoFar :: Int
processedGoalsSoFar
              nGoal :: Named sentence
nGoal verbose :: Bool
verbose (retval :: ATPRetval
retval, res_cfg :: GenericConfig proof_tree
res_cfg)
              = do
                (Bool, GoalStatus)
goalPair <- MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO (Bool, GoalStatus)
forall proof_tree sentence pst.
Ord proof_tree =>
MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO (Bool, GoalStatus)
goalProcRetVal MVar (GenericState sentence proof_tree pst)
stateMVar Int
tLimit [String]
extOpts
                            Int
numGoals String
prName Int
processedGoalsSoFar Named sentence
nGoal Bool
verbose (ATPRetval
retval, GenericConfig proof_tree
res_cfg)
                Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ (Bool, GoalStatus) -> Bool
forall a b. (a, b) -> a
fst (Bool, GoalStatus)
goalPair

-- same function as goalProcessed but it also returnes the goalStatus
goalProcRetVal :: (Ord proof_tree) =>
                 Conc.MVar (GenericState sentence proof_tree pst)
                 -- ^ IORef pointing to the backing State data structure
              -> Int -- ^ batch time limit
              -> [String] -- ^ extra options
              -> Int -- class Unpair f where  Source^ total number of goals
              -> String -- ^ name of the prover
              -> Int -- ^ number of goals processed so far
              -> AS_Anno.Named sentence -- ^ goal that has just been processed
              -> Bool -- ^ wether to be verbose: print goal status (CMDL mode)
              -> (ATPRetval, GenericConfig proof_tree)
              -> IO (Bool, GoalStatus)
goalProcRetVal :: MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO (Bool, GoalStatus)
goalProcRetVal stateMVar :: MVar (GenericState sentence proof_tree pst)
stateMVar tLimit :: Int
tLimit extOpts :: [String]
extOpts numGoals :: Int
numGoals prName :: String
prName processedGoalsSoFar :: Int
processedGoalsSoFar
              nGoal :: Named sentence
nGoal verbose :: Bool
verbose (retval :: ATPRetval
retval, res_cfg :: GenericConfig proof_tree
res_cfg) = do
  let n :: ProofStatus proof_tree
n = GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
res_cfg
  MVar (GenericState sentence proof_tree pst)
-> (GenericState sentence proof_tree pst
    -> IO (GenericState sentence proof_tree pst))
-> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
Conc.modifyMVar_ MVar (GenericState sentence proof_tree pst)
stateMVar ((GenericState sentence proof_tree pst
  -> IO (GenericState sentence proof_tree pst))
 -> IO ())
-> (GenericState sentence proof_tree pst
    -> IO (GenericState sentence proof_tree pst))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \ s :: GenericState sentence proof_tree pst
s -> GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenericState sentence proof_tree pst
 -> IO (GenericState sentence proof_tree pst))
-> GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
s
    { configsMap :: GenericConfigsMap proof_tree
configsMap = (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall proof_tree.
Ord proof_tree =>
(GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
adjustOrSetConfig (\ c :: GenericConfig proof_tree
c -> GenericConfig proof_tree
c
        { timeLimitExceeded :: Bool
timeLimitExceeded = ATPRetval -> Bool
isTimeLimitExceeded ATPRetval
retval
        , timeLimit :: Maybe Int
timeLimit = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
tLimit
        , extraOpts :: [String]
extraOpts = [String]
extOpts
        , proofStatus :: ProofStatus proof_tree
proofStatus = ProofStatus proof_tree
n { usedTime :: TimeOfDay
usedTime = GenericConfig proof_tree -> TimeOfDay
forall proof_tree. GenericConfig proof_tree -> TimeOfDay
timeUsed GenericConfig proof_tree
res_cfg}
        , resultOutput :: [String]
resultOutput = GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
resultOutput GenericConfig proof_tree
res_cfg
        , timeUsed :: TimeOfDay
timeUsed = GenericConfig proof_tree -> TimeOfDay
forall proof_tree. GenericConfig proof_tree -> TimeOfDay
timeUsed GenericConfig proof_tree
res_cfg
        }) String
prName (Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named sentence
nGoal) (GenericState sentence proof_tree pst -> proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> proof_tree
currentProofTree GenericState sentence proof_tree pst
s) (GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s)}
  let
    theGoalStatus :: GoalStatus
theGoalStatus = ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
n
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
verbose (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ case GoalStatus
theGoalStatus of
         Open _ -> "still open."
         Disproved -> "disproved."
         Proved _ -> "proved."
  (Bool, GoalStatus) -> IO (Bool, GoalStatus)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool, GoalStatus) -> IO (Bool, GoalStatus))
-> (Bool, GoalStatus) -> IO (Bool, GoalStatus)
forall a b. (a -> b) -> a -> b
$ case ATPRetval
retval of
    ATPError _ -> (Bool
False, GoalStatus
theGoalStatus)
    ATPBatchStopped -> (Bool
False, GoalStatus
theGoalStatus)
    _ -> (Int
numGoals Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
processedGoalsSoFar Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0, GoalStatus
theGoalStatus)

-- ** Implementation

{- |
  A non-GUI batch mode prover. The list of goals is processed sequentially.
  Proved goals are inserted as axioms.
-}
genericProveBatch :: (Show sentence, Ord sentence, Ord proof_tree) =>
                     Bool -- ^ True means use tLimit\/options from GenericState
                  -> Int -- ^ batch time limit
                  -> [String] -- ^ extra options passed
                  -> Bool -- ^ True means include proved theorems
                  -> Bool -- True means save problem file
                  -> (Int
                      -> AS_Anno.Named sentence
                      -> Maybe (AS_Anno.Named sentence)
                      -> (ATPRetval, GenericConfig proof_tree)
                      -> IO Bool)
                      {- ^ called after every prover run.
                      return True if you want the prover to continue. -}
                  -> (pst -> AS_Anno.Named sentence -> pst)
                      -- ^ inserts a Namend sentence into a logicalPart
                  -> RunProver sentence proof_tree pst -- prover to run batch
                  -> String -- ^ prover name
                  -> String -- ^ theory name
                  -> GenericState sentence proof_tree pst
                  -> Maybe (Conc.MVar (Result [ProofStatus proof_tree]))
                     -- ^ empty MVar to be filled after each proof attempt
                  -> IO [ProofStatus proof_tree]
                  -- ^ proof status for each goal
genericProveBatch :: Bool
-> Int
-> [String]
-> Bool
-> Bool
-> (Int
    -> Named sentence
    -> Maybe (Named sentence)
    -> (ATPRetval, GenericConfig proof_tree)
    -> IO Bool)
-> (pst -> Named sentence -> pst)
-> RunProver sentence proof_tree pst
-> String
-> String
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO [ProofStatus proof_tree]
genericProveBatch useStOpt :: Bool
useStOpt tLimit :: Int
tLimit extraOptions :: [String]
extraOptions inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch
                  afterEachProofAttempt :: Int
-> Named sentence
-> Maybe (Named sentence)
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
afterEachProofAttempt
                  inSen :: pst -> Named sentence -> pst
inSen runGivenProver :: RunProver sentence proof_tree pst
runGivenProver prName :: String
prName thName :: String
thName st :: GenericState sentence proof_tree pst
st resultMVar :: Maybe (MVar (Result [ProofStatus proof_tree]))
resultMVar =
    pst
-> Int
-> [ProofStatus proof_tree]
-> [Named sentence]
-> IO [ProofStatus proof_tree]
batchProve (GenericState sentence proof_tree pst -> pst
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> pst
proverState GenericState sentence proof_tree pst
st) 0 [] (GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
st)
  where
    openGoals :: GenericConfigsMap proof_tree
openGoals = GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
forall proof_tree.
GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
filterOpenGoals (GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
st)
    addToLP :: Named sentence -> ProofStatus proof_tree -> pst -> pst
addToLP g :: Named sentence
g res :: ProofStatus proof_tree
res pst :: pst
pst =
        if ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
res Bool -> Bool -> Bool
&& Bool
inclProvedThs
        then pst -> Named sentence -> pst
inSen pst
pst (Named sentence
g {isAxiom :: Bool
AS_Anno.isAxiom = Bool
True, wasTheorem :: Bool
AS_Anno.wasTheorem = Bool
True})
        else pst
pst
    batchProve :: pst
-> Int
-> [ProofStatus proof_tree]
-> [Named sentence]
-> IO [ProofStatus proof_tree]
batchProve _ _ resDone :: [ProofStatus proof_tree]
resDone [] = [ProofStatus proof_tree] -> IO [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return ([ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. [a] -> [a]
reverse [ProofStatus proof_tree]
resDone)
    batchProve pst :: pst
pst goalsProcessedSoFar :: Int
goalsProcessedSoFar resDone :: [ProofStatus proof_tree]
resDone (g :: Named sentence
g : gs :: [Named sentence]
gs) =
     let gName :: String
gName = Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named sentence
g
         pt :: proof_tree
pt = GenericState sentence proof_tree pst -> proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> proof_tree
currentProofTree GenericState sentence proof_tree pst
st
     in
      if String -> GenericConfigsMap proof_tree -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
gName GenericConfigsMap proof_tree
openGoals
      then do
        -- putStrLn $ "Trying to prove goal: " ++ gName
        let initEmptyCfg :: GenericConfig proof_tree
initEmptyCfg = String -> String -> proof_tree -> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig String
prName String
gName proof_tree
pt
            curCfg :: GenericConfig proof_tree
curCfg = GenericConfig proof_tree
-> String
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault GenericConfig proof_tree
initEmptyCfg String
gName GenericConfigsMap proof_tree
openGoals
            runConfig :: GenericConfig proof_tree
runConfig = GenericConfig proof_tree
initEmptyCfg
                { timeLimit :: Maybe Int
timeLimit = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$
                              if Bool
useStOpt then Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
tLimit (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$
                                                     GenericConfig proof_tree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig proof_tree
curCfg
                                          else Int
tLimit
                , extraOpts :: [String]
extraOpts = if Bool
useStOpt Bool -> Bool -> Bool
&& (Bool -> Bool
not (Bool -> Bool) -> ([String] -> Bool) -> [String] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig proof_tree
curCfg)
                                 then GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig proof_tree
curCfg
                                 else [String]
extraOptions }
        (err :: ATPRetval
err, res_cfg :: GenericConfig proof_tree
res_cfg) <-
              RunProver sentence proof_tree pst
runGivenProver pst
pst GenericConfig proof_tree
runConfig Bool
saveProblem_batch String
thName Named sentence
g
        {- putStrLn $ prName ++ " returned: " ++ (show err)
        if the batch prover runs in a separate thread
        that's killed via killThread
        runGivenProver will return ATPBatchStopped. We have to stop the
        recursion in that case
        add proved goals as axioms -}
        let res0 :: ProofStatus proof_tree
res0 = GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
res_cfg
            res :: ProofStatus proof_tree
res = ProofStatus proof_tree
res0 { proofLines :: [String]
proofLines = GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
resultOutput GenericConfig proof_tree
res_cfg,
              goalStatus :: GoalStatus
goalStatus = case ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
res0 of
                Open (Reason l :: [String]
l) | ATPRetval
err ATPRetval -> ATPRetval -> Bool
forall a. Eq a => a -> a -> Bool
== ATPRetval
ATPTLimitExceeded ->
                  Reason -> GoalStatus
Open ([String] -> Reason
Reason ([String] -> Reason) -> [String] -> Reason
forall a b. (a -> b) -> a -> b
$ "Timeout" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l)
                r :: GoalStatus
r -> GoalStatus
r }
            pst' :: pst
pst' = Named sentence -> ProofStatus proof_tree -> pst -> pst
forall proof_tree.
Named sentence -> ProofStatus proof_tree -> pst -> pst
addToLP Named sentence
g ProofStatus proof_tree
res pst
pst
            goalsProcessedSoFar' :: Int
goalsProcessedSoFar' = Int
goalsProcessedSoFar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
            ioProofStatus :: [ProofStatus proof_tree]
ioProofStatus = [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. [a] -> [a]
reverse (ProofStatus proof_tree
res ProofStatus proof_tree
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. a -> [a] -> [a]
: [ProofStatus proof_tree]
resDone)
        IO ()
-> (MVar (Result [ProofStatus proof_tree]) -> IO ())
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
              (\ rr :: MVar (Result [ProofStatus proof_tree])
rr -> do
                 Maybe (Result [ProofStatus proof_tree])
mOldVal <- MVar (Result [ProofStatus proof_tree])
-> IO (Maybe (Result [ProofStatus proof_tree]))
forall a. MVar a -> IO (Maybe a)
Conc.tryTakeMVar MVar (Result [ProofStatus proof_tree])
rr
                 let newRes :: Result [ProofStatus proof_tree]
newRes = [Diagnosis] -> Result ()
appendDiags (String -> ATPRetval -> [Diagnosis]
atpRetvalToDiags String
gName ATPRetval
err)
                              Result ()
-> Result [ProofStatus proof_tree]
-> Result [ProofStatus proof_tree]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenericState sentence proof_tree pst
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall sentence proof_tree pst.
(Ord sentence, Ord proof_tree) =>
GenericState sentence proof_tree pst
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
revertRenamingOfLabels GenericState sentence proof_tree pst
st [ProofStatus proof_tree
res]
                     -- transform new result in Monad Result
                     newVal :: Result [ProofStatus proof_tree]
newVal = (Result [ProofStatus proof_tree]
 -> Result [ProofStatus proof_tree])
-> (Result [ProofStatus proof_tree]
    -> Result [ProofStatus proof_tree]
    -> Result [ProofStatus proof_tree])
-> Maybe (Result [ProofStatus proof_tree])
-> Result [ProofStatus proof_tree]
-> Result [ProofStatus proof_tree]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Result [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall a. a -> a
id (([ProofStatus proof_tree]
 -> [ProofStatus proof_tree] -> [ProofStatus proof_tree])
-> Result [ProofStatus proof_tree]
-> Result [ProofStatus proof_tree]
-> Result [ProofStatus proof_tree]
forall a b c. (a -> b -> c) -> Result a -> Result b -> Result c
joinResultWith [ProofStatus proof_tree]
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. [a] -> [a] -> [a]
(++)) Maybe (Result [ProofStatus proof_tree])
mOldVal Result [ProofStatus proof_tree]
newRes
                     -- concat the oldValue with the new Result
                 MVar (Result [ProofStatus proof_tree])
-> Result [ProofStatus proof_tree] -> IO ()
forall a. MVar a -> a -> IO ()
Conc.putMVar MVar (Result [ProofStatus proof_tree])
rr Result [ProofStatus proof_tree]
newVal)
              Maybe (MVar (Result [ProofStatus proof_tree]))
resultMVar
        Bool
cont <- Int
-> Named sentence
-> Maybe (Named sentence)
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
afterEachProofAttempt Int
goalsProcessedSoFar' Named sentence
g
                         ((Named sentence -> Bool)
-> [Named sentence] -> Maybe (Named sentence)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String -> GenericConfigsMap proof_tree -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` GenericConfigsMap proof_tree
openGoals) (String -> Bool)
-> (Named sentence -> String) -> Named sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr) [Named sentence]
gs)
                         (ATPRetval
err, GenericConfig proof_tree
res_cfg)
        if Bool
cont
           then pst
-> Int
-> [ProofStatus proof_tree]
-> [Named sentence]
-> IO [ProofStatus proof_tree]
batchProve pst
pst' Int
goalsProcessedSoFar' (ProofStatus proof_tree
res ProofStatus proof_tree
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. a -> [a] -> [a]
: [ProofStatus proof_tree]
resDone) [Named sentence]
gs
           else [ProofStatus proof_tree] -> IO [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return [ProofStatus proof_tree]
ioProofStatus
      else pst
-> Int
-> [ProofStatus proof_tree]
-> [Named sentence]
-> IO [ProofStatus proof_tree]
batchProve (Named sentence -> ProofStatus proof_tree -> pst -> pst
forall proof_tree.
Named sentence -> ProofStatus proof_tree -> pst -> pst
addToLP Named sentence
g (GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus (GenericConfig proof_tree -> ProofStatus proof_tree)
-> GenericConfig proof_tree -> ProofStatus proof_tree
forall a b. (a -> b) -> a -> b
$
                                  GenericConfig proof_tree
-> String
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                                         (String -> String -> proof_tree -> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig String
prName String
gName proof_tree
pt)
                                         String
gName (GenericConfigsMap proof_tree -> GenericConfig proof_tree)
-> GenericConfigsMap proof_tree -> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
st) pst
pst)
                      Int
goalsProcessedSoFar [ProofStatus proof_tree]
resDone [Named sentence]
gs

atpRetvalToDiags :: String -- ^ name of goal
                 -> ATPRetval -> [Diagnosis]
atpRetvalToDiags :: String -> ATPRetval -> [Diagnosis]
atpRetvalToDiags gName :: String
gName err :: ATPRetval
err = case ATPRetval
err of
  ATPError msg :: String
msg ->
    [Diag :: DiagKind -> String -> Range -> Diagnosis
Diag { diagKind :: DiagKind
diagKind = DiagKind
Error, diagString :: String
diagString = String
msg, diagPos :: Range
diagPos = Range
Id.nullRange }]
  ATPTLimitExceeded ->
    [Diag :: DiagKind -> String -> Range -> Diagnosis
Diag { diagKind :: DiagKind
diagKind = DiagKind
Warning
          , diagString :: String
diagString = "Time limit exceeded (goal \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
gName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\")."
          , diagPos :: Range
diagPos = Range
Id.nullRange }]
  _ -> []

-- * Generic command line prover function

{- |
  Automatic command line prover using batch mode.
-}
genericCMDLautomaticBatch ::
        (Show sentence, Ord proof_tree, Ord sentence)
        => ATPFunctions sign sentence mor proof_tree pst {- ^ prover specific
                                                     functions -}
        -> Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> Conc.MVar (Result [ProofStatus proof_tree])
           -- ^ used to store the result of each attempt in the batch run
        -> String -- ^ prover name
        -> String -- ^ theory name
        -> ATPTacticScript -- ^ default prover specific tactic script
        -> Theory sign sentence proof_tree
           -- ^ theory consisting of a signature and a list of Named sentence
        -> [FreeDefMorphism sentence mor] -- ^ freeness constraints
        -> proof_tree -- ^ initial empty proof_tree
        -> IO (Conc.ThreadId, Conc.MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
genericCMDLautomaticBatch :: 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 atpFun :: ATPFunctions sign sentence mor proof_tree pst
atpFun inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus proof_tree])
resultMVar
                          prName :: String
prName thName :: String
thName defaultTacticScript :: ATPTacticScript
defaultTacticScript th :: Theory sign sentence proof_tree
th freedefs :: [FreeDefMorphism sentence mor]
freedefs pt :: proof_tree
pt = do
    -- putStrLn $ show defaultTacticScript
    let iGS :: GenericState sentence proof_tree pst
iGS = String
-> InitialProverState sign sentence mor pst
-> (String -> String)
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> GenericState sentence proof_tree pst
forall sentence proof_tree sign morphism pst.
(Ord sentence, Ord proof_tree) =>
String
-> InitialProverState sign sentence morphism pst
-> (String -> String)
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> proof_tree
-> GenericState sentence proof_tree pst
initialGenericState String
prName
                                  (ATPFunctions sign sentence mor proof_tree pst
-> InitialProverState sign sentence mor pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> InitialProverState sign sentence morphism pst
initialProverState ATPFunctions sign sentence mor proof_tree pst
atpFun)
                                  (ATPFunctions sign sentence mor proof_tree pst -> String -> String
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> String -> String
atpTransSenName ATPFunctions sign sentence mor proof_tree pst
atpFun) Theory sign sentence proof_tree
th [FreeDefMorphism sentence mor]
freedefs proof_tree
pt
    MVar (GenericState sentence proof_tree pst)
stateMVar <- GenericState sentence proof_tree pst
-> IO (MVar (GenericState sentence proof_tree pst))
forall a. a -> IO (MVar a)
Conc.newMVar GenericState sentence proof_tree pst
iGS
    let tLimit :: Int
tLimit = ATPTacticScript -> Int
tsTimeLimit ATPTacticScript
defaultTacticScript
        extOpts :: [String]
extOpts = ATPTacticScript -> [String]
tsExtraOpts ATPTacticScript
defaultTacticScript
        numGoals :: Int
numGoals = Map String (GenericConfig proof_tree) -> Int
forall k a. Map k a -> Int
Map.size (Map String (GenericConfig proof_tree) -> Int)
-> Map String (GenericConfig proof_tree) -> Int
forall a b. (a -> b) -> a -> b
$ Map String (GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
forall proof_tree.
GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
filterOpenGoals (Map String (GenericConfig proof_tree)
 -> Map String (GenericConfig proof_tree))
-> Map String (GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
iGS
    MVar ()
mvar <- IO (MVar ())
forall a. IO (MVar a)
Conc.newEmptyMVar
    ThreadId
threadID <- IO () -> IO ThreadId
Conc.forkIO
                 (Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
numGoals Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
                  (Bool
-> Int
-> [String]
-> Bool
-> Bool
-> (Int
    -> Named sentence
    -> Maybe (Named sentence)
    -> (ATPRetval, GenericConfig proof_tree)
    -> IO Bool)
-> (pst -> Named sentence -> pst)
-> RunProver sentence proof_tree pst
-> String
-> String
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO [ProofStatus proof_tree]
forall sentence proof_tree pst.
(Show sentence, Ord sentence, Ord proof_tree) =>
Bool
-> Int
-> [String]
-> Bool
-> Bool
-> (Int
    -> Named sentence
    -> Maybe (Named sentence)
    -> (ATPRetval, GenericConfig proof_tree)
    -> IO Bool)
-> (pst -> Named sentence -> pst)
-> RunProver sentence proof_tree pst
-> String
-> String
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO [ProofStatus proof_tree]
genericProveBatch Bool
True Int
tLimit [String]
extOpts Bool
inclProvedThs
                                      Bool
saveProblem_batch
                        (\ gPSF :: Int
gPSF nSen :: Named sentence
nSen _ conf :: (ATPRetval, GenericConfig proof_tree)
conf ->
                             MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
forall proof_tree sentence pst.
Ord proof_tree =>
MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
goalProcessed MVar (GenericState sentence proof_tree pst)
stateMVar Int
tLimit [String]
extOpts Int
numGoals
                                           String
prName Int
gPSF Named sentence
nSen Bool
True (ATPRetval, GenericConfig proof_tree)
conf)
                        (ATPFunctions sign sentence mor proof_tree pst
-> pst -> Named sentence -> pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> pst
atpInsertSentence ATPFunctions sign sentence mor proof_tree pst
atpFun) (ATPFunctions sign sentence mor proof_tree pst
-> RunProver sentence proof_tree pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> RunProver sentence proof_tree pst
runProver ATPFunctions sign sentence mor proof_tree pst
atpFun)
                        String
prName String
thName GenericState sentence proof_tree pst
iGS (MVar (Result [ProofStatus proof_tree])
-> Maybe (MVar (Result [ProofStatus proof_tree]))
forall a. a -> Maybe a
Just MVar (Result [ProofStatus proof_tree])
resultMVar)
                      IO [ProofStatus proof_tree] -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                   IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO a
`Exception.finally` MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
Conc.putMVar MVar ()
mvar ())
    (ThreadId, MVar ()) -> IO (ThreadId, MVar ())
forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
threadID, MVar ()
mvar)