da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem{- |

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemModule : $Header$

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemDescription : Logic for manipulating the graph in the Central GUI

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemLicense : GPLv2 or higher, see LICENSE.txt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemMaintainer : till@informatik.uni-bremen.de

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemStability : provisional

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemPortability : non-portable (imports Logic)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemThis module provides functions for all the menus in the Hets GUI.

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemThese are then assembled to the GUI in "GUI.GraphMenu".

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemmodule GUI.GraphLogic

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ( undo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , updateGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , openProofStatus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , saveProofStatus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , proofMenu

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showDGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showReferencedLibrary

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , getTheoryOfNode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , translateTheoryOfNode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , displaySubsortGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , displayConceptGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showProofStatusOfNode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , proveAtNode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showNodeInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showDiagMess

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showDiagMessAux

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showEdgeInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , checkconservativityOfNode

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe , checkconservativityOfEdge

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , toggleHideNames

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe , toggleHideNodes

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , toggleHideEdges

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe , translateGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , showLibGraph

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe , runAndLock

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , saveUDGraph

bf1b7f1e251c6f12ac13a46479942f42612def4eminfrin , focusNode

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe ) where

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awroweimport Logic.Coerce (coerceSign)

bf1b7f1e251c6f12ac13a46479942f42612def4eminfrinimport Logic.Grothendieck

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Logic.Comorphism

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Logic.Prover hiding (openProofStatus)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Comorphisms.LogicGraph (logicGraph)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Static.GTheory

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Static.DevGraph

bf1b7f1e251c6f12ac13a46479942f42612def4eminfrinimport Static.PrintDevGraph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Static.DGTranslation (libEnv_translation, getDGLogic)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Static.History

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Static.ComputeTheory

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Proofs.EdgeUtils

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Proofs.InferBasic (basicInferenceNode)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Proofs.StatusUtils (lookupHistory, removeContraryChanges)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport GUI.Taxonomy (displayConceptGraph, displaySubsortGraph)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport GUI.GraphTypes

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport qualified GUI.GraphAbstraction as GA

e4437c7dec2bf46171f15ab5ac4aa17e8c8a0fe8trawickimport GUI.Utils

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Graphs.GraphConfigure

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Reactor.InfoBus (encapsulateWaitTermAct)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Common.DocUtils (showDoc)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Common.AS_Annotation (isAxiom)

e4437c7dec2bf46171f15ab5ac4aa17e8c8a0fe8trawickimport Common.ExtSign

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Common.LibName

e4437c7dec2bf46171f15ab5ac4aa17e8c8a0fe8trawickimport Common.Result

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport qualified Common.OrderedMap as OMap

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport qualified Common.Lib.SizedList as SizedList

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Driver.Options ( HetcatsOpts, putIfVerbose, outtypes, doDump, verbose

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , rmSuffix)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Driver.WriteLibDefn (writeShATermFile)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Driver.ReadFn (libNameToFile, readVerbose)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Driver.AnaLib (anaLib)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Data.IORef

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Data.Char (toLower)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Data.List (partition, delete, isPrefixOf)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Data.Graph.Inductive.Graph (Node, LEdge, LNode)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport qualified Data.Map as Map

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Control.Monad

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinimport Control.Concurrent.MVar

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Interfaces.Command

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Interfaces.History

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Interfaces.DataTypes

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemimport Interfaces.Utils

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | Locks the global lock and runs function

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemrunAndLock :: GInfo -> IO () -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemrunAndLock (GInfo { functionLock = lock

8c92aeeb75b1b393f61a3e01c495484737a0ff8cminfrin , graphInfo = gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem }) function = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem locked <- tryPutMVar lock ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if locked then do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem function

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem takeMVar lock

185aa71728867671e105178b4c66fbc22b65ae26sf else GA.showTemporaryMessage gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem "an other function is still working ... please wait ..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | Undo one step of the History

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemundo :: GInfo -> Bool -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemundo gInfo isUndo = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem intSt <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwSt <- if isUndo then undoOneStepWithUpdate intSt $ updateGraphAux gInfo

185aa71728867671e105178b4c66fbc22b65ae26sf else redoOneStepWithUpdate intSt $ updateGraphAux gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef (intState gInfo) nwSt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemupdateGraph :: GInfo -> [DGChange] -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemupdateGraph gInfo@(GInfo { libName = ln }) changes = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

185aa71728867671e105178b4c66fbc22b65ae26sf case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> updateGraphAux gInfo ln changes $ lookupDGraph ln $ i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemupdateGraphAux :: GInfo -> LibName -> [DGChange] -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemupdateGraphAux gInfo' ln changes dg = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem og <- readIORef $ openGraphs gInfo'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case Map.lookup ln og of

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin Nothing -> return ()

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin Just gInfo@(GInfo { graphInfo = gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin , options = opts }) -> do

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin flags <- readIORef opts

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin let edges = if flagHideEdges flags then hideEdgesAux dg else []

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin (nodes, comp) = if flagHideNodes flags then hideNodesAux dg edges

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin else ([], [])

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.showTemporaryMessage gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin "Applying development graph calculus proof rule..."

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.deactivateGraphWindow gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.applyChanges gi (removeContraryChanges changes) nodes edges comp

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.showTemporaryMessage gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin "Updating graph..."

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.redisplay gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin hideNames gInfo

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.layoutImproveAll gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.activateGraphWindow gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin GA.showTemporaryMessage gi

a77e5e9b423083b5436bbfd84e8b57329b738febminfrin "Development graph calculus proof rule finished."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | Toggles to display internal node names

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideNames :: GInfo -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideNames (GInfo { options = opts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , internalNames = updaterIORef }) = do

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin flags <- readIORef opts

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin updater <- readIORef updaterIORef

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin mapM_ (\ (s, upd) -> upd (const $ if flagHideNames flags then "" else s))

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin updater

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | Toggles to display internal node names

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtoggleHideNames :: GInfo -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtoggleHideNames gInfo@(GInfo { graphInfo = gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , options = opts }) = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem flags <- readIORef opts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let hide = not $ flagHideNames flags

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef opts $ flags { flagHideNames = hide }

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.showTemporaryMessage gi $ if hide then "Hiding internal names..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else "Revealing internal names..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem updateGraph gInfo []

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | hides all unnamed internal nodes that are proven

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideNodesAux :: DGraph -> [EdgeId]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)])

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideNodesAux dg ignoreEdges =

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let nodes = selectNodesByType dg

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem edges = getCompressedEdges dg nodes ignoreEdges

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin in (nodes, edges)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtoggleHideNodes :: GInfo -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtoggleHideNodes gInfo@(GInfo { graphInfo = gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , options = opts }) = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem flags <- readIORef opts

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin let hide = not $ flagHideNodes flags

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin writeIORef opts $ flags { flagHideNodes = hide }

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin GA.showTemporaryMessage gi $ if hide then "Hiding unnamed nodes..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else "Revealing hidden nodes..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem updateGraph gInfo []

185aa71728867671e105178b4c66fbc22b65ae26sf

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideEdgesAux :: DGraph -> [EdgeId]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhideEdgesAux dg = map dgl_id

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ filter (\ (DGLink { dgl_type = linktype }) ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case linktype of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ScopedLink _ (ThmLink s) c ->

185aa71728867671e105178b4c66fbc22b65ae26sf isProvenThmLinkStatus s && isProvenConsStatusLink c

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem HidingFreeOrCofreeThm _ _ s -> isProvenThmLinkStatus s

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem _ -> False

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem )

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ foldl (\ e c -> case c of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem InsertEdge (_, _, lbl) -> lbl : e

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin DeleteEdge (_, _, lbl) -> delete lbl e

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin _ -> e

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin ) [] $ flattenHistory (SizedList.toList $ proofHistory dg) []

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrin

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrintoggleHideEdges :: GInfo -> IO ()

5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrintoggleHideEdges gInfo@(GInfo { graphInfo = gi

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin , options = opts }) = do

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin flags <- readIORef opts

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin let hide = not $ flagHideEdges flags

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin writeIORef opts $ flags { flagHideEdges = hide }

9d766f93eefb9358f9a24bb99ff424ad399b9b39minfrin GA.showTemporaryMessage gi $ if hide then "Hiding new proven edges..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else "Revealing hidden proven edges..."

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem updateGraph gInfo []

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

185aa71728867671e105178b4c66fbc22b65ae26sf-- | generates from list of HistElem one list of DGChanges

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemflattenHistory :: [HistElem] -> [DGChange] -> [DGChange]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemflattenHistory [] cs = cs

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemflattenHistory (HistElem c : r) cs = flattenHistory r $ c : cs

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemflattenHistory (HistGroup _ ph : r) cs =

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem flattenHistory r $ flattenHistory (SizedList.toList ph) cs

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | selects all nodes of a type with outgoing edges

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemselectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node]

185aa71728867671e105178b4c66fbc22b65ae26sfselectNodesByType dg types =

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem filter (\ n -> not (null $ outDG dg n) && hasUnprovenEdges dg n) $ map fst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhasUnprovenEdges :: DGraph -> Node -> Bool

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhasUnprovenEdges dg =

185aa71728867671e105178b4c66fbc22b65ae26sf foldl (\ b (_, _, l) -> case edgeTypeModInc $ getRealDGLinkType l of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ThmType { isProvenEdge = False } -> False

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem _ -> b) True . (\ n -> innDG dg n ++ outDG dg n)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | compresses a list of types to the highest one

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcompressTypes :: Bool -> [DGEdgeType] -> (DGEdgeType, Bool)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcompressTypes _ [] = error "compressTypes: wrong usage"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcompressTypes b (t : []) = (t, b)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcompressTypes b (t1 : t2 : r)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem | t1 == t2 = compressTypes b (t1 : r)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem | t1 > t2 = compressTypes False (t1 : r)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem | otherwise = compressTypes False (t2 : r)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | innDG with filter of not shown edges

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefInnDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . innDG dg

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe-- | outDG with filter of not shown edges

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab]

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefOutDG ignore dg = filter (\ (_, _, l) -> notElem (dgl_id l) ignore) . outDG dg

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe-- | returns a list of compressed edges

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowegetCompressedEdges :: DGraph -> [Node] -> [EdgeId]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin -> [(Node, Node, DGEdgeType, Bool)]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfringetCompressedEdges dg hidden ign = filterDuplicates $ getShortPaths

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe $ concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden [] ign) inEdges

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe where

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin inEdges = filter (\ (_, t, _) -> elem t hidden)

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin $ concatMap (fOutDG ign dg)

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin $ foldr (\ (n, _, _) i -> if elem n hidden

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin || elem n i then i else n : i) []

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin $ concatMap (fInnDG ign dg) hidden

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe-- | filter duplicate paths

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefilterDuplicates :: [(Node, Node, DGEdgeType, Bool)]

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe -> [(Node, Node, DGEdgeType, Bool)]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinfilterDuplicates [] = []

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinfilterDuplicates r@((s, t, _, _) : _) = edges ++ filterDuplicates others

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe where

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (same, others) = partition (\ (s', t', _, _) -> s == s' && t == t') r

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (mtypes, stypes) = partition (\ (_, _, _, b) -> not b) same

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe stypes' = foldr (\ e es -> if elem e es then es else e : es) [] stypes

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (et', _) = compressTypes False $ map (\ (_, _, et, _) -> et) mtypes

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe edges = if null mtypes then stypes' else (s, t, et', False) : stypes'

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe-- | returns the pahts of a given node through hidden nodes

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowegetPaths :: DGraph -> Node -> [Node] -> [Node] -> [EdgeId]

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe -> [[LEdge DGLinkLab]]

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowegetPaths dg node hidden seen' ign = if elem node hidden then

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe if null edges then []

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe else concatMap (\ e@(_, t, _) -> map (e :) $ getPaths dg t hidden seen ign)

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe edges

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin else [[]]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin where

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe seen = node : seen'

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe edges = filter (\ (_, t, _) -> notElem t seen) $ fOutDG ign dg node

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin-- | returns source and target node of a path with the compressed type

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfringetShortPaths :: [[LEdge DGLinkLab]]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin -> [(Node, Node, DGEdgeType, Bool)]

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfringetShortPaths [] = []

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowegetShortPaths (p : r) =

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (s, t, et, b)

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe : getShortPaths r

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe where

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (s, _, _) = head p

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (_, t, _) = last p

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe (et, b) = compressTypes True $ map (\ (_, _, e) -> getRealDGLinkType e) p

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe-- | Let the user select a Node to focus

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowefocusNode :: GInfo -> IO ()

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinfocusNode gInfo@(GInfo { graphInfo = gi

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe , libName = ln }) = do

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let le = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem idsnodes <- filterM (fmap not . GA.isHiddenNode gi . fst)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ labNodesDG $ lookupDGraph ln le

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem selection <- listBox "Select a node to focus"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case selection of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just idx -> GA.focusNode gi $ fst $ idsnodes !! idx

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowLibGraph :: GInfo -> LibFunc -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowLibGraph gInfo showLib = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem showLib gInfo

563787eb542f06298242d9e681c18be6611a6214minfrin return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemsaveProofStatus :: GInfo -> FilePath -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemsaveProofStatus gInfo@(GInfo { hetcatsOpts = opts

563787eb542f06298242d9e681c18be6611a6214minfrin , libName = ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem }) file = encapsulateWaitTermAct $ do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let proofStatus = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeShATermFile file (ln, lookupHistory ln proofStatus)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem putIfVerbose opts 2 $ "Wrote " ++ file

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | implementation of open menu, read in a proof status

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemopenProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemopenProofStatus gInfo@(GInfo { hetcatsOpts = opts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , libName = ln }) file convGraph showLib = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem mh <- readVerbose logicGraph opts ln file

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case mh of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> errorDialog "Error" $

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem "Could not read proof status from file '" ++ file ++ "'"

e2de0e939faab767454a164c7d2e8ea710fd1a26sf Just h -> do

e2de0e939faab767454a164c7d2e8ea710fd1a26sf let libfile = libNameToFile ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem m <- anaLib opts { outtypes = [] } libfile

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case m of

8abb19ac6c29f60bb7df36f4303ce66a4ed6d783jailletc Nothing -> errorDialog "Error"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ "Could not read original development graph from '"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ libfile ++ "'"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just (_, libEnv) -> case Map.lookup ln libEnv of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> errorDialog "Error" $ "Could not get original"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ "development graph for '" ++ showDoc ln "'"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just dg -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let oldEnv = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem proofStatus = Map.insert ln (applyProofHistory h dg) oldEnv

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwst = ost { i_state = Just ist { i_libEnv = proofStatus } }

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef (intState gInfo) nwst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem gInfo' <- copyGInfo gInfo ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem convGraph gInfo' "Proof Status " showLib

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let gi = graphInfo gInfo'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.deactivateGraphWindow gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.redisplay gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.layoutImproveAll gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.activateGraphWindow gi

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | apply a rule of the development graph calculus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemproofMenu :: GInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> Command

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> (LibEnv -> IO (Result LibEnv))

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> IO ()

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinproofMenu gInfo@(GInfo { hetcatsOpts = hOpts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , libName = ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem }) cmd proofFun = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let proofStatus = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem putIfVerbose hOpts 4 "Proof started via menu"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Result ds res <- proofFun proofStatus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem putIfVerbose hOpts 4 "Analyzing result of proof"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case res of

fc251eb7714d158c2952bc2ddbbcfb9169098212sf Nothing -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem printDiags 2 ds

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just newProofStatus -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let newGr = lookupDGraph ln newProofStatus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lln = map DgCommandChange $ calcGlobalHistory

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem proofStatus newProofStatus

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nst = add2history cmd ost lln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwst = nst { i_state = Just ist { i_libEnv = newProofStatus}}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem doDump hOpts "PrintHistory" $ do

563787eb542f06298242d9e681c18be6611a6214minfrin putStrLn "History"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem print $ prettyHistory history

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef (intState gInfo) nwst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem updateGraph gInfo (reverse $ flatHistory history)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcalcGlobalHistory :: LibEnv -> LibEnv -> [LibName]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcalcGlobalHistory old new = let

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem length' ln = SizedList.size . proofHistory . lookupDGraph ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowNodeInfo :: Int -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowNodeInfo descr dgraph = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let dgnode = labDG dgraph descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem title = (if isDGRef dgnode then ("reference " ++) else

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if isInternalNode dgnode then ("internal " ++) else id)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem "node " ++ getDGNodeName dgnode ++ " " ++ show descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDiagMessAux :: Int -> [Diagnosis] -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDiagMessAux v ds = let es = filterDiags v ds in

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unless (null es) $ (if hasErrors es then errorDialog "Error"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else infoDialog "Info") $ unlines $ map show es

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDiagMess = showDiagMessAux . verbose

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

ba6d2154a44db73e1d94ef0b74ca0ce72d13aa04minfrin{- | outputs the theory of a node in a window;

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem used by the node menu -}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemgetTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemgetTheoryOfNode gInfo descr dgraph = do

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe ost <- readIORef $ intState gInfo

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> case computeTheory (i_libEnv ist) (libName gInfo) descr of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem errorDialog "Error" $ "no global theory for node " ++ show descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just th -> displayTheoryWithWarning "Theory" (getNameOfNode descr dgraph)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (addHasInHidingWarning dgraph descr) th

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem{- | translate the theory of a node in a window;

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem used by the node menu -}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtranslateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtranslateTheoryOfNode gInfo@(GInfo { hetcatsOpts = opts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem , libName = ln }) node dgraph = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin case i_state ost of

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let libEnv = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case computeTheory libEnv ln node of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just th@(G_theory lid sign _ sens _) -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -- find all comorphism paths starting from lid

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let paths = findComorphismPaths logicGraph (sublogicOfTh th)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -- let the user choose one

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem sel <- listBox "Choose a node logic translation" $ map show paths

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case sel of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> errorDialog "Error" "no node logic translation chosen"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just i -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Comorphism cid <- return (paths !! i)

5725c3eb0c6c572049ba61dedd92b4e5da078081minfrin -- adjust lid's

5725c3eb0c6c572049ba61dedd92b4e5da078081minfrin let lidS = sourceLogic cid

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lidT = targetLogic cid

2e1a0fb12bdf1c20064ffe900a8f44979ec946fcminfrin sign' <- coerceSign lid lidS "" sign

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe sens' <- coerceThSens lid lidS "" sens

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -- translate theory along chosen comorphism

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let Result es mTh = wrapMapTheory cid

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (plainSign sign', toNamedList sens')

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case mTh of

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin Nothing -> showDiagMess opts es

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin Just (sign'', sens1) -> displayTheoryWithWarning

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem "Translated Theory" (getNameOfNode node dgraph)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (addHasInHidingWarning dgraph node)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ G_theory lidT (mkExtSign sign'') startSigId (toThSens sens1)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem startThId

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem errorDialog "Error" $ "no global theory for node " ++ show node

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | Show proof status of a node

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowProofStatusOfNode _ descr dgraph =

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let dgnode = labDG dgraph descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem stat = showStatusAux dgnode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem title = "Proof status of node " ++ showName (dgn_name dgnode)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem in createTextDisplay title stat

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

b72b768176398d8cd00d61b289c8e0f8ce09469fwroweshowStatusAux :: DGNodeLab -> String

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowStatusAux dgnode = case dgn_theory dgnode of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem G_theory _ _ _ sens _ ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let goals = OMap.filter (not . isAxiom) sens

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (proven, open) = OMap.partition isProvenSenStatus goals

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem consGoal = "\nconservativity of this node"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem in "Proven proof goals:\n"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ showDoc proven ""

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ if not $ hasOpenNodeConsStatus True dgnode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem then consGoal

ba6d2154a44db73e1d94ef0b74ca0ce72d13aa04minfrin else ""

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ "\nOpen proof goals:\n"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ showDoc open ""

ba6d2154a44db73e1d94ef0b74ca0ce72d13aa04minfrin ++ if hasOpenNodeConsStatus False dgnode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem then consGoal

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else ""

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhidingWarnDiag :: DGNodeLab -> IO Bool

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemhidingWarnDiag dgn = if labelHasHiding dgn then

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem warningDialog "Warning" $ unwords $ hidingWarning ++ ["Try anyway?"]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else return True

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | start local theorem proving or consistency checking at a node

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinproveAtNode :: GInfo -> Int -> DGraph -> IO ()

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrinproveAtNode gInfo descr dgraph = do

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin let ln = libName gInfo

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin iSt = intState gInfo

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin ost <- readIORef iSt

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin case i_state ost of

867590a29c3d6c84a8e4eee3b65eb91a428089bfminfrin Nothing -> return ()

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let le = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem dgn = labDG dgraph descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (dgraph', dgn', le') <- if hasLock dgn then return (dgraph, dgn, le)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (dgraph', dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let nwle = Map.insert ln dgraph' le

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwst = ost { i_state = Just $ ist { i_libEnv = nwle} }

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef iSt nwst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem return (dgraph', dgn', nwle)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem acquired <- tryLockLocal dgn'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if acquired then do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let action = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem res@(Result d _) <- basicInferenceNode logicGraph ln dgraph'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (descr, dgn') le' iSt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem when (null d || diagString (head d) /= "Proofs.Proofs: selection")

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem $ runProveAtNode gInfo (descr, dgn') res

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem b <- hidingWarnDiag dgn'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem when b action

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockLocal dgn'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else errorDialog "Error" "Proofwindow already open"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemrunProveAtNode :: GInfo -> LNode DGNodeLab

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem -> Result G_theory -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemrunProveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just newTh ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let oldTh = dgn_theory dgnode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem rTh = propagateProofs oldTh newTh in

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unless (rTh == oldTh) $ do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem showDiagMessAux 2 ds

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let ln = libName gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem iSt = intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef iSt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost' of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just _ -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef iSt ost'

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem runAndLock gInfo $ updateGraph gInfo hist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem _ -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcheckconservativityOfNode :: GInfo -> Int -> DGraph -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcheckconservativityOfNode gInfo descr dgraph = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let iSt = intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ln = libName gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nlbl = labDG dgraph descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef iSt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just iist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem b <- hidingWarnDiag nlbl

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem when b $ do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (str, libEnv', ph) <- checkConservativityNode True (descr, nlbl)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (i_libEnv iist) ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if isPrefixOf "No conservativity" str then

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem errorDialog "Result of conservativity check" str

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem createTextDisplay "Result of conservativity check" str

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let nst = add2history (SelectCmd Node $ showDoc descr "")

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost [DgCommandChange ln]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwst = nst { i_state = Just $ iist { i_libEnv = libEnv' }}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef iSt nwst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem runAndLock gInfo $ updateGraph gInfo (reverse $ flatHistory ph)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemedgeErr :: Int -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemedgeErr descr = errorDialog "Error" $ "edge with descriptor " ++ show descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ++ " not found in the development graph"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | print the id, origin, type, proof-status and morphism of the edge

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowEdgeInfo descr me = case me of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just e@(_, _, l) -> let estr = showLEdge e in

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem createTextDisplay ("Info of " ++ estr)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (estr ++ "\n" ++ showDoc l "")

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> edgeErr descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | check conservativity of the edge

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcheckconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemcheckconservativityOfEdge descr gInfo me = case me of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> edgeErr descr

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just lnk@(_, _, lbl) -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let iSt = intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ln = libName gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef iSt

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Just iist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem lockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (str, nwle, _, ph) <- checkConservativityEdge True lnk

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem (i_libEnv iist) ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if isPrefixOf "No conservativity" str

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem then

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem errorDialog "Result of conservativity check" str

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem createTextDisplay "Result of conservativity check" str

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let nst = add2history (SelectCmd Link $ showDoc (dgl_id lbl) "")

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost [DgCommandChange ln]

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem nwst = nst { i_state = Just $ iist { i_libEnv = nwle}}

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem writeIORef iSt nwst

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem runAndLock gInfo $ updateGraph gInfo $ reverse $ flatHistory ph

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem unlockGlobal gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | show development graph for library

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDGraph :: GInfo -> LibName -> ConvFunc -> LibFunc -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowDGraph gi ln convGraph showLib = do

835d676191444a46d695171e8760d55a66c60fecminfrin putIfVerbose (hetcatsOpts gi) 3 $ "Converting graph for " ++ show ln

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem og <- readIORef $ openGraphs gi

835d676191444a46d695171e8760d55a66c60fecminfrin case Map.lookup ln og of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> do

835d676191444a46d695171e8760d55a66c60fecminfrin updateWindowCount gi succ

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem gi' <- copyGInfo gi ln

835d676191444a46d695171e8760d55a66c60fecminfrin convGraph gi' "Development Graph" showLib

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.showTemporaryMessage (graphInfo gi') "Development Graph initialized."

835d676191444a46d695171e8760d55a66c60fecminfrin Just gi' ->

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem GA.showTemporaryMessage (graphInfo gi') "Development Graph requested."

835d676191444a46d695171e8760d55a66c60fecminfrin

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | show library referened by a DGRef node (=node drawn as a box)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemshowReferencedLibrary descr gInfo convGraph showLib = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return ()

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let le = i_libEnv ist

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe ln = libName gInfo

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe refNode = labDG (lookupDGraph ln le) descr

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe refLibname = if isDGRef refNode then dgn_libname refNode

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else error "showReferencedLibrary"

54ab5681d5d6c36b0429b74dbd3b132380c4bf8awrowe case Map.lookup refLibname le of

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe Just _ -> showDGraph gInfo refLibname convGraph showLib

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe Nothing -> error $ "The referenced library (" ++ show refLibname

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe ++ ") is unknown"

b72b768176398d8cd00d61b289c8e0f8ce09469fwrowe

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem-- | display a window of translated graph with maximal sublogic.

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtranslateGraph :: GInfo -> IO (Maybe LibEnv)

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluemtranslateGraph gInfo@(GInfo { hetcatsOpts = opts }) = do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem ost <- readIORef $ intState gInfo

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem case i_state ost of

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Nothing -> return Nothing

36ef8f77bffe75d1aa327882be1b5bdbe2ff567asf Just ist -> do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem let

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem le = i_libEnv ist

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem Result diagsSl mSublogic = getDGLogic le

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem myErrMess = showDiagMess opts

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem error' = errorDialog "Error"

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem if hasErrors diagsSl then do

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem myErrMess diagsSl

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem return Nothing

da9d691bd7c0094bffdc19aab2dd4e6dc5637b75rpluem else case mSublogic of

Nothing -> do

error' "No maximal sublogic found."

return Nothing

Just sublogic -> do

let paths = findComorphismPaths logicGraph sublogic

if null paths then do

error' "This graph has no comorphism to translation."

return Nothing

else do

sel <- listBox "Choose a logic translation" $ map show paths

case sel of

Nothing -> do

error' "no logic translation chosen"

return Nothing

Just j -> do

let Result diag mle = libEnv_translation le $ paths !! j

case mle of

Just newLibEnv -> do

showDiagMess opts $ diagsSl ++ diag

return $ Just newLibEnv

Nothing -> do

myErrMess $ diagsSl ++ diag

return Nothing

-- | saves the uDrawGraph graph to a file

saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)

-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()

saveUDGraph gInfo@(GInfo { graphInfo = gi

, libName = ln }) nodemap linkmap = do

ost <- readIORef $ intState gInfo

case i_state ost of

Nothing -> return ()

Just _ -> do

maybeFilePath <- fileSaveDialog (rmSuffix (libNameToFile ln) ++ ".udg")

[ ("uDrawGraph", ["*.udg"])

, ("All Files", ["*"])] Nothing

case maybeFilePath of

Just filepath -> do

GA.showTemporaryMessage gi "Converting graph..."

nstring <- nodes2String gInfo nodemap linkmap

writeFile filepath nstring

GA.showTemporaryMessage gi $ "Graph stored to " ++ filepath ++ "!"

Nothing -> GA.showTemporaryMessage gi "Aborted!"

-- | Converts the nodes of the graph to String representation

nodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)

-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)

-> IO String

nodes2String gInfo@(GInfo { graphInfo = gi

, libName = ln }) nodemap linkmap = do

ost <- readIORef $ intState gInfo

case i_state ost of

Nothing -> return []

Just ist -> do

let le = i_libEnv ist

nodes <- filterM (fmap not . GA.isHiddenNode gi . fst)

$ labNodesDG $ lookupDGraph ln le

nstring <- foldM (\ s ->

fmap ((if null s then s else s ++ ",\n") ++)

. node2String gInfo nodemap linkmap)

"" nodes

return $ "[" ++ nstring ++ "]"

-- | Converts a node to String representation

node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)

-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)

-> LNode DGNodeLab -> IO String

node2String gInfo nodemap linkmap (nid, dgnode) = do

label <- getNodeLabel gInfo dgnode

let ntype = getRealDGNodeType dgnode

(shape, color) <- case Map.lookup ntype nodemap of

Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype

Just (s, c) -> return (s, c)

let

object = "a(\"OBJECT\",\"" ++ label ++ "\"),"

color' = "a(\"COLOR\",\"" ++ color ++ "\"),"

shape' = "a(\"_GO\",\"" ++ map toLower (show shape) ++ "\")"

links <- links2String gInfo linkmap nid

return $ "l(\"" ++ show nid ++ "\",n(\"" ++ show ntype ++ "\","

++ "[" ++ object ++ color' ++ shape' ++ "],"

++ "\n [" ++ links ++ "]))"

-- | Converts all links of a node to String representation

links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)

-> Int -> IO String

links2String gInfo@(GInfo { graphInfo = gi

, libName = ln }) linkmap nodeid = do

ost <- readIORef $ intState gInfo

case i_state ost of

Nothing -> return []

Just ist -> do

let le = i_libEnv ist

edges <- filterM (\ (src, _, edge) -> do

let eid = dgl_id edge

b <- GA.isHiddenEdge gi eid

return $ not b && src == nodeid)

$ labEdgesDG $ lookupDGraph ln le

foldM (\ s edge -> do

s' <- link2String linkmap edge

return $ (if null s then "" else s ++ ",\n") ++ s') "" edges

-- | Converts a link to String representation

link2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)

-> LEdge DGLinkLab -> IO String

link2String linkmap (nodeid1, nodeid2, edge) = do

let (EdgeId linkid) = dgl_id edge

ltype = getRealDGLinkType edge

(line, color) <- case Map.lookup ltype linkmap of

Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype

Just (l, c) -> return (l, c)

let

nm = "\"" ++ show linkid ++ ":" ++ show nodeid1 ++ "->"

++ show nodeid2 ++ "\""

color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"

line' = "a(\"EDGEPATTERN\",\"" ++ map toLower (show line) ++ "\")"

return $ "l(" ++ nm ++ ",e(\"" ++ show ltype ++ "\","

++ "[" ++ color' ++ line' ++ "],"

++ "r(\"" ++ show nodeid2 ++ "\")))"

-- | Returns the name of the Node

getNodeLabel :: GInfo -> DGNodeLab -> IO String

getNodeLabel (GInfo { options = opts }) dgnode = do

flags <- readIORef opts

return $ if flagHideNames flags && isInternalNode dgnode

then "" else getDGNodeName dgnode