{-# LANGUAGE CPP, RecordWildCards #-}

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

Interfaces.Utils contains different utilitary functions for the
abstract interface

-}

module Interfaces.Utils
         ( getAllNodes
         , getAllEdges
         , initNodeInfo
         , emptyIntIState
         , emptyIntState
         , wasProved
         , parseTimeLimit
         , addCommandHistoryToState
         , checkConservativityNode
         , checkConservativityEdge
         , checkConservativityEdgeWith
         , recordConservativityResult
         , getUsableConservativityCheckers
         , updateNodeProof
         ) where

import Interfaces.Command ( Command(CommentCmd) )
import Interfaces.DataTypes
import Interfaces.GenericATPState
import qualified Interfaces.Command as IC
import Interfaces.History

import Control.Monad (unless, filterM)

import Data.Graph.Inductive.Graph
import Data.Maybe (isNothing)
import Data.List
import Data.IORef

import Static.DevGraph
import Static.DgUtils
import Static.GTheory
import Static.History
import Static.ComputeTheory

import Proofs.AbstractState

import Driver.Options (rmSuffix)
import System.Directory (getCurrentDirectory)

import Logic.Comorphism
import Logic.Prover
import Logic.Logic
import Logic.Grothendieck
import Logic.Coerce
import Comorphisms.LogicGraph (logicGraph)

import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.IRI
import Common.Result
import Common.LibName
import qualified Common.Lib.SizedList as SizedList
import Common.Consistency
import Common.ExtSign
import Common.AS_Annotation (SenAttr (..), makeNamed, mapNamed)
import qualified Common.Doc as Pretty
import Common.Utils
import qualified Control.Monad.Fail as Fail
import Common.ResultT (ResultT(runResultT, ResultT))

#ifdef UNI_PACKAGE
import GUI.Utils
#endif

{- | Returns the list of all nodes, if it is not up to date
the function recomputes the list -}
getAllNodes :: IntIState -> [LNode DGNodeLab]
getAllNodes :: IntIState -> [LNode DGNodeLab]
getAllNodes st :: IntIState
st
 = DGraph -> [LNode DGNodeLab]
labNodesDG (DGraph -> [LNode DGNodeLab]) -> DGraph -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph (IntIState -> LibName
i_ln IntIState
st) (IntIState -> LibEnv
i_libEnv IntIState
st)

{- | Returns the list of all edges, if it is not up to date
the funcrion recomputes the list -}
getAllEdges :: IntIState -> [LEdge DGLinkLab]
getAllEdges :: IntIState -> [LEdge DGLinkLab]
getAllEdges st :: IntIState
st = DGraph -> [LEdge DGLinkLab]
labEdgesDG (DGraph -> [LEdge DGLinkLab]) -> DGraph -> [LEdge DGLinkLab]
forall a b. (a -> b) -> a -> b
$ LibName -> LibEnv -> DGraph
lookupDGraph (IntIState -> LibName
i_ln IntIState
st) (IntIState -> LibEnv
i_libEnv IntIState
st)

-- | Constructor for CMDLProofGUIState datatype
initNodeInfo :: ProofState -> Int -> Int_NodeInfo
initNodeInfo :: ProofState -> Int -> Int_NodeInfo
initNodeInfo = ProofState -> Int -> Int_NodeInfo
Element

emptyIntIState :: LibEnv -> LibName -> IntIState
emptyIntIState :: LibEnv -> LibName -> IntIState
emptyIntIState le :: LibEnv
le ln :: LibName
ln =
  IntIState :: LibEnv
-> LibName
-> [Int_NodeInfo]
-> Maybe AnyComorphism
-> Maybe G_prover
-> Maybe G_cons_checker
-> Bool
-> Bool
-> Bool
-> ATPTacticScript
-> Bool
-> IntIState
IntIState {
    i_libEnv :: LibEnv
i_libEnv = LibEnv
le,
    i_ln :: LibName
i_ln = LibName
ln,
    elements :: [Int_NodeInfo]
elements = [],
    cComorphism :: Maybe AnyComorphism
cComorphism = Maybe AnyComorphism
forall a. Maybe a
Nothing,
    prover :: Maybe G_prover
prover = Maybe G_prover
forall a. Maybe a
Nothing,
    consChecker :: Maybe G_cons_checker
consChecker = Maybe G_cons_checker
forall a. Maybe a
Nothing,
    save2file :: Bool
save2file = Bool
False,
    useTheorems :: Bool
useTheorems = Bool
False,
    showOutput :: Bool
showOutput = Bool
False,
    script :: ATPTacticScript
script = ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript {
                 tsTimeLimit :: Int
tsTimeLimit = 20,
                 tsExtraOpts :: [String]
tsExtraOpts = [] },
    loadScript :: Bool
loadScript = Bool
False
    }

emptyIntState :: IntState
emptyIntState :: IntState
emptyIntState =
    IntState :: IntHistory -> Maybe IntIState -> String -> IntState
IntState { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> IntIState
emptyIntIState LibEnv
emptyLibEnv (LibName -> IntIState) -> LibName -> IntIState
forall a b. (a -> b) -> a -> b
$ IRI -> LibName
iriLibName IRI
nullIRI
             , i_hist :: IntHistory
i_hist = IntHistory :: [CmdHistory] -> [CmdHistory] -> IntHistory
IntHistory { undoList :: [CmdHistory]
undoList = []
                                    , redoList :: [CmdHistory]
redoList = [] }
             , filename :: String
filename = []
             }

{- If an absolute path is given,
it tries to remove the current working directory as prefix of it. -}
tryRemoveAbsolutePathComponent :: String -> IO String
tryRemoveAbsolutePathComponent :: String -> IO String
tryRemoveAbsolutePathComponent f :: String
f
   | "/" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
f = do
                           String
dir <- IO String
getCurrentDirectory
                           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
$ String -> String -> String
tryToStripPrefix (String
dir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/") String
f
   | Bool
otherwise = String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
f

-- Converts a list of proof-trees to a prove
proofTreeToProve :: FilePath
     -> ProofState                         -- current proofstate
     -> Maybe (G_prover, AnyComorphism)    -- possible used translation
     -> [ProofStatus proof_tree]           -- goals included in prove
     -> String
     -> (Bool, Int)
     -> [IC.Command]
proofTreeToProve :: String
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> [Command]
proofTreeToProve fn :: String
fn st :: ProofState
st pcm :: Maybe (G_prover, AnyComorphism)
pcm pt :: [ProofStatus proof_tree]
pt nodeName :: String
nodeName (useTm :: Bool
useTm, tm :: Int
tm) =
    [ SelectCmd -> String -> Command
IC.SelectCmd SelectCmd
IC.Node String
nodeName', GlobCmd -> Command
IC.GlobCmd GlobCmd
IC.DropTranslation ]
    [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ [Command]
-> (AnyComorphism -> [Command]) -> Maybe AnyComorphism -> [Command]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\ (Comorphism cid :: cid
cid) -> (String -> Command) -> [String] -> [Command]
forall a b. (a -> b) -> [a] -> [b]
map
                 (SelectCmd -> String -> Command
IC.SelectCmd SelectCmd
IC.ComorphismTranslation)
                 (Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop 1 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ';' (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid)) Maybe AnyComorphism
commorf
    [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ [Command] -> (String -> [Command]) -> Maybe String -> [Command]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((Command -> [Command] -> [Command]
forall a. a -> [a] -> [a]
: []) (Command -> [Command])
-> (String -> Command) -> String -> [Command]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SelectCmd -> String -> Command
IC.SelectCmd SelectCmd
IC.Prover) Maybe String
prvr
    [Command] -> [Command] -> [Command]
forall a. [a] -> [a] -> [a]
++ ((String, Int) -> [Command]) -> [(String, Int)] -> [Command]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Int) -> [Command]
goalToCommands [(String, Int)]
goals
    where
      -- selected prover
      prvr :: Maybe String
prvr = Maybe String
-> ((G_prover, AnyComorphism) -> Maybe String)
-> Maybe (G_prover, AnyComorphism)
-> Maybe String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ProofState -> Maybe String
selectedProver ProofState
st) (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> ((G_prover, AnyComorphism) -> String)
-> (G_prover, AnyComorphism)
-> Maybe String
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) Maybe (G_prover, AnyComorphism)
pcm
      -- selected translation
      commorf :: Maybe AnyComorphism
commorf = case ProofState -> Maybe String
selectedProver ProofState
st of
          Nothing -> Maybe AnyComorphism
forall a. Maybe a
Nothing
          Just theProver :: String
theProver ->
            case String -> Map String [AnyComorphism] -> Maybe [AnyComorphism]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
theProver (Map String [AnyComorphism] -> Maybe [AnyComorphism])
-> Map String [AnyComorphism] -> Maybe [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ ProofState -> Map String [AnyComorphism]
proversMap ProofState
st of
              Nothing -> Maybe AnyComorphism
forall a. Maybe a
Nothing
              Just com :: [AnyComorphism]
com -> AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just (AnyComorphism -> Maybe AnyComorphism)
-> AnyComorphism -> Maybe AnyComorphism
forall a b. (a -> b) -> a -> b
$ [AnyComorphism] -> AnyComorphism
forall a. [a] -> a
head [AnyComorphism]
com
      {- 1. filter out the not proven goals
      2. reverse the list, because the last proven goals are on top
      3. convert all proof-trees to goals
      4. merge goals with same used axioms -}
      goals :: [(String, Int)]
goals = [(String, Int)] -> [(String, Int)]
mergeGoals ([(String, Int)] -> [(String, Int)])
-> [(String, Int)] -> [(String, Int)]
forall a b. (a -> b) -> a -> b
$ [(String, Int)] -> [(String, Int)]
forall a. [a] -> [a]
reverse
                  ([(String, Int)] -> [(String, Int)])
-> [(String, Int)] -> [(String, Int)]
forall a b. (a -> b) -> a -> b
$ (ProofStatus proof_tree -> (String, Int))
-> [ProofStatus proof_tree] -> [(String, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: ProofStatus proof_tree
x -> (ProofStatus proof_tree -> String
forall proof_tree. ProofStatus proof_tree -> String
goalName ProofStatus proof_tree
x, ProofStatus proof_tree -> Int
forall proof_tree. ProofStatus proof_tree -> Int
parseTimeLimit ProofStatus proof_tree
x))
                  ([ProofStatus proof_tree] -> [(String, Int)])
-> [ProofStatus proof_tree] -> [(String, Int)]
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
wasProved [ProofStatus proof_tree]
pt
      -- axioms to include in prove
      allax :: [String]
allax = ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst ([(String, Bool)] -> [String]) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> a -> b
$ ProofState -> [(String, Bool)]
getAxioms ProofState
st
      nodeName' :: String
nodeName' = if String
nodeName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then String -> String -> String
dropName String
fn (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ ProofState -> String
theoryName ProofState
st
                                    else String
nodeName
      -- A goal is a pair of a name as String and time limit as Int
      goalToCommands :: (String, Int) -> [IC.Command]
      goalToCommands :: (String, Int) -> [Command]
goalToCommands (n :: String
n, t :: Int
t) =
          [ SelectCmd -> String -> Command
IC.SelectCmd SelectCmd
IC.Goal String
n
          , [String] -> Command
IC.SetAxioms [String]
allax
          , Int -> Command
IC.TimeLimit (if Bool
useTm then Int
tm else Int
t)
          , GlobCmd -> Command
IC.GlobCmd GlobCmd
IC.ProveCurrent]

-- Merge goals with the same time-limit
mergeGoals :: [(String, Int)] -> [(String, Int)]
mergeGoals :: [(String, Int)] -> [(String, Int)]
mergeGoals i :: [(String, Int)]
i = case [(String, Int)]
i of
  (n :: String
n, l :: Int
l) : t :: [(String, Int)]
t@((n' :: String
n', l' :: Int
l') : tl :: [(String, Int)]
tl) ->
    if Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
l' then [(String, Int)] -> [(String, Int)]
mergeGoals ([(String, Int)] -> [(String, Int)])
-> [(String, Int)] -> [(String, Int)]
forall a b. (a -> b) -> a -> b
$ (String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
n', Int
l) (String, Int) -> [(String, Int)] -> [(String, Int)]
forall a. a -> [a] -> [a]
: [(String, Int)]
tl
    else (String
n, Int
l) (String, Int) -> [(String, Int)] -> [(String, Int)]
forall a. a -> [a] -> [a]
: [(String, Int)] -> [(String, Int)]
mergeGoals [(String, Int)]
t
  _ -> [(String, Int)]
i

dropName :: String -> String -> String
dropName :: String -> String -> String
dropName fch :: String
fch s :: String
s = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
s String -> String
forall a. [a] -> [a]
tail (String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
fch String
s)

-- This checks wether a goal was proved or not
wasProved :: ProofStatus proof_Tree -> Bool
wasProved :: ProofStatus proof_Tree -> Bool
wasProved g :: ProofStatus proof_Tree
g = case ProofStatus proof_Tree -> GoalStatus
forall proof_tree. ProofStatus proof_tree -> GoalStatus
goalStatus ProofStatus proof_Tree
g of
    Proved _ -> Bool
True
    _ -> Bool
False

-- Converts a proof-tree into a goal.
parseTimeLimit :: ProofStatus proof_tree -> Int
parseTimeLimit :: ProofStatus proof_tree -> Int
parseTimeLimit pt :: ProofStatus proof_tree
pt =
  if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
lns then 20 else String -> Int
forall a. Read a => String -> a
read (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
tlStr) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. [a] -> a
last [String]
lns
  where
    TacticScript scrpt :: String
scrpt = ProofStatus proof_tree -> TacticScript
forall proof_tree. ProofStatus proof_tree -> TacticScript
tacticScript ProofStatus proof_tree
pt
    lns :: [String]
lns = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
tlStr) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn '\n' String
scrpt
    tlStr :: String
tlStr = "Time limit: "

addCommandHistoryToState :: IORef IntState
    -> ProofState                    -- current proofstate
    -> Maybe (G_prover, AnyComorphism) -- possible used translation
    -> [ProofStatus proof_tree]       -- goals included in prove
    -> String
    -> (Bool, Int)
    -> IO ()
addCommandHistoryToState :: IORef IntState
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> IO ()
addCommandHistoryToState intSt :: IORef IntState
intSt st :: ProofState
st pcm :: Maybe (G_prover, AnyComorphism)
pcm pt :: [ProofStatus proof_tree]
pt str :: String
str (useTm :: Bool
useTm, timeout :: Int
timeout) =
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (ProofStatus proof_tree -> Bool)
-> [ProofStatus proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProofStatus proof_tree -> Bool
forall proof_Tree. ProofStatus proof_Tree -> Bool
wasProved [ProofStatus proof_tree]
pt) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
intSt
        String
fn <- String -> IO String
tryRemoveAbsolutePathComponent (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ IntState -> String
filename IntState
ost
        IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
intSt (IntState -> IO ()) -> IntState -> IO ()
forall a b. (a -> b) -> a -> b
$ Command -> IntState -> [UndoRedoElem] -> IntState
add2history
           ([Command] -> Command
IC.GroupCmd ([Command] -> Command) -> [Command] -> Command
forall a b. (a -> b) -> a -> b
$ String
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> [Command]
forall proof_tree.
String
-> ProofState
-> Maybe (G_prover, AnyComorphism)
-> [ProofStatus proof_tree]
-> String
-> (Bool, Int)
-> [Command]
proofTreeToProve (String -> String
rmSuffix String
fn) ProofState
st Maybe (G_prover, AnyComorphism)
pcm [ProofStatus proof_tree]
pt String
str
            (Bool
useTm, Int
timeout)) IntState
ost [Maybe IntIState -> UndoRedoElem
IStateChange (Maybe IntIState -> UndoRedoElem)
-> Maybe IntIState -> UndoRedoElem
forall a b. (a -> b) -> a -> b
$ IntState -> Maybe IntIState
i_state IntState
ost]

conservativityRule :: DGRule
conservativityRule :: DGRule
conservativityRule = String -> DGRule
DGRule "ConservativityCheck"

conservativityChoser :: Bool -> [ConservativityChecker sign sentence morphism]
  -> IO (Result (ConservativityChecker sign sentence morphism))
#ifdef UNI_PACKAGE
conservativityChoser :: Bool
-> [ConservativityChecker sign sentence morphism]
-> IO (Result (ConservativityChecker sign sentence morphism))
conservativityChoser useGUI :: Bool
useGUI checkers :: [ConservativityChecker sign sentence morphism]
checkers = case [ConservativityChecker sign sentence morphism]
checkers of
  [] -> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (ConservativityChecker sign sentence morphism)
 -> IO (Result (ConservativityChecker sign sentence morphism)))
-> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall a b. (a -> b) -> a -> b
$ String -> Result (ConservativityChecker sign sentence morphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "No conservativity checker available"
  hd :: ConservativityChecker sign sentence morphism
hd : tl :: [ConservativityChecker sign sentence morphism]
tl ->
    if Bool
useGUI Bool -> Bool -> Bool
&& Bool -> Bool
not ([ConservativityChecker sign sentence morphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConservativityChecker sign sentence morphism]
tl) then do
      Maybe Int
chosenOne <- String -> [String] -> IO (Maybe Int)
listBox "Pick a conservativity checker"
                                ([String] -> IO (Maybe Int)) -> [String] -> IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ (ConservativityChecker sign sentence morphism -> String)
-> [ConservativityChecker sign sentence morphism] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ConservativityChecker sign sentence morphism -> String
forall sign sentence morphism.
ConservativityChecker sign sentence morphism -> String
checkerId [ConservativityChecker sign sentence morphism]
checkers
      case Maybe Int
chosenOne of
        Nothing -> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (ConservativityChecker sign sentence morphism)
 -> IO (Result (ConservativityChecker sign sentence morphism)))
-> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall a b. (a -> b) -> a -> b
$ String -> Result (ConservativityChecker sign sentence morphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "No conservativity checker chosen"
        Just i :: Int
i -> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (ConservativityChecker sign sentence morphism)
 -> IO (Result (ConservativityChecker sign sentence morphism)))
-> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall a b. (a -> b) -> a -> b
$ ConservativityChecker sign sentence morphism
-> Result (ConservativityChecker sign sentence morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConservativityChecker sign sentence morphism
 -> Result (ConservativityChecker sign sentence morphism))
-> ConservativityChecker sign sentence morphism
-> Result (ConservativityChecker sign sentence morphism)
forall a b. (a -> b) -> a -> b
$ [ConservativityChecker sign sentence morphism]
checkers [ConservativityChecker sign sentence morphism]
-> Int -> ConservativityChecker sign sentence morphism
forall a. [a] -> Int -> a
!! Int
i
   else
#else
conservativityChoser _ checkers = case checkers of
  [] -> return $ Fail.fail "No conservativity checker available"
  hd : _ ->
#endif
   Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (ConservativityChecker sign sentence morphism)
 -> IO (Result (ConservativityChecker sign sentence morphism)))
-> Result (ConservativityChecker sign sentence morphism)
-> IO (Result (ConservativityChecker sign sentence morphism))
forall a b. (a -> b) -> a -> b
$ ConservativityChecker sign sentence morphism
-> Result (ConservativityChecker sign sentence morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return ConservativityChecker sign sentence morphism
hd

checkConservativityNode :: Bool -> LNode DGNodeLab -> LibEnv -> LibName
  -> IO (String, LibEnv, ProofHistory)
checkConservativityNode :: Bool
-> LNode DGNodeLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, ProofHistory)
checkConservativityNode useGUI :: Bool
useGUI (nodeId :: Int
nodeId, nodeLab :: DGNodeLab
nodeLab) libEnv :: LibEnv
libEnv ln :: LibName
ln = do
  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
      emptyTh :: G_theory
emptyTh = case DGNodeLab -> G_sign
dgn_sign DGNodeLab
nodeLab of
        G_sign lid :: lid
lid _ _ ->
            lid -> ExtSign sign symbol -> SigId -> 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 -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign (sign -> ExtSign sign symbol) -> sign -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid) SigId
startSigId
      newN :: Int
newN = DGraph -> Int
getNewNodeDG DGraph
dg
      newL :: DGNodeLab
newL = (NodeName -> DGOrigin -> G_theory -> DGNodeLab
newNodeLab NodeName
emptyNodeName DGOrigin
DGProof G_theory
emptyTh)
             { globalTheory :: Maybe G_theory
globalTheory = G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just G_theory
emptyTh }
      morphism :: GMorphism
morphism = String -> Result GMorphism -> GMorphism
forall a. String -> Result a -> a
propagateErrors "Utils.checkConservativityNode"
                 (Result GMorphism -> GMorphism) -> Result GMorphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
logicGraph (DGNodeLab -> G_sign
dgn_sign DGNodeLab
newL) (G_sign -> Result GMorphism) -> G_sign -> Result GMorphism
forall a b. (a -> b) -> a -> b
$
                   DGNodeLab -> G_sign
dgn_sign DGNodeLab
nodeLab
      lnk :: LEdge DGLinkLab
lnk = (Int
newN, Int
nodeId, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink
        GMorphism
morphism (Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
Global LinkKind
DefLink (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> ConsStatus
getNodeConsStatus DGNodeLab
nodeLab)
        DGLinkOrigin
SeeSource)
      (tmpDG :: DGraph
tmpDG, _) = DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly DGraph
dg (DGChange -> (DGraph, DGChange)) -> DGChange -> (DGraph, DGChange)
forall a b. (a -> b) -> a -> b
$ LNode DGNodeLab -> DGChange
InsertNode (Int
newN, DGNodeLab
newL)
      (tempDG :: DGraph
tempDG, InsertEdge lnk' :: LEdge DGLinkLab
lnk') = DGraph -> DGChange -> (DGraph, DGChange)
updateDGOnly DGraph
tmpDG (DGChange -> (DGraph, DGChange)) -> DGChange -> (DGraph, DGChange)
forall a b. (a -> b) -> a -> b
$ LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
lnk
      tempLibEnv :: LibEnv
tempLibEnv = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
tempDG LibEnv
libEnv
  (str :: String
str, _, (_, _, lnkLab :: DGLinkLab
lnkLab), _) <-
    Bool
-> LEdge DGLinkLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
checkConservativityEdge Bool
useGUI LEdge DGLinkLab
lnk' LibEnv
tempLibEnv LibName
ln
  if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "No conservativity" String
str
    then (String, LibEnv, ProofHistory) -> IO (String, LibEnv, ProofHistory)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
str, LibEnv
libEnv, ProofHistory
forall a. SizedList a
SizedList.empty)
    else do
         let nInfo :: DGNodeInfo
nInfo = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nodeLab
             nodeLab' :: DGNodeLab
nodeLab' = DGNodeLab
nodeLab { nodeInfo :: DGNodeInfo
nodeInfo = DGNodeInfo
nInfo { node_cons_status :: ConsStatus
node_cons_status =
                          DGLinkLab -> ConsStatus
getEdgeConsStatus DGLinkLab
lnkLab } }
             changes :: [DGChange]
changes = [ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
nodeLab (Int
nodeId, DGNodeLab
nodeLab') ]
             dg' :: DGraph
dg' = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
changes
             history :: ProofHistory
history = (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a, b) -> b
snd ((ProofHistory, ProofHistory) -> ProofHistory)
-> (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory DGraph
dg DGraph
dg'
             libEnv' :: LibEnv
libEnv' = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
conservativityRule DGraph
dg')
               LibEnv
libEnv
         (String, LibEnv, ProofHistory) -> IO (String, LibEnv, ProofHistory)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
str, LibEnv
libEnv', ProofHistory
history)

getUsableConservativityCheckersForLogic :: Logic lid sublogics
    basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree
    => lid -> IO [ConservativityChecker sign sentence morphism]
getUsableConservativityCheckersForLogic :: lid -> IO [ConservativityChecker sign sentence morphism]
getUsableConservativityCheckersForLogic lid :: lid
lid = (ConservativityChecker sign sentence morphism -> IO Bool)
-> [ConservativityChecker sign sentence morphism]
-> IO [ConservativityChecker sign sentence morphism]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool)
-> (ConservativityChecker sign sentence morphism
    -> IO (Maybe String))
-> ConservativityChecker sign sentence morphism
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConservativityChecker sign sentence morphism -> IO (Maybe String)
forall sign sentence morphism.
ConservativityChecker sign sentence morphism -> IO (Maybe String)
checkerUsable) ([ConservativityChecker sign sentence morphism]
 -> IO [ConservativityChecker sign sentence morphism])
-> [ConservativityChecker sign sentence morphism]
-> IO [ConservativityChecker sign sentence morphism]
forall a b. (a -> b) -> a -> b
$ lid -> [ConservativityChecker sign sentence morphism]
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 -> [ConservativityChecker sign sentence morphism]
conservativityCheck lid
lid


getUsableConservativityCheckers :: LEdge DGLinkLab -> LibEnv -> LibName -> IO [G_conservativity_checker]
getUsableConservativityCheckers :: LEdge DGLinkLab
-> LibEnv -> LibName -> IO [G_conservativity_checker]
getUsableConservativityCheckers (_, target :: Int
target, _) libEnv :: LibEnv
libEnv ln :: LibName
ln = do
  Just (G_theory lidT :: lid
lidT _ _ _ _ _) <- Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> IO (Maybe G_theory))
-> Maybe G_theory -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Int
target
  [ConservativityChecker sign sentence morphism]
usableCCs <- lid -> IO [ConservativityChecker sign sentence morphism]
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 -> IO [ConservativityChecker sign sentence morphism]
getUsableConservativityCheckersForLogic lid
lidT
  [G_conservativity_checker] -> IO [G_conservativity_checker]
forall (m :: * -> *) a. Monad m => a -> m a
return ([G_conservativity_checker] -> IO [G_conservativity_checker])
-> [G_conservativity_checker] -> IO [G_conservativity_checker]
forall a b. (a -> b) -> a -> b
$ lid
-> ConservativityChecker sign sentence morphism
-> G_conservativity_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
-> ConservativityChecker sign sentence morphism
-> G_conservativity_checker
G_conservativity_checker lid
lidT (ConservativityChecker sign sentence morphism
 -> G_conservativity_checker)
-> [ConservativityChecker sign sentence morphism]
-> [G_conservativity_checker]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ConservativityChecker sign sentence morphism]
usableCCs


checkConservativityEdgeWith ::  LEdge DGLinkLab -> LibEnv -> LibName -> G_conservativity_checker
  -> IO (Result (Conservativity, G_theory, G_theory)) -- (conservativity, obligations holding in the source theory, obligations required to hold in an imported theory)
checkConservativityEdgeWith :: LEdge DGLinkLab
-> LibEnv
-> LibName
-> G_conservativity_checker
-> IO (Result (Conservativity, G_theory, G_theory))
checkConservativityEdgeWith (source :: Int
source, target :: Int
target, linklab :: DGLinkLab
linklab) libEnv :: LibEnv
libEnv ln :: LibName
ln (G_conservativity_checker lidCC :: lid
lidCC cc :: ConservativityChecker sign sentence morphism
cc) = do
  Just (G_theory lidT :: lid
lidT _ signT :: ExtSign sign symbol
signT _ sensT :: ThSens sentence (AnyComorphism, BasicProof)
sensT _) <-
      Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> IO (Maybe G_theory))
-> Maybe G_theory -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Int
target
  Just (G_theory lidS :: lid
lidS _ signS :: ExtSign sign symbol
signS _ sensS :: ThSens sentence (AnyComorphism, BasicProof)
sensS _) <-
      Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> IO (Maybe G_theory))
-> Maybe G_theory -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Int
source
  ConservativityChecker sign sentence morphism
cc' <- lid
-> lid
-> String
-> ConservativityChecker sign sentence morphism
-> IO (ConservativityChecker sign sentence morphism)
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
-> ConservativityChecker sign1 sentence1 morphism1
-> m (ConservativityChecker sign2 sentence2 morphism2)
coerceConservativityChecker lid
lidCC lid
lidT "checkconservativityOfEdge0" ConservativityChecker sign sentence morphism
cc
  ThSens sentence (AnyComorphism, BasicProof)
sensS' <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (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
lidS lid
lidT "checkconservativityOfEdge1" ThSens sentence (AnyComorphism, BasicProof)
sensS
  GMorphism cid :: cid
cid _ _ morphism :: morphism2
morphism _ <- GMorphism -> IO GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> IO GMorphism) -> GMorphism -> IO GMorphism
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
linklab
  morphism
morphism' <- lid2 -> lid -> String -> morphism2 -> IO morphism
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 -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid) lid
lidT
                "checkconservativityOfEdge" morphism2
morphism
  let compMor :: morphism
compMor = case DGNodeLab -> Maybe GMorphism
dgn_sigma (DGNodeLab -> Maybe GMorphism) -> DGNodeLab -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> DGNodeLab
labDG (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv) Int
target of
          Nothing -> morphism
morphism'
          Just (GMorphism cid' :: cid
cid' _ _ morphism2 :: morphism2
morphism2 _) -> case
            lid2 -> lid -> String -> morphism2 -> Result morphism
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 -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid') lid
lidT
                  "checkconservativityOfEdge" morphism2
morphism2
              Result morphism -> (morphism -> Result morphism) -> Result morphism
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= morphism -> morphism -> Result morphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism
morphism' of
                Result _ (Just phi :: morphism
phi) -> morphism
phi
                _ -> String -> morphism
forall a. HasCallStack => String -> a
error "checkconservativityOfEdge: comp"
  let sensTransS :: ThSens sentence (AnyComorphism, BasicProof)
sensTransS = String
-> Result (ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
forall a. String -> Result a -> a
propagateErrors "checkConservativityEdge2"
        (Result (ThSens sentence (AnyComorphism, BasicProof))
 -> ThSens sentence (AnyComorphism, BasicProof))
-> Result (ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ (sentence -> Result sentence)
-> ThSens sentence (AnyComorphism, BasicProof)
-> Result (ThSens sentence (AnyComorphism, BasicProof))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> ThSens a c -> m (ThSens b c)
mapThSensValueM (lid -> morphism -> sentence -> Result sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> sentence -> Result sentence
map_sen lid
lidT morphism
compMor) ThSens sentence (AnyComorphism, BasicProof)
sensS'
  let sensTransS' :: Set sentence
sensTransS' = [sentence] -> Set sentence
forall a. Ord a => [a] -> Set a
Set.fromList ([sentence] -> Set sentence) -> [sentence] -> Set sentence
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence String -> sentence)
-> [SenAttr sentence String] -> [sentence]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr sentence String -> sentence
forall s a. SenAttr s a -> s
sentence ([SenAttr sentence String] -> [sentence])
-> [SenAttr sentence String] -> [sentence]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence String]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sensTransS
      axiomsT :: [SenAttr sentence String]
axiomsT = (SenAttr sentence String -> Bool)
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a. (a -> Bool) -> [a] -> [a]
filter SenAttr sentence String -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ([SenAttr sentence String] -> [SenAttr sentence String])
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence String]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sensT
      inputSensT :: [SenAttr sentence String]
inputSensT = (SenAttr sentence String -> Bool)
-> [SenAttr sentence String] -> [SenAttr sentence String]
forall a. (a -> Bool) -> [a] -> [a]
filter ((sentence -> Set sentence -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set sentence
sensTransS') (sentence -> Bool)
-> (SenAttr sentence String -> sentence)
-> SenAttr sentence String
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenAttr sentence String -> sentence
forall s a. SenAttr s a -> s
sentence) [SenAttr sentence String]
axiomsT
  case lid
-> lid
-> String
-> ExtSign sign symbol
-> Maybe (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lidS lid
lidT "checkconservativityOfEdge.coerceSign" ExtSign sign symbol
signS of
    Nothing -> String -> IO (Result (Conservativity, G_theory, G_theory))
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "no implementation for heterogeneous links"
    Just signS' :: ExtSign sign symbol
signS' -> ResultT IO (Conservativity, G_theory, G_theory)
-> IO (Result (Conservativity, G_theory, G_theory))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (Conservativity, G_theory, G_theory)
 -> IO (Result (Conservativity, G_theory, G_theory)))
-> ResultT IO (Conservativity, G_theory, G_theory)
-> IO (Result (Conservativity, G_theory, G_theory))
forall a b. (a -> b) -> a -> b
$ do
      (consv :: Conservativity
consv, outputSensT :: [sentence]
outputSensT) <- IO (Result (Conservativity, [sentence]))
-> ResultT IO (Conservativity, [sentence])
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result (Conservativity, [sentence]))
 -> ResultT IO (Conservativity, [sentence]))
-> IO (Result (Conservativity, [sentence]))
-> ResultT IO (Conservativity, [sentence])
forall a b. (a -> b) -> a -> b
$ ConservativityChecker sign sentence morphism
-> (sign, [SenAttr sentence String])
-> morphism
-> [SenAttr sentence String]
-> IO (Result (Conservativity, [sentence]))
forall sign sentence morphism.
ConservativityChecker sign sentence morphism
-> (sign, [Named sentence])
-> morphism
-> [Named sentence]
-> IO (Result (Conservativity, [sentence]))
checkConservativity ConservativityChecker sign sentence morphism
cc'
                (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
signS', ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence String]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sensS')
                morphism
compMor [SenAttr sentence String]
inputSensT
      let (explanations :: [sentence]
explanations, obligations :: [sentence]
obligations) = (sentence -> Bool) -> [sentence] -> ([sentence], [sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (sentence -> Set sentence -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set sentence
sensTransS') [sentence]
outputSensT
      let theoryForObligations :: [sentence] -> G_theory
theoryForObligations sens :: [sentence]
sens = 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 {
            gTheoryLogic :: lid
gTheoryLogic = lid
lidT
            , gTheorySyntax :: Maybe IRI
gTheorySyntax = Maybe IRI
forall a. Maybe a
Nothing
            , gTheorySign :: ExtSign sign symbol
gTheorySign = ExtSign sign symbol
signT
            , gTheorySignIdx :: SigId
gTheorySignIdx = SigId
startSigId
            , gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)
gTheorySens = [Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof))
-> [Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ (sentence -> Named sentence) -> [sentence] -> [Named sentence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\o :: sentence
o -> (String -> sentence -> Named sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" sentence
o) {isAxiom :: Bool
isAxiom = Bool
False}) [sentence]
sens
            , gTheorySelfIdx :: ThId
gTheorySelfIdx = ThId
startThId
          }
      (Conservativity, G_theory, G_theory)
-> ResultT IO (Conservativity, G_theory, G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity
consv, [sentence] -> G_theory
forall sublogics basic_spec sentence symb_items symb_map_items
       morphism raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
[sentence] -> G_theory
theoryForObligations [sentence]
explanations, [sentence] -> G_theory
forall sublogics basic_spec sentence symb_items symb_map_items
       morphism raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
[sentence] -> G_theory
theoryForObligations [sentence]
obligations)

conservativityResultToNewEdge :: LEdge DGLinkLab -> (Conservativity, G_theory, G_theory) -> (LEdge DGLinkLab, Bool)
conservativityResultToNewEdge :: LEdge DGLinkLab
-> (Conservativity, G_theory, G_theory) -> (LEdge DGLinkLab, Bool)
conservativityResultToNewEdge (source :: Int
source, target :: Int
target, linklab :: DGLinkLab
linklab) (consv :: Conservativity
consv, _, G_theory { gTheorySens :: ()
gTheorySens = ThSens sentence (AnyComorphism, BasicProof)
obligations }) =
  let consv' :: Conservativity
consv' = if ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
obligations then Conservativity
consv else String -> Conservativity
Unknown "unchecked obligations"
      (newDglType :: DGLinkType
newDglType, edgeChanged :: Bool
edgeChanged) = case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
linklab of
        ScopedLink sc :: Scope
sc dl :: LinkKind
dl (ConsStatus consv'' :: Conservativity
consv'' cs :: Conservativity
cs op :: ThmLinkStatus
op) ->
            let np :: ThmLinkStatus
np = if Conservativity
consv' Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
>= Conservativity
consv''
                      then DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
conservativityRule ProofBasis
emptyProofBasis
                      else ThmLinkStatus
LeftOpen
            in (Scope -> LinkKind -> ConsStatus -> DGLinkType
ScopedLink Scope
sc LinkKind
dl (ConsStatus -> DGLinkType) -> ConsStatus -> DGLinkType
forall a b. (a -> b) -> a -> b
$
                  Conservativity -> Conservativity -> ThmLinkStatus -> ConsStatus
ConsStatus Conservativity
consv'' (Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
max Conservativity
cs (Conservativity -> Conservativity)
-> Conservativity -> Conservativity
forall a b. (a -> b) -> a -> b
$ Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
max Conservativity
consv'' Conservativity
consv') ThmLinkStatus
np, ThmLinkStatus
np ThmLinkStatus -> ThmLinkStatus -> Bool
forall a. Eq a => a -> a -> Bool
/= ThmLinkStatus
op)
        t :: DGLinkType
t -> (DGLinkType
t, Bool
False)
  in ((Int
source, Int
target, DGLinkLab
linklab { dgl_type :: DGLinkType
dgl_type = DGLinkType
newDglType }), Bool
edgeChanged)

recordConservativityResult :: LEdge DGLinkLab -> LibEnv -> LibName -> (Conservativity, G_theory, G_theory) -> LibEnv
recordConservativityResult :: LEdge DGLinkLab
-> LibEnv
-> LibName
-> (Conservativity, G_theory, G_theory)
-> LibEnv
recordConservativityResult edge :: LEdge DGLinkLab
edge@(source :: Int
source, target :: Int
target, linklab :: DGLinkLab
linklab) libEnv :: LibEnv
libEnv ln :: LibName
ln checkResult :: (Conservativity, G_theory, G_theory)
checkResult =
  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
      (provenEdge :: LEdge DGLinkLab
provenEdge, edgeChanged :: Bool
edgeChanged) = LEdge DGLinkLab
-> (Conservativity, G_theory, G_theory) -> (LEdge DGLinkLab, Bool)
conservativityResultToNewEdge LEdge DGLinkLab
edge (Conservativity, G_theory, G_theory)
checkResult
      edgeChanges :: [DGChange]
edgeChanges = if Bool
edgeChanged then
                  [ LEdge DGLinkLab -> DGChange
DeleteEdge (Int
source, Int
target, DGLinkLab
linklab)
                  , LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
provenEdge ] else []
      nextDG :: DGraph
nextDG = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
edgeChanges
  in if Bool -> Bool
not Bool
edgeChanged then LibEnv
libEnv else
    LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln (DGraph -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
conservativityRule DGraph
nextDG) LibEnv
libEnv


checkConservativityEdge :: Bool -> LEdge DGLinkLab -> LibEnv -> LibName
  -> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
checkConservativityEdge :: Bool
-> LEdge DGLinkLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
checkConservativityEdge useGUI :: Bool
useGUI link :: LEdge DGLinkLab
link@(_, target :: Int
target, _) libEnv :: LibEnv
libEnv ln :: LibName
ln = do
  Just (G_theory lidT :: lid
lidT _ sigT :: ExtSign sign symbol
sigT _ _ _) <-
    Maybe G_theory -> IO (Maybe G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe G_theory -> IO (Maybe G_theory))
-> Maybe G_theory -> IO (Maybe G_theory)
forall a b. (a -> b) -> a -> b
$ LibEnv -> LibName -> Int -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Int
target
  [ConservativityChecker sign sentence morphism]
usableCs <- lid -> IO [ConservativityChecker sign sentence morphism]
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 -> IO [ConservativityChecker sign sentence morphism]
getUsableConservativityCheckersForLogic lid
lidT
  Result (ConservativityChecker sign sentence morphism)
checkerR <- Bool
-> [ConservativityChecker sign sentence morphism]
-> IO (Result (ConservativityChecker sign sentence morphism))
forall sign sentence morphism.
Bool
-> [ConservativityChecker sign sentence morphism]
-> IO (Result (ConservativityChecker sign sentence morphism))
conservativityChoser Bool
useGUI [ConservativityChecker sign sentence morphism]
usableCs
  case Result (ConservativityChecker sign sentence morphism)
-> Maybe (ConservativityChecker sign sentence morphism)
forall a. Result a -> Maybe a
maybeResult Result (ConservativityChecker sign sentence morphism)
checkerR of
    Nothing -> (String, LibEnv, LEdge DGLinkLab, ProofHistory)
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Diagnosis -> String) -> [Diagnosis] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Diagnosis -> String
diagString ([Diagnosis] -> String) -> [Diagnosis] -> String
forall a b. (a -> b) -> a -> b
$ Result (ConservativityChecker sign sentence morphism)
-> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags Result (ConservativityChecker sign sentence morphism)
checkerR,
                        LibEnv
libEnv, LEdge DGLinkLab
link, ProofHistory
forall a. SizedList a
SizedList.empty)
    Just theChecker :: ConservativityChecker sign sentence morphism
theChecker -> do
      Result ds :: [Diagnosis]
ds res :: Maybe (Conservativity, G_theory, G_theory)
res <- LEdge DGLinkLab
-> LibEnv
-> LibName
-> G_conservativity_checker
-> IO (Result (Conservativity, G_theory, G_theory))
checkConservativityEdgeWith LEdge DGLinkLab
link LibEnv
libEnv LibName
ln (lid
-> ConservativityChecker sign sentence morphism
-> G_conservativity_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
-> ConservativityChecker sign sentence morphism
-> G_conservativity_checker
G_conservativity_checker lid
lidT ConservativityChecker sign sentence morphism
theChecker)
      (_, showRes :: String
showRes, newLibEnv :: LibEnv
newLibEnv, provenEdge :: LEdge DGLinkLab
provenEdge) <- case Maybe (Conservativity, G_theory, G_theory)
res of
            Just conservativityResult :: (Conservativity, G_theory, G_theory)
conservativityResult@(consv :: Conservativity
consv, G_theory {gTheoryLogic :: ()
gTheoryLogic = lid
lidR1, gTheorySens :: ()
gTheorySens = ThSens sentence (AnyComorphism, BasicProof)
explanations}, G_theory {gTheoryLogic :: ()
gTheoryLogic = lid
lidR2, gTheorySens :: ()
gTheorySens = ThSens sentence (AnyComorphism, BasicProof)
obligations}) -> do
              [Named sentence]
explanations' <- ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence])
-> IO (ThSens sentence (AnyComorphism, BasicProof))
-> IO [Named sentence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (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
lidR1 lid
lidT "checkConservativityEdge" ThSens sentence (AnyComorphism, BasicProof)
explanations
              [Named sentence]
obligations' <- ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence])
-> IO (ThSens sentence (AnyComorphism, BasicProof))
-> IO [Named sentence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> IO (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
lidR2 lid
lidT "checkConservativityEdge" ThSens sentence (AnyComorphism, BasicProof)
obligations
              let showObls :: [Named sentence] -> String
showObls = Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> ([Named sentence] -> Doc) -> [Named sentence] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
Pretty.vsep
                    ([Doc] -> Doc)
-> ([Named sentence] -> [Doc]) -> [Named sentence] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named sentence -> Doc) -> [Named sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> Named sentence -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lidT (Named sentence -> Doc)
-> (Named sentence -> Named sentence) -> Named sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                     (sentence -> sentence) -> Named sentence -> Named sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lidT
                                        (sign -> sentence -> sentence) -> sign -> sentence -> sentence
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sigT))
              let libEnv' :: LibEnv
libEnv' = LEdge DGLinkLab
-> LibEnv
-> LibName
-> (Conservativity, G_theory, G_theory)
-> LibEnv
recordConservativityResult LEdge DGLinkLab
link LibEnv
libEnv LibName
ln (Conservativity, G_theory, G_theory)
conservativityResult
              let (provenEdge' :: LEdge DGLinkLab
provenEdge', _) = LEdge DGLinkLab
-> (Conservativity, G_theory, G_theory) -> (LEdge DGLinkLab, Bool)
conservativityResultToNewEdge LEdge DGLinkLab
link (Conservativity, G_theory, G_theory)
conservativityResult
              (Conservativity, String, LibEnv, LEdge DGLinkLab)
-> IO (Conservativity, String, LibEnv, LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
obligations' then Conservativity
consv
                else String -> Conservativity
Unknown "unchecked obligations"
                , "The link is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Conservativity -> String
showConsistencyStatus Conservativity
consv
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
obligations' then
                    (if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
explanations' then ""
                    else " because of the following axioms:\n"
                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Named sentence] -> String
showObls [Named sentence]
explanations')
                  else " provided that the following obligations\n"
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ "hold in an imported theory:\n"
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Named sentence] -> String
showObls [Named sentence]
obligations', LibEnv
libEnv', LEdge DGLinkLab
provenEdge')
            Nothing -> (Conservativity, String, LibEnv, LEdge DGLinkLab)
-> IO (Conservativity, String, LibEnv, LEdge DGLinkLab)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Conservativity
Unknown "Unknown", "Could not determine whether link is conservative", LibEnv
libEnv, LEdge DGLinkLab
link)
      let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
          newDG :: DGraph
newDG = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
newLibEnv
          history :: ProofHistory
history = (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a, b) -> b
snd ((ProofHistory, ProofHistory) -> ProofHistory)
-> (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory DGraph
dg DGraph
newDG
          myDiags :: String
myDiags = Int -> [Diagnosis] -> String
showRelDiags 4 [Diagnosis]
ds
      (String, LibEnv, LEdge DGLinkLab, ProofHistory)
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
forall (m :: * -> *) a. Monad m => a -> m a
return ( String
showRes String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
myDiags
              , LibEnv
newLibEnv, LEdge DGLinkLab
provenEdge, ProofHistory
history)

updateNodeProof :: LibName -> IntState -> LNode DGNodeLab
                -> G_theory -> (IntState, [DGChange])
updateNodeProof :: LibName
-> IntState
-> LNode DGNodeLab
-> G_theory
-> (IntState, [DGChange])
updateNodeProof ln :: LibName
ln ost :: IntState
ost (k :: Int
k, dgnode :: DGNodeLab
dgnode) thry :: G_theory
thry =
    case IntState -> Maybe IntIState
i_state IntState
ost of
      Nothing -> (IntState
ost, [])
      Just iist :: IntIState
iist ->
        let le :: LibEnv
le = IntIState -> LibEnv
i_libEnv IntIState
iist
            dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
            nn :: String
nn = DGNodeLab -> String
getDGNodeName DGNodeLab
dgnode
            newDg :: DGraph
newDg = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
le LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> DGChange -> DGraph
changeDGH DGraph
dg
              (DGChange -> DGraph) -> DGChange -> DGraph
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
dgnode (Int
k, DGNodeLab
dgnode { dgn_theory :: G_theory
dgn_theory = G_theory
thry })
            history :: [DGChange]
history = [DGChange] -> [DGChange]
forall a. [a] -> [a]
reverse ([DGChange] -> [DGChange]) -> [DGChange] -> [DGChange]
forall a b. (a -> b) -> a -> b
$ ProofHistory -> [DGChange]
flatHistory (ProofHistory -> [DGChange]) -> ProofHistory -> [DGChange]
forall a b. (a -> b) -> a -> b
$ (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a, b) -> b
snd ((ProofHistory, ProofHistory) -> ProofHistory)
-> (ProofHistory, ProofHistory) -> ProofHistory
forall a b. (a -> b) -> a -> b
$ DGraph -> DGraph -> (ProofHistory, ProofHistory)
splitHistory DGraph
dg DGraph
newDg
            nst :: IntState
nst = Command -> IntState -> [UndoRedoElem] -> IntState
add2history
                    (String -> Command
CommentCmd (String -> Command) -> String -> Command
forall a b. (a -> b) -> a -> b
$ "basic inference done on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
                    IntState
ost [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 } }
        in (IntState
nwst, [DGChange]
history)