{- |
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 (
    getAvailableComorphisms
    , getUsableProvers
    , getUsableConsistencyCheckers

    , proveNode
    , recordProofResult
    , proveNodeAndRecord

    , checkConsistency
    , recordConsistencyResult
    , checkConsistencyAndRecord

    , checkConservativityNode

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

import HetsAPI.DataTypes

import Data.Functor ()
import qualified Data.Map as Map
import Data.Graph.Inductive (LNode)

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

import Common.LibName (LibName)
import Common.ResultT (ResultT)

import Comorphisms.LogicGraph (logicGraph)

import qualified Interfaces.Utils (checkConservativityNode)

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

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

import Static.ComputeTheory(updateLabelTheory, recomputeNodeLabel)
import Static.DevGraph (LibEnv, DGraph, DGNodeLab, ProofHistory, DGChange(..), dgn_theory, markNodeInconsistent, markNodeConsistent)
import Static.GTheory (G_theory (..), sublogicOfTh)
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



-- | @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 :: G_theory -> ProofOptions -> ResultT IO ProofResult
proveNode :: G_theory -> ProofOptions -> ResultT IO ProofResult
proveNode theory :: G_theory
theory (ProofOptions proverM :: Maybe G_prover
proverM comorphismM :: Maybe AnyComorphism
comorphismM useTh :: Bool
useTh goals :: [String]
goals axioms :: [String]
axioms timeout :: Int
timeout) = do
    (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 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
theory) LibEnv
env

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 <- G_theory -> ProofOptions -> ResultT IO ProofResult
proveNode (DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> G_theory) -> LNode DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab
node) 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)  =  do
    let theory :: G_theory
theory = DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory)
-> (LNode DGNodeLab -> DGNodeLab) -> LNode DGNodeLab -> G_theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd (LNode DGNodeLab -> G_theory) -> LNode DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab
lnode
    (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)

checkConservativityNode ::LNode DGNodeLab -> LibEnv -> LibName
  -> IO (String, LibEnv, ProofHistory)
checkConservativityNode :: LNode DGNodeLab
-> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
checkConservativityNode = Bool
-> LNode DGNodeLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, ProofHistory)
Interfaces.Utils.checkConservativityNode Bool
False

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