hets/GUI/ShowLibGraph.hs

3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov{- |
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovModule      :  ./GUI/ShowLibGraph.hs
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovCopyright   :  (c) Uni Bremen 2003-2007
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovLicense     :  GPLv2 or higher, see LICENSE.txt
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovMaintainer  :  raider@informatik.uni-bremen.de
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovStability   :  unstable
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovPortability :  non-portable
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovThis Modul provides a function to display a Library Dependency Graph.
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov-}
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovmodule GUI.ShowLibGraph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  ( showLibGraph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  , mShowGraph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  , closeOpenWindows
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  ) where
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Driver.Options (HetcatsOpts (outtypes, verbose))
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Driver.ReadFn
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Driver.WriteFn
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Driver.AnaLib
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Static.DevGraph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Static.History
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Static.ToXml as ToXml
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Static.ApplyChanges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport GUI.UDGUtils as UDG
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport GUI.Utils
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport GUI.GraphTypes
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport GUI.GraphLogic (translateGraph, showDGraph)
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport GUI.ShowLogicGraph
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport GUI.GraphDisplay
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport qualified GUI.GraphAbstraction as GA
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Common.LibName
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport qualified Common.Lib.Rel as Rel
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport Common.Result
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport Common.ResultT
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashovimport Common.XmlDiff
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Text.XML.Light
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Data.IORef
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport qualified Data.Map as Map
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport qualified Data.Set as Set
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Control.Concurrent.MVar
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Control.Monad
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Interfaces.DataTypes
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovimport Interfaces.Utils
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashovtype NodeEdgeList = ([DaVinciNode LibName], [DaVinciArc (IO String)])
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov{- | Creates a  new uDrawGraph Window and shows the Library Dependency Graph of
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov     the given LibEnv. -}
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovshowLibGraph :: LibFunc
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovshowLibGraph gi = do
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  let lock = libGraphLock gi
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  isEmpty <- isEmptyMVar lock
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  when isEmpty $ do
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov    putMVar lock ()
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov    updateWindowCount gi succ
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov    graph <- newIORef daVinciSort
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov    nodesEdges <- newIORef (([], []) :: NodeEdgeList)
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov    let
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov      globalMenu =
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov        GlobalMenu (UDG.Menu Nothing
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov          [ Button "Reload Library" $ reloadLibGraph gi graph nodesEdges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov          , Button "Experimental reload changed Library"
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                       $ changeLibGraph gi graph nodesEdges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov          , Button "Translate Library" $ translate gi
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov          , Button "Show Logic Graph" showLG
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov          ])
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov      graphParms = globalMenu $$
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                   GraphTitle "Hets Library Graph" $$
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                   OptimiseLayout True $$
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                   AllowClose (closeGInfo gi) $$
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                   FileMenuAct ExitMenuOption (Just (exitGInfo gi)) $$
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                   emptyGraphParms
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov    graph' <- newGraph daVinciSort graphParms
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov    addNodesAndEdges gi graph graph' nodesEdges
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai KondrashovcloseGInfo :: GInfo -> IO Bool
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovcloseGInfo gi = do
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  updateWindowCount gi pred
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  takeMVar (libGraphLock gi)
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  return True
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov-- | Reloads all Libraries and the Library Dependency Graph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovreloadLibGraph :: GInfo -> IORef DaVinciGraphTypeSyn -> IORef NodeEdgeList
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov               -> IO ()
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovreloadLibGraph gi graph nodesEdges = do
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  b <- warningDialog "Reload library" warnTxt
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  when b $ reloadLibGraph' gi graph nodesEdges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovwarnTxt :: String
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovwarnTxt = unlines
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  [ "Are you sure to recreate Library?"
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  , "All development graph windows will be closed and proofs will be lost."
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  , "", "This operation can not be undone." ]
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov-- | Reloads all Libraries and the Library Dependency Graph
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai KondrashovreloadLibGraph' :: GInfo -> IORef DaVinciGraphTypeSyn -> IORef NodeEdgeList
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov                -> IO ()
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai KondrashovreloadLibGraph' gi graph nodesEdges = do
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  graph' <- readIORef graph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  (nodes, edges) <- readIORef nodesEdges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  let ln = libName gi
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov      libfile = libNameToFile ln
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  m <- anaLib (hetcatsOpts gi) { outtypes = [] } libfile
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  case m of
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov    Nothing -> errorDialog "Error" $ "Error when reloading file '"
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov                                     ++ libfile ++ "'"
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov    Just (_, le) -> do
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov      closeOpenWindows gi
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov      mapM_ (deleteArc graph') edges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov      mapM_ (deleteNode graph') nodes
96544fca522e66b4f69b4252854a5f672c96f9c4Nikolai Kondrashov      addNodesAndEdges gi graph graph' nodesEdges
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov      writeIORef (intState gi) emptyIntState
96544fca522e66b4f69b4252854a5f672c96f9c4Nikolai Kondrashov                 { i_state = Just $ emptyIntIState le ln
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov                 , filename = libfile }
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov      mShowGraph gi ln
96544fca522e66b4f69b4252854a5f672c96f9c4Nikolai Kondrashov
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai KondrashovchangeLibGraph :: GInfo -> IORef DaVinciGraphTypeSyn -> IORef NodeEdgeList
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  -> IO ()
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai KondrashovchangeLibGraph gi graph nodesEdges = do
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  let ln = libName gi
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov      opts = hetcatsOpts gi
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  ost <- readIORef $ intState gi
5f4f0428c182a9e77d29b39f3749fce03643ac8dNikolai Kondrashov  graph' <- readIORef graph
3ce85a5f5264e7118beb6524e120fd8b53a13da4Nikolai Kondrashov  (nodes, edges) <- readIORef nodesEdges
  case i_state ost of
    Nothing -> return ()
    Just ist -> do
      let le = i_libEnv ist
          dg = lookupDGraph ln le
          fn = libNameToFile ln
          dgold = undoAllChanges dg
          c2 = ToXml.dGraph opts le ln dgold
      m <- anaLib opts { outtypes = [] } fn
      case m of
        Just (nln, nle) | nln == ln -> do
          let dg2 = lookupDGraph nln nle
              ndg = undoAllChanges dg2
              c3 = ToXml.dGraph opts nle ln ndg
              xs = hetsXmlDiff c2 c3
          writeVerbFile opts (libNameToFile ln ++ ".xupdate")
            $ ppTopElement xs
          Result ds mdg <- runResultT $ dgXUpdateMods opts c2
            (getNewEdgeId dgold) xs le ln dg
          case mdg of
                Just (nLn, fle) -> do
                  closeOpenWindows gi
                  mapM_ (deleteArc graph') edges
                  mapM_ (deleteNode graph') nodes
                  addNodesAndEdges gi graph graph' nodesEdges
                  writeIORef (intState gi) emptyIntState
                        { i_state = Just $ emptyIntIState fle nLn
                        , filename = fn }
                  mShowGraph gi nLn
                Nothing ->
                  errorDialog "Error" $ showRelDiags (verbose opts) ds
        _ -> errorDialog "Error" $ "Error when reloading file '" ++ fn ++ "'"

-- | Translate Graph
translate :: GInfo -> IO ()
translate gi = do
  b <- warningDialog "Translate library" warnTxt
  when b $ translate' gi

-- | Translate Graph
translate' :: GInfo -> IO ()
translate' gi = do
  mle <- translateGraph gi
  case mle of
    Just le -> do
      closeOpenWindows gi
      let ln = libName gi
          ost = emptyIntState
          nwst = case i_state ost of
            Nothing -> ost
            Just ist -> ost { i_state = Just $ ist { i_libEnv = le
                                                   , i_ln = ln }
                            , filename = libNameToFile ln }
      writeIORef (intState gi) nwst
      mShowGraph gi ln
    Nothing -> return ()

-- | closes the open graphs to be reopened later
closeOpenWindows :: GInfo -> IO ()
closeOpenWindows gi = do
  let iorOpenGraphs = openGraphs gi
  oGraphs <- readIORef iorOpenGraphs
  mapM_ (GA.closeGraphWindow . graphInfo) $ Map.elems oGraphs
  updateWindowCount gi (const 1)
  writeIORef iorOpenGraphs Map.empty

-- | Adds the Librarys and the Dependencies to the Graph
addNodesAndEdges :: GInfo -> IORef DaVinciGraphTypeSyn -> DaVinciGraphTypeSyn
  -> IORef NodeEdgeList -> IO ()
addNodesAndEdges gi graphR graph nodesEdges = do
 ost <- readIORef $ intState gi
 case i_state ost of
  Nothing -> return ()
  Just ist -> do
   let
    le = i_libEnv ist
    opts = hetcatsOpts gi
    lookup' x y = Map.findWithDefault
      (error $ "lookup2': node not found " ++ show y) y x
    keySet = Map.keysSet le
    keys = Set.toList keySet
    subNodeMenu = LocalMenu (UDG.Menu Nothing [
      Button "Show Graph" $ mShowGraph gi,
      Button "Show spec/View Names" $ showSpec le])
    subNodeTypeParms = subNodeMenu $$$
                       Box $$$
                       ValueTitle (return . show) $$$
                       Color (getColor opts Green True True) $$$
                       emptyNodeTypeParms
   subNodeType <- newNodeType graph subNodeTypeParms
   subNodeList <- mapM (newNode graph subNodeType) keys
   let
    nodes' = Map.fromList $ zip keys subNodeList
    subArcMenu = LocalMenu (UDG.Menu Nothing [])
    subArcTypeParms = subArcMenu $$$
                      ValueTitle id $$$
                      Color (getColor opts Black False False) $$$
                      emptyArcTypeParms
   subArcType <- newArcType graph subArcTypeParms
   let insertSubArc (node1, node2) = newArc graph subArcType (return "")
                                            (lookup' nodes' node1)
                                            (lookup' nodes' node2)
   subArcList <- mapM insertSubArc $ getLibDeps keySet le
   writeIORef nodesEdges (subNodeList, subArcList)
   writeIORef graphR graph
   redraw graph

-- | Creates a list of all LibName pairs, which have a dependency
getLibDeps :: Set.Set LibName -> LibEnv -> [(LibName, LibName)]
getLibDeps ks =
  Rel.toList . Rel.intransKernel . (`Rel.restrict` ks) . getLibDepRel

mShowGraph :: GInfo -> LibName -> IO ()
mShowGraph gi ln = showDGraph gi ln convertGraph showLibGraph

-- | Displays the Specs of a Library in a Textwindow
showSpec :: LibEnv -> LibName -> IO ()
showSpec le ln =
  createTextDisplay ("Contents of " ++ show ln)
                    $ unlines . map show . Map.keys . globalEnv
                    $ lookupDGraph ln le