{-# LANGUAGE CPP #-}
{- |
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
         , updateNodeProof
         ) where

import Interfaces.Command
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


#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)

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@(source :: Int
source, target :: Int
target, linklab :: DGLinkLab
linklab) libEnv :: LibEnv
libEnv ln :: LibName
ln
 = do

    Just (G_theory lidT :: lid
lidT _ sigT :: ExtSign sign symbol
sigT _ 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
    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"
    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
    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, LibEnv, LEdge DGLinkLab, ProofHistory)
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
forall (m :: * -> *) a. Monad m => a -> m a
return ( "no implementation for heterogeneous links"
                       , LibEnv
libEnv, LEdge DGLinkLab
link, ProofHistory
forall a. SizedList a
SizedList.empty)
     Just signS' :: ExtSign sign symbol
signS' -> do
      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
      let transSensSrc :: ThSens sentence (AnyComorphism, BasicProof)
transSensSrc = 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'
      [ConservativityChecker sign sentence morphism]
usableCs <- (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
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
               let inputThSens1 :: [SenAttr sentence String]
inputThSens1 = (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
                   transSrcSens :: Set sentence
transSrcSens = [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)
transSensSrc
                   inputThSens :: [SenAttr sentence String]
inputThSens = (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
transSrcSens) (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]
inputThSens1
                   showObls :: [sentence] -> String
showObls = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> ([sentence] -> Doc) -> [sentence] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
Pretty.vsep
                     ([Doc] -> Doc) -> ([sentence] -> [Doc]) -> [sentence] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sentence -> Doc) -> [sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ o :: sentence
o -> lid -> SenAttr sentence String -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lidT (SenAttr sentence String -> Doc)
-> (SenAttr sentence String -> SenAttr sentence String)
-> SenAttr sentence String
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                     (sentence -> sentence)
-> SenAttr sentence String -> SenAttr sentence String
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)
                           (SenAttr sentence String -> Doc) -> SenAttr sentence String -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> sentence -> SenAttr sentence String
forall a s. a -> s -> SenAttr s a
makeNamed "" sentence
o) {isAxiom :: Bool
isAxiom = Bool
False})
               Result ds :: [Diagnosis]
ds res :: Maybe (Conservativity, [sentence])
res <-
                       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
theChecker
                          (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]
inputThSens
               let (cs' :: Conservativity
cs', showRes :: String
showRes) = case Maybe (Conservativity, [sentence])
res of
                     Just (cst :: Conservativity
cst, obs :: [sentence]
obs) ->
                       let (exSens :: [sentence]
exSens, resObls :: [sentence]
resObls) = (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
transSrcSens) [sentence]
obs
                       in (if [sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [sentence]
resObls then Conservativity
cst
                           else String -> Conservativity
Unknown "unchecked obligations"
                       , "The link is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Conservativity -> String
showConsistencyStatus Conservativity
cst
                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ case [sentence]
resObls of
                              [] -> case [sentence]
exSens of
                                [] -> ""
                                _ -> " because of the following axioms:\n"
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ [sentence] -> String
showObls [sentence]
exSens
                              _ -> " 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]
++ [sentence] -> String
showObls [sentence]
resObls)
                     Nothing -> (String -> Conservativity
Unknown "Unknown"
                       , "Could not determine whether link is conservative")
                   consNew :: Conservativity -> ThmLinkStatus
consNew csv :: Conservativity
csv = if Conservativity
cs' Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
>= Conservativity
csv
                              then DGRule -> ProofBasis -> ThmLinkStatus
Proven DGRule
conservativityRule ProofBasis
emptyProofBasis
                              else ThmLinkStatus
LeftOpen
                   (newDglType :: DGLinkType
newDglType, edgeChange :: Bool
edgeChange) = 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 = Conservativity -> ThmLinkStatus
consNew Conservativity
consv 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
cs') ThmLinkStatus
np, ThmLinkStatus
np ThmLinkStatus -> ThmLinkStatus -> Bool
forall a. Eq a => a -> a -> Bool
/= ThmLinkStatus
op)
                     t :: DGLinkType
t -> (DGLinkType
t, Bool
False)
                   provenEdge :: LEdge DGLinkLab
provenEdge = ( Int
source
                                , Int
target
                                , DGLinkLab
linklab { dgl_type :: DGLinkType
dgl_type = DGLinkType
newDglType }
                                )
                   dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
libEnv
               let edgeChanges :: [DGChange]
edgeChanges = if Bool
edgeChange then
                            [ LEdge DGLinkLab -> DGChange
DeleteEdge (Int
source, Int
target, DGLinkLab
linklab)
                            , LEdge DGLinkLab -> DGChange
InsertEdge LEdge DGLinkLab
provenEdge ] else []
                   nextGr :: DGraph
nextGr = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
edgeChanges
                   newLibEnv :: LibEnv
newLibEnv = if Bool
edgeChange then 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
nextGr) LibEnv
libEnv
                     else LibEnv
libEnv
                   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
nextGr
                   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)