{- |
Module      : ./CMDL/ProveConsistency.hs
Description : CMDL interface commands
Copyright   : uni-bremen and DFKI
License     : GPLv2 or higher, see LICENSE.txt
Maintainer  : r.pascanu@jacobs-university.de
Stability   : provisional
Portability : portable

CMDL.ProveConsistency contains prove and consistency check command
-}


module CMDL.ProveConsistency
       ( cProver
       , cConsChecker
       , doLoop
       , sigIntHandler
       ) where

import Interfaces.Command
import Interfaces.DataTypes
import Interfaces.GenericATPState (ATPTacticScript (..))
import Interfaces.History
import Interfaces.Utils

import CMDL.DataTypes (CmdlState (intState), ProveCmdType (..))
import CMDL.DataTypesUtils

import Comorphisms.LogicGraph (logicGraph)

import Proofs.AbstractState

import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.DocUtils

import Logic.Comorphism
import Logic.Grothendieck
import Logic.Logic
import Logic.Prover as P
import Logic.Coerce

import Common.Consistency
import Common.LibName (LibName)
import Common.Result (Result (Result))
import Common.Utils (trim)

import qualified Common.OrderedMap as OMap
import Common.AS_Annotation

import Data.List
import qualified Data.Map as Map

import Control.Concurrent (ThreadId, killThread)
import Control.Concurrent.MVar (MVar, newMVar, putMVar, takeMVar, readMVar,
                               swapMVar, modifyMVar_)

import Control.Monad

import Data.Foldable (forM_)

negate_th_with_cons_checker :: G_theory_with_cons_checker -> String ->
                               Maybe G_theory_with_cons_checker
negate_th_with_cons_checker :: G_theory_with_cons_checker
-> String -> Maybe G_theory_with_cons_checker
negate_th_with_cons_checker g_th :: G_theory_with_cons_checker
g_th goal :: String
goal = case G_theory_with_cons_checker
g_th of
  G_theory_with_cons_checker lid1 :: lid
lid1 th :: TheoryMorphism sign sentence morphism proof_tree
th cons_check :: ConsChecker sign sentence sublogics morphism proof_tree
cons_check ->
    case TheoryMorphism sign sentence morphism proof_tree
-> Theory sign sentence proof_tree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
P.tTarget TheoryMorphism sign sentence morphism proof_tree
th of
      P.Theory lid2 :: sign
lid2 sens :: ThSens sentence (ProofStatus proof_tree)
sens -> case 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
goal ThSens sentence (ProofStatus proof_tree)
sens of
        Nothing -> Maybe G_theory_with_cons_checker
forall a. Maybe a
Nothing
        Just sen :: SenStatus sentence (ProofStatus proof_tree)
sen -> case lid -> sentence -> Maybe sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sentence -> Maybe sentence
negation lid
lid1 (sentence -> Maybe sentence) -> sentence -> Maybe sentence
forall a b. (a -> b) -> a -> b
$ SenStatus sentence (ProofStatus proof_tree) -> sentence
forall s a. SenAttr s a -> s
sentence SenStatus sentence (ProofStatus proof_tree)
sen of
                                Nothing -> Maybe G_theory_with_cons_checker
forall a. Maybe a
Nothing
                                Just sen' :: sentence
sen' -> let
                                  negSen :: SenStatus sentence (ProofStatus proof_tree)
negSen = SenStatus sentence (ProofStatus proof_tree)
sen { sentence :: sentence
sentence = sentence
sen',
                                                 isAxiom :: Bool
isAxiom = Bool
True }
                                  sens' :: ThSens sentence (ProofStatus proof_tree)
sens' = String
-> SenStatus sentence (ProofStatus proof_tree)
-> ThSens sentence (ProofStatus proof_tree)
-> ThSens sentence (ProofStatus proof_tree)
forall k a. Ord k => k -> a -> OMap k a -> OMap k a
OMap.insert String
goal SenStatus sentence (ProofStatus proof_tree)
negSen (ThSens sentence (ProofStatus proof_tree)
 -> ThSens sentence (ProofStatus proof_tree))
-> ThSens sentence (ProofStatus proof_tree)
-> ThSens sentence (ProofStatus proof_tree)
forall a b. (a -> b) -> a -> b
$
                                           (SenStatus sentence (ProofStatus proof_tree) -> Bool)
-> ThSens sentence (ProofStatus proof_tree)
-> ThSens sentence (ProofStatus proof_tree)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenStatus sentence (ProofStatus proof_tree) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (ProofStatus proof_tree)
sens
                                  target' :: Theory sign sentence proof_tree
target' = sign
-> ThSens sentence (ProofStatus proof_tree)
-> Theory sign sentence proof_tree
forall sign sen proof_tree.
sign
-> ThSens sen (ProofStatus proof_tree)
-> Theory sign sen proof_tree
P.Theory sign
lid2 ThSens sentence (ProofStatus proof_tree)
sens'
                                 in G_theory_with_cons_checker -> Maybe G_theory_with_cons_checker
forall a. a -> Maybe a
Just (G_theory_with_cons_checker -> Maybe G_theory_with_cons_checker)
-> G_theory_with_cons_checker -> Maybe G_theory_with_cons_checker
forall a b. (a -> b) -> a -> b
$ lid
-> TheoryMorphism sign sentence morphism proof_tree
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_theory_with_cons_checker
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> TheoryMorphism sign sentence morphism proof_tree
-> ConsChecker sign sentence sublogics morphism proof_tree
-> G_theory_with_cons_checker
G_theory_with_cons_checker lid
lid1 TheoryMorphism sign sentence morphism proof_tree
th
                                            {tTarget :: Theory sign sentence proof_tree
P.tTarget = Theory sign sentence proof_tree
target'} ConsChecker sign sentence sublogics morphism proof_tree
cons_check

getProversAutomatic :: G_sublogics -> IO [(G_prover, AnyComorphism)]
getProversAutomatic :: G_sublogics -> IO [(G_prover, AnyComorphism)]
getProversAutomatic sl :: G_sublogics
sl = ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
getUsableProvers ProverKind
P.ProveCMDLautomatic G_sublogics
sl LogicGraph
logicGraph

-- | Select a prover
cProver :: String -> CmdlState -> IO CmdlState
cProver :: String -> CmdlState -> IO CmdlState
cProver input :: String
input state :: CmdlState
state =
  do
   -- trimed input
   let inp :: String
inp = String -> String
trim String
input
   case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
    Just pS :: IntIState
pS ->
     -- check that some theories are selected
     case IntIState -> [Int_NodeInfo]
elements IntIState
pS of
      [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
      Element z :: ProofState
z _ : _ -> do
        [(G_prover, AnyComorphism)]
prov <- G_sublogics -> IO [(G_prover, AnyComorphism)]
getProversAutomatic (ProofState -> G_sublogics
sublogicOfTheory ProofState
z)
        let pl :: [(G_prover, AnyComorphism)]
pl = ((G_prover, AnyComorphism) -> Bool)
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
inp) (String -> Bool)
-> ((G_prover, AnyComorphism) -> String)
-> (G_prover, AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_prover -> String
getProverName (G_prover -> String)
-> ((G_prover, AnyComorphism) -> G_prover)
-> (G_prover, AnyComorphism)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_prover, AnyComorphism) -> G_prover
forall a b. (a, b) -> a
fst) [(G_prover, AnyComorphism)]
prov
            prover_names :: [String]
prover_names = ((G_prover, AnyComorphism) -> String)
-> [(G_prover, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (G_prover -> String
getProverName (G_prover -> String)
-> ((G_prover, AnyComorphism) -> G_prover)
-> (G_prover, AnyComorphism)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_prover, AnyComorphism) -> G_prover
forall a b. (a, b) -> a
fst) [(G_prover, AnyComorphism)]
prov
        case case IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS of
                   Nothing -> [(G_prover, AnyComorphism)]
pl
                   Just x :: AnyComorphism
x -> ((G_prover, AnyComorphism) -> Bool)
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AnyComorphism -> AnyComorphism -> Bool
forall a. Eq a => a -> a -> Bool
== AnyComorphism
x) (AnyComorphism -> Bool)
-> ((G_prover, AnyComorphism) -> AnyComorphism)
-> (G_prover, AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_prover, AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd) [(G_prover, AnyComorphism)]
pl [(G_prover, AnyComorphism)]
-> [(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)]
forall a. [a] -> [a] -> [a]
++ [(G_prover, AnyComorphism)]
pl of
             [] -> if String
inp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then do
                            (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String]
prover_names)
                            CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
                               else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                 ("No applicable prover with name \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
inp String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" found") 1
                 CmdlState
state)
             (p :: G_prover
p, nCm :: AnyComorphism
nCm@(Comorphism cid :: cid
cid)) : _ ->
               CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [ Maybe G_prover -> UndoRedoElem
ProverChange (Maybe G_prover -> UndoRedoElem) -> Maybe G_prover -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe G_prover
prover IntIState
pS
                                 , Maybe AnyComorphism -> UndoRedoElem
CComorphismChange (Maybe AnyComorphism -> UndoRedoElem)
-> Maybe AnyComorphism -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS ]
                     (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage "" ("Hint: Using comorphism `"
                            String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid String -> String -> String
forall a. [a] -> [a] -> [a]
++ "`")
                            CmdlState
state {
                              intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                                i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
pS
                                             { cComorphism :: Maybe AnyComorphism
cComorphism = AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just AnyComorphism
nCm
                                             , prover :: Maybe G_prover
prover = G_prover -> Maybe G_prover
forall a. a -> Maybe a
Just G_prover
p } } }

-- | Selects a consistency checker
cConsChecker :: String -> CmdlState -> IO CmdlState
cConsChecker :: String -> CmdlState -> IO CmdlState
cConsChecker input :: String
input state :: CmdlState
state =
  do
   -- trimed input
   let inp :: String
inp = String -> String
trim String
input
   case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
    Just pS :: IntIState
pS ->
     -- check that some theories are selected
     case IntIState -> [Int_NodeInfo]
elements IntIState
pS of
      [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
      Element z :: ProofState
z _ : _ ->
       do
        [(G_cons_checker, AnyComorphism)]
consCheckList <- [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers ([AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)])
-> [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths
                                LogicGraph
logicGraph (G_sublogics -> [AnyComorphism]) -> G_sublogics -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ ProofState -> G_sublogics
sublogicOfTheory ProofState
z
        -- see if any comorphism was used
        case IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS of
        {- if none use the theory of the first selected node
        to find possible comorphisms -}
         Nothing -> case ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> Maybe (G_cons_checker, AnyComorphism)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (y :: G_cons_checker
y, _) -> G_cons_checker -> String
getCcName G_cons_checker
y String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
inp) [(G_cons_checker, AnyComorphism)]
consCheckList of
                    Nothing -> if String
inp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then do
                                            let shortConsCList :: [String]
shortConsCList = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ((G_cons_checker, AnyComorphism) -> String)
-> [(G_cons_checker, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
                                                 (\ (y :: G_cons_checker
y, _) -> G_cons_checker -> String
getCcName G_cons_checker
y)
                                                 [(G_cons_checker, AnyComorphism)]
consCheckList
                                            (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
shortConsCList
                                            CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
                                          else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                                ("No applicable " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                 "consistency checker with this name found") 1
                                 CmdlState
state
                    Just (p :: G_cons_checker
p, _) -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist
                                    [Maybe G_cons_checker -> UndoRedoElem
ConsCheckerChange (Maybe G_cons_checker -> UndoRedoElem)
-> Maybe G_cons_checker -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe G_cons_checker
consChecker IntIState
pS]
                                    CmdlState
state {
                                      intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                                         i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
pS {
                                             consChecker :: Maybe G_cons_checker
consChecker = G_cons_checker -> Maybe G_cons_checker
forall a. a -> Maybe a
Just G_cons_checker
p }
                                          }
                                      }
         Just x :: AnyComorphism
x -> do
          [(G_cons_checker, AnyComorphism)]
cs <- [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers [AnyComorphism
x]
          case ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> Maybe (G_cons_checker, AnyComorphism)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (y :: G_cons_checker
y, _) -> G_cons_checker -> String
getCcName G_cons_checker
y String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
inp) [(G_cons_checker, AnyComorphism)]
cs of
           Nothing ->
            case ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> Maybe (G_cons_checker, AnyComorphism)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (y :: G_cons_checker
y, _) -> G_cons_checker -> String
getCcName G_cons_checker
y String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
inp) [(G_cons_checker, AnyComorphism)]
consCheckList of
             Nothing -> if String
inp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then do
                                            let shortConsCList :: [String]
shortConsCList = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ ((G_cons_checker, AnyComorphism) -> String)
-> [(G_cons_checker, AnyComorphism)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map
                                                 (\ (y :: G_cons_checker
y, _) -> G_cons_checker -> String
getCcName G_cons_checker
y)
                                                 [(G_cons_checker, AnyComorphism)]
consCheckList
                                            (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
shortConsCList
                                            CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return CmdlState
state
                                    else CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode
                                ("No applicable " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                 "consistency checker with this name found") 1
                                 CmdlState
state
             Just (p :: G_cons_checker
p, nCm :: AnyComorphism
nCm@(Comorphism cid :: cid
cid)) ->
               CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [ Maybe G_cons_checker -> UndoRedoElem
ConsCheckerChange (Maybe G_cons_checker -> UndoRedoElem)
-> Maybe G_cons_checker -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe G_cons_checker
consChecker IntIState
pS
                                 , Maybe AnyComorphism -> UndoRedoElem
CComorphismChange (Maybe AnyComorphism -> UndoRedoElem)
-> Maybe AnyComorphism -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS ]
                  (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage "" ("Hint: Using default comorphism `"
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid String -> String -> String
forall a. [a] -> [a] -> [a]
++ "`")
                      CmdlState
state {
                       intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                         i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
pS {
                                    cComorphism :: Maybe AnyComorphism
cComorphism = AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just AnyComorphism
nCm,
                                    consChecker :: Maybe G_cons_checker
consChecker = G_cons_checker -> Maybe G_cons_checker
forall a. a -> Maybe a
Just G_cons_checker
p } } }
           Just (p :: G_cons_checker
p, _) -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return
                           (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [Maybe G_cons_checker -> UndoRedoElem
ConsCheckerChange (Maybe G_cons_checker -> UndoRedoElem)
-> Maybe G_cons_checker -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntIState -> Maybe G_cons_checker
consChecker IntIState
pS]
                            (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$ CmdlState
state {
                            intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                              i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
pS { consChecker :: Maybe G_cons_checker
consChecker = G_cons_checker -> Maybe G_cons_checker
forall a. a -> Maybe a
Just G_cons_checker
p } } }

{- | Given a proofstatus the function does the actual call of the
prover for consistency checking -}

checkNode ::
              -- Tactic script
              ATPTacticScript ->
              {- proofState of the node that needs proving
              all theorems, goals and axioms should have
              been selected before, but the theory should have
              not been recomputed -}
              Int_NodeInfo ->
              -- node name
              String ->
              {- selected prover, if non one will be automatically
              selected -}
              Maybe G_cons_checker ->
              {- selected comorphism, if non one will be automatically
              selected -}
              Maybe AnyComorphism ->
              MVar (Maybe Int_NodeInfo) ->
              MVar IntState ->
              LibName ->
              -- returns an error message if anything happens
              IO String
checkNode :: ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_cons_checker
-> Maybe AnyComorphism
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
checkNode sTxt :: ATPTacticScript
sTxt ndpf :: Int_NodeInfo
ndpf ndnm :: String
ndnm mp :: Maybe G_cons_checker
mp mcm :: Maybe AnyComorphism
mcm mSt :: MVar (Maybe Int_NodeInfo)
mSt miSt :: MVar IntState
miSt ln :: LibName
ln =
  case Int_NodeInfo
ndpf of
    Element pf_st :: ProofState
pf_st nd :: Int
nd ->
     do
     {- recompute the theory (to make effective the selected axioms,
     goals) !? needed? -}
     let st :: ProofState
st = ProofState -> ProofState
recalculateSublogicAndSelectedTheory ProofState
pf_st
     {- compute a prover,comorphism pair to be used in preparing
     the theory -}
     p_cm :: (G_cons_checker, AnyComorphism)
p_cm@(_, acm :: AnyComorphism
acm) <- case Maybe AnyComorphism
mcm of
           Nothing -> ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
           Just cm' :: AnyComorphism
cm' -> case Maybe G_cons_checker
mp of
             Nothing -> ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
             Just p' :: G_cons_checker
p' -> (G_cons_checker, AnyComorphism)
-> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker
p', AnyComorphism
cm')

     -- try to prepare the theory
     Maybe (G_theory_with_cons_checker, AnyComorphism)
prep <- case ProofState
-> (G_cons_checker, AnyComorphism)
-> Result G_theory_with_cons_checker
prepareForConsChecking ProofState
st (G_cons_checker, AnyComorphism)
p_cm of
             Result _ Nothing ->
               do
                p_cm' :: (G_cons_checker, AnyComorphism)
p_cm'@(prv' :: G_cons_checker
prv', acm' :: AnyComorphism
acm'@(Comorphism cid :: cid
cid)) <-
                          ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
                String -> IO ()
putStrLn ("Analyzing node for consistency " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ndnm)
                String -> IO ()
putStrLn ("Using the comorphism " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
                String -> IO ()
putStrLn ("Using consistency checker " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_cons_checker -> String
getCcName G_cons_checker
prv')
                Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_cons_checker, AnyComorphism)
 -> IO (Maybe (G_theory_with_cons_checker, AnyComorphism)))
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ case ProofState
-> (G_cons_checker, AnyComorphism)
-> Result G_theory_with_cons_checker
prepareForConsChecking ProofState
st (G_cons_checker, AnyComorphism)
p_cm' of
                          Result _ Nothing -> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. Maybe a
Nothing
                          Result _ (Just sm :: G_theory_with_cons_checker
sm) -> (G_theory_with_cons_checker, AnyComorphism)
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_cons_checker
sm, AnyComorphism
acm')
             Result _ (Just sm :: G_theory_with_cons_checker
sm) -> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_cons_checker, AnyComorphism)
 -> IO (Maybe (G_theory_with_cons_checker, AnyComorphism)))
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ (G_theory_with_cons_checker, AnyComorphism)
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_cons_checker
sm, AnyComorphism
acm)
     case Maybe (G_theory_with_cons_checker, AnyComorphism)
prep of
     -- theory could not be computed
      Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "No suitable prover and comorphism found"
      Just (G_theory_with_cons_checker _ th :: TheoryMorphism sign sentence morphism proof_tree
th p :: ConsChecker sign sentence sublogics morphism proof_tree
p, _) ->
        case ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
P.ccAutomatic ConsChecker sign sentence sublogics morphism proof_tree
p of
         fn :: String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
fn ->
          do
          let st' :: ProofState
st' = ProofState
st { proverRunning :: Bool
proverRunning = Bool
True}
          -- store initial input of the prover
          let tLimit :: String
tLimit = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> Int
tsTimeLimit ATPTacticScript
sTxt
          MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element ProofState
st' Int
nd
          CCStatus proof_tree
cstat <- String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
fn (ProofState -> String
theoryName ProofState
st)
                      (String -> TacticScript
P.TacticScript String
tLimit)
                      TheoryMorphism sign sentence morphism proof_tree
th []
          MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element ProofState
st Int
nd
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ case CCStatus proof_tree -> Maybe Bool
forall proof_tree. CCStatus proof_tree -> Maybe Bool
P.ccResult CCStatus proof_tree
cstat of
            Nothing -> "Timeout after " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tLimit String -> String -> String
forall a. [a] -> [a] -> [a]
++ "seconds."
            Just b :: Bool
b -> "node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ndnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "" else "in") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "consistent."
          IntState
ist <- MVar IntState -> IO IntState
forall a. MVar a -> IO a
readMVar MVar IntState
miSt
          case IntState -> Maybe IntIState
i_state IntState
ist of
            Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "no library"
            Just iist :: IntIState
iist -> case CCStatus proof_tree -> Maybe Bool
forall proof_tree. CCStatus proof_tree -> Maybe Bool
P.ccResult CCStatus proof_tree
cstat of
             Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
             Just b :: Bool
b -> do
              if IntIState -> Bool
showOutput IntIState
iist then
                do
                  String -> IO ()
putStrLn "____________________________"
                  proof_tree -> IO ()
forall a. Show a => a -> IO ()
print (proof_tree -> IO ()) -> proof_tree -> IO ()
forall a b. (a -> b) -> a -> b
$ CCStatus proof_tree -> proof_tree
forall proof_tree. CCStatus proof_tree -> proof_tree
P.ccProofTree CCStatus proof_tree
cstat
                  String -> IO ()
putStrLn "____________________________"
                                   else String -> IO ()
putStr ""
              let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
iist
                  dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
                  nl :: DGNodeLab
nl = DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
nd
                  nn :: String
nn = DGNodeLab -> String
getDGNodeName DGNodeLab
nl
                  newDg0 :: DGraph
newDg0 = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
nl (Int
nd,
                    Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency
                    (if Bool
b then Conservativity
Cons else Conservativity
Inconsistent) "" DGNodeLab
nl)
                  newDg :: DGraph
newDg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg (String -> DGRule
DGRule "Consistency check") DGraph
newDg0
                  nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history
                    (String -> Command
CommentCmd (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ "consistency check done on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
                    IntState
ist [LibName -> UndoRedoElem
DgCommandChange LibName
ln]
                  nwst :: IntState
nwst = IntState
nst { i_state :: Maybe IntIState
i_state =
                           IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
iist { i_libEnv :: LibEnv
i_libEnv = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
newDg LibEnv
le } }
              MVar IntState -> IntState -> IO IntState
forall a. MVar a -> a -> IO a
swapMVar MVar IntState
miSt IntState
nwst
              String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""

{- | Given a proofstatus the function does the actual call of the
prover for proving the node or check consistency -}
proveNode ::
              -- use theorems is subsequent proofs
              Bool ->
              -- save problem file for each goal
              Bool ->
              -- Tactic script
              ATPTacticScript ->
              {- proofState of the node that needs proving
              all theorems, goals and axioms should have
              been selected before,but the theory should have
              not beed recomputed -}
              Int_NodeInfo ->
              -- node name
              String ->
              {- selected prover, if non one will be automatically
              selected -}
              Maybe G_prover ->
              {- selected comorphism, if non one will be automatically
              selected -}
              Maybe AnyComorphism ->
              MVar (Maybe ThreadId) ->
              MVar (Maybe Int_NodeInfo) ->
              MVar IntState ->
              LibName ->
              -- returns an error message if anything happens
              IO String
proveNode :: Bool
-> Bool
-> ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_prover
-> Maybe AnyComorphism
-> MVar (Maybe ThreadId)
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
proveNode useTh :: Bool
useTh save2File :: Bool
save2File sTxt :: ATPTacticScript
sTxt ndpf :: Int_NodeInfo
ndpf ndnm :: String
ndnm mp :: Maybe G_prover
mp mcm :: Maybe AnyComorphism
mcm mThr :: MVar (Maybe ThreadId)
mThr mSt :: MVar (Maybe Int_NodeInfo)
mSt miSt :: MVar IntState
miSt libname :: LibName
libname =
  case Int_NodeInfo
ndpf of
    Element pf_st :: ProofState
pf_st nd :: Int
nd ->
     do
     {- recompute the theory (to make effective the selected axioms,
     goals) -}
     let st :: ProofState
st = ProofState -> ProofState
recalculateSublogicAndSelectedTheory ProofState
pf_st
     {- compute a prover,comorphism pair to be used in preparing
     the theory -}
     p_cm :: (G_prover, AnyComorphism)
p_cm@(_, acm :: AnyComorphism
acm) <- case Maybe AnyComorphism
mcm of
           Nothing -> ProofState -> ProverKind -> IO (G_prover, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownProver ProofState
st ProverKind
P.ProveCMDLautomatic
           Just cm' :: AnyComorphism
cm' -> case Maybe G_prover
mp of
             Nothing -> ProofState -> ProverKind -> IO (G_prover, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownProver ProofState
st ProverKind
P.ProveCMDLautomatic
             Just p' :: G_prover
p' -> (G_prover, AnyComorphism) -> IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover
p', AnyComorphism
cm')

     -- try to prepare the theory
     Maybe (G_theory_with_prover, AnyComorphism)
prep <- case ProofState
-> (G_prover, AnyComorphism) -> Result G_theory_with_prover
prepareForProving ProofState
st (G_prover, AnyComorphism)
p_cm of
             Result _ Nothing ->
               do
                p_cm' :: (G_prover, AnyComorphism)
p_cm'@(prv' :: G_prover
prv', acm' :: AnyComorphism
acm'@(Comorphism cid :: cid
cid)) <-
                          ProofState -> ProverKind -> IO (G_prover, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> ProverKind -> m (G_prover, AnyComorphism)
lookupKnownProver ProofState
st ProverKind
P.ProveCMDLautomatic
                String -> IO ()
putStrLn ("Analyzing node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ndnm)
                String -> IO ()
putStrLn ("Using the comorphism " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
                String -> IO ()
putStrLn ("Using prover " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_prover -> String
getProverName G_prover
prv')
                Maybe (G_theory_with_prover, AnyComorphism)
-> IO (Maybe (G_theory_with_prover, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_prover, AnyComorphism)
 -> IO (Maybe (G_theory_with_prover, AnyComorphism)))
-> Maybe (G_theory_with_prover, AnyComorphism)
-> IO (Maybe (G_theory_with_prover, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ case ProofState
-> (G_prover, AnyComorphism) -> Result G_theory_with_prover
prepareForProving ProofState
st (G_prover, AnyComorphism)
p_cm' of
                          Result _ Nothing -> Maybe (G_theory_with_prover, AnyComorphism)
forall a. Maybe a
Nothing
                          Result _ (Just sm :: G_theory_with_prover
sm) -> (G_theory_with_prover, AnyComorphism)
-> Maybe (G_theory_with_prover, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_prover
sm, AnyComorphism
acm')
             Result _ (Just sm :: G_theory_with_prover
sm) -> Maybe (G_theory_with_prover, AnyComorphism)
-> IO (Maybe (G_theory_with_prover, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_prover, AnyComorphism)
 -> IO (Maybe (G_theory_with_prover, AnyComorphism)))
-> Maybe (G_theory_with_prover, AnyComorphism)
-> IO (Maybe (G_theory_with_prover, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ (G_theory_with_prover, AnyComorphism)
-> Maybe (G_theory_with_prover, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_prover
sm, AnyComorphism
acm)
     case Maybe (G_theory_with_prover, AnyComorphism)
prep of
     -- theory could not be computed
      Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "No suitable prover and comorphism found"
      Just (G_theory_with_prover lid1 :: lid
lid1 th :: Theory sign sentence proof_tree
th p :: Prover sign sentence morphism sublogics proof_tree
p, cmp :: AnyComorphism
cmp) -> 
        case Prover sign sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> Theory sign sentence proof_tree
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus proof_tree])
      -> String
      -> TacticScript
      -> theory
      -> [FreeDefMorphism sentence morphism]
      -> IO (ThreadId, MVar ()))
P.proveCMDLautomaticBatch Prover sign sentence morphism sublogics proof_tree
p of
         Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "Error obtaining the prover"
         Just fn :: Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
fn ->
          do
          -- mVar to poll the prover for results
          MVar (Result [ProofStatus proof_tree])
answ <- Result [ProofStatus proof_tree]
-> IO (MVar (Result [ProofStatus proof_tree]))
forall a. a -> IO (MVar a)
newMVar ([ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
          let st' :: ProofState
st' = ProofState
st { proverRunning :: Bool
proverRunning = Bool
True}
          -- store initial input of the prover
          MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element ProofState
st' Int
nd
          {- putStrLn ((theoryName st)++"\n"++
                    (showDoc sign "") ++
                    show (vsep (map (print_named lid1)
                                        $ P.toNamedList sens))) -}
          case ProofState -> [String]
selectedGoals ProofState
st' of
           [] -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "No goals selected. Nothing to prove"
           _ ->
            do
             String -> IO ()
putStrLn "selectedGoals:"
             String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines (ProofState -> [String]
selectedGoals ProofState
st')
             (ThreadId, MVar ())
tmp <- Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> TacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (ThreadId, MVar ())
fn Bool
useTh
                      Bool
save2File
                      MVar (Result [ProofStatus proof_tree])
answ
                      (ProofState -> String
theoryName ProofState
st)
                      (String -> TacticScript
P.TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript
sTxt)
                      Theory sign sentence proof_tree
th []
             MVar (Maybe ThreadId) -> Maybe ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe ThreadId)
mThr (Maybe ThreadId -> IO (Maybe ThreadId))
-> Maybe ThreadId -> IO (Maybe ThreadId)
forall a b. (a -> b) -> a -> b
$ ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just (ThreadId -> Maybe ThreadId) -> ThreadId -> Maybe ThreadId
forall a b. (a -> b) -> a -> b
$ (ThreadId, MVar ()) -> ThreadId
forall a b. (a, b) -> a
fst (ThreadId, MVar ())
tmp
             lid
-> AnyComorphism
-> MVar ()
-> MVar (Result [ProofStatus proof_tree])
-> MVar (Maybe Int_NodeInfo)
-> Theory sign sentence proof_tree
-> IO ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
(Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree,
 Pretty sentence) =>
lid
-> AnyComorphism
-> MVar ()
-> MVar (Result [ProofStatus proof_tree])
-> MVar (Maybe Int_NodeInfo)
-> Theory sign sentence proof_tree
-> IO ()
getResults lid
lid1 AnyComorphism
cmp ((ThreadId, MVar ()) -> MVar ()
forall a b. (a, b) -> b
snd (ThreadId, MVar ())
tmp) MVar (Result [ProofStatus proof_tree])
answ MVar (Maybe Int_NodeInfo)
mSt Theory sign sentence proof_tree
th
             MVar (Maybe ThreadId) -> Maybe ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe ThreadId)
mThr Maybe ThreadId
forall a. Maybe a
Nothing
             IntState
ist <- MVar IntState -> IO IntState
forall a. MVar a -> IO a
readMVar MVar IntState
miSt
             Maybe Int_NodeInfo
state <- MVar (Maybe Int_NodeInfo) -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> IO a
readMVar MVar (Maybe Int_NodeInfo)
mSt
             case Maybe Int_NodeInfo
state of
              Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
              Just state' :: Int_NodeInfo
state' ->
               do
                MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt Maybe Int_NodeInfo
forall a. Maybe a
Nothing
                MVar IntState -> IntState -> IO IntState
forall a. MVar a -> a -> IO a
swapMVar MVar IntState
miSt (IntState -> IO IntState) -> IntState -> IO IntState
forall a b. (a -> b) -> a -> b
$ IntState -> LibName -> Int_NodeInfo -> IntState
addResults IntState
ist LibName
libname Int_NodeInfo
state'
                String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""

disproveNode ::
               -- Tactic script
              ATPTacticScript ->
              {- proofState of the node that needs proving
              all theorems, goals and axioms should have
              been selected before, but the theory should have
              not been recomputed -}
              Int_NodeInfo ->
              -- node name
              String ->
              {- selected prover, if non one will be automatically
              selected -}
              Maybe G_cons_checker ->
              {- selected comorphism, if non one will be automatically
              selected -}
              Maybe AnyComorphism ->
              MVar (Maybe Int_NodeInfo) ->
              MVar IntState ->
              LibName ->
              -- returns an error message if anything happens
              IO String
disproveNode :: ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_cons_checker
-> Maybe AnyComorphism
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
disproveNode sTxt :: ATPTacticScript
sTxt ndpf :: Int_NodeInfo
ndpf ndnm :: String
ndnm mp :: Maybe G_cons_checker
mp mcm :: Maybe AnyComorphism
mcm mSt :: MVar (Maybe Int_NodeInfo)
mSt miSt :: MVar IntState
miSt ln :: LibName
ln =
  case Int_NodeInfo
ndpf of
    Element pf_st :: ProofState
pf_st nd :: Int
nd ->
     do
     {- recompute the theory (to make effective the selected axioms,
     goals) !? needed? -}
     let st :: ProofState
st = ProofState -> ProofState
recalculateSublogicAndSelectedTheory ProofState
pf_st
     {- compute a prover,comorphism pair to be used in preparing
     the theory -}
     p_cm :: (G_cons_checker, AnyComorphism)
p_cm@(_, acm :: AnyComorphism
acm) <- case Maybe AnyComorphism
mcm of
           Nothing -> ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
           Just cm' :: AnyComorphism
cm' -> case Maybe G_cons_checker
mp of
             Nothing -> ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
             Just p' :: G_cons_checker
p' -> (G_cons_checker, AnyComorphism)
-> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker
p', AnyComorphism
cm')

     -- try to prepare the theory
     Maybe (G_theory_with_cons_checker, AnyComorphism)
prep <- case ProofState
-> (G_cons_checker, AnyComorphism)
-> Result G_theory_with_cons_checker
prepareForConsChecking ProofState
st (G_cons_checker, AnyComorphism)
p_cm of
             Result _ Nothing ->
               do
                p_cm' :: (G_cons_checker, AnyComorphism)
p_cm'@(prv' :: G_cons_checker
prv', acm' :: AnyComorphism
acm'@(Comorphism cid :: cid
cid)) <-
                          ProofState -> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *).
MonadFail m =>
ProofState -> m (G_cons_checker, AnyComorphism)
lookupKnownConsChecker ProofState
st
                String -> IO ()
putStrLn ("Analyzing node for consistency " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ndnm)
                String -> IO ()
putStrLn ("Using the comorphism " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)
                String -> IO ()
putStrLn ("Using consistency checker " String -> String -> String
forall a. [a] -> [a] -> [a]
++ G_cons_checker -> String
getCcName G_cons_checker
prv')
                Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_cons_checker, AnyComorphism)
 -> IO (Maybe (G_theory_with_cons_checker, AnyComorphism)))
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ case ProofState
-> (G_cons_checker, AnyComorphism)
-> Result G_theory_with_cons_checker
prepareForConsChecking ProofState
st (G_cons_checker, AnyComorphism)
p_cm' of
                          Result _ Nothing -> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. Maybe a
Nothing
                          Result _ (Just sm :: G_theory_with_cons_checker
sm) -> (G_theory_with_cons_checker, AnyComorphism)
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_cons_checker
sm, AnyComorphism
acm')
             Result _ (Just sm :: G_theory_with_cons_checker
sm) -> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (G_theory_with_cons_checker, AnyComorphism)
 -> IO (Maybe (G_theory_with_cons_checker, AnyComorphism)))
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
-> IO (Maybe (G_theory_with_cons_checker, AnyComorphism))
forall a b. (a -> b) -> a -> b
$ (G_theory_with_cons_checker, AnyComorphism)
-> Maybe (G_theory_with_cons_checker, AnyComorphism)
forall a. a -> Maybe a
Just (G_theory_with_cons_checker
sm, AnyComorphism
acm)
     case Maybe (G_theory_with_cons_checker, AnyComorphism)
prep of
     -- theory could not be computed
      Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "No suitable prover and comorphism found"
      Just (theory :: G_theory_with_cons_checker
theory@(G_theory_with_cons_checker l :: lid
l _ p :: ConsChecker sign sentence sublogics morphism proof_tree
p), _) ->
        case ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
P.ccAutomatic ConsChecker sign sentence sublogics morphism proof_tree
p of
         fn :: String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
fn ->
          do
          let goals :: [String]
goals = ProofState -> [String]
selectedGoals ProofState
st
              st' :: ProofState
st' = ProofState
st { proverRunning :: Bool
proverRunning = Bool
True }
              negate_theory :: String -> Maybe G_theory_with_cons_checker
negate_theory = G_theory_with_cons_checker
-> String -> Maybe G_theory_with_cons_checker
negate_th_with_cons_checker G_theory_with_cons_checker
theory
              theories :: [Maybe G_theory_with_cons_checker]
theories = (String -> Maybe G_theory_with_cons_checker)
-> [String] -> [Maybe G_theory_with_cons_checker]
forall a b. (a -> b) -> [a] -> [b]
map String -> Maybe G_theory_with_cons_checker
negate_theory [String]
goals
              th_and_goals :: [(Maybe G_theory_with_cons_checker, String)]
th_and_goals = [Maybe G_theory_with_cons_checker]
-> [String] -> [(Maybe G_theory_with_cons_checker, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe G_theory_with_cons_checker]
theories [String]
goals
              disprove_goal :: (Maybe G_theory_with_cons_checker, String) -> IO String
disprove_goal (theory' :: Maybe G_theory_with_cons_checker
theory', goal :: String
goal) =
                case Maybe G_theory_with_cons_checker
theory' of
                  Nothing -> 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
$ "Negating goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goal String -> String -> String
forall a. [a] -> [a] -> [a]
++ " failed"
                  Just (G_theory_with_cons_checker l2 :: lid
l2 th' :: TheoryMorphism sign sentence morphism proof_tree
th' _) ->
                    do
                    -- store initial input of the prover
                    let tLimit :: String
tLimit = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> Int
tsTimeLimit ATPTacticScript
sTxt
                    TheoryMorphism sign sentence morphism proof_tree
th2 <- lid
-> lid
-> String
-> TheoryMorphism sign sentence morphism proof_tree
-> IO (TheoryMorphism sign sentence morphism proof_tree)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> TheoryMorphism sign1 sentence1 morphism1 proof_tree1
-> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
coerceTheoryMorphism lid
l2 lid
l
                            "coerce error CMDL.ProveConsistency " TheoryMorphism sign sentence morphism proof_tree
th'
                    MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element ProofState
st' Int
nd
                    CCStatus proof_tree
cstat <- String
-> TacticScript
-> TheoryMorphism sign sentence morphism proof_tree
-> [FreeDefMorphism sentence morphism]
-> IO (CCStatus proof_tree)
fn (ProofState -> String
theoryName ProofState
st)
                          (String -> TacticScript
P.TacticScript String
tLimit)
                          TheoryMorphism sign sentence morphism proof_tree
th2 []
                    MVar (Maybe Int_NodeInfo)
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> a -> IO a
swapMVar MVar (Maybe Int_NodeInfo)
mSt (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element ProofState
st Int
nd
                    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ case CCStatus proof_tree -> Maybe Bool
forall proof_tree. CCStatus proof_tree -> Maybe Bool
P.ccResult CCStatus proof_tree
cstat of
                      Nothing -> "Timeout after " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tLimit String -> String -> String
forall a. [a] -> [a] -> [a]
++ "seconds."
                      Just b :: Bool
b -> "goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goal String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is "
                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "" else "not ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ "disproved."
                    IntState
ist <- MVar IntState -> IO IntState
forall a. MVar a -> IO a
readMVar MVar IntState
miSt
                    case IntState -> Maybe IntIState
i_state IntState
ist of
                      Nothing -> 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
$ "goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goal String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": no library"
                      Just iist :: IntIState
iist -> case CCStatus proof_tree -> Maybe Bool
forall proof_tree. CCStatus proof_tree -> Maybe Bool
P.ccResult CCStatus proof_tree
cstat of
                       Nothing -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
                       Just b :: Bool
b -> do
                        let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
iist
                            dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
                            nl :: DGNodeLab
nl = DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
nd
                            nn :: String
nn = DGNodeLab -> String
getDGNodeName DGNodeLab
nl
                            newDg0 :: DGraph
newDg0 = DGraph -> DGChange -> DGraph
changeDGH DGraph
dg (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
nl (Int
nd,
                              Conservativity -> String -> DGNodeLab -> DGNodeLab
markNodeConsistency
                              (if Bool
b then Conservativity
Cons else Conservativity
Inconsistent) "" DGNodeLab
nl)
                            newDg :: DGraph
newDg = DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg
                                     (String -> DGRule
DGRule "Consistency check") DGraph
newDg0
                            nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history
                              (String -> Command
CommentCmd (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ "disprove at goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goal String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                            ", node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
                              IntState
ist [LibName -> UndoRedoElem
DgCommandChange LibName
ln]
                            nwst :: IntState
nwst = IntState
nst { i_state :: Maybe IntIState
i_state =
                                     IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
iist { i_libEnv :: LibEnv
i_libEnv = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln
                                                             DGraph
newDg LibEnv
le } }
                        MVar IntState -> IntState -> IO IntState
forall a. MVar a -> a -> IO a
swapMVar MVar IntState
miSt IntState
nwst
                        String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
          ((Maybe G_theory_with_cons_checker, String) -> IO ())
-> [(Maybe G_theory_with_cons_checker, String)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((\ x :: IO String
x -> do
                           String
y <- IO String
x
                           String -> IO ()
putStrLn String
y
                           () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () ) (IO String -> IO ())
-> ((Maybe G_theory_with_cons_checker, String) -> IO String)
-> (Maybe G_theory_with_cons_checker, String)
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe G_theory_with_cons_checker, String) -> IO String
disprove_goal) [(Maybe G_theory_with_cons_checker, String)]
th_and_goals
          String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""

getResults :: (Logic lid sublogics basic_spec sentence
                     symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree, Pretty sentence) =>
              lid ->
              AnyComorphism ->
              MVar () ->
              MVar (Result [P.ProofStatus proof_tree]) ->
              MVar (Maybe Int_NodeInfo) -> 
              P.Theory sign sentence proof_tree ->
              IO ()
getResults :: lid
-> AnyComorphism
-> MVar ()
-> MVar (Result [ProofStatus proof_tree])
-> MVar (Maybe Int_NodeInfo)
-> Theory sign sentence proof_tree
-> IO ()
getResults lid :: lid
lid acm :: AnyComorphism
acm mStop :: MVar ()
mStop mData :: MVar (Result [ProofStatus proof_tree])
mData mState :: MVar (Maybe Int_NodeInfo)
mState (P.Theory _ sensMap :: ThSens sentence (ProofStatus proof_tree)
sensMap) =
  do
    MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
mStop
    Result [ProofStatus proof_tree]
d <- MVar (Result [ProofStatus proof_tree])
-> IO (Result [ProofStatus proof_tree])
forall a. MVar a -> IO a
takeMVar MVar (Result [ProofStatus proof_tree])
mData
    case Result [ProofStatus proof_tree]
d of
      Result _ Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Result _ (Just d' :: [ProofStatus proof_tree]
d') -> do
        (ProofStatus proof_tree -> IO ())
-> [ProofStatus proof_tree] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ gs :: ProofStatus proof_tree
gs -> let
                  uAx :: [String]
uAx = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map 
                          (\x :: String
x -> let ax :: String
ax =  case 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
x ThSens sentence (ProofStatus proof_tree)
sensMap of
                                            Nothing -> String -> String
forall a. HasCallStack => String -> a
error "Proof using a missing axiom"
                                            Just s :: SenStatus sentence (ProofStatus proof_tree)
s -> Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ sentence -> Doc
forall a. Pretty a => a -> Doc
pretty (sentence -> Doc) -> sentence -> Doc
forall a b. (a -> b) -> a -> b
$ SenStatus sentence (ProofStatus proof_tree) -> sentence
forall s a. SenAttr s a -> s
sentence SenStatus sentence (ProofStatus proof_tree)
s
                                  in String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ax String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n") ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
                        ProofStatus proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
P.usedAxioms ProofStatus proof_tree
gs
                in  
               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
P.goalName ProofStatus proof_tree
gs
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ " used \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
uAx)
          ([ProofStatus proof_tree] -> IO ())
-> [ProofStatus proof_tree] -> IO ()
forall a b. (a -> b) -> a -> b
$ (ProofStatus proof_tree -> Bool)
-> [ProofStatus proof_tree] -> [ProofStatus proof_tree]
forall a. (a -> Bool) -> [a] -> [a]
filter ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
P.isProvedStat [ProofStatus proof_tree]
d'
        MVar (Maybe Int_NodeInfo)
-> (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar (Maybe Int_NodeInfo)
mState (\ s :: Maybe Int_NodeInfo
s -> case Maybe Int_NodeInfo
s of
                  Nothing -> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int_NodeInfo
s
                  Just (Element st :: ProofState
st node :: Int
node) -> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo))
-> Maybe Int_NodeInfo -> IO (Maybe Int_NodeInfo)
forall a b. (a -> b) -> a -> b
$ Int_NodeInfo -> Maybe Int_NodeInfo
forall a. a -> Maybe a
Just (Int_NodeInfo -> Maybe Int_NodeInfo)
-> Int_NodeInfo -> Maybe Int_NodeInfo
forall a b. (a -> b) -> a -> b
$ ProofState -> Int -> Int_NodeInfo
Element
                                            (AnyComorphism
-> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
AnyComorphism
-> lid -> [ProofStatus proof_tree] -> ProofState -> ProofState
markProved AnyComorphism
acm lid
lid [ProofStatus proof_tree]
d' ProofState
st) Int
node)

-- | inserts the results of the proof in the development graph
addResults :: IntState -> LibName -> Int_NodeInfo -> IntState
addResults :: IntState -> LibName -> Int_NodeInfo -> IntState
addResults ist :: IntState
ist libname :: LibName
libname ndps :: Int_NodeInfo
ndps =
  case IntState -> Maybe IntIState
i_state IntState
ist of
    Nothing -> IntState
ist
    Just pS :: IntIState
pS ->
      case Int_NodeInfo
ndps of
       Element ps'' :: ProofState
ps'' node :: Int
node -> let
               dGraph :: DGraph
dGraph = LibName -> LibEnv -> DGraph
lookupDGraph LibName
libname (IntIState -> LibEnv
i_libEnv IntIState
pS)
               nl :: DGNodeLab
nl = DGraph -> Int -> DGNodeLab
labDG DGraph
dGraph Int
node
               in (IntState, [DGChange]) -> IntState
forall a b. (a, b) -> a
fst ((IntState, [DGChange]) -> IntState)
-> (IntState, [DGChange]) -> IntState
forall a b. (a -> b) -> a -> b
$ LibName
-> IntState
-> LNode DGNodeLab
-> G_theory
-> (IntState, [DGChange])
updateNodeProof LibName
libname IntState
ist (Int
node, DGNodeLab
nl)
                      (G_theory -> (IntState, [DGChange]))
-> G_theory -> (IntState, [DGChange])
forall a b. (a -> b) -> a -> b
$ ProofState -> G_theory
currentTheory ProofState
ps''

{- | Signal handler that stops the prover from running
when SIGINT is send -}
sigIntHandler :: MVar (Maybe ThreadId) ->
                 MVar IntState ->
                 MVar (Maybe Int_NodeInfo) ->
                 ThreadId ->
                 MVar IntState ->
                 LibName ->
                 IO ()
sigIntHandler :: MVar (Maybe ThreadId)
-> MVar IntState
-> MVar (Maybe Int_NodeInfo)
-> ThreadId
-> MVar IntState
-> LibName
-> IO ()
sigIntHandler mthr :: MVar (Maybe ThreadId)
mthr miSt :: MVar IntState
miSt mSt :: MVar (Maybe Int_NodeInfo)
mSt thr :: ThreadId
thr mOut :: MVar IntState
mOut libname :: LibName
libname =
  do
   {- print a message
   ? shellputStr ! should be used ! -}
   String -> IO ()
putStrLn "Prover stopped."
   -- check if the prover is runnig
   Maybe ThreadId
tmp <- MVar (Maybe ThreadId) -> IO (Maybe ThreadId)
forall a. MVar a -> IO a
readMVar MVar (Maybe ThreadId)
mthr
   Maybe ThreadId -> (ThreadId -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Data.Foldable.forM_ Maybe ThreadId
tmp ThreadId -> IO ()
killThread
   -- kill the prove/prove-all thread
   ThreadId -> IO ()
killThread ThreadId
thr
   -- update LibEnv with intermidiar results !?
   IntState
ist <- MVar IntState -> IO IntState
forall a. MVar a -> IO a
readMVar MVar IntState
miSt

   Maybe Int_NodeInfo
st <- MVar (Maybe Int_NodeInfo) -> IO (Maybe Int_NodeInfo)
forall a. MVar a -> IO a
readMVar MVar (Maybe Int_NodeInfo)
mSt
   -- add to the output mvar results until now
   MVar IntState -> IntState -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar IntState
mOut (IntState -> IO ()) -> IntState -> IO ()
forall a b. (a -> b) -> a -> b
$ case Maybe Int_NodeInfo
st of
     Nothing -> IntState
ist
     Just st' :: Int_NodeInfo
st' -> IntState -> LibName -> Int_NodeInfo -> IntState
addResults IntState
ist LibName
libname Int_NodeInfo
st'
   () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

doLoop :: MVar IntState
       -> MVar (Maybe ThreadId)
       -> MVar (Maybe Int_NodeInfo)
       -> MVar IntState
       -> [Int_NodeInfo]
       -> ProveCmdType
       -> IO ()
doLoop :: MVar IntState
-> MVar (Maybe ThreadId)
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> [Int_NodeInfo]
-> ProveCmdType
-> IO ()
doLoop miSt :: MVar IntState
miSt mThr :: MVar (Maybe ThreadId)
mThr mSt :: MVar (Maybe Int_NodeInfo)
mSt mOut :: MVar IntState
mOut ls :: [Int_NodeInfo]
ls proveCmdType :: ProveCmdType
proveCmdType = do
  IntState
ist <- MVar IntState -> IO IntState
forall a. MVar a -> IO a
readMVar MVar IntState
miSt
  case IntState -> Maybe IntIState
i_state IntState
ist of
    Nothing -> do
                 MVar IntState -> IntState -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar IntState
mOut IntState
ist
                 () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just pS :: IntIState
pS ->
        case [Int_NodeInfo]
ls of
         -- we are done
          [] -> do
                 MVar IntState -> IntState -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar IntState
mOut IntState
ist
                 () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          x :: Int_NodeInfo
x : l :: [Int_NodeInfo]
l -> do
                 let nodeName :: Int_NodeInfo -> String
nodeName x' :: Int_NodeInfo
x' = case Int_NodeInfo
x' of
                       Element _ t :: Int
t -> case Int -> [LNode DGNodeLab] -> Maybe DGNodeLab
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
t ([LNode DGNodeLab] -> Maybe DGNodeLab)
-> [LNode DGNodeLab] -> Maybe DGNodeLab
forall a b. (a -> b) -> a -> b
$ IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
pS of
                         Nothing -> "Unkown node"
                         Just ll :: DGNodeLab
ll -> DGNodeLab -> String
getDGNodeName DGNodeLab
ll
                 String -> IO ()
putStrLn ("Analyzing node " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int_NodeInfo -> String
nodeName Int_NodeInfo
x)
                 String
err <- case ProveCmdType
proveCmdType of
                           ConsCheck -> ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_cons_checker
-> Maybe AnyComorphism
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
checkNode (IntIState -> ATPTacticScript
script IntIState
pS)
                                          Int_NodeInfo
x
                                          (Int_NodeInfo -> String
nodeName Int_NodeInfo
x)
                                          (IntIState -> Maybe G_cons_checker
consChecker IntIState
pS)
                                          (IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS)
                                          MVar (Maybe Int_NodeInfo)
mSt
                                          MVar IntState
miSt
                                          (IntIState -> LibName
i_ln IntIState
pS)
                           Prove -> Bool
-> Bool
-> ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_prover
-> Maybe AnyComorphism
-> MVar (Maybe ThreadId)
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
proveNode (IntIState -> Bool
useTheorems IntIState
pS)
                                          (IntIState -> Bool
save2file IntIState
pS)
                                          (IntIState -> ATPTacticScript
script IntIState
pS)
                                          Int_NodeInfo
x
                                          (Int_NodeInfo -> String
nodeName Int_NodeInfo
x)
                                          (IntIState -> Maybe G_prover
prover IntIState
pS)
                                          (IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS)
                                          MVar (Maybe ThreadId)
mThr
                                          MVar (Maybe Int_NodeInfo)
mSt
                                          MVar IntState
miSt
                                          (IntIState -> LibName
i_ln IntIState
pS)
                           Disprove -> ATPTacticScript
-> Int_NodeInfo
-> String
-> Maybe G_cons_checker
-> Maybe AnyComorphism
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> LibName
-> IO String
disproveNode (IntIState -> ATPTacticScript
script IntIState
pS)
                                             Int_NodeInfo
x
                                             (Int_NodeInfo -> String
nodeName Int_NodeInfo
x)
                                             (IntIState -> Maybe G_cons_checker
consChecker IntIState
pS)
                                             (IntIState -> Maybe AnyComorphism
cComorphism IntIState
pS)
                                             MVar (Maybe Int_NodeInfo)
mSt
                                             MVar IntState
miSt
                                             (IntIState -> LibName
i_ln IntIState
pS)
                 Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err) (String -> IO ()
putStrLn String
err)
                 MVar IntState
-> MVar (Maybe ThreadId)
-> MVar (Maybe Int_NodeInfo)
-> MVar IntState
-> [Int_NodeInfo]
-> ProveCmdType
-> IO ()
doLoop MVar IntState
miSt MVar (Maybe ThreadId)
mThr MVar (Maybe Int_NodeInfo)
mSt MVar IntState
mOut [Int_NodeInfo]
l ProveCmdType
proveCmdType