GraphTypes.hs revision 966a6c024c828387023fccb0cd0049f78687e5dc
97a9a944b5887e91042b019776c41d5dd74557aferikabeleModule : $Header$
97a9a944b5887e91042b019776c41d5dd74557aferikabeleDescription : Types for the Central GUI of Hets
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
fe64b2ba25510d8c9dba5560a2d537763566cf40ndMaintainer : till@informatik.uni-bremen.de
fe64b2ba25510d8c9dba5560a2d537763566cf40ndStability : provisional
fe64b2ba25510d8c9dba5560a2d537763566cf40ndPortability : non-portable (imports Logic)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd ( GInfo(..)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , ConversionMaps(..)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , DGraphAndAGraphNode
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , DGraphAndAGraphEdge
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , InternalNames(..)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , ConvFunc
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , DaVinciGraphTypeSyn
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , emptyConversionMaps
a63f0ab647ad2ab72efc9bea7a66e24e9ebc5cc2nd , emptyGInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , copyGInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , lockGlobal
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , tryLockGlobal
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , unlockGlobal
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.AbstractGraphView(Descr, GraphInfo, initgraphs)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GUI.ProofManagement (GUIMVar)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.Id(nullRange)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.Doc(text, ($+$))
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport Common.DocUtils(Pretty, pretty)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport qualified Common.InjMap as InjMap
5f86589186bcc15ee13e288a9d73acbeab2409fbdpejeshimport Driver.Options(HetcatsOpts, defaultHetcatsOpts)
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport DaVinciGraph
117c1f888a14e73cdd821dc6c23eb0411144a41cndimport GraphDisp
117c1f888a14e73cdd821dc6c23eb0411144a41cnd{- Maps used to track which node resp edge of the abstract graph
117c1f888a14e73cdd821dc6c23eb0411144a41cndcorrespondes with which of the development graph and vice versa and
117c1f888a14e73cdd821dc6c23eb0411144a41cndone Map to store which libname belongs to which development graph-}
117c1f888a14e73cdd821dc6c23eb0411144a41cnddata ConversionMaps = ConversionMaps
117c1f888a14e73cdd821dc6c23eb0411144a41cnd { dgAndabstrNode :: DGraphAndAGraphNode
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , dgAndabstrEdge :: DGraphAndAGraphEdge
117c1f888a14e73cdd821dc6c23eb0411144a41cnd } deriving Show
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | Pretty instance for ConversionMaps
117c1f888a14e73cdd821dc6c23eb0411144a41cndinstance Pretty ConversionMaps where
117c1f888a14e73cdd821dc6c23eb0411144a41cnd pretty convMaps =
117c1f888a14e73cdd821dc6c23eb0411144a41cnd text "dg2abstrNode"
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ pretty (InjMap.getAToB $ dgAndabstrNode convMaps)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ text "dg2abstrEdge"
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ pretty (InjMap.getAToB $ dgAndabstrEdge convMaps)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ text "abstr2dgNode"
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ pretty (InjMap.getBToA $ dgAndabstrNode convMaps)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ text "abstr2dgEdge"
117c1f888a14e73cdd821dc6c23eb0411144a41cnd $+$ pretty (InjMap.getBToA $ dgAndabstrEdge convMaps)
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | types of the Maps above
117c1f888a14e73cdd821dc6c23eb0411144a41cndtype DGraphAndAGraphNode = InjMap.InjMap (LIB_NAME, Node) Descr
117c1f888a14e73cdd821dc6c23eb0411144a41cndtype DGraphAndAGraphEdge =
117c1f888a14e73cdd821dc6c23eb0411144a41cnd InjMap.InjMap (LIB_NAME, (Descr, Descr, String)) Descr
117c1f888a14e73cdd821dc6c23eb0411144a41cnddata InternalNames =
117c1f888a14e73cdd821dc6c23eb0411144a41cnd InternalNames { showNames :: Bool
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , updater :: [(String,(String -> String) -> IO ())]
117c1f888a14e73cdd821dc6c23eb0411144a41cnd-- | Global datatype for all GUI functions
117c1f888a14e73cdd821dc6c23eb0411144a41cnddata GInfo = GInfo
117c1f888a14e73cdd821dc6c23eb0411144a41cnd { -- Global
117c1f888a14e73cdd821dc6c23eb0411144a41cnd libEnvIORef :: IORef LibEnv
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , gi_hetcatsOpts :: HetcatsOpts
117c1f888a14e73cdd821dc6c23eb0411144a41cnd , windowCount :: MVar Integer
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , exitMVar :: MVar ()
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , globalLock :: MVar ()
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , globalHist :: MVar ([[LIB_NAME]],[[LIB_NAME]])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , descrIORef :: IORef Descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , conversionMapsIORef :: IORef ConversionMaps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , graphId :: Descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , nextGraphId :: IORef Descr
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_LIB_NAME :: LIB_NAME
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , gi_GraphInfo :: GraphInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , internalNamesIORef :: IORef InternalNames
fe64b2ba25510d8c9dba5560a2d537763566cf40nd -- show internal names?
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , visibleNodesIORef :: IORef [[Node]]
fe64b2ba25510d8c9dba5560a2d537763566cf40nd , proofGUIMVar :: GUIMVar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{- | Type of the convertGraph function. Used as type of a parameter of some
06ba4a61654b3763ad65f52283832ebf058fdf1cslive functions in GraphMenu and GraphLogic. -}
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetype ConvFunc = GInfo -> String -> LibFunc
06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> IO (Descr, GraphInfo, ConversionMaps)
fb77c505254b6e9c925e23e734463e87574f8f40kesstype LibFunc = GInfo -> IO DaVinciGraphTypeSyn
06ba4a61654b3763ad65f52283832ebf058fdf1cslivetype DaVinciGraphTypeSyn =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Graph DaVinciGraph
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DaVinciGraphParms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DaVinciNode
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DaVinciNodeType
fb77c505254b6e9c925e23e734463e87574f8f40kess DaVinciNodeTypeParms
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DaVinciArcType
06ba4a61654b3763ad65f52283832ebf058fdf1cslive DaVinciArcTypeParms
fb77c505254b6e9c925e23e734463e87574f8f40kess-- | Creates empty conversionmaps
06ba4a61654b3763ad65f52283832ebf058fdf1csliveemptyConversionMaps :: ConversionMaps
06ba4a61654b3763ad65f52283832ebf058fdf1csliveemptyConversionMaps =
06ba4a61654b3763ad65f52283832ebf058fdf1cslive ConversionMaps { dgAndabstrNode = InjMap.empty::DGraphAndAGraphNode
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , dgAndabstrEdge = InjMap.empty::DGraphAndAGraphEdge
06ba4a61654b3763ad65f52283832ebf058fdf1cslive-- | Creates an empty GInfo
06ba4a61654b3763ad65f52283832ebf058fdf1csliveemptyGInfo :: IO GInfo
06ba4a61654b3763ad65f52283832ebf058fdf1csliveemptyGInfo = do
fb77c505254b6e9c925e23e734463e87574f8f40kess iorLE <- newIORef emptyLibEnv
fb77c505254b6e9c925e23e734463e87574f8f40kess iorD <- newIORef (0 :: Descr)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive iorNGI <- newIORef (0 :: Descr)
fb77c505254b6e9c925e23e734463e87574f8f40kess iorCM <- newIORef emptyConversionMaps
fb77c505254b6e9c925e23e734463e87574f8f40kess graphInfo <- initgraphs
fb77c505254b6e9c925e23e734463e87574f8f40kess iorIN <- newIORef $ InternalNames False []
06ba4a61654b3763ad65f52283832ebf058fdf1cslive iorVN <- newIORef ([] :: [[Node]])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive guiMVar <- newEmptyMVar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive gl <- newEmptyMVar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive exit <- newEmptyMVar
fb77c505254b6e9c925e23e734463e87574f8f40kess wc <- newMVar 0
fb77c505254b6e9c925e23e734463e87574f8f40kess gh <- newMVar ([],[])
06ba4a61654b3763ad65f52283832ebf058fdf1cslive return $ GInfo { libEnvIORef = iorLE
fb77c505254b6e9c925e23e734463e87574f8f40kess , descrIORef = iorD
fb77c505254b6e9c925e23e734463e87574f8f40kess , conversionMapsIORef = iorCM
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , graphId = 0
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , nextGraphId = iorNGI
130d299c4b2b15be45532a176604c71fdc7bea5bnd , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
130d299c4b2b15be45532a176604c71fdc7bea5bnd , gi_GraphInfo = graphInfo
130d299c4b2b15be45532a176604c71fdc7bea5bnd , internalNamesIORef = iorIN
130d299c4b2b15be45532a176604c71fdc7bea5bnd , gi_hetcatsOpts = defaultHetcatsOpts
130d299c4b2b15be45532a176604c71fdc7bea5bnd , visibleNodesIORef = iorVN
130d299c4b2b15be45532a176604c71fdc7bea5bnd , proofGUIMVar = guiMVar
130d299c4b2b15be45532a176604c71fdc7bea5bnd , windowCount = wc
130d299c4b2b15be45532a176604c71fdc7bea5bnd , exitMVar = exit
130d299c4b2b15be45532a176604c71fdc7bea5bnd , globalLock = gl
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , globalHist = gh
fe64b2ba25510d8c9dba5560a2d537763566cf40nd-- | Creates an empty GInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcopyGInfo :: GInfo -> IO GInfo
fe64b2ba25510d8c9dba5560a2d537763566cf40ndcopyGInfo gInfo = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd iorD <- newIORef (0 :: Descr)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd iorNGI <- newIORef (0 :: Descr)
fe64b2ba25510d8c9dba5560a2d537763566cf40nd iorCM <- newIORef emptyConversionMaps
fe64b2ba25510d8c9dba5560a2d537763566cf40nd graphInfo <- initgraphs
fe64b2ba25510d8c9dba5560a2d537763566cf40nd iorIN <- newIORef $ InternalNames False []
fe64b2ba25510d8c9dba5560a2d537763566cf40nd iorVN <- newIORef ([] :: [[Node]])
fe64b2ba25510d8c9dba5560a2d537763566cf40nd guiMVar <- newEmptyMVar
313bb560bc5c323cfd40c9cad7335b4b8e060aedkess return $ gInfo { descrIORef = iorD
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , conversionMapsIORef = iorCM
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , graphId = 0
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , nextGraphId = iorNGI
ff797e743eb73c1d45b08158aa6b288c2d0c46eeslive , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
06ba4a61654b3763ad65f52283832ebf058fdf1cslive , gi_GraphInfo = graphInfo
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , internalNamesIORef = iorIN
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , visibleNodesIORef = iorVN
a7f40ca49262952d6dd69d021cf5b0c2b452ae4cnd , proofGUIMVar = guiMVar
06ba4a61654b3763ad65f52283832ebf058fdf1cslive{- | Acquire the global lock. If already locked it waits till it is unlocked
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelockGlobal :: GInfo -> IO ()
06ba4a61654b3763ad65f52283832ebf058fdf1cslivelockGlobal (GInfo { globalLock = lock }) = putMVar lock ()
130d299c4b2b15be45532a176604c71fdc7bea5bnd-- | Tries to acquire the global lock. Return False if already acquired.
130d299c4b2b15be45532a176604c71fdc7bea5bndtryLockGlobal :: GInfo -> IO Bool
130d299c4b2b15be45532a176604c71fdc7bea5bndtryLockGlobal (GInfo { globalLock = lock }) = tryPutMVar lock ()
130d299c4b2b15be45532a176604c71fdc7bea5bnd-- | Releases the global lock.
130d299c4b2b15be45532a176604c71fdc7bea5bndunlockGlobal :: GInfo -> IO ()
130d299c4b2b15be45532a176604c71fdc7bea5bndunlockGlobal (GInfo { globalLock = lock }) = do
fe64b2ba25510d8c9dba5560a2d537763566cf40nd unlocked <- tryTakeMVar lock
fe64b2ba25510d8c9dba5560a2d537763566cf40nd case unlocked of
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Just () -> return ()
fe64b2ba25510d8c9dba5560a2d537763566cf40nd Nothing -> error "Global lock wasn't locked."