Utils.hs revision 4eefbf3ad21b510729d5423d08de513b310e9cd0
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder{-# LANGUAGE CPP #-}
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederModule :$Header$
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederDescription : utilitary functions
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederCopyright : uni-bremen and DFKI
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederMaintainer : r.pascanu@jacobs-university.de
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederStability : provisional
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : portable
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederInterfaces.Utils contains different utilitary functions for the
f799084b320209cdd71a29e74fff1be054c1d342Christian Maederabstract interface
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder ( getAllNodes
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , getAllEdges
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang , initNodeInfo
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang , emptyIntIState
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , emptyIntState
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , parseTimeLimit
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maeder , addCommandHistoryToState
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder , checkConservativityNode
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder , checkConservativityEdge
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder , updateNodeProof
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport qualified Interfaces.Command as IC
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport Data.Maybe (fromMaybe)
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maederimport Driver.Options (rmSuffix)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maederimport System.Directory (getCurrentDirectory)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maederimport Comorphisms.LogicGraph (logicGraph)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maederimport qualified Data.Map as Map
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport qualified Data.Set as Set
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport Common.Utils (splitOn)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maederimport qualified Common.Lib.SizedList as SizedList
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport Common.AS_Annotation (SenAttr (..), makeNamed, mapNamed)
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wangimport qualified Common.Doc as Pretty
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang#ifdef UNI_PACKAGE
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang{- | Returns the list of all nodes, if it is not up to date
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wangthe function recomputes the list -}
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian MaedergetAllNodes :: IntIState -> [LNode DGNodeLab]
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian MaedergetAllNodes st
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian Maeder = labNodesDG $ lookupDGraph (i_ln st) (i_libEnv st)
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang{- | Returns the list of all edges, if it is not up to date
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wangthe funcrion recomputes the list -}
264b794970b6f2bd437f14233f367f1067565728Jian Chun WanggetAllEdges :: IntIState -> [LEdge DGLinkLab]
264b794970b6f2bd437f14233f367f1067565728Jian Chun WanggetAllEdges st = labEdgesDG $ lookupDGraph (i_ln st) (i_libEnv st)
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder-- | Constructor for CMDLProofGUIState datatype
264b794970b6f2bd437f14233f367f1067565728Jian Chun WanginitNodeInfo :: ProofState -> Int -> Int_NodeInfo
264b794970b6f2bd437f14233f367f1067565728Jian Chun WanginitNodeInfo = Element
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian MaederemptyIntIState :: LibEnv -> LibName -> IntIState
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangemptyIntIState le ln =
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang i_libEnv = le,
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang elements = [],
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder cComorphism = Nothing,
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder prover = Nothing,
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang consChecker = Nothing,
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder save2file = False,
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder useTheorems = False,
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang script = ATPTacticScript {
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang tsTimeLimit = 20,
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder tsExtraOpts = [] },
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder loadScript = False
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangemptyIntState :: IntState
264b794970b6f2bd437f14233f367f1067565728Jian Chun WangemptyIntState =
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang IntState { i_state = Just $ emptyIntIState emptyLibEnv $ emptyLibName ""
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder , i_hist = IntHistory { undoList = []
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder , redoList = [] }
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder , filename = []
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder{- If an absolute path is given,
84855a862ab77950c0c5059b1bba98cce0fb8ac3Christian Maederit tries to remove the current working directory as prefix of it. -}
84855a862ab77950c0c5059b1bba98cce0fb8ac3Christian MaedertryRemoveAbsolutePathComponent :: String -> IO String
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian MaedertryRemoveAbsolutePathComponent f
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder | "/" `isPrefixOf` f = do
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang dir <- getCurrentDirectory
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder return $ fromMaybe f (stripPrefix (dir ++ "/") f)
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang | otherwise = return f
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder-- Converts a list of proof-trees to a prove
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederproofTreeToProve :: FilePath
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> ProofState -- current proofstate
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> Maybe (G_prover, AnyComorphism) -- possible used translation
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> [ProofStatus proof_tree] -- goals included in prove
479da8506f391abe070ced2fb93c9759a280fa68Christian MaederproofTreeToProve fn st pcm pt nodeName =
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder [ IC.SelectCmd IC.Node nodeName', IC.GlobCmd IC.DropTranslation ]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ++ maybe [] (\ (Comorphism cid) -> map (IC.SelectCmd
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder drop 1 $ splitOn ';' $ language_name cid) trans
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder ++ maybe [] ((: []) . IC.SelectCmd IC.Prover) prvr
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder ++ concatMap goalToCommands goals
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder -- selected prover
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder prvr = maybe (selectedProver st) (Just . getProverName . fst) pcm
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder -- selected translation
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder trans = fmap snd pcm
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder {- 1. filter out the not proven goals
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder 2. reverse the list, because the last proven goals are on top
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder 3. convert all proof-trees to goals
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder 4. merge goals with same used axioms -}
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder goals = mergeGoals $ reverse
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder $ map (\ x -> (goalName x, parseTimeLimit x))
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder $ filter wasProved pt
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian Maeder -- axioms to include in prove
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder allax = map fst $ getAxioms st
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder nodeName' = if (nodeName == "") then dropName fn $ theoryName st
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang else nodeName
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang -- A goal is a pair of a name as String and time limit as Int
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang goalToCommands :: (String, Int) -> [IC.Command]
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang goalToCommands (n, t) =
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder [ IC.SelectCmd IC.Goal n, IC.SetAxioms allax, IC.TimeLimit t,
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- Merge goals with the same time-limit
0015e1756b734b34d4b550318c078f9a0c585611Christian MaedermergeGoals :: [(String, Int)] -> [(String, Int)]
0015e1756b734b34d4b550318c078f9a0c585611Christian MaedermergeGoals [] = []
0015e1756b734b34d4b550318c078f9a0c585611Christian MaedermergeGoals (h : []) = [h]
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian MaedermergeGoals ((n, l) : t@((n', l') : tl))
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder | l == l' = mergeGoals $ (n ++ ' ' : n', l) : tl
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder | otherwise = (n, l) : mergeGoals t
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederdropName :: String -> String -> String
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian MaederdropName fch s = maybe s tail (stripPrefix fch s)
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder-- This checks wether a goal was proved or not
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian MaederwasProved :: ProofStatus proof_Tree -> Bool
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian MaederwasProved g = case goalStatus g of
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Proved _ -> True
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder-- Converts a proof-tree into a goal.
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederparseTimeLimit :: ProofStatus proof_tree -> Int
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederparseTimeLimit pt =
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder if null lns then 20 else read $ drop (length tlStr) $ last lns
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder TacticScript scrpt = tacticScript pt
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian Maeder lns = filter (isPrefixOf tlStr) $ splitOn '\n' scrpt
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian Maeder tlStr = "Time limit: "
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian MaederaddCommandHistoryToState :: IORef IntState
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> ProofState -- current proofstate
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang -> Maybe (G_prover, AnyComorphism) -- possible used translation
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang -> [ProofStatus proof_tree] -- goals included in prove
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaederaddCommandHistoryToState intSt st pcm pt str =
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder unless (not $ any wasProved pt) $ do
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ost <- readIORef intSt
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder fn <- tryRemoveAbsolutePathComponent $ filename ost
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder writeIORef intSt $ add2history
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder (IC.GroupCmd $ proofTreeToProve (rmSuffix fn) st pcm pt str)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ost [ IStateChange $ i_state ost ]
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian MaederconservativityRule :: DGRule
50ed946595d60c06f773e73bb22b21f5cf1199caChristian MaederconservativityRule = DGRule "ConservativityCheck"
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederconservativityChoser :: Bool -> [ConservativityChecker sign sentence morphism]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> IO (Result (ConservativityChecker sign sentence morphism))
50ed946595d60c06f773e73bb22b21f5cf1199caChristian Maeder#ifdef UNI_PACKAGE
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederconservativityChoser useGUI checkers = case checkers of
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder [] -> return $ fail "No conservativity checker available"
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder if useGUI && not (null tl) then do
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder chosenOne <- listBox "Pick a conservativity checker"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder $ map checkerId checkers
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder case chosenOne of
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder Nothing -> return $ fail "No conservativity checker chosen"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Just i -> return $ return $ checkers !! i
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaederconservativityChoser _ checkers = case checkers of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [] -> return $ fail "No conservativity checker available"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return $ return hd
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedercheckConservativityNode :: Bool -> LNode DGNodeLab -> LibEnv -> LibName
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder -> IO (String, LibEnv, ProofHistory)
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian MaedercheckConservativityNode useGUI (nodeId, nodeLab) libEnv ln = do
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let dg = lookupDGraph ln libEnv
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder emptyTh = case dgn_sign nodeLab of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder G_sign lid _ _ ->
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder noSensGTheory lid (mkExtSign $ empty_signature lid) startSigId
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder newN = getNewNodeDG dg
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder newL = (newNodeLab emptyNodeName DGProof emptyTh)
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder { globalTheory = Just emptyTh }
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder morphism = propagateErrors "Utils.checkConservativityNode"
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder $ ginclusion logicGraph (dgn_sign newL) $
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang dgn_sign nodeLab
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang lnk = (newN, nodeId, defDGLink
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang morphism (ScopedLink Global DefLink $ getNodeConsStatus nodeLab)
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder (tmpDG, _) = updateDGOnly dg $ InsertNode (newN, newL)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (tempDG, InsertEdge lnk') = updateDGOnly tmpDG $ InsertEdge lnk
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang tempLibEnv = Map.insert ln tempDG libEnv
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (str, _, (_, _, lnkLab), _) <-
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang checkConservativityEdge useGUI lnk' tempLibEnv ln
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang if isPrefixOf "No conservativity" str
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang then return (str, libEnv, SizedList.empty)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let nInfo = nodeInfo nodeLab
224e5f347275f5e9ada6cd976f195de2e77e41cbChristian Maeder nodeLab' = nodeLab { nodeInfo = nInfo { node_cons_status =
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang getEdgeConsStatus lnkLab } }
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang changes = [ SetNodeLab nodeLab (nodeId, nodeLab') ]
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang dg' = changesDGH dg changes
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang history = snd $ splitHistory dg dg'
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang libEnv' = Map.insert ln (groupHistory dg conservativityRule dg')
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return (str, libEnv', history)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangcheckConservativityEdge :: Bool -> LEdge DGLinkLab -> LibEnv -> LibName
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangcheckConservativityEdge useGUI link@(source, target, linklab) libEnv ln
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder Just (G_theory lidT _ sigT _ sensT _) <-
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return $ computeTheory libEnv ln target
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang GMorphism cid _ _ morphism _ <- return $ dgl_morphism linklab
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang morphism' <- coerceMorphism (targetLogic cid) lidT
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang "checkconservativityOfEdge" morphism
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let compMor = case dgn_sigma $ labDG (lookupDGraph ln libEnv) target of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Nothing -> morphism'
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Just (GMorphism cid' _ _ morphism2 _) -> case
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang coerceMorphism (targetLogic cid') lidT
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang "checkconservativityOfEdge" morphism2
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang >>= comp morphism' of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Result _ (Just phi) -> phi
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang _ -> error "checkconservativityOfEdge: comp"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Just (G_theory lidS _ signS _ sensS _) <-
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return $ computeTheory libEnv ln source
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder case coerceSign lidS lidT "checkconservativityOfEdge.coerceSign" signS of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Nothing -> return ( "no implementation for heterogeneous links"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , libEnv, link, SizedList.empty)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Just signS' -> do
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang sensS' <- coerceThSens lidS lidT "checkconservativityOfEdge1" sensS
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang let transSensSrc = propagateErrors "checkConservativityEdge2"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $ mapThSensValueM (map_sen lidT compMor) sensS'
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang checkerR <- conservativityChoser useGUI $ conservativityCheck lidT
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang case maybeResult checkerR of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Nothing -> return (concatMap diagString $ diags checkerR,
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Just theChecker -> do
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder let inputThSens1 = filter isAxiom $ toNamedList sensT
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $ map sentence $ toNamedList transSensSrc
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder inputThSens = filter
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ((`Set.notMember` transSrcSens) . sentence)
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder showObls = show . Pretty.vsep
84855a862ab77950c0c5059b1bba98cce0fb8ac3Christian Maeder . map (\ o -> print_named lidT .
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder mapNamed (simplify_sen lidT
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder $ plainSign sigT)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder $ (makeNamed "" o) {isAxiom = False})
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder Result ds res <-
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder checkConservativity theChecker
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder (plainSign signS', toNamedList sensS')
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder compMor inputThSens
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let (cs', showRes) = case res of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Just (cst, obs) ->
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let (exSens, resObls) = partition
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder (`Set.member` transSrcSens) obs
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder in (if null resObls then cst
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder else Unknown "unchecked obligations"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , "The link is " ++ showConsistencyStatus cst
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ++ case resObls of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [] -> case exSens of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder _ -> " because of the following axioms:\n"
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder ++ showObls exSens
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder _ -> " provided that the following obligations\n"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ++ "hold in an imported theory:\n"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ++ showObls resObls)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Nothing -> (Unknown "Unknown"
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , "Could not determine whether link is conservative")
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder consNew csv = if cs' >= csv
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder then Proven conservativityRule emptyProofBasis
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder else LeftOpen
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder (newDglType, edgeChange) = case dgl_type linklab of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ScopedLink sc dl (ConsStatus consv cs op) ->
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let np = consNew consv in
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder (ScopedLink sc dl $
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder ConsStatus consv (max cs $ max consv cs') np, np /= op)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder t -> (t, False)
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder provenEdge = ( source
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , linklab { dgl_type = newDglType }
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder dg = lookupDGraph ln libEnv
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder let edgeChanges = if edgeChange then
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder [ DeleteEdge (source, target, linklab)
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder , InsertEdge provenEdge ] else []
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder nextGr = changesDGH dg edgeChanges
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder newLibEnv = if edgeChange then Map.insert ln
b68f7c26243f3f99df2ddf8de966c73ad78a3741Christian Maeder (groupHistory dg conservativityRule nextGr) libEnv
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder history = snd $ splitHistory dg nextGr
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder myDiags = showRelDiags 4 ds
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder return ( showRes ++ "\n" ++ myDiags
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder , newLibEnv, provenEdge, history)
abcb1baa565c878598d732d0aa7724f474c9265cChristian MaederupdateNodeProof :: LibName -> IntState -> LNode DGNodeLab
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder -> G_theory -> (IntState, [DGChange])
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederupdateNodeProof ln ost (k, dgnode) thry =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder case i_state ost of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Nothing -> (ost, [])
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder let le = i_libEnv iist
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder dg = lookupDGraph ln le
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder nn = getDGNodeName dgnode
ce944c156ca6b4a56e81e232d7a22e582fbdcf33Christian Maeder newDg = computeDGraphTheories le $ changeDGH dg
ce944c156ca6b4a56e81e232d7a22e582fbdcf33Christian Maeder $ SetNodeLab dgnode (k, dgnode { dgn_theory = thry })
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder history = reverse $ flatHistory $ snd $ splitHistory dg newDg
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder nst = add2history
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder (CommentCmd $ "basic inference done on " ++ nn ++ "\n")
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder ost [DgCommandChange ln]
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder nwst = nst { i_state =
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder Just iist { i_libEnv = Map.insert ln newDg le } }
3ab1e7a18f3fc3eb004464bc54b7df4483f1f060Christian Maeder in (nwst, history)