GraphLogic.hs revision ba7903578ca168160ed411ef534fa95c5cddf8f0
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Logic for manipulating the graph in the Central GUI
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : till@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : non-portable (imports Logic)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederThis module provides functions for all the menus in the Hets GUI.
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThese are then assembled to the GUI in "GUI.GraphMenu".
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , updateGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , openProofStatus
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , saveProofStatus
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showReferencedLibrary
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , getTheoryOfNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , translateTheoryOfNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , displaySubsortGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , displayConceptGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showProofStatusOfNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , proveAtNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showNodeInfo
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showDiagMess
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showEdgeInfo
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , checkconservativityOfNode
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , checkconservativityOfEdge
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , toggleHideNames
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , toggleHideNodes
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , toggleHideEdges
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , translateGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , showLibGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , saveUDGraph
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Logic.Coerce (coerceSign)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Logic.Prover hiding (openProofStatus)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Comorphisms.LogicGraph (logicGraph)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Static.DGTranslation (libEnv_translation, getDGLogic)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Proofs.InferBasic (basicInferenceNode)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified GUI.GraphAbstraction as GA
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Reactor.InfoBus (encapsulateWaitTermAct)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.OrderedMap as OMap
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Common.Lib.SizedList as SizedList
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Driver.Options ( HetcatsOpts, putIfVerbose, outtypes, doDump, verbose
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport Driver.WriteLibDefn (writeShATermFile)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maederimport Driver.ReadFn (libNameToFile, readVerbose)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Data.Char (toLower)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Data.List (partition, delete, isPrefixOf)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport qualified Data.Map as Map
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | Locks the global lock and runs function
c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescurunAndLock :: GInfo -> IO () -> IO ()
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederrunAndLock (GInfo { functionLock = lock
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder , graphInfo = gi
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder }) function = do
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder locked <- tryPutMVar lock ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if locked then do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder takeMVar lock
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "an other function is still working ... please wait ..."
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder-- | Undo one step of the History
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederundo :: GInfo -> Bool -> IO ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederundo gInfo isUndo = do
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder intSt <- readIORef $ intState gInfo
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder else redoOneStepWithUpdate intSt $ updateGraphAux gInfo
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder writeIORef (intState gInfo) nwSt
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederupdateGraph :: GInfo -> [DGChange] -> IO ()
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederupdateGraph gInfo@(GInfo { libName = ln }) changes = do
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder ost <- readIORef $ intState gInfo
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder case i_state ost of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Nothing -> return ()
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederupdateGraphAux gInfo' ln changes dg = do
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder og <- readIORef $ openGraphs gInfo'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Nothing -> return ()
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder Just gInfo@(GInfo { graphInfo = gi
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , options = opts }) -> do
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder flags <- readIORef opts
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder let edges = if flagHideEdges flags then hideEdgesAux dg else []
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder "Applying development graph calculus proof rule..."
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder GA.applyChanges gi (removeContraryChanges changes) nodes edges comp
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder "Updating graph..."
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder hideNames gInfo
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder "Development graph calculus proof rule finished."
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-- | Toggles to display internal node names
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederhideNames :: GInfo -> IO ()
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederhideNames (GInfo { options = opts
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , internalNames = updaterIORef }) = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder flags <- readIORef opts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder updater <- readIORef updaterIORef
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mapM_ (\(s,upd) -> upd (\_ -> if flagHideNames flags then "" else s)) updater
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | Toggles to display internal node names
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedertoggleHideNames :: GInfo -> IO ()
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoggleHideNames gInfo@(GInfo { graphInfo = gi
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , options = opts }) = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder flags <- readIORef opts
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let hide = not $ flagHideNames flags
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder writeIORef opts $ flags { flagHideNames = hide }
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else "Revealing internal names..."
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder updateGraph gInfo []
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | hides all unnamed internal nodes that are proven
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaederhideNodesAux :: DGraph -> [EdgeId]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederhideNodesAux dg ignoreEdges =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let nodes = selectNodesByType dg
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski edges = getCompressedEdges dg nodes ignoreEdges
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in (nodes, edges)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertoggleHideNodes :: GInfo -> IO ()
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedertoggleHideNodes gInfo@(GInfo { graphInfo = gi
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , options = opts }) = do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder flags <- readIORef opts
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let hide = not $ flagHideNodes flags
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder writeIORef opts $ flags { flagHideNodes = hide }
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder else "Revealing hidden nodes..."
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder updateGraph gInfo []
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederhideEdgesAux :: DGraph -> [EdgeId]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederhideEdgesAux dg = map dgl_id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ filter (\ (DGLink { dgl_type = linktype }) ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder case linktype of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ScopedLink _ (ThmLink s) c ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder isProvenThmLinkStatus s && isProvenConsStatusLink c
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder HidingFreeOrCofreeThm _ _ s -> isProvenThmLinkStatus s
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ foldl (\ e c -> case c of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder InsertEdge (_, _, lbl) -> lbl:e
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder DeleteEdge (_, _, lbl) -> delete lbl e
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoggleHideEdges :: GInfo -> IO ()
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedertoggleHideEdges gInfo@(GInfo { graphInfo = gi
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , options = opts }) = do
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder flags <- readIORef opts
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder let hide = not $ flagHideEdges flags
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder writeIORef opts $ flags { flagHideEdges = hide }
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder else "Revealing hidden proven edges..."
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder updateGraph gInfo []
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- | generates from list of HistElem one list of DGChanges
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederflattenHistory [] cs = cs
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederflattenHistory ((HistElem c):r) cs = flattenHistory r $ c:cs
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzflattenHistory ((HistGroup _ ph):r) cs =
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder flattenHistory r $ flattenHistory (SizedList.toList ph) cs
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- | selects all nodes of a type with outgoing edges
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederselectNodesByType dg types =
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederhasUnprovenEdges :: DGraph -> Node -> Bool
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederhasUnprovenEdges dg =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz foldl (\ b (_,_,l) -> case edgeTypeModInc $ getRealDGLinkType l of
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz ThmType { isProvenEdge = False } -> False
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- | compresses a list of types to the highest one
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercompressTypes _ [] = error "compressTypes: wrong usage"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercompressTypes b (t:[]) = (t,b)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercompressTypes b (t1:t2:r)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | t1 == t2 = compressTypes b (t1:r)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | t1 > t2 = compressTypes False (t1:r)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | otherwise = compressTypes False (t2:r)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- | innDG with filter of not shown edges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfInnDG ignore dg = filter (\ (_,_,l) -> notElem (dgl_id l) ignore) . innDG dg
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- | outDG with filter of not shown edges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaederfOutDG ignore dg = filter (\ (_,_,l) -> notElem (dgl_id l) ignore) . outDG dg
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- | returns a list of compressed edges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaedergetCompressedEdges :: DGraph -> [Node] -> [EdgeId]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> [(Node,Node,DGEdgeType, Bool)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaedergetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder $ concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [] ign) inEdges
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder inEdges = filter (\ (_,t,_) -> elem t hidden)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder $ concatMap (fOutDG ign dg)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder $ foldr (\ n i -> if elem n hidden
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder || elem n i then i else n:i) []
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder $ map (\ (s,_,_) -> s) $ concatMap (fInnDG ign dg) hidden
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder-- | filter duplicate paths
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederfilterDuplicates :: [(Node,Node,DGEdgeType, Bool)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder -> [(Node,Node,DGEdgeType, Bool)]
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederfilterDuplicates [] = []
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder (same,others) = partition (\ (s',t', _, _) -> s == s' && t == t') r
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder (mtypes,stypes) = partition (\ (_,_,_,b) -> not b) same
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder stypes' = foldr (\e es -> if elem e es then es else e:es) [] stypes
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (et',_) = compressTypes False $ map (\ (_,_,et,_) -> et) mtypes
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder edges = if null mtypes then stypes' else (s,t,et',False):stypes'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | returns the pahts of a given node through hidden nodes
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> [[LEdge DGLinkLab]]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaedergetPaths dg node hidden seen' ign = if elem node hidden then
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if null edges then []
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder else concatMap (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen ign)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder seen = node:seen'
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder edges = filter (\ (_,t,_) -> notElem t seen) $ fOutDG ign dg node
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- | returns source and target node of a path with the compressed type
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaedergetShortPaths :: [[LEdge DGLinkLab]]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> [(Node,Node,DGEdgeType,Bool)]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaedergetShortPaths [] = []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetShortPaths (p : r) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (s, t, et, b)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder : getShortPaths r
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (s,_,_) = head p
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (_,t,_) = last p
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (et, b) = compressTypes True $ map (\ (_,_,e) -> getRealDGLinkType e) p
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- | Let the user select a Node to focus
99476ac2689c74251219db4782e57fe713a24a52Christian MaederfocusNode :: GInfo -> IO ()
99476ac2689c74251219db4782e57fe713a24a52Christian MaederfocusNode gInfo@(GInfo { graphInfo = gi
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder , libName = ln }) = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ost <- readIORef $ intState gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder case i_state ost of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> return ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ist -> do
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder let le = i_libEnv ist
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder $ labNodesDG $ lookupDGraph ln le
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder selection <- listBox "Select a node to focus"
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder case selection of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> return ()
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedershowLibGraph :: GInfo -> LibFunc -> IO ()
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedershowLibGraph gInfo showLib = do
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder showLib gInfo
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaedersaveProofStatus :: GInfo -> FilePath -> IO ()
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaedersaveProofStatus gInfo@(GInfo { hetcatsOpts = opts
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder , libName = ln
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder }) file = encapsulateWaitTermAct $ do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ost <- readIORef $ intState gInfo
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder case i_state ost of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> return ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ist -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let proofStatus = i_libEnv ist
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder writeShATermFile file (ln, lookupHistory ln proofStatus)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder putIfVerbose opts 2 $ "Wrote " ++ file
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder-- | implementation of open menu, read in a proof status
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederopenProofStatus gInfo@(GInfo { hetcatsOpts = opts
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , libName = ln }) file convGraph showLib = do
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder ost <- readIORef $ intState gInfo
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder case i_state ost of
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Nothing -> return ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ist -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mh <- readVerbose logicGraph opts ln file
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> errorDialog "Error" $
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder "Could not read proof status from file '" ++ file ++ "'"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let libfile = libNameToFile ln
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder m <- anaLib opts { outtypes = [] } libfile
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> errorDialog "Error"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ "Could not read original development graph from '"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ++ libfile ++ "'"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just (_, libEnv) -> case Map.lookup ln libEnv of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Nothing -> errorDialog "Error" $ "Could not get original"
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder ++ "development graph for '" ++ showDoc ln "'"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Just dg -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder lockGlobal gInfo
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let oldEnv = i_libEnv ist
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder writeIORef (intState gInfo) nwst
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder unlockGlobal gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder gInfo' <- copyGInfo gInfo ln
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder convGraph gInfo' "Proof Status " showLib
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let gi = graphInfo gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | apply a rule of the development graph calculus
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederproofMenu :: GInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> (LibEnv -> IO (Result LibEnv))
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederproofMenu gInfo@(GInfo { hetcatsOpts = hOpts
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , libName = ln
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder }) cmd proofFun = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ost <- readIORef $ intState gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder case i_state ost of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> return ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just ist -> do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder lockGlobal gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let proofStatus = i_libEnv ist
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder putIfVerbose hOpts 4 "Proof started via menu"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Result ds res <- proofFun proofStatus
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder putIfVerbose hOpts 4 "Analyzing result of proof"
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Nothing -> do
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder unlockGlobal gInfo
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder printDiags 2 ds
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Just newProofStatus -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let newGr = lookupDGraph ln newProofStatus
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder lln = map DgCommandChange $ calcGlobalHistory
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder proofStatus newProofStatus
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder nst = add2history cmd ost lln
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder nwst = nst { i_state = Just ist { i_libEnv=newProofStatus}}
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder doDump hOpts "PrintHistory" $ do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder putStrLn "History"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder print $ prettyHistory history
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder writeIORef (intState gInfo) nwst
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder updateGraph gInfo (reverse $ flatHistory history)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder unlockGlobal gInfo
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedercalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedercalcGlobalHistory old new = let
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder length' ln = SizedList.size . proofHistory . lookupDGraph ln
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedershowNodeInfo :: Int -> DGraph -> IO ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedershowNodeInfo descr dgraph = do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let dgnode = labDG dgraph descr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder title = (if isDGRef dgnode then ("reference " ++) else
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if isInternalNode dgnode then ("internal " ++) else id)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder "node " ++ getDGNodeName dgnode ++ " " ++ show descr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedershowDiagMessAux :: Int -> [Diagnosis] -> IO ()
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedershowDiagMessAux v ds = let es = filterDiags v ds in
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder unless (null es) $ (if hasErrors es then errorDialog "Error"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else infoDialog "Info") $ unlines $ map show es
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedershowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedershowDiagMess = showDiagMessAux . verbose
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder{- | outputs the theory of a node in a window;
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder used by the node menu -}
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedergetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetTheoryOfNode gInfo descr dgraph = do
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ost <- readIORef $ intState gInfo
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder case i_state ost of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Nothing -> return ()
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Just ist -> do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder showDiagMess (hetcatsOpts gInfo) ds
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder maybe (return ())
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder $ addHasInHidingWarning dgraph descr) res
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder{- | translate the theory of a node in a window;
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder used by the node menu -}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedertranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedertranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , libName = ln }) node dgraph = do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ost <- readIORef $ intState gInfo
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder case i_state ost of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> return ()
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just ist -> do
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder let libEnv = i_libEnv ist
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Result ds moTh = computeTheory libEnv ln node
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Just th@(G_theory lid sign _ sens _) -> do
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -- find all comorphism paths starting from lid
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let paths = findComorphismPaths logicGraph (sublogicOfTh th)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -- let the user choose one
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder sel <- listBox "Choose a node logic translation" $ map show paths
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> errorDialog "Error" "no node logic translation chosen"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Comorphism cid <- return (paths!!i)
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -- adjust lid's
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let lidS = sourceLogic cid
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder lidT = targetLogic cid
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder sign' <- coerceSign lid lidS "" sign
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder sens' <- coerceThSens lid lidS "" sens
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- translate theory along chosen comorphism
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let Result es mTh = wrapMapTheory cid
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (plainSign sign', toNamedList sens')
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Nothing -> showDiagMess opts es
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Just (sign'', sens1) -> displayTheoryWithWarning
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder "Translated Theory" (getNameOfNode node dgraph)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (addHasInHidingWarning dgraph node)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Nothing -> showDiagMess opts ds
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder-- | Show proof status of a node
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaedershowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaedershowProofStatusOfNode _ descr dgraph =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let dgnode = labDG dgraph descr
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder stat = showStatusAux dgnode
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder title = "Proof status of node "++showName (dgn_name dgnode)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in createTextDisplay title stat
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaedershowStatusAux :: DGNodeLab -> String
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedershowStatusAux dgnode = case dgn_theory dgnode of
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder G_theory _ _ _ sens _ ->
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder let goals = OMap.filter (not . isAxiom) sens
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (proven,open) = OMap.partition isProvenSenStatus goals
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder consGoal = "\nconservativity of this node"
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder in "Proven proof goals:\n"
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder ++ showDoc proven ""
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder ++ if not $ hasOpenNodeConsStatus True dgnode
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski then consGoal
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ++ "\nOpen proof goals:\n"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ++ showDoc open ""
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ++ if hasOpenNodeConsStatus False dgnode
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski then consGoal
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederhidingWarnDiag :: DGNodeLab -> IO Bool
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederhidingWarnDiag dgn = if labelHasHiding dgn then
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder else return True
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder-- | start local theorem proving or consistency checking at a node
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederproveAtNode :: GInfo -> Int -> DGraph -> IO ()
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederproveAtNode gInfo descr dgraph = do
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder let ln = libName gInfo
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder iSt = intState gInfo
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder ost <- readIORef iSt
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder case i_state ost of
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Nothing -> return ()
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Just ist -> do
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder let le = i_libEnv ist
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder dgn = labDG dgraph descr
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder lockGlobal gInfo
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let nwle = Map.insert ln dgraph' le
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder writeIORef iSt nwst
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder unlockGlobal gInfo
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder return (dgraph', dgn', nwle)
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder acquired <- tryLockLocal dgn'
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder if acquired then do
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder let action = do
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (descr, dgn') le' iSt
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder when (null d || diagString (head d) /= "Proofs.Proofs: selection")
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder $ runProveAtNode gInfo (descr, dgn') res
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder b <- hidingWarnDiag dgn'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder when b action
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder unlockLocal dgn'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder else errorDialog "Error" "Proofwindow already open"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrunProveAtNode :: GInfo -> LNode DGNodeLab
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder -> Result G_theory -> IO ()
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just newTh ->
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder let oldTh = dgn_theory dgnode
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder rTh = propagateProofs oldTh newTh in
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder unless (rTh == oldTh) $ do
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder showDiagMessAux 2 ds
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder lockGlobal gInfo
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder let ln = libName gInfo
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder iSt = intState gInfo
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ost <- readIORef iSt
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let (ost', mhist) = updateNodeProof ln ost (v, dgnode) $ Just rTh
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder case mhist of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just hist -> do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder writeIORef iSt ost'
2feea92963a4b1b7482a4b72ee85148d842d9ad6Christian Maeder runAndLock gInfo $ updateGraph gInfo hist
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder Nothing -> return ()
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder unlockGlobal gInfo
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder _ -> return ()
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercheckconservativityOfNode :: Int -> GInfo -> DGraph -> IO ()
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercheckconservativityOfNode descr gInfo dgraph = do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let iSt = intState gInfo
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ln = libName gInfo
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder nlbl = labDG dgraph descr
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder ost <- readIORef iSt
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder case i_state ost of
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder Nothing -> return ()
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Just iist -> do
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder b <- hidingWarnDiag nlbl
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lockGlobal gInfo
32562a567baac248a00782d2727716c13117dc4aChristian Maeder (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder (i_libEnv iist) ln
32562a567baac248a00782d2727716c13117dc4aChristian Maeder if isPrefixOf "No conservativity" str then
32562a567baac248a00782d2727716c13117dc4aChristian Maeder errorDialog "Result of conservativity check" str
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder createTextDisplay "Result of conservativity check" str
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder let nst = add2history (SelectCmd Node $ showDoc descr "")
fa373bc327620e08861294716b4454be8d25669fChristian Maeder ost [DgCommandChange ln]
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}
fa373bc327620e08861294716b4454be8d25669fChristian Maeder writeIORef iSt nwst
fa373bc327620e08861294716b4454be8d25669fChristian Maeder runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder unlockGlobal gInfo
fa373bc327620e08861294716b4454be8d25669fChristian MaederedgeErr :: Int -> IO ()
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ++ " not found in the development graph"
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- | print the id, origin, type, proof-status and morphism of the edge
32562a567baac248a00782d2727716c13117dc4aChristian MaedershowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
fa373bc327620e08861294716b4454be8d25669fChristian MaedershowEdgeInfo descr me = case me of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Just e@(_, _, l) -> let estr = showLEdge e in
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder createTextDisplay ("Info of " ++ estr)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (estr ++ "\n" ++ showDoc l "")
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> edgeErr descr
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | check conservativity of the edge
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedercheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedercheckconservativityOfEdge descr gInfo me = case me of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> edgeErr descr
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder Just lnk@(_, _, lbl) -> do
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder let iSt = intState gInfo
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ln = libName gInfo
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ost <- readIORef iSt
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case i_state ost of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> return ()
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Just iist -> do
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder lockGlobal gInfo
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (str, nwle, _, ph) <- checkConservativityEdge True lnk
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (i_libEnv iist) ln
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder if isPrefixOf "No conservativity" str
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder errorDialog "Result of conservativity check" str
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder createTextDisplay "Result of conservativity check" str
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ost [DgCommandChange ln]
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder writeIORef iSt nwst
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder unlockGlobal gInfo
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | show library referened by a DGRef node (=node drawn as a box)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedershowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedershowReferencedLibrary descr gInfo@(GInfo{ libName = ln })
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder convGraph showLib = do
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ost <- readIORef $ intState gInfo
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case i_state ost of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> return ()
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Just ist -> do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder let le = i_libEnv ist
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder refNode = labDG (lookupDGraph ln le) descr
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder refLibname = if isDGRef refNode then dgn_libname refNode
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder else error "showReferencedLibrary"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder case Map.lookup refLibname le of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder gInfo' <- copyGInfo gInfo refLibname
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder convGraph gInfo' "development graph" showLib
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let gi = graphInfo gInfo'
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder GA.showTemporaryMessage gi "Development Graph initialized."
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> error $ "The referenced library (" ++ show refLibname
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ++ ") is unknown"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | display a window of translated graph with maximal sublogic.
32562a567baac248a00782d2727716c13117dc4aChristian MaedertranslateGraph :: GInfo -> IO (Maybe LibEnv)
32562a567baac248a00782d2727716c13117dc4aChristian MaedertranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do
32562a567baac248a00782d2727716c13117dc4aChristian Maeder ost <- readIORef $ intState gInfo
fa373bc327620e08861294716b4454be8d25669fChristian Maeder case i_state ost of
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder Nothing -> return Nothing
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Just ist -> do
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder le = i_libEnv ist
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder Result diagsSl mSublogic = getDGLogic le
32562a567baac248a00782d2727716c13117dc4aChristian Maeder myErrMess = showDiagMess opts
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski error' = errorDialog "Error"
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder if hasErrors diagsSl then do
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder myErrMess diagsSl
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder return Nothing
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder else case mSublogic of
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder Nothing -> do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder error' "No maximal sublogic found."
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder return Nothing
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder Just sublogic -> do
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski let paths = findComorphismPaths logicGraph sublogic
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if null paths then do
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder error' "This graph has no comorphism to translation."
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder return Nothing
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder sel <- listBox "Choose a logic translation" $ map show paths
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Nothing -> do
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder error' "no logic translation chosen"
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski return Nothing
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder let Result diag mle = libEnv_translation le $ paths !! j
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Just newLibEnv -> do
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder showDiagMess opts $ diagsSl ++ diag
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder return $ Just newLibEnv
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Nothing -> do
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski myErrMess $ diagsSl ++ diag
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return Nothing
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- DaVinciGraph to String
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- Functions to convert a DaVinciGraph to a String to store as a .udg file
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder-- | saves the uDrawGraph graph to a file
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaedersaveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaedersaveUDGraph gInfo@(GInfo { graphInfo = gi
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder , libName = ln }) nodemap linkmap = do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ost <- readIORef $ intState gInfo
5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder case i_state ost of
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder Nothing -> return ()
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder maybeFilePath <- fileSaveDialog (rmSuffix (libNameToFile ln) ++ ".udg")
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder [ ("uDrawGraph",["*.udg"])
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder , ("All Files", ["*"])] Nothing
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder case maybeFilePath of
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder Just filepath -> do
fc033b8680245bf692c9c09723fd3046ff38971eChristian Maeder GA.showTemporaryMessage gi "Converting graph..."
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder nstring <- nodes2String gInfo nodemap linkmap
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder writeFile filepath nstring
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Nothing -> GA.showTemporaryMessage gi "Aborted!"
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder-- | Converts the nodes of the graph to String representation
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangnodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maedernodes2String gInfo@(GInfo { graphInfo = gi
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder , libName = ln }) nodemap linkmap = do
nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode gi n
node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
(shape, color) <- case Map.lookup ntype nodemap of
b <- GA.isHiddenEdge gi eid
(line, color) <- case Map.lookup ltype linkmap of