{- |
Description :  All commands to prove or check the consistency of a theory, node or edge
Copyright   :  (c) Otto-von-Guericke University of Magdeburg
License     :  GPLv2 or higher, see LICENSE.txt
-}
module HetsAPI.ProveCommands (
    getTheoryForSelection
    , getAvailableComorphisms
    , getUsableProvers
    , getUsableConsistencyCheckers
    , Interfaces.Utils.getUsableConservativityCheckers

    , proveNode
    , recordProofResult
    , proveNodeAndRecord

    , checkConsistency
    , recordConsistencyResult
    , checkConsistencyAndRecord

    , checkConservativityEdge
    , recordConservativityResult
    , checkConservativityEdgeAndRecord

    , ProofOptions(..)
    , defaultProofOptions
    , ConsCheckingOptions(..)
    , defaultConsCheckingOptions
    , recomputeNode

    , genericProveBatch
) where

import HetsAPI.DataTypes

import Data.Functor ()
import qualified Data.Map as Map
import Data.Maybe (fromJust)
import Data.Graph.Inductive (LNode, LEdge)

import Control.Monad.Trans ( MonadTrans(lift) )

import Common.Consistency (Conservativity)
import Common.Id (nullRange)
import Common.LibName (LibName)
import qualified Common.OrderedMap as OMap
import Common.Result (Result(maybeResult, Result), maybeToResult)
import Common.ResultT (ResultT (..), liftR)

import Comorphisms.LogicGraph (logicGraph)

import qualified Interfaces.Utils (checkConservativityNode, getUsableConservativityCheckers, checkConservativityEdgeWith, recordConservativityResult)

import Logic.Comorphism (AnyComorphism)
import Logic.Grothendieck (findComorphismPaths)
import Logic.Prover (ProofStatus (goalName), ProverKind (..))

import Proofs.AbstractState (G_prover, ProofState, G_proof_tree, autoProofAtNode, G_cons_checker (..), G_conservativity_checker (..), getProverName, getConsCheckers, getCcName, makeTheoryForSentences)
import qualified Proofs.AbstractState as PAS
import Proofs.ConsistencyCheck (ConsistencyStatus, SType(..), consistencyCheck, sType)
import Proofs.BatchProcessing (genericProveBatch)

import Static.ComputeTheory(updateLabelTheory, recomputeNodeLabel)
import Static.DevGraph (LibEnv, DGraph, DGNodeLab, DGLinkLab, ProofHistory, DGChange(..), globalTheory, markNodeInconsistent, markNodeConsistent)
import Static.GTheory (G_theory (..), sublogicOfTh, coerceThSens)
import Static.History (changeDGH)

data ProofOptions = ProofOptions {
    ProofOptions -> Maybe G_prover
proofOptsProver :: Maybe G_prover -- ^ The prover to use. If not set, it is selected automatically
    , ProofOptions -> Maybe AnyComorphism
proofOptsComorphism :: Maybe AnyComorphism -- ^ The comorphism to use. If not set, it is selected automatically
    , ProofOptions -> Bool
proofOptsUseTheorems :: Bool -- ^ Indicates whether or not to use theorems is subsequent proofs
    , ProofOptions -> [String]
proofOptsGoalsToProve :: [String] -- ^ The names of the goals to prove. If empty, all goals are proven
    , ProofOptions -> [String]
proofOptsAxiomsToInclude :: [String] -- ^ The names of the axioms to include in the prove. If empty, all axioms are included
    , ProofOptions -> Int
proofOptsTimeout :: Int -- ^ The timeout in seconds
}

defaultProofOptions :: ProofOptions
defaultProofOptions :: ProofOptions
defaultProofOptions = ProofOptions :: Maybe G_prover
-> Maybe AnyComorphism
-> Bool
-> [String]
-> [String]
-> Int
-> ProofOptions
ProofOptions {
    proofOptsProver :: Maybe G_prover
proofOptsProver = Maybe G_prover
forall a. Maybe a
Nothing -- Automatically choose a prover
    , proofOptsComorphism :: Maybe AnyComorphism
proofOptsComorphism = Maybe AnyComorphism
forall a. Maybe a
Nothing -- Autormatically select a comorphism
    , proofOptsUseTheorems :: Bool
proofOptsUseTheorems = Bool
True
    , proofOptsGoalsToProve :: [String]
proofOptsGoalsToProve = [] -- Prove all goals
    , proofOptsAxiomsToInclude :: [String]
proofOptsAxiomsToInclude = [] -- Use all axioms
    , proofOptsTimeout :: Int
proofOptsTimeout = 600 -- Timeout 10min
}

data ConsCheckingOptions = ConsCheckingOptions {
    ConsCheckingOptions -> Maybe G_cons_checker
consOptsConsChecker :: Maybe G_cons_checker -- ^ The conschecker to use. If not set, it is selected automatically
    , ConsCheckingOptions -> Maybe AnyComorphism
consOptsComorphism :: Maybe AnyComorphism -- ^ The comorphism to use. If not set, it is selected automatically
    , ConsCheckingOptions -> Bool
consOptsIncludeTheorems :: Bool -- ^ Indicates whether or not to include theorems in the consistency check
    , ConsCheckingOptions -> Int
consOptsTimeout :: Int -- ^ The timeout in seconds
}

defaultConsCheckingOptions :: ConsCheckingOptions
defaultConsCheckingOptions :: ConsCheckingOptions
defaultConsCheckingOptions = ConsCheckingOptions :: Maybe G_cons_checker
-> Maybe AnyComorphism -> Bool -> Int -> ConsCheckingOptions
ConsCheckingOptions {
    consOptsConsChecker :: Maybe G_cons_checker
consOptsConsChecker = Maybe G_cons_checker
forall a. Maybe a
Nothing -- Automatically choose a cons checker
    , consOptsComorphism :: Maybe AnyComorphism
consOptsComorphism = Maybe AnyComorphism
forall a. Maybe a
Nothing -- Autormatically select a comorphism
    , consOptsIncludeTheorems :: Bool
consOptsIncludeTheorems = Bool
True
    , consOptsTimeout :: Int
consOptsTimeout = 600 -- Timeout 10min
}

type ProofResult = (G_theory -- The new theory
    , [ProofStatus G_proof_tree]) -- ProofStatus of each goal

type ConservativityResult = (Conservativity, G_theory, G_theory)


getTheoryForSelection :: [String] -> [String] -> [String] -> G_theory -> G_theory
getTheoryForSelection :: [String] -> [String] -> [String] -> G_theory -> G_theory
getTheoryForSelection = [String] -> [String] -> [String] -> G_theory -> G_theory
makeTheoryForSentences

-- | @getAvailableComorphisms theory@ yields all available comorphisms for @theory@
getAvailableComorphisms :: G_theory -> [AnyComorphism]
getAvailableComorphisms :: G_theory -> [AnyComorphism]
getAvailableComorphisms = LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths LogicGraph
logicGraph (G_sublogics -> [AnyComorphism])
-> (G_theory -> G_sublogics) -> G_theory -> [AnyComorphism]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> G_sublogics
sublogicOfTh

-- | @getUsableConsistencyCheckers theory@ checks for usable consistencey checkers  
--   for @theory@ available on the machine
getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConsistencyCheckers = [AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)]
getConsCheckers ([AnyComorphism] -> IO [(G_cons_checker, AnyComorphism)])
-> (G_theory -> [AnyComorphism])
-> G_theory
-> IO [(G_cons_checker, AnyComorphism)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_theory -> [AnyComorphism]
getAvailableComorphisms

-- | @getUsableProvers theory@ checks for usable provers available on the machine
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
getUsableProvers th :: G_theory
th = ProverKind
-> G_sublogics -> LogicGraph -> IO [(G_prover, AnyComorphism)]
PAS.getUsableProvers ProverKind
ProveCMDLautomatic (G_theory -> G_sublogics
sublogicOfTh G_theory
th) LogicGraph
logicGraph

-- | @proveNode theory prover comorphism@ proves all goals in @theory@ using all
--   all axioms in @theory@. If @prover@ or @comorphism@ is @Nothing@ the first
--   usable prover or comorphism, respectively, is used. 
proveNode :: TheoryPointer -> ProofOptions -> ResultT IO ProofResult
proveNode :: TheoryPointer -> ProofOptions -> ResultT IO ProofResult
proveNode (_, _, _, node :: LNode DGNodeLab
node) (ProofOptions proverM :: Maybe G_prover
proverM comorphismM :: Maybe AnyComorphism
comorphismM useTh :: Bool
useTh goals :: [String]
goals axioms :: [String]
axioms timeout :: Int
timeout) = do
    G_theory
theory <- Result G_theory -> ResultT IO G_theory
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result G_theory -> ResultT IO G_theory)
-> (LNode DGNodeLab -> Result G_theory)
-> LNode DGNodeLab
-> ResultT IO G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> String -> Maybe G_theory -> Result G_theory
forall a. Range -> String -> Maybe a -> Result a
maybeToResult Range
nullRange "No global theory!" (Maybe G_theory -> Result G_theory)
-> (LNode DGNodeLab -> Maybe G_theory)
-> LNode DGNodeLab
-> Result G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> ResultT IO G_theory)
-> LNode DGNodeLab -> ResultT IO G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab
node
    (prover :: G_prover
prover, comorphism :: AnyComorphism
comorphism) <- case (Maybe G_prover
proverM, Maybe AnyComorphism
comorphismM) of
        (Just prover :: G_prover
prover, Just comorphism :: AnyComorphism
comorphism) -> (G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover
prover, AnyComorphism
comorphism)
        (Just prover :: G_prover
prover, Nothing) -> do
            let proverName :: String
proverName = G_prover -> String
getProverName G_prover
prover
            AnyComorphism
comorphism <- IO AnyComorphism -> ResultT IO AnyComorphism
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                ((G_prover, AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd ((G_prover, AnyComorphism) -> AnyComorphism)
-> ([(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism))
-> [(G_prover, AnyComorphism)]
-> AnyComorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism)
forall a. [a] -> a
head ([(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism))
-> ([(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)])
-> [(G_prover, AnyComorphism)]
-> (G_prover, AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((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
proverName) (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)] -> AnyComorphism)
-> IO [(G_prover, AnyComorphism)] -> IO AnyComorphism
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> G_theory -> IO [(G_prover, AnyComorphism)]
getUsableProvers G_theory
theory)
            (G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover
prover, AnyComorphism
comorphism)
        (Nothing, Just comorphism :: AnyComorphism
comorphism) -> do
            G_prover
prover <- IO G_prover -> ResultT IO G_prover
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                ((G_prover, AnyComorphism) -> G_prover
forall a b. (a, b) -> a
fst ((G_prover, AnyComorphism) -> G_prover)
-> ([(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism))
-> [(G_prover, AnyComorphism)]
-> G_prover
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism)
forall a. [a] -> a
head ([(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism))
-> ([(G_prover, AnyComorphism)] -> [(G_prover, AnyComorphism)])
-> [(G_prover, AnyComorphism)]
-> (G_prover, AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((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
comorphism) (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)] -> G_prover)
-> IO [(G_prover, AnyComorphism)] -> IO G_prover
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> G_theory -> IO [(G_prover, AnyComorphism)]
getUsableProvers G_theory
theory)
            (G_prover, AnyComorphism) -> ResultT IO (G_prover, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_prover
prover, AnyComorphism
comorphism)
        (Nothing, Nothing) -> [(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism)
forall a. [a] -> a
head ([(G_prover, AnyComorphism)] -> (G_prover, AnyComorphism))
-> ResultT IO [(G_prover, AnyComorphism)]
-> ResultT IO (G_prover, AnyComorphism)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [(G_prover, AnyComorphism)]
-> ResultT IO [(G_prover, AnyComorphism)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (G_theory -> IO [(G_prover, AnyComorphism)]
getUsableProvers G_theory
theory)

    ((th :: G_theory
th, sens :: [(String, String, String)]
sens), (state :: ProofState
state, steps :: [ProofStatus G_proof_tree]
steps)) <- Bool
-> Int
-> [String]
-> [String]
-> G_theory
-> (G_prover, AnyComorphism)
-> ResultT
     IO
     ((G_theory, [(String, String, String)]),
      (ProofState, [ProofStatus G_proof_tree]))
autoProofAtNode Bool
useTh Int
timeout [String]
goals [String]
axioms G_theory
theory (G_prover
prover, AnyComorphism
comorphism)
    ProofResult -> ResultT IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
th, [ProofStatus G_proof_tree]
steps)

recordProofResult :: TheoryPointer -> ProofResult -> LibEnv
recordProofResult :: TheoryPointer -> ProofResult -> LibEnv
recordProofResult (name :: LibName
name, env :: LibEnv
env, graph :: DGraph
graph, node :: LNode DGNodeLab
node) (theory :: G_theory
theory, statuses :: [ProofStatus G_proof_tree]
statuses) =
    if [ProofStatus G_proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProofStatus G_proof_tree]
statuses
    then LibEnv
env
    else case Maybe G_theory
new_theory of
        Just th :: G_theory
th -> LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
name ( LibEnv
-> LibName -> DGraph -> LNode DGNodeLab -> G_theory -> DGraph
updateLabelTheory LibEnv
env LibName
name DGraph
graph LNode DGNodeLab
node G_theory
th) LibEnv
env
        Nothing -> LibEnv
env
    where new_theory :: Maybe G_theory
new_theory = do
            G_theory
original_theory <- DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> Maybe G_theory)
-> LNode DGNodeLab -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab
node
            G_theory
-> G_theory -> [ProofStatus G_proof_tree] -> Maybe G_theory
recordProofResult' G_theory
original_theory G_theory
theory [ProofStatus G_proof_tree]
statuses

recordProofResult' :: G_theory -> G_theory -> [ProofStatus G_proof_tree] -> Maybe G_theory
recordProofResult' :: G_theory
-> G_theory -> [ProofStatus G_proof_tree] -> Maybe G_theory
recordProofResult' (G_theory lid1 :: lid
lid1 _ _ _ original_sens :: ThSens sentence (AnyComorphism, BasicProof)
original_sens _) (G_theory lid2 :: lid
lid2 syn :: Maybe IRI
syn sign :: ExtSign sign symbol
sign signIdx :: SigId
signIdx result_sens :: ThSens sentence (AnyComorphism, BasicProof)
result_sens sensIdx :: ThId
sensIdx) statuses :: [ProofStatus G_proof_tree]
statuses = do
    ThSens sentence (AnyComorphism, BasicProof)
original_sens' <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
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 :: * -> *) b.
(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, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid1 lid
lid2 "String" ThSens sentence (AnyComorphism, BasicProof)
original_sens
    let new_sens :: ThSens sentence (AnyComorphism, BasicProof)
new_sens = (ProofStatus G_proof_tree
 -> ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> [ProofStatus G_proof_tree]
-> ThSens sentence (AnyComorphism, BasicProof)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\status :: ProofStatus G_proof_tree
status sens :: ThSens sentence (AnyComorphism, BasicProof)
sens -> String
-> SenStatus sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => k -> a -> OMap k a -> OMap k a
OMap.insert (ProofStatus G_proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus G_proof_tree
status) (Maybe (SenStatus sentence (AnyComorphism, BasicProof))
-> SenStatus sentence (AnyComorphism, BasicProof)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SenStatus sentence (AnyComorphism, BasicProof))
 -> SenStatus sentence (AnyComorphism, BasicProof))
-> (ThSens sentence (AnyComorphism, BasicProof)
    -> Maybe (SenStatus sentence (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> SenStatus sentence (AnyComorphism, BasicProof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenStatus sentence (AnyComorphism, BasicProof))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup (ProofStatus G_proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus G_proof_tree
status) (ThSens sentence (AnyComorphism, BasicProof)
 -> SenStatus sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> SenStatus sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
result_sens) ThSens sentence (AnyComorphism, BasicProof)
sens) ThSens sentence (AnyComorphism, BasicProof)
original_sens' [ProofStatus G_proof_tree]
statuses
    G_theory -> Maybe G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid2 Maybe IRI
syn ExtSign sign symbol
sign SigId
signIdx ThSens sentence (AnyComorphism, BasicProof)
new_sens ThId
sensIdx

proveNodeAndRecord :: TheoryPointer -> ProofOptions -> ResultT IO (ProofResult, LibEnv)
proveNodeAndRecord :: TheoryPointer -> ProofOptions -> ResultT IO (ProofResult, LibEnv)
proveNodeAndRecord p :: TheoryPointer
p@(_, _, _, node :: LNode DGNodeLab
node) opts :: ProofOptions
opts = do
    ProofResult
r <- TheoryPointer -> ProofOptions -> ResultT IO ProofResult
proveNode TheoryPointer
p ProofOptions
opts
    let env :: LibEnv
env = TheoryPointer -> ProofResult -> LibEnv
recordProofResult TheoryPointer
p ProofResult
r
    (ProofResult, LibEnv) -> ResultT IO (ProofResult, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofResult
r, LibEnv
env)

checkConsistency :: TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus
checkConsistency :: TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus
checkConsistency (libName :: LibName
libName, libEnv :: LibEnv
libEnv, dgraph :: DGraph
dgraph, lnode :: LNode DGNodeLab
lnode) (ConsCheckingOptions ccM :: Maybe G_cons_checker
ccM comorphismM :: Maybe AnyComorphism
comorphismM b :: Bool
b timeout :: Int
timeout)  = case DGNodeLab -> Maybe G_theory
globalTheory (DGNodeLab -> Maybe G_theory)
-> (LNode DGNodeLab -> DGNodeLab)
-> LNode DGNodeLab
-> Maybe G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> Maybe G_theory)
-> LNode DGNodeLab -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab
lnode of
    Nothing -> String -> IO ConsistencyStatus
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "No global theory!"
    Just theory :: G_theory
theory -> do
        (cc :: G_cons_checker
cc, comorphism :: AnyComorphism
comorphism) <- case (Maybe G_cons_checker
ccM, Maybe AnyComorphism
comorphismM) of
            (Just cc :: G_cons_checker
cc, Just comorphism :: AnyComorphism
comorphism) -> (G_cons_checker, AnyComorphism)
-> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker
cc, AnyComorphism
comorphism)
            (Just cc :: G_cons_checker
cc, Nothing) -> do
                let ccName :: String
ccName = G_cons_checker -> String
getCcName G_cons_checker
cc
                AnyComorphism
comorphism <-  (G_cons_checker, AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd ((G_cons_checker, AnyComorphism) -> AnyComorphism)
-> ([(G_cons_checker, AnyComorphism)]
    -> (G_cons_checker, AnyComorphism))
-> [(G_cons_checker, AnyComorphism)]
-> AnyComorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(G_cons_checker, AnyComorphism)]
-> (G_cons_checker, AnyComorphism)
forall a. [a] -> a
head ([(G_cons_checker, AnyComorphism)]
 -> (G_cons_checker, AnyComorphism))
-> ([(G_cons_checker, AnyComorphism)]
    -> [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
-> (G_cons_checker, AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
ccName) (String -> Bool)
-> ((G_cons_checker, AnyComorphism) -> String)
-> (G_cons_checker, AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_cons_checker -> String
getCcName (G_cons_checker -> String)
-> ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> (G_cons_checker, AnyComorphism)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst) ([(G_cons_checker, AnyComorphism)] -> AnyComorphism)
-> IO [(G_cons_checker, AnyComorphism)] -> IO AnyComorphism
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConsistencyCheckers G_theory
theory
                (G_cons_checker, AnyComorphism)
-> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker
cc, AnyComorphism
comorphism)
            (Nothing, Just comorphism :: AnyComorphism
comorphism) -> do
                G_cons_checker
cc <- (G_cons_checker, AnyComorphism) -> G_cons_checker
forall a b. (a, b) -> a
fst ((G_cons_checker, AnyComorphism) -> G_cons_checker)
-> ([(G_cons_checker, AnyComorphism)]
    -> (G_cons_checker, AnyComorphism))
-> [(G_cons_checker, AnyComorphism)]
-> G_cons_checker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(G_cons_checker, AnyComorphism)]
-> (G_cons_checker, AnyComorphism)
forall a. [a] -> a
head ([(G_cons_checker, AnyComorphism)]
 -> (G_cons_checker, AnyComorphism))
-> ([(G_cons_checker, AnyComorphism)]
    -> [(G_cons_checker, AnyComorphism)])
-> [(G_cons_checker, AnyComorphism)]
-> (G_cons_checker, AnyComorphism)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((G_cons_checker, AnyComorphism) -> Bool)
-> [(G_cons_checker, AnyComorphism)]
-> [(G_cons_checker, AnyComorphism)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AnyComorphism -> AnyComorphism -> Bool
forall a. Eq a => a -> a -> Bool
== AnyComorphism
comorphism) (AnyComorphism -> Bool)
-> ((G_cons_checker, AnyComorphism) -> AnyComorphism)
-> (G_cons_checker, AnyComorphism)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (G_cons_checker, AnyComorphism) -> AnyComorphism
forall a b. (a, b) -> b
snd) ([(G_cons_checker, AnyComorphism)] -> G_cons_checker)
-> IO [(G_cons_checker, AnyComorphism)] -> IO G_cons_checker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConsistencyCheckers G_theory
theory
                (G_cons_checker, AnyComorphism)
-> IO (G_cons_checker, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_cons_checker
cc, AnyComorphism
comorphism)
            (Nothing, Nothing) -> [(G_cons_checker, AnyComorphism)]
-> (G_cons_checker, AnyComorphism)
forall a. [a] -> a
head ([(G_cons_checker, AnyComorphism)]
 -> (G_cons_checker, AnyComorphism))
-> IO [(G_cons_checker, AnyComorphism)]
-> IO (G_cons_checker, AnyComorphism)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConsistencyCheckers G_theory
theory

        Bool
-> G_cons_checker
-> AnyComorphism
-> LibName
-> LibEnv
-> DGraph
-> LNode DGNodeLab
-> Int
-> IO ConsistencyStatus
consistencyCheck Bool
b G_cons_checker
cc AnyComorphism
comorphism LibName
libName LibEnv
libEnv DGraph
dgraph LNode DGNodeLab
lnode Int
timeout

recordConsistencyResult :: TheoryPointer -> ConsistencyStatus -> LibEnv
recordConsistencyResult :: TheoryPointer -> ConsistencyStatus -> LibEnv
recordConsistencyResult (name :: LibName
name, env :: LibEnv
env, graph :: DGraph
graph, node :: LNode DGNodeLab
node@(i :: Int
i, label :: DGNodeLab
label)) consStatus :: ConsistencyStatus
consStatus =
    if ConsistencyStatus -> SType
sType ConsistencyStatus
consStatus SType -> SType -> Bool
forall a. Eq a => a -> a -> Bool
== SType
CSUnchecked
    then LibEnv
env
    else LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
name (DGraph -> DGChange -> DGraph
changeDGH DGraph
graph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
label
                 (Int
i, case ConsistencyStatus -> SType
sType ConsistencyStatus
consStatus of
                       CSInconsistent -> String -> DGNodeLab -> DGNodeLab
markNodeInconsistent "" DGNodeLab
label
                       CSConsistent -> String -> DGNodeLab -> DGNodeLab
markNodeConsistent "" DGNodeLab
label
                       _ -> DGNodeLab
label)) LibEnv
env

checkConsistencyAndRecord :: TheoryPointer -> ConsCheckingOptions -> IO (ConsistencyStatus, LibEnv)
checkConsistencyAndRecord :: TheoryPointer
-> ConsCheckingOptions -> IO (ConsistencyStatus, LibEnv)
checkConsistencyAndRecord p :: TheoryPointer
p opts :: ConsCheckingOptions
opts = do
    ConsistencyStatus
r <- TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus
checkConsistency TheoryPointer
p ConsCheckingOptions
opts
    let env :: LibEnv
env = TheoryPointer -> ConsistencyStatus -> LibEnv
recordConsistencyResult TheoryPointer
p ConsistencyStatus
r
    (ConsistencyStatus, LibEnv) -> IO (ConsistencyStatus, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConsistencyStatus
r, LibEnv
env)

checkConservativityEdge :: LinkPointer -> G_conservativity_checker -> IO (Result ConservativityResult)
checkConservativityEdge :: LinkPointer
-> G_conservativity_checker -> IO (Result ConservativityResult)
checkConservativityEdge (name :: LibName
name, env :: LibEnv
env, edge :: LEdge DGLinkLab
edge) = LEdge DGLinkLab
-> LibEnv
-> LibName
-> G_conservativity_checker
-> IO (Result ConservativityResult)
Interfaces.Utils.checkConservativityEdgeWith LEdge DGLinkLab
edge LibEnv
env LibName
name

recordConservativityResult :: LinkPointer -> ConservativityResult -> LibEnv
recordConservativityResult :: LinkPointer -> ConservativityResult -> LibEnv
recordConservativityResult (name :: LibName
name, env :: LibEnv
env, edge :: LEdge DGLinkLab
edge) = LEdge DGLinkLab
-> LibEnv -> LibName -> ConservativityResult -> LibEnv
Interfaces.Utils.recordConservativityResult LEdge DGLinkLab
edge LibEnv
env LibName
name

checkConservativityEdgeAndRecord :: LinkPointer -> G_conservativity_checker -> IO (Result (ConservativityResult, LibEnv))
checkConservativityEdgeAndRecord :: LinkPointer
-> G_conservativity_checker
-> IO (Result (ConservativityResult, LibEnv))
checkConservativityEdgeAndRecord linkPtr :: LinkPointer
linkPtr cc :: G_conservativity_checker
cc = ResultT IO (ConservativityResult, LibEnv)
-> IO (Result (ConservativityResult, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (ConservativityResult, LibEnv)
 -> IO (Result (ConservativityResult, LibEnv)))
-> ResultT IO (ConservativityResult, LibEnv)
-> IO (Result (ConservativityResult, LibEnv))
forall a b. (a -> b) -> a -> b
$ do
    ConservativityResult
r <- IO (Result ConservativityResult) -> ResultT IO ConservativityResult
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result ConservativityResult)
 -> ResultT IO ConservativityResult)
-> IO (Result ConservativityResult)
-> ResultT IO ConservativityResult
forall a b. (a -> b) -> a -> b
$ LinkPointer
-> G_conservativity_checker -> IO (Result ConservativityResult)
checkConservativityEdge LinkPointer
linkPtr G_conservativity_checker
cc
    let env :: LibEnv
env = LinkPointer -> ConservativityResult -> LibEnv
recordConservativityResult LinkPointer
linkPtr ConservativityResult
r
    (ConservativityResult, LibEnv)
-> ResultT IO (ConservativityResult, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConservativityResult
r, LibEnv
env)

recomputeNode :: TheoryPointer -> LibEnv
recomputeNode :: TheoryPointer -> LibEnv
recomputeNode (name :: LibName
name, env :: LibEnv
env, graph :: DGraph
graph, node :: LNode DGNodeLab
node@(i :: Int
i, label :: DGNodeLab
label)) =
    LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
name (DGraph -> DGChange -> DGraph
changeDGH DGraph
graph (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
label
        (Int
i, LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> DGNodeLab
recomputeNodeLabel LibEnv
env LibName
name DGraph
graph LNode DGNodeLab
node)) LibEnv
env