hets/GUI/GraphTypes.hs

	GraphTypes.hs revision 4112d6e50d7f90b5120ecbd1c49452f222021579
{- |
Module      :  $Header$
Description :  Types for the Central GUI of Hets
Copyright   :  (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic)
-}

module GUI.GraphTypes
    ( GInfo(..)
    , ConversionMaps(..)
    , DGraphAndAGraphNode
    , DGraphAndAGraphEdge
    , InternalNames(..)
    , ConvFunc
    , LibFunc
    , DaVinciGraphTypeSyn
    , emptyConversionMaps
    , emptyGInfo
    , copyGInfo
    , lockGlobal
    , tryLockGlobal
    , unlockGlobal
    , mergeDG
    )
    where

import GUI.AbstractGraphView(Descr, GraphInfo, initgraphs)
import GUI.ProofManagement (GUIMVar)

import Syntax.AS_Library
import Syntax.Print_AS_Library()

import Static.DevGraph

import Common.Id(nullRange)
import Common.Doc(text, ($+$))
import Common.DocUtils(Pretty, pretty)
import qualified Common.InjMap as InjMap

import Driver.Options(HetcatsOpts, defaultHetcatsOpts)

import Data.IORef
import Data.Graph.Inductive.Graph(Node)
import qualified Data.Map as Map

import Control.Concurrent.MVar

import DaVinciGraph
import GraphDisp

{- Maps used to track which node resp edge of the abstract graph
correspondes with which of the development graph and vice versa and
one Map to store which libname belongs to which development graph-}
data ConversionMaps = ConversionMaps
    { dgAndabstrNode :: DGraphAndAGraphNode
    , dgAndabstrEdge :: DGraphAndAGraphEdge
    } deriving Show

-- | Pretty instance for ConversionMaps
instance Pretty ConversionMaps where
  pretty convMaps =
       text "dg2abstrNode"
    $+$ pretty (InjMap.getAToB $ dgAndabstrNode convMaps)
    $+$ text "dg2abstrEdge"
    $+$ pretty (InjMap.getAToB $ dgAndabstrEdge convMaps)
    $+$ text "abstr2dgNode"
    $+$ pretty (InjMap.getBToA $ dgAndabstrNode convMaps)
    $+$ text "abstr2dgEdge"
    $+$ pretty (InjMap.getBToA $ dgAndabstrEdge convMaps)

-- | types of the Maps above
type DGraphAndAGraphNode = InjMap.InjMap (LIB_NAME, Node) Descr
type DGraphAndAGraphEdge =
    InjMap.InjMap (LIB_NAME, (Descr, Descr, String)) Descr

data InternalNames =
     InternalNames { showNames :: Bool
                   , updater :: [(String,(String -> String) -> IO ())]
                   }

-- | Global datatype for all GUI functions
data GInfo = GInfo
             { -- Global
               libEnvIORef :: IORef LibEnv
             , gi_hetcatsOpts :: HetcatsOpts
             , windowCount :: MVar Integer
             , exitMVar :: MVar ()
             , globalLock :: MVar ()
             , globalHist :: MVar ([[LIB_NAME]],[[LIB_NAME]])
               -- Local
             , descrIORef :: IORef Descr
             , conversionMapsIORef :: IORef ConversionMaps
             , graphId :: Descr
             , nextGraphId :: IORef Descr
             , gi_LIB_NAME :: LIB_NAME
             , gi_GraphInfo :: GraphInfo
             , internalNamesIORef :: IORef InternalNames
               -- show internal names?
             , visibleNodesIORef :: IORef [[Node]]
             , proofGUIMVar :: GUIMVar
             }

{- | Type of the convertGraph function. Used as type of a parameter of some
     functions in GraphMenu and GraphLogic. -}
type ConvFunc = GInfo -> String -> LibFunc
             -> IO (Descr, GraphInfo, ConversionMaps)

type LibFunc =  GInfo -> IO DaVinciGraphTypeSyn

type DaVinciGraphTypeSyn =
     Graph DaVinciGraph
           DaVinciGraphParms
           DaVinciNode
           DaVinciNodeType
           DaVinciNodeTypeParms
           DaVinciArc
           DaVinciArcType
           DaVinciArcTypeParms

-- | Creates empty conversionmaps
emptyConversionMaps :: ConversionMaps
emptyConversionMaps =
  ConversionMaps { dgAndabstrNode = InjMap.empty::DGraphAndAGraphNode
                 , dgAndabstrEdge = InjMap.empty::DGraphAndAGraphEdge
                 }

-- | Creates an empty GInfo
emptyGInfo :: IO GInfo
emptyGInfo = do
  iorLE <- newIORef emptyLibEnv
  iorD <- newIORef (0 :: Descr)
  iorNGI <- newIORef (0 :: Descr)
  iorCM <- newIORef emptyConversionMaps
  graphInfo <- initgraphs
  iorIN <- newIORef $ InternalNames False []
  iorVN <- newIORef ([] :: [[Node]])
  guiMVar <- newEmptyMVar
  gl <- newEmptyMVar
  exit <- newEmptyMVar
  wc <- newMVar 0
  gh <- newMVar ([],[])
  return $ GInfo { libEnvIORef = iorLE
                 , descrIORef = iorD
                 , conversionMapsIORef = iorCM
                 , graphId = 0
                 , nextGraphId = iorNGI
                 , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
                 , gi_GraphInfo = graphInfo
                 , internalNamesIORef = iorIN
                 , gi_hetcatsOpts = defaultHetcatsOpts
                 , visibleNodesIORef = iorVN
                 , proofGUIMVar = guiMVar
                 , windowCount = wc
                 , exitMVar = exit
                 , globalLock = gl
                 , globalHist = gh
                 }

-- | Creates an empty GInfo
copyGInfo :: GInfo -> IO GInfo
copyGInfo gInfo = do
  iorD <- newIORef (0 :: Descr)
  iorNGI <- newIORef (0 :: Descr)
  iorCM <- newIORef emptyConversionMaps
  graphInfo <- initgraphs
  iorIN <- newIORef $ InternalNames False []
  iorVN <- newIORef ([] :: [[Node]])
  guiMVar <- newEmptyMVar
  return $ gInfo { descrIORef = iorD
                 , conversionMapsIORef = iorCM
                 , graphId = 0
                 , nextGraphId = iorNGI
                 , gi_LIB_NAME = Lib_id $ Indirect_link "" nullRange "" noTime
                 , gi_GraphInfo = graphInfo
                 , internalNamesIORef = iorIN
                 , visibleNodesIORef = iorVN
                 , proofGUIMVar = guiMVar
                 }

{- | Acquire the global lock. If already locked it waits till it is unlocked
     again.-}
lockGlobal :: GInfo -> IO ()
lockGlobal (GInfo { globalLock = lock }) = putMVar lock ()

-- | Tries to acquire the global lock. Return False if already acquired.
tryLockGlobal :: GInfo -> IO Bool
tryLockGlobal (GInfo { globalLock = lock }) = tryPutMVar lock ()

-- | Releases the global lock.
unlockGlobal :: GInfo -> IO ()
unlockGlobal (GInfo { globalLock = lock }) = do
  unlocked <- tryTakeMVar lock
  case unlocked of
    Just () -> return ()
    Nothing -> error "Global lock wasn't locked."

mergeDG :: GInfo -> DGraph -> LIB_NAME -> IO ()
mergeDG gInfo@(GInfo{ libEnvIORef = iorLE
                    }) dgraph ln = do
  le <- readIORef iorLE
  let changes = filter (\chg -> notElem chg $ proofHistory
                       $ lookupDGraph ln le) $ proofHistory dgraph
  mapM_ (mergeChange gInfo ln) changes
  return ()

mergeChange :: GInfo -> LIB_NAME -> ([DGRule], [DGChange])
            -> IO ([DGRule], [DGChange])
mergeChange _ _ ([], _) = return ([], [])
mergeChange _ _ (_, []) = return ([], [])
mergeChange gInfo@(GInfo{ libEnvIORef = iorLE
                        }) ln (rule:rules, change:changes) = do
  lockGlobal gInfo
  le <- readIORef iorLE
  let g = lookupDGraph ln le
  (g', change') <- case change of
    InsertNode n -> return (insLNodeDG n g, InsertNode n)
    DeleteNode n -> return (delLNodeDG n g, DeleteNode n)
    InsertEdge e -> -- let newEdge = initEdgeID e g in
                    -- return (insLNodeDG e g, InsertEdge newEdge)
                    return (insLEdgeDG e g, InsertEdge e)
    DeleteEdge e -> return (delLEdgeDG e g, DeleteEdge e)
    SetNodeLab _ (_, _) -> do
      -- dgn_theory' <- joinG_sentences (dgn_theory old) $ dgn_theory new
      return (g, change)
  writeIORef iorLE $ Map.insert ln g' le
  unlockGlobal gInfo
  (rules',changes') <- mergeChange gInfo ln (rules, changes)
  return (rule:rules', change':changes')