{- |
Module      :  ./Interfaces/GenericATPState.hs
Description :  Help functions for GUI.GenericATP
Copyright   :  (c) Klaus Luettich, Rainer Grabbe, Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (regex-base needs MPTC+FD)

Data structures and initialising functions for Prover state and configurations.
Used by GUI.GenericATP.

-}

module Interfaces.GenericATPState where

import Logic.Prover

import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Common.OrderedMap as OMap
import qualified Common.AS_Annotation as AS_Anno
import Common.ProofTree
import Common.ProofUtils
import Common.Result
import Common.Id
import Common.Doc
import Common.Utils

import Data.Maybe (fromMaybe)
import Data.Time (TimeOfDay, midnight)

import Control.Monad
import qualified Control.Exception as Exception

-- * Data Structures

type ATPIdentifier = String

data GenericConfig proof_tree = GenericConfig {
    {- | Time limit in seconds passed
    to prover via extra option. Default will be used if Nothing. -}
    GenericConfig proof_tree -> Maybe Int
timeLimit :: Maybe Int,
    -- | True if timelimit exceeded during last prover run.
    GenericConfig proof_tree -> Bool
timeLimitExceeded :: Bool,
    {- | Extra options passed verbatimely to prover.
    -DocProof, -Stdin, and -TimeLimit will be overridden. -}
    GenericConfig proof_tree -> [String]
extraOpts :: [String],
    -- | Represents the result of a prover run.
    GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus :: ProofStatus proof_tree,
    GenericConfig proof_tree -> [String]
resultOutput :: [String],
    -- | global time used in milliseconds
    GenericConfig proof_tree -> TimeOfDay
timeUsed :: TimeOfDay
    } deriving (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
(GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> Eq (GenericConfig proof_tree)
forall proof_tree.
Eq proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c/= :: forall proof_tree.
Eq proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
== :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c== :: forall proof_tree.
Eq proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
Eq, Eq (GenericConfig proof_tree)
Eq (GenericConfig proof_tree) =>
(GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering)
-> (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> (GenericConfig proof_tree -> GenericConfig proof_tree -> Bool)
-> (GenericConfig proof_tree
    -> GenericConfig proof_tree -> GenericConfig proof_tree)
-> (GenericConfig proof_tree
    -> GenericConfig proof_tree -> GenericConfig proof_tree)
-> Ord (GenericConfig proof_tree)
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering
GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall proof_tree. Ord proof_tree => Eq (GenericConfig proof_tree)
forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering
forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
min :: GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
$cmin :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
max :: GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
$cmax :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree
-> GenericConfig proof_tree -> GenericConfig proof_tree
>= :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c>= :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
> :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c> :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
<= :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c<= :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
< :: GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
$c< :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Bool
compare :: GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering
$ccompare :: forall proof_tree.
Ord proof_tree =>
GenericConfig proof_tree -> GenericConfig proof_tree -> Ordering
$cp1Ord :: forall proof_tree. Ord proof_tree => Eq (GenericConfig proof_tree)
Ord, Int -> GenericConfig proof_tree -> ShowS
[GenericConfig proof_tree] -> ShowS
GenericConfig proof_tree -> String
(Int -> GenericConfig proof_tree -> ShowS)
-> (GenericConfig proof_tree -> String)
-> ([GenericConfig proof_tree] -> ShowS)
-> Show (GenericConfig proof_tree)
forall proof_tree.
Show proof_tree =>
Int -> GenericConfig proof_tree -> ShowS
forall proof_tree.
Show proof_tree =>
[GenericConfig proof_tree] -> ShowS
forall proof_tree.
Show proof_tree =>
GenericConfig proof_tree -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenericConfig proof_tree] -> ShowS
$cshowList :: forall proof_tree.
Show proof_tree =>
[GenericConfig proof_tree] -> ShowS
show :: GenericConfig proof_tree -> String
$cshow :: forall proof_tree.
Show proof_tree =>
GenericConfig proof_tree -> String
showsPrec :: Int -> GenericConfig proof_tree -> ShowS
$cshowsPrec :: forall proof_tree.
Show proof_tree =>
Int -> GenericConfig proof_tree -> ShowS
Show)

{- |
  Creates an empty GenericConfig with a given goal name.
  Default time limit, no resultOutput and no extra options.
-}
emptyConfig :: (Ord proof_tree) =>
               String -- ^ name of the prover
            -> String -- ^ name of the goal
            -> proof_tree -- ^ initial empty proof_tree
            -> GenericConfig proof_tree
emptyConfig :: String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig prName :: String
prName n :: String
n pt :: proof_tree
pt =
    GenericConfig :: forall proof_tree.
Maybe Int
-> Bool
-> [String]
-> ProofStatus proof_tree
-> [String]
-> TimeOfDay
-> GenericConfig proof_tree
GenericConfig {timeLimit :: Maybe Int
timeLimit = Maybe Int
forall a. Maybe a
Nothing,
                   timeLimitExceeded :: Bool
timeLimitExceeded = Bool
False,
                   extraOpts :: [String]
extraOpts = [],
                   proofStatus :: ProofStatus proof_tree
proofStatus = String -> String -> proof_tree -> ProofStatus proof_tree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
n String
prName proof_tree
pt,
                   resultOutput :: [String]
resultOutput = [],
                   timeUsed :: TimeOfDay
timeUsed = TimeOfDay
midnight
                  }

{- |
  Performs a lookup on the ConfigsMap. Returns the config for the goal or an
  empty config if none is set yet.
-}
getConfig :: (Ord proof_tree) =>
             String -- ^ name of the prover
          -> ATPIdentifier -- ^ name of the goal
          -> proof_tree -- ^ initial empty proof_tree
          -> GenericConfigsMap proof_tree
          -> GenericConfig proof_tree
getConfig :: String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree
getConfig prName :: String
prName genid :: String
genid pt :: proof_tree
pt m :: GenericConfigsMap proof_tree
m = GenericConfig proof_tree
-> Maybe (GenericConfig proof_tree) -> GenericConfig proof_tree
forall a. a -> Maybe a -> a
fromMaybe (String -> String -> proof_tree -> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig String
prName String
genid proof_tree
pt) Maybe (GenericConfig proof_tree)
lookupId
  where
    lookupId :: Maybe (GenericConfig proof_tree)
lookupId = String
-> GenericConfigsMap proof_tree -> Maybe (GenericConfig proof_tree)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
genid GenericConfigsMap proof_tree
m

{- |
  We need to store one GenericConfig per goal.
-}
type GenericConfigsMap proof_tree = Map.Map ATPIdentifier
                                            (GenericConfig proof_tree)

{- |
  New goal name mapped to old goal name
-}
type GenericGoalNameMap = Map.Map String String

{- |
  Represents the global state of the prover GUI.
-}
data GenericState sentence proof_tree pst = GenericState {
    -- | currently selected goal or Nothing
    GenericState sentence proof_tree pst -> Maybe String
currentGoal :: Maybe ATPIdentifier,
    -- | initial empty proof_tree
    GenericState sentence proof_tree pst -> proof_tree
currentProofTree :: proof_tree,
    {- | stores the prover configurations for each goal
    and the results retrieved by running prover for each goal -}
    GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap :: GenericConfigsMap proof_tree,
    {- | stores a mapping from the ATP compliant
    labels to the original labels for all goals -}
    GenericState sentence proof_tree pst -> GenericGoalNameMap
namesMap :: GenericGoalNameMap,
    -- | list of all goals
    GenericState sentence proof_tree pst -> [Named sentence]
goalsList :: [AS_Anno.Named sentence],
    -- | logical part without theorems
    GenericState sentence proof_tree pst -> pst
proverState :: pst
  }

{- |
  Initialising the specific prover state containing logical part.
-}
type InitialProverState sign sentence morphism pst =
  sign -> [AS_Anno.Named sentence] -> [FreeDefMorphism sentence morphism] -> pst
type TransSenName = String -> String

{- |
  Creates an initial GenericState around a Theory.
-}
initialGenericState
    :: (Ord sentence, Ord proof_tree)
    => String -- ^ name of the prover
    -> InitialProverState sign sentence morphism pst
    -> TransSenName
    -> Theory sign sentence proof_tree
    -> [FreeDefMorphism sentence morphism] -- ^ freeness constraints
    -> proof_tree -- ^ initial empty proof_tree
    -> GenericState sentence proof_tree pst
initialGenericState :: String
-> InitialProverState sign sentence morphism pst
-> ShowS
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> proof_tree
-> GenericState sentence proof_tree pst
initialGenericState prName :: String
prName ips :: InitialProverState sign sentence morphism pst
ips trSenName :: ShowS
trSenName th :: Theory sign sentence proof_tree
th freedefs :: [FreeDefMorphism sentence morphism]
freedefs pt :: proof_tree
pt =
    GenericState :: forall sentence proof_tree pst.
Maybe String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericGoalNameMap
-> [Named sentence]
-> pst
-> GenericState sentence proof_tree pst
GenericState {currentGoal :: Maybe String
currentGoal = Maybe String
forall a. Maybe a
Nothing,
                  currentProofTree :: proof_tree
currentProofTree = proof_tree
pt,
                  configsMap :: GenericConfigsMap proof_tree
configsMap = [(String, GenericConfig proof_tree)]
-> GenericConfigsMap proof_tree
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, GenericConfig proof_tree)]
 -> GenericConfigsMap proof_tree)
-> [(String, GenericConfig proof_tree)]
-> GenericConfigsMap proof_tree
forall a b. (a -> b) -> a -> b
$
                               (SenAttr sentence String -> (String, GenericConfig proof_tree))
-> [SenAttr sentence String]
-> [(String, GenericConfig proof_tree)]
forall a b. (a -> b) -> [a] -> [b]
map (\ g :: SenAttr sentence String
g ->
                                        let gName :: String
gName = SenAttr sentence String -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr SenAttr sentence String
g
                                            ec :: GenericConfig proof_tree
ec = 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
                                        in (String
gName, GenericConfig proof_tree
ec {proofStatus :: ProofStatus proof_tree
proofStatus =
                       ProofStatus proof_tree -> String -> ProofStatus proof_tree
forall proof_tree.
ProofStatus proof_tree -> String -> ProofStatus proof_tree
updateTacticScript (GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
ec) String
gName}))
                                   [SenAttr sentence String]
goals,
                  namesMap :: GenericGoalNameMap
namesMap = [SenAttr sentence String]
-> [SenAttr sentence String] -> GenericGoalNameMap
forall a. [Named a] -> [Named a] -> GenericGoalNameMap
collectNameMapping [SenAttr sentence String]
nSens [SenAttr sentence String]
oSens',
                  goalsList :: [SenAttr sentence String]
goalsList = [SenAttr sentence String]
goals,
                  proverState :: pst
proverState = InitialProverState sign sentence morphism pst
ips sign
sign [SenAttr sentence String]
oSens' [FreeDefMorphism sentence morphism]
freedefs
                 }
    where Theory sign :: sign
sign oSens :: ThSens sentence (ProofStatus proof_tree)
oSens = Theory sign sentence proof_tree
th
          {- Search in list of ProofStatus for first occurence of an Open goal
          with non-empty TacticScript and update TacticScript if found. -}
          updateTacticScript :: ProofStatus proof_tree -> String -> ProofStatus proof_tree
updateTacticScript prStat :: ProofStatus proof_tree
prStat gn :: String
gn =
            ProofStatus proof_tree
-> (SenStatus sentence (ProofStatus proof_tree)
    -> ProofStatus proof_tree)
-> Maybe (SenStatus sentence (ProofStatus proof_tree))
-> ProofStatus proof_tree
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ProofStatus proof_tree
prStat
                  (\ senSt :: SenStatus sentence (ProofStatus proof_tree)
senSt ->
                    let validThmStatus :: [ProofStatus proof_tree]
validThmStatus = (ProofStatus proof_tree -> Bool)
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ tStatus :: ProofStatus proof_tree
tStatus ->
                            GoalStatus -> Bool
isOpenGoal (ProofStatus proof_tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_tree
tStatus) Bool -> Bool -> Bool
&&
                            ProofStatus proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
tacticScript ProofStatus proof_tree
tStatus TacticScript -> TacticScript -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> TacticScript
TacticScript "")
                                                ([ProofStatus proof_tree] -> [ProofStatus proof_tree])
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a b. (a -> b) -> a -> b
$ SenStatus sentence (ProofStatus proof_tree)
-> [ProofStatus proof_tree]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenStatus sentence (ProofStatus proof_tree)
senSt
                    in if [ProofStatus proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProofStatus proof_tree]
validThmStatus
                          then ProofStatus proof_tree
prStat
                          else ProofStatus proof_tree
prStat { tacticScript :: TacticScript
tacticScript = ProofStatus proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
tacticScript
                                                       (ProofStatus proof_tree -> TacticScript)
-> ProofStatus proof_tree -> TacticScript
forall a b. (a -> b) -> a -> b
$ [ProofStatus proof_tree] -> ProofStatus proof_tree
forall a. [a] -> a
head [ProofStatus proof_tree]
validThmStatus })
                  (Maybe (SenStatus sentence (ProofStatus proof_tree))
 -> ProofStatus proof_tree)
-> Maybe (SenStatus sentence (ProofStatus proof_tree))
-> ProofStatus proof_tree
forall a b. (a -> b) -> a -> b
$ String
-> ThSens sentence (ProofStatus proof_tree)
-> Maybe (SenStatus sentence (ProofStatus proof_tree))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup String
gn ThSens sentence (ProofStatus proof_tree)
oSens
          oSens' :: [SenAttr sentence String]
oSens' = ThSens sentence (ProofStatus proof_tree)
-> [SenAttr sentence String]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (ProofStatus proof_tree)
oSens
          nSens :: [SenAttr sentence String]
nSens = Set String
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a. Set String -> [Named a] -> [Named a]
disambiguateSens Set String
forall a. Set a
Set.empty ([SenAttr sentence String] -> [SenAttr sentence String])
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a b. (a -> b) -> a -> b
$ ShowS -> [SenAttr sentence String] -> [SenAttr sentence String]
forall a. ShowS -> [Named a] -> [Named a]
prepareSenNames ShowS
trSenName [SenAttr sentence String]
oSens'
          goals :: [SenAttr sentence String]
goals = (SenAttr sentence String -> Bool)
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (SenAttr sentence String -> Bool)
-> SenAttr sentence String
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence String -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom) [SenAttr sentence String]
nSens

{- | applies the recorded name mapping (in the state) of prover
  specific names to the original names to the list of ProofStatus
  (the name of the goal and the names of used axioms are translated);
  additionally the axioms generated from typing information are
  removed and warnings are generated. -}

revertRenamingOfLabels :: (Ord sentence, Ord proof_tree) =>
                           GenericState sentence proof_tree pst
                        -> [ProofStatus proof_tree]
                        -> Result [ProofStatus proof_tree]
revertRenamingOfLabels :: GenericState sentence proof_tree pst
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
revertRenamingOfLabels st :: GenericState sentence proof_tree pst
st = ([ProofStatus proof_tree]
 -> ProofStatus proof_tree -> Result [ProofStatus proof_tree])
-> [ProofStatus proof_tree]
-> [ProofStatus proof_tree]
-> Result [ProofStatus proof_tree]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [ProofStatus proof_tree]
-> ProofStatus proof_tree -> Result [ProofStatus proof_tree]
forall proof_tree.
[ProofStatus proof_tree]
-> ProofStatus proof_tree -> Result [ProofStatus proof_tree]
transNames []
    where trN :: ShowS
trN x' :: String
x' = String -> String -> GenericGoalNameMap -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                      (ShowS
forall a. HasCallStack => String -> a
error ("GenericATPState: Lookup of name failed: (2) " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                              "should not happen \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x' String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\""))
                      String
x' (GenericState sentence proof_tree pst -> GenericGoalNameMap
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> GenericGoalNameMap
namesMap GenericState sentence proof_tree pst
st)
          transNames :: [ProofStatus proof_tree]
-> ProofStatus proof_tree -> Result [ProofStatus proof_tree]
transNames tr_pStats :: [ProofStatus proof_tree]
tr_pStats pStat :: ProofStatus proof_tree
pStat =
              do [String]
uAxs <- ([String] -> String -> Result [String])
-> [String] -> [String] -> Result [String]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [String] -> String -> Result [String]
fil [] ([String] -> Result [String]) -> [String] -> Result [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
usedAxioms ProofStatus proof_tree
pStat
                 [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return ((ProofStatus proof_tree
pStat { goalName :: String
goalName = ShowS
trN ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
pStat
                                , usedAxioms :: [String]
usedAxioms = [String]
uAxs }) ProofStatus proof_tree
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. a -> [a] -> [a]
: [ProofStatus proof_tree]
tr_pStats)
           where fil :: [String] -> String -> Result [String]
fil axs :: [String]
axs ax :: String
ax =
                  Result [String]
-> (String -> Result [String]) -> Maybe String -> Result [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning
                                          ("by interface to " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                           ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
usedProver ProofStatus proof_tree
pStat String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                           ": unknown axiom \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ax String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                           "\" omitted from list of used " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                           "axioms of goal \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                           ShowS
trN (ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
pStat) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\"")
                                          Range
nullRange]
                         Result () -> Result [String] -> Result [String]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> Result [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
axs)
                        ([String] -> Result [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> Result [String])
-> (String -> [String]) -> String -> Result [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
axs))
                       (String -> GenericGoalNameMap -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
ax (GenericState sentence proof_tree pst -> GenericGoalNameMap
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> GenericGoalNameMap
namesMap GenericState sentence proof_tree pst
st))

{- |
  Represents the general return value of a prover run.
-}
data ATPRetval
  -- | prover completed successfully
  = ATPSuccess
  -- | prover did not terminate before the time limit exceeded
  | ATPTLimitExceeded
  -- | an error occured while running the prover
  | ATPError String
  -- | ATP batch mode was stopped with killthread
  | ATPBatchStopped
  deriving (ATPRetval -> ATPRetval -> Bool
(ATPRetval -> ATPRetval -> Bool)
-> (ATPRetval -> ATPRetval -> Bool) -> Eq ATPRetval
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ATPRetval -> ATPRetval -> Bool
$c/= :: ATPRetval -> ATPRetval -> Bool
== :: ATPRetval -> ATPRetval -> Bool
$c== :: ATPRetval -> ATPRetval -> Bool
Eq, Int -> ATPRetval -> ShowS
[ATPRetval] -> ShowS
ATPRetval -> String
(Int -> ATPRetval -> ShowS)
-> (ATPRetval -> String)
-> ([ATPRetval] -> ShowS)
-> Show ATPRetval
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ATPRetval] -> ShowS
$cshowList :: [ATPRetval] -> ShowS
show :: ATPRetval -> String
$cshow :: ATPRetval -> String
showsPrec :: Int -> ATPRetval -> ShowS
$cshowsPrec :: Int -> ATPRetval -> ShowS
Show)

type RunProver sentence proof_tree pst =
  pst -- prover state containing logical part
  -> GenericConfig proof_tree -- configuration to use
  -> Bool -- True means save problem file
  -> String -- name of the theory in the DevGraph
  -> AS_Anno.Named sentence -- goal to prove
  -> IO (ATPRetval, GenericConfig proof_tree) {- (retval, configuration with
                                                   proofStatus and complete
                                                   output) -}

{- |
  Prover specific functions
-}
data ATPFunctions sign sentence morphism proof_tree pst = ATPFunctions {
    -- | initial prover specific state
    ATPFunctions sign sentence morphism proof_tree pst
-> InitialProverState sign sentence morphism pst
initialProverState :: InitialProverState sign sentence morphism pst,
    -- | prover specific translation of goal name
    ATPFunctions sign sentence morphism proof_tree pst -> ShowS
atpTransSenName :: TransSenName,
    -- | inserts a goal into prover state
    ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> pst
atpInsertSentence :: pst -> AS_Anno.Named sentence -> pst,
    -- | output of a goal in a prover specific format
    ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> [String] -> IO String
goalOutput :: pst -> AS_Anno.Named sentence -> [String] -> IO String,
    -- | help text
    ATPFunctions sign sentence morphism proof_tree pst -> String
proverHelpText :: String,
    -- | environment variable containing time limit for batch time
    ATPFunctions sign sentence morphism proof_tree pst -> String
batchTimeEnv :: String,
    -- | file extensions for all output formats
    ATPFunctions sign sentence morphism proof_tree pst
-> FileExtensions
fileExtensions :: FileExtensions,
    -- | runs the prover
    ATPFunctions sign sentence morphism proof_tree pst
-> RunProver sentence proof_tree pst
runProver :: RunProver sentence proof_tree pst,
    -- | list of all options the prover finally runs with
    ATPFunctions sign sentence morphism proof_tree pst
-> GenericConfig proof_tree -> [String]
createProverOptions :: GenericConfig proof_tree -> [String]
  }

{- |
  File extensions for all prover specific output formats.
  Given extensions should begin with a dot.
-}
data FileExtensions = FileExtensions {
    -- | file extension for saving problem
    FileExtensions -> String
problemOutput :: String,
    -- | file extension for saving prover output
    FileExtensions -> String
proverOutput :: String,
    -- | file extension for saving theory configuration
    FileExtensions -> String
theoryConfiguration :: String
  }

{- |
  Tactic script implementation for ATPs. Read and show functions are derived.
-}
data ATPTacticScript = ATPTacticScript
    { ATPTacticScript -> Int
tsTimeLimit :: Int, -- ^ used time limit
      ATPTacticScript -> [String]
tsExtraOpts :: [String] -- ^ used extra options (if any)
    } deriving (ATPTacticScript -> ATPTacticScript -> Bool
(ATPTacticScript -> ATPTacticScript -> Bool)
-> (ATPTacticScript -> ATPTacticScript -> Bool)
-> Eq ATPTacticScript
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ATPTacticScript -> ATPTacticScript -> Bool
$c/= :: ATPTacticScript -> ATPTacticScript -> Bool
== :: ATPTacticScript -> ATPTacticScript -> Bool
$c== :: ATPTacticScript -> ATPTacticScript -> Bool
Eq, Eq ATPTacticScript
Eq ATPTacticScript =>
(ATPTacticScript -> ATPTacticScript -> Ordering)
-> (ATPTacticScript -> ATPTacticScript -> Bool)
-> (ATPTacticScript -> ATPTacticScript -> Bool)
-> (ATPTacticScript -> ATPTacticScript -> Bool)
-> (ATPTacticScript -> ATPTacticScript -> Bool)
-> (ATPTacticScript -> ATPTacticScript -> ATPTacticScript)
-> (ATPTacticScript -> ATPTacticScript -> ATPTacticScript)
-> Ord ATPTacticScript
ATPTacticScript -> ATPTacticScript -> Bool
ATPTacticScript -> ATPTacticScript -> Ordering
ATPTacticScript -> ATPTacticScript -> ATPTacticScript
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript
$cmin :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript
max :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript
$cmax :: ATPTacticScript -> ATPTacticScript -> ATPTacticScript
>= :: ATPTacticScript -> ATPTacticScript -> Bool
$c>= :: ATPTacticScript -> ATPTacticScript -> Bool
> :: ATPTacticScript -> ATPTacticScript -> Bool
$c> :: ATPTacticScript -> ATPTacticScript -> Bool
<= :: ATPTacticScript -> ATPTacticScript -> Bool
$c<= :: ATPTacticScript -> ATPTacticScript -> Bool
< :: ATPTacticScript -> ATPTacticScript -> Bool
$c< :: ATPTacticScript -> ATPTacticScript -> Bool
compare :: ATPTacticScript -> ATPTacticScript -> Ordering
$ccompare :: ATPTacticScript -> ATPTacticScript -> Ordering
$cp1Ord :: Eq ATPTacticScript
Ord, Int -> ATPTacticScript -> ShowS
[ATPTacticScript] -> ShowS
ATPTacticScript -> String
(Int -> ATPTacticScript -> ShowS)
-> (ATPTacticScript -> String)
-> ([ATPTacticScript] -> ShowS)
-> Show ATPTacticScript
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ATPTacticScript] -> ShowS
$cshowList :: [ATPTacticScript] -> ShowS
show :: ATPTacticScript -> String
$cshow :: ATPTacticScript -> String
showsPrec :: Int -> ATPTacticScript -> ShowS
$cshowsPrec :: Int -> ATPTacticScript -> ShowS
Show, ReadPrec [ATPTacticScript]
ReadPrec ATPTacticScript
Int -> ReadS ATPTacticScript
ReadS [ATPTacticScript]
(Int -> ReadS ATPTacticScript)
-> ReadS [ATPTacticScript]
-> ReadPrec ATPTacticScript
-> ReadPrec [ATPTacticScript]
-> Read ATPTacticScript
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ATPTacticScript]
$creadListPrec :: ReadPrec [ATPTacticScript]
readPrec :: ReadPrec ATPTacticScript
$creadPrec :: ReadPrec ATPTacticScript
readList :: ReadS [ATPTacticScript]
$creadList :: ReadS [ATPTacticScript]
readsPrec :: Int -> ReadS ATPTacticScript
$creadsPrec :: Int -> ReadS ATPTacticScript
Read)

{- |
  Default time limit for the GUI mode prover in seconds.
-}
guiDefaultTimeLimit :: Int
guiDefaultTimeLimit :: Int
guiDefaultTimeLimit = 10

{- |
  Returns the time limit from GenericConfig if available. Otherwise
  guiDefaultTimeLimit is returned.
-}
configTimeLimit :: GenericConfig proof_tree -> Int
configTimeLimit :: GenericConfig proof_tree -> Int
configTimeLimit = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
guiDefaultTimeLimit (Maybe Int -> Int)
-> (GenericConfig proof_tree -> Maybe Int)
-> GenericConfig proof_tree
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig proof_tree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit

{- |
  Parses a given default tactic script into a
  'Interfaces.GenericATPState.ATPTacticScript' if possible. Otherwise a default
  prover's tactic script is returned.
-}
parseTacticScript
    :: Int {- ^ default time limit (standard:
           'Proofs.BatchProcessing.batchTimeLimit') -}
    -> [String] -- ^ default extra options (prover specific)
    -> TacticScript
    -> ATPTacticScript
parseTacticScript :: Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript tLimit :: Int
tLimit extOpts :: [String]
extOpts (TacticScript ts :: String
ts) =
    let defl :: ATPTacticScript
defl = ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
          { tsTimeLimit :: Int
tsTimeLimit = Int
tLimit
          , tsExtraOpts :: [String]
tsExtraOpts = [String]
extOpts }
    in case String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
ts of
         Nothing -> ATPTacticScript -> Maybe ATPTacticScript -> ATPTacticScript
forall a. a -> Maybe a -> a
fromMaybe ATPTacticScript
defl (Maybe ATPTacticScript -> ATPTacticScript)
-> Maybe ATPTacticScript -> ATPTacticScript
forall a b. (a -> b) -> a -> b
$ String -> Maybe ATPTacticScript
forall a. Read a => String -> Maybe a
readMaybe String
ts
         Just tl :: Int
tl -> ATPTacticScript
defl { tsTimeLimit :: Int
tsTimeLimit = Int
tl }

{- |
  Pretty printing of prover configuration.
-}
printCfgText :: Map.Map ATPIdentifier (GenericConfig proof_tree)
             -> Doc -- ^ prover configuration
printCfgText :: Map String (GenericConfig proof_tree) -> Doc
printCfgText mp :: Map String (GenericConfig proof_tree)
mp = String -> Doc
text "* Configuration *" Doc -> Doc -> Doc
$+$ Doc
dc
             Doc -> Doc -> Doc
$++$ String -> Doc
text "* Results *" Doc -> Doc -> Doc
$+$ Doc
dr
  where
  (dc :: Doc
dc, dr :: Doc
dr) = (String -> GenericConfig proof_tree -> (Doc, Doc) -> (Doc, Doc))
-> (Doc, Doc)
-> Map String (GenericConfig proof_tree)
-> (Doc, Doc)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ k :: String
k cfg :: GenericConfig proof_tree
cfg (dCfg :: Doc
dCfg, dRes :: Doc
dRes) ->
      let r :: ProofStatus proof_tree
r = GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
cfg
      in
      (Doc -> Doc
quotes (String -> Doc
text String
k) Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> Doc -> Doc
specBraces (
          String -> Doc
text "goalStatus" Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
                            (String -> Doc
text (String -> Doc)
-> (ProofStatus proof_tree -> String)
-> ProofStatus proof_tree
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GoalStatus -> String
forall a. Show a => a -> String
show (GoalStatus -> String)
-> (ProofStatus proof_tree -> GoalStatus)
-> ProofStatus proof_tree
-> String
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
r Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
          Doc -> Doc -> Doc
$+$ String -> Doc
text "timeLimitExceeded" Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
                            (String -> Doc
text (String -> Doc)
-> (GenericConfig proof_tree -> String)
-> GenericConfig proof_tree
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show (Bool -> String)
-> (GenericConfig proof_tree -> Bool)
-> GenericConfig proof_tree
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig proof_tree -> Bool
forall proof_tree. GenericConfig proof_tree -> Bool
timeLimitExceeded) GenericConfig proof_tree
cfg Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma
          Doc -> Doc -> Doc
$+$ String -> Doc
text "timeUsed" Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
                            (String -> Doc
text (String -> Doc)
-> (GenericConfig proof_tree -> String)
-> GenericConfig proof_tree
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TimeOfDay -> String
forall a. Show a => a -> String
show (TimeOfDay -> String)
-> (GenericConfig proof_tree -> TimeOfDay)
-> GenericConfig proof_tree
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericConfig proof_tree -> TimeOfDay
forall proof_tree. GenericConfig proof_tree -> TimeOfDay
timeUsed) GenericConfig proof_tree
cfg
          Doc -> Doc -> Doc
$+$ String -> Doc
text "tacticScript" Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+>
                            (String -> Doc
text (String -> Doc)
-> (ProofStatus proof_tree -> String)
-> ProofStatus proof_tree
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticScript -> String
forall a. Show a => a -> String
show (TacticScript -> String)
-> (ProofStatus proof_tree -> TacticScript)
-> ProofStatus proof_tree
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStatus proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
tacticScript) ProofStatus proof_tree
r
          ) Doc -> Doc -> Doc
$+$ Doc
dCfg,
       String -> Doc
text "Output of goal" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (String -> Doc
text String
k) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon
            Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
resultOutput GenericConfig proof_tree
cfg)
          Doc -> Doc -> Doc
$++$ Doc
dRes))
    (Doc
empty, Doc
empty) Map String (GenericConfig proof_tree)
mp

-- | Converts a thrown exception into an ATP result (ATPRetval and proof tree).
excepToATPResult
  :: String -- ^ name of running prover
  -> String -- ^ goal name to prove
  -> Exception.SomeException -- ^ occured exception
  -> IO (ATPRetval, GenericConfig ProofTree)
     -- ^ (retval, configuration with proof status and complete output)
excepToATPResult :: String
-> String
-> SomeException
-> IO (ATPRetval, GenericConfig ProofTree)
excepToATPResult prName :: String
prName nGoalName :: String
nGoalName excep :: SomeException
excep = do
  let emptyCfg :: GenericConfig ProofTree
emptyCfg = String -> String -> ProofTree -> GenericConfig ProofTree
forall proof_tree.
Ord proof_tree =>
String -> String -> proof_tree -> GenericConfig proof_tree
emptyConfig String
prName String
nGoalName ProofTree
emptyProofTree
  (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATPRetval, GenericConfig ProofTree)
 -> IO (ATPRetval, GenericConfig ProofTree))
-> (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ case SomeException -> Maybe IOException
forall e. Exception e => SomeException -> Maybe e
Exception.fromException SomeException
excep of
    {- this is supposed to distinguish "fd ... vanished"
    errors from other exceptions -}
    Just e :: IOException
e ->
        (String -> ATPRetval
ATPError (String -> ATPRetval) -> String -> ATPRetval
forall a b. (a -> b) -> a -> b
$ "Internal error communicating with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
prName String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".\n"
         String -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show (IOException
e :: Exception.IOException), GenericConfig ProofTree
emptyCfg)
    Nothing -> case SomeException -> Maybe AsyncException
forall e. Exception e => SomeException -> Maybe e
Exception.fromException SomeException
excep of
      Just Exception.ThreadKilled -> (ATPRetval
ATPBatchStopped, GenericConfig ProofTree
emptyCfg)
      _ ->
        (String -> ATPRetval
ATPError ("Error running " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
prName String -> ShowS
forall a. [a] -> [a] -> [a]
++ ".\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
excep), GenericConfig ProofTree
emptyCfg)