ConvertDevToAbstractGraph.hs revision 97018cf5fa25b494adffd7e9b4e87320dae6bf47
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- |
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorriniModule : $Header$
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorriniMaintainer : jfgerken@tzi.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : non-portable (imports Logic)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Conversion of development graphs from Logic.DevGraph
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder to abstract graphs of the graph display interface
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{-
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder todo:
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder share strings to avoid typos
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder hiding of internal nodes:
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder internal nodes that are not between named nodes should be kept
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder display inclusions and inter-logic links in special colour
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder try different graph layout algorithms for daVinci (dot?)
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini close program when all windows are closed
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini issue warning when theory cannot be flattened
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder different linktypes for local and hiding definition links
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedermodule GUI.ConvertDevToAbstractGraph where
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederimport Logic.Logic
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederimport Logic.Grothendieck
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Logic.Comorphism
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederimport Comorphisms.LogicGraph
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torriniimport Syntax.AS_Library
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torriniimport Static.DevGraph
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederimport Static.DGToSpec
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.Proofs
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.InferBasic
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.Global
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.Local
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.HideTheoremShift
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Proofs.TheoremHideShift
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport GUI.AbstractGraphView
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maederimport GUI.ShowLogicGraph
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maederimport GUI.Utils
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maederimport GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport FileDialog
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Events
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport System.Directory
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Broadcaster(newSimpleBroadcaster,applySimpleUpdate)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Sources(toSimpleSource)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport DaVinciGraph
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport GraphDisp
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport GraphConfigure
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport TextDisplay
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Configuration
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport qualified HTk
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport qualified Common.Lib.Map as Map
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Common.Lib.Pretty as Pretty hiding (isEmpty)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Common.Id
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Common.PrettyPrint
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport qualified Common.Result as Res
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Common.GlobalAnnotations
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Driver.Options
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Driver.WriteFn
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maederimport Driver.ReadFn
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Data.Graph.Inductive.Graph as Graph
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maederimport Data.IORef
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Data.Maybe
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport List(nub)
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maederimport Control.Monad
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- Maps used to track which node resp edge of the abstract graph
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedercorrespondes with which of the development graph and vice versa and
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederone Map to store which libname belongs to which development graph-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maederdata ConversionMaps = ConversionMaps {
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder dg2abstrNode :: DGraphToAGraphNode,
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder dg2abstrEdge :: DGraphToAGraphEdge,
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder abstr2dgNode :: AGraphToDGraphNode,
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder abstr2dgEdge :: AGraphToDGraphEdge,
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder libname2dg :: LibEnv}
2f65d931e866162d39d09c43021a55314040b377Christian Maeder deriving Show
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederinstance PrettyPrint String where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder printText0 ga c = ptext (take 25 c)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederinstance Common.PrettyPrint.PrettyPrint ConversionMaps where
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder printText0 ga convMaps =
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder ptext "dg2abstrNode"
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Pretty.$$ (printText0 ga $ dg2abstrNode convMaps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Pretty.$$ ptext "dg2abstrEdge"
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Pretty.$$ (printText0 ga $ dg2abstrEdge convMaps)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Pretty.$$ ptext "abstr2dgNode"
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Pretty.$$ (printText0 ga $ abstr2dgNode convMaps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Pretty.$$ ptext "abstr2dgEdge"
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Pretty.$$ (printText0 ga $ abstr2dgEdge convMaps)
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maederdata GraphMem = GraphMem {
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder graphInfo :: GraphInfo,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder nextGraphId :: Descr}
81eaac399d69af15425d06b054e5d0331dbc132bChristian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- types of the Maps above
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype DGraphToAGraphNode = Map.Map (LIB_NAME,Node) Descr
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedertype DGraphToAGraphEdge = Map.Map (LIB_NAME,(Descr,Descr,String)) Descr
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinitype AGraphToDGraphNode = Map.Map Descr (LIB_NAME,Node)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype AGraphToDGraphEdge = Map.Map Descr (LIB_NAME,(Descr,Descr,String))
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maederdata InternalNames =
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder InternalNames { showNames :: Bool,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder updater :: [(String,(String -> String) -> IO ())] }
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype GInfo = (IORef ProofStatus,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder IORef Descr,
f1082bc15d1cbd06522cf49842929d73ba4214fcChristian Maeder IORef ConversionMaps,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Descr,
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder LIB_NAME,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder GraphInfo,
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder IORef InternalNames, -- show internal names?
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder HetcatsOpts,
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder IORef [[Node]]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder )
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederinitializeConverter :: IO (IORef GraphMem)
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederinitializeConverter =
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder do HTk.initHTk [HTk.withdrawMainWin]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder showLogicGraph daVinciSort
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder initGraphInfo <- initgraphs
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder graphMem <- (newIORef GraphMem{nextGraphId = 0,
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder graphInfo = initGraphInfo})
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder return graphMem
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder{- converts the development graph given by its libname into an abstract graph
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torriniand returns the descriptor of the latter, the graphInfo it is contained in
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torriniand the conversion maps (see above)-}
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconvertGraph :: IORef GraphMem -> LIB_NAME -> LibEnv -> HetcatsOpts
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -> IO (Descr, GraphInfo, ConversionMaps)
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederconvertGraph graphMem libname libEnv hetsOpts =
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder do let convMaps = ConversionMaps
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder {dg2abstrNode = Map.empty::DGraphToAGraphNode,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder abstr2dgNode = Map.empty::AGraphToDGraphNode,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder dg2abstrEdge = Map.empty::DGraphToAGraphEdge,
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder abstr2dgEdge = Map.empty::AGraphToDGraphEdge,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder libname2dg = libEnv}
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder case Map.lookup libname libEnv of
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just globContext@(_,_,dgraph) ->
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder do (abstractGraph,graphInfo,convRef) <-
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder initializeGraph graphMem libname dgraph convMaps globContext hetsOpts
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder if (isEmpty dgraph) then
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder return (abstractGraph, graphInfo,convMaps)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder else
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder do newConvMaps <- convertNodes convMaps abstractGraph
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder graphInfo dgraph libname
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder finalConvMaps <- convertEdges newConvMaps abstractGraph
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder graphInfo dgraph libname
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder writeIORef convRef finalConvMaps
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (abstractGraph, graphInfo, finalConvMaps)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Nothing -> error ("development graph with libname "
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ++ (show libname)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder ++ " does not exist")
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder{- initializes an empty abstract graph with the needed node and edge types,
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederreturn type equals the one of convertGraph -}
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederinitializeGraph :: IORef GraphMem ->LIB_NAME -> DGraph -> ConversionMaps
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -> GlobalContext -> HetcatsOpts
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -> IO (Descr,GraphInfo,IORef ConversionMaps)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederinitializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder graphMem <- readIORef ioRefGraphMem
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder event <- newIORef 0
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder convRef <- newIORef convMaps
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder showInternalNames <- newIORef (InternalNames False [])
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let proofHistory = Map.fromList [(key,[([]::[DGRule], []::[DGChange])])|
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder key <- Map.keys (libname2dg convMaps)]
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ioRefProofStatus <- newIORef (ln, libname2dg convMaps,proofHistory)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ioRefSubtreeEvents <- newIORef (Map.empty::(Map.Map Descr Descr))
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ioRefVisibleNodes <- newIORef [(Graph.nodes dGraph)]
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let gid = nextGraphId graphMem
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder actGraphInfo = graphInfo graphMem
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder let gInfo = (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, showInternalNames, hetsOpts, ioRefVisibleNodes)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder Result descr _ <-
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder makegraph ("Development graph for "++show ln)
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder -- action on "open"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (do currentPath <- getCurrentDirectory
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder event <- fileDialogStr "Open..." currentPath
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder maybeFilePath <- sync event
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder case maybeFilePath of
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder Just filePath ->
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder do openProofStatus filePath ioRefProofStatus convRef hetsOpts
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder Nothing ->
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini do error ("Could not open file.")
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini )
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini -- action on "save"
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini (do proofStatus <- readIORef ioRefProofStatus
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini writeShATermFile ("./" ++ (show ln) ++ ".log") proofStatus)
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini -- action on "save as...:"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (do currentPath <- getCurrentDirectory
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder event <- newFileDialogStr "Save as..." currentPath
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder maybeFilePath <- sync event
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder case maybeFilePath of
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder Just filePath -> do
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder proofStatus <- readIORef ioRefProofStatus
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder writeShATermFile filePath proofStatus
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder Nothing ->
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder do error ("Could not save file.")
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder )
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder -- the global menu
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder [GlobalMenu (Menu Nothing
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini [Menu (Just "Unnamed nodes")
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini [Button "Hide/show names"
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini (do (int::InternalNames) <- readIORef showInternalNames
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini let showThem = not $ showNames int
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini showIt s = if showThem then s else ""
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini mapM_ (\(s,upd) -> upd (\_ -> showIt s)) (updater int)
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder writeIORef showInternalNames (int {showNames = showThem})
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder redisplay gid actGraphInfo
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder return () ),
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder Button "Hide nodes"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder (do Result descr _ <- hideSetOfNodeTypes gid
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder ["internal",
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder "locallyEmpty_internal"]
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder actGraphInfo
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder writeIORef event descr
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder redisplay gid actGraphInfo
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder return () ),
81eaac399d69af15425d06b054e5d0331dbc132bChristian Maeder
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder Button "Show nodes"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (do descr <- readIORef event
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder showIt gid descr actGraphInfo
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder redisplay gid actGraphInfo
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder return () )],
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder Menu (Just "Proofs")
613bf0ed7d98a961755408ead328687ec17f74fdChristian Maeder [Button "Automatic"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (proofMenu gInfo (fmap return . automatic)),
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Button "Global Subsumption"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder (proofMenu gInfo (fmap return . globSubsume)),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Button "Global Decomposition"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (proofMenu gInfo (fmap return . globDecomp)),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Button "Local Subsumption"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (proofMenu gInfo (fmap return . locSubsume)),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Button "Local Decomposition (merge of rules)"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (proofMenu gInfo (fmap return . locDecomp)),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Button "Hide Theorem Shift"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (proofMenu gInfo (fmap return .
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (hideTheoremShift False))),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Button "Theorem Hide Shift"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (proofMenu gInfo (fmap return . theoremHideShift))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ]])]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- the node types
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder [("spec",
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder createLocalMenuNodeTypeSpec "Magenta" ioRefSubtreeEvents
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder actGraphInfo ioRefGraphMem gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("locallyEmpty_spec",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder createLocalMenuNodeTypeSpec "Violet" ioRefSubtreeEvents
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder actGraphInfo ioRefGraphMem gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("internal",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder createLocalMenuNodeTypeInternal "Grey" gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("locallyEmpty_internal",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder createLocalMenuNodeTypeInternal "LightGrey" gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("dg_ref",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder createLocalMenuNodeTypeDgRef "SteelBlue" actGraphInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ioRefGraphMem graphMem gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("locallyEmpty_dg_ref",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder createLocalMenuNodeTypeDgRef "LightSteelBlue"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder actGraphInfo ioRefGraphMem graphMem gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ) ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- the link types (share strings to avoid typos)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [("globaldef",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenu gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("def",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Steelblue"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenu gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hidingdef",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Lightblue"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenu gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder GraphConfigure.Double
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenu gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Green"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalMenuValueTitleShowConservativity
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unproventhm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Red"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalMenuValueTitleShowConservativity
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localproventhm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Dashed $$$ Color "Green"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalMenuValueTitleShowConservativity
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Dashed $$$ Color "Red"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalMenuValueTitleShowConservativity
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unprovenhidingthm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Orange"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("provenhidingthm",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Solid $$$ Color "Lightgreen"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenuThmEdge gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -- > ######### welche Farbe fuer reference ##########
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("reference",
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Dotted $$$ Color "Grey"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ createLocalEdgeMenu gInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue)]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [("globaldef","globaldef","globaldef"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("globaldef","def","def"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("globaldef","hetdef","hetdef"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("globaldef","proventhm","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("globaldef","unproventhm","unproventhm"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("globaldef","localunproventhm","localunproventhm"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("def","globaldef","def"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("def","def","def"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("def","hetdef","hetdef"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("def","proventhm","proventhm"),
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder ("def","unproventhm","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("def","localunproventhm","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","globaldef","hetdef"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","def","hetdef"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","hetdef","hetdef"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","proventhm","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","unproventhm","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("hetdef","localunproventhm","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm","globaldef","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm","def","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm","hetdef","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm","proventhm","proventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("proventhm","unproventhm","unproventhm"),
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder ("proventhm","localunproventhm","localunproventhm"),
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder ("unproventhm","globaldef","unproventhm"),
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder ("unproventhm","def","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unproventhm","hetdef","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unproventhm","proventhm","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unproventhm","unproventhm","unproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("unproventhm","localunproventhm","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","globaldef","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","def","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","hetdef","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","proventhm","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","unproventhm","localunproventhm"),
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ("localunproventhm","localunproventhm","localunproventhm")]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder actGraphInfo
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder writeIORef ioRefGraphMem graphMem{nextGraphId = gid+1}
e96fb97935ac710a295b04d60b8ac90ef8364079Christian Maeder graphMem'<- readIORef ioRefGraphMem
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (descr,graphInfo graphMem',convRef)
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederopenProofStatus :: FilePath -> (IORef ProofStatus) -> (IORef ConversionMaps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -> HetcatsOpts -> IO()
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederopenProofStatus filename ioRefProofStatus convRef hetsOpts =
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder do resultProofStatus <- proofStatusFromShATerm filename
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder case Res.maybeResult resultProofStatus of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Nothing -> error ("Could not read proof status from file '"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ (show filename) ++ "'")
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just proofStatus@(ln,libEnv',_) ->
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder do writeIORef ioRefProofStatus proofStatus
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder initGraphInfo <- initgraphs
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder graphMem' <- (newIORef GraphMem{nextGraphId = 0,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder graphInfo = initGraphInfo})
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (gid, actGraphInfo, convMaps)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder <- convertGraph graphMem' ln libEnv' hetsOpts
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder writeIORef convRef convMaps
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder redisplay gid actGraphInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return ()
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederproofMenu :: GInfo
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -> (ProofStatus -> IO (Res.Result ProofStatus))
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder -> IO ()
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederproofMenu (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, _, _, ioRefVisibleNodes) proofFun
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder = do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder proofStatus <- readIORef ioRefProofStatus
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Res.Result diags res <- proofFun proofStatus
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder case res of
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder Nothing -> do sequence $ map (putStrLn . show) diags
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return ()
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder Just newProofStatus@(ln,libEnv,proofHistory) -> do
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder let (Just history) = Map.lookup ln proofHistory
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Just newGlobContext) = Map.lookup ln libEnv
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder writeIORef ioRefProofStatus newProofStatus
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder descr <- readIORef event
convMaps <- readIORef convRef
(newDescr,convMapsAux)
<- applyChanges gid ln actGraphInfo descr ioRefVisibleNodes
convMaps history
let newConvMaps =
convMapsAux {libname2dg =
Map.insert ln newGlobContext (libname2dg convMapsAux)}
writeIORef event newDescr
writeIORef convRef newConvMaps
redisplay gid actGraphInfo
return ()
proofMenuSef :: GInfo
-> (ProofStatus -> ProofStatus)
-> IO ()
proofMenuSef gInfo proofFun =
proofMenu gInfo (return . return . proofFun)
-- -------------------------------------------------------------
-- methods to create the local menus of the different nodetypes
-- -------------------------------------------------------------
-- local menu for the nodetypes spec and locallyEmpty_spec
createLocalMenuNodeTypeSpec color ioRefSubtreeEvents actGraphInfo
ioRefGraphMem gInfo@(_,_,convRef,_,_,_,_,_,ioRefVisibleNodes) =
Ellipse $$$ Color color
$$$ ValueTitle (\ (s,_,_) -> return s)
$$$ LocalMenu (Menu (Just "node menu")
[createLocalMenuButtonShowSpec gInfo,
createLocalMenuButtonShowNumberOfNode,
createLocalMenuButtonShowSignature gInfo,
createLocalMenuButtonShowTheory gInfo,
createLocalMenuButtonTranslateTheory gInfo,
createLocalMenuTaxonomy gInfo,
createLocalMenuButtonShowSublogic gInfo,
createLocalMenuButtonShowNodeOrigin gInfo,
createLocalMenuButtonProveAtNode gInfo,
createLocalMenuButtonCCCAtNode gInfo,
createLocalMenuButtonShowJustSubtree ioRefSubtreeEvents
convRef ioRefVisibleNodes ioRefGraphMem
actGraphInfo,
createLocalMenuButtonUndoShowJustSubtree ioRefVisibleNodes
ioRefSubtreeEvents actGraphInfo
]) -- ??? Should be globalized somehow
-- >$$$ LocalMenu (Button "xxx" undefined)
$$$ emptyNodeTypeParms
:: DaVinciNodeTypeParms (String,Int,Int)
-- local menu for the nodetypes internal and locallyEmpty_internal
createLocalMenuNodeTypeInternal color
gInfo@(_,_,convRef,_,_,_,showInternalNames,_,_) =
Ellipse $$$ Color color
$$$ ValueTitleSource (\ (s,_,_) -> do
b <- newSimpleBroadcaster ""
int <- readIORef showInternalNames
let upd = (s,applySimpleUpdate b)
writeIORef showInternalNames (int {updater = upd:updater int})
return $ toSimpleSource b)
$$$ LocalMenu (Menu (Just "node menu")
[createLocalMenuButtonShowSpec gInfo,
createLocalMenuButtonShowNumberOfNode,
createLocalMenuButtonShowSignature gInfo,
createLocalMenuButtonShowTheory gInfo,
createLocalMenuButtonTranslateTheory gInfo,
createLocalMenuTaxonomy gInfo,
createLocalMenuButtonShowSublogic gInfo,
createLocalMenuButtonProveAtNode gInfo,
createLocalMenuButtonCCCAtNode gInfo,
createLocalMenuButtonShowNodeOrigin gInfo])
$$$ emptyNodeTypeParms
:: DaVinciNodeTypeParms (String,Int,Int)
-- local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
createLocalMenuNodeTypeDgRef color actGraphInfo
ioRefGraphMem graphMem (_,_,convRef,_,_,_,_,hetsOpts,_) =
Box $$$ Color color
$$$ ValueTitle (\ (s,_,_) -> return s)
$$$ LocalMenu (Button "Show referenced library"
(\ (name,descr,gid) ->
do convMaps <- readIORef convRef
(refDescr, newGraphInfo, refConvMaps) <-
showReferencedLibrary ioRefGraphMem descr
gid
actGraphInfo
convMaps
hetsOpts
--writeIORef convRef newConvMaps
writeIORef ioRefGraphMem
graphMem{graphInfo = newGraphInfo,
nextGraphId = refDescr +1}
redisplay refDescr newGraphInfo
return ()
))
$$$ emptyNodeTypeParms
:: DaVinciNodeTypeParms (String,Int,Int)
-- menu button for local menus
createMenuButton title menuFun (ioProofStatus,_,convRef,_,_,_,_,_,_) =
(Button title
(\ (name,descr,gid) ->
do convMaps <- readIORef convRef
(ln,libEnv,_) <- readIORef ioProofStatus
let (Just (_,_,dGraph)) = Map.lookup ln libEnv
menuFun descr
(abstr2dgNode convMaps)
dGraph
return ()
)
)
createLocalMenuButtonShowSpec = createMenuButton "Show spec" showSpec
createLocalMenuButtonShowSignature =
createMenuButton "Show signature" getSignatureOfNode
createLocalMenuButtonShowTheory gInfo =
createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo
createLocalMenuButtonTranslateTheory gInfo =
createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo
{- |
create a sub Menu for taxonomy visualisation
(added by KL)
-}
--createLocalMenuTaxonomy :: IORef ProofStatus -> Descr -> AGraphToDGraphNode ->
-- DGraph -> IO ()
createLocalMenuTaxonomy ginfo@(proofStatus,_,_,_,_,_,_,_,_) =
(Menu (Just "Taxonomy graphs")
[createMenuButton "Subsort graph"
(passTh displaySubsortGraph) ginfo,
createMenuButton "Concept graph"
(passTh displayConceptGraph) ginfo])
where passTh displayFun descr ab2dgNode dgraph =
do r <- lookupTheoryOfNode proofStatus
descr ab2dgNode dgraph
case r of
Res.Result [] (Just (n, gth)) ->
displayFun (showPretty n "") gth
Res.Result diags _ ->
showDiags defaultHetcatsOpts diags
createLocalMenuButtonShowSublogic gInfo@(proofStatus,_,_,_,_,_,_,_,_) =
createMenuButton "Show sublogic" (getSublogicOfNode proofStatus) gInfo
createLocalMenuButtonShowNodeOrigin =
createMenuButton "Show origin" showOriginOfNode
createLocalMenuButtonProveAtNode gInfo =
createMenuButton "Prove" (proveAtNode False gInfo) gInfo
createLocalMenuButtonCCCAtNode gInfo =
createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo
createLocalMenuButtonShowJustSubtree ioRefSubtreeEvents convRef
ioRefVisibleNodes ioRefGraphMem actGraphInfo =
(Button "Show just subtree"
(\ (name,descr,gid) ->
do subtreeEvents <- readIORef ioRefSubtreeEvents
case Map.lookup descr subtreeEvents of
Just _ -> putStrLn
("it is already just the subtree of node "
++ (show descr) ++" shown")
Nothing ->
do convMaps <- readIORef convRef
visibleNodes <- readIORef ioRefVisibleNodes
(eventDescr,newVisibleNodes,errorMsg) <-
showJustSubtree ioRefGraphMem
descr gid convMaps visibleNodes
case errorMsg of
Nothing -> do let newSubtreeEvents =
Map.insert descr
eventDescr
subtreeEvents
writeIORef ioRefSubtreeEvents
newSubtreeEvents
writeIORef ioRefVisibleNodes
newVisibleNodes
redisplay gid actGraphInfo
return()
Just text -> do putStrLn text
return()
)
)
createLocalMenuButtonUndoShowJustSubtree ioRefVisibleNodes
ioRefSubtreeEvents actGraphInfo =
(Button "Undo show just subtree"
(\ (name,descr,gid) ->
do visibleNodes <- readIORef ioRefVisibleNodes
case (tail visibleNodes) of
[] -> do putStrLn
"Complete graph is already shown"
return()
newVisibleNodes@(x:xs) ->
do subtreeEvents <- readIORef ioRefSubtreeEvents
case Map.lookup descr subtreeEvents of
Just hide_event ->
do showIt gid hide_event actGraphInfo
writeIORef ioRefSubtreeEvents
(Map.delete descr subtreeEvents)
writeIORef ioRefVisibleNodes
newVisibleNodes
redisplay gid actGraphInfo
return ()
Nothing -> do putStrLn "undo not possible"
return()
)
)
-- for debugging
createLocalMenuButtonShowNumberOfNode =
(Button "Show number of node"
(\ (name, descr, gid) ->
getNumberOfNode descr))
-- -------------------------------------------------------------
-- methods to create the local menus for the edges
-- -------------------------------------------------------------
createLocalEdgeMenu gInfo =
LocalMenu (Menu (Just "edge menu")
[createLocalMenuButtonShowMorphismOfEdge gInfo,
createLocalMenuButtonShowOriginOfEdge gInfo,
createLocalMenuButtonCheckconsistencyOfEdge gInfo]
)
createLocalEdgeMenuThmEdge gInfo =
LocalMenu (Menu (Just "thm egde menu")
[createLocalMenuButtonShowMorphismOfEdge gInfo,
createLocalMenuButtonShowOriginOfEdge gInfo,
createLocalMenuButtonShowProofStatusOfThm gInfo,
createLocalMenuButtonCheckconsistencyOfEdge gInfo]
)
createLocalMenuButtonShowMorphismOfEdge _ =
(Button "Show morphism"
(\ (_,descr,maybeLEdge) ->
do showMorphismOfEdge descr maybeLEdge
return ()
))
createLocalMenuButtonShowOriginOfEdge _ =
(Button "Show origin"
(\ (_,descr,maybeLEdge) ->
do showOriginOfEdge descr maybeLEdge
return ()
))
createLocalMenuButtonCheckconsistencyOfEdge gInfo =
(Button "Check conservativity (preliminary)"
(\ (ginfo,descr,maybeLEdge) ->
do checkconsistencyOfEdge descr gInfo maybeLEdge
return ()
))
createLocalMenuButtonShowProofStatusOfThm _ =
(Button "Show proof status"
(\ (_,descr,maybeLEdge) ->
do showProofStatusOfThm descr maybeLEdge
return ()
))
createLocalMenuValueTitleShowConservativity =
(ValueTitle
(\ (_,_,maybeLEdge) ->
case maybeLEdge of
Just (_,_,edgelab) ->
case dgl_type edgelab of
GlobalThm _ c status -> return (showCons c status)
LocalThm _ c status -> return (showCons c status)
_ -> return ""
Nothing -> return ""
))
where
showCons :: Conservativity -> ThmLinkStatus -> String
showCons c status =
case (c,status) of
(None,_) -> show c
(_,Open) -> (show c) ++ "?"
_ -> show c
-- ------------------------------
-- end of local menu definitions
-- ------------------------------
showSpec descr convMap dgraph =
case Map.lookup descr convMap of
Nothing -> return ()
Just (libname,node) -> do
let sp = dgToSpec dgraph node
putStrLn (showPretty sp "")
{- auxiliary method for debugging. shows the number of the given node in the abstraction graph -}
getNumberOfNode :: Descr -> IO()
getNumberOfNode descr =
let title = "Number of node"
in createTextDisplay title (showPretty descr "") [size(10,10)]
{- outputs the signature of a node in a window;
used by the node menu defined in initializeGraph-}
getSignatureOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()
getSignatureOfNode descr ab2dgNode dgraph =
case Map.lookup descr ab2dgNode of
Just (libname, node) ->
do let dgnode = lab' (context dgraph node)
case dgnode of
(DGNode name (G_sign _ sig) _ _ _ _) ->
let title = "Signature of "++showName name
in createTextDisplay title (showPretty sig "") [size(80,50)]
(DGRef _ _ _ _ _) -> error
"nodes of type dg_ref do not have a signature"
Nothing -> error ("node with descriptor "
++ (show descr)
++ " has no corresponding node in the development graph")
{- |
fetches the theory from a node inside the IO Monad
(added by KL based on code in getTheoryOfNode) -}
lookupTheoryOfNode :: IORef ProofStatus -> Descr -> AGraphToDGraphNode ->
DGraph -> IO (Res.Result (Node,G_theory))
lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph = do
(ln,libEnv,_) <- readIORef proofStatusRef
case (do
(_libname, node) <-
Res.maybeToResult nullPos ("Node "++show descr++" not found")
$ Map.lookup descr ab2dgNode
gth <- computeTheory libEnv _libname dgraph node
return (node, gth)
) of
r -> return r
{- outputs the theory of a node in a window;
used by the node menu defined in initializeGraph-}
getTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode ->
DGraph -> IO()
getTheoryOfNode (proofStatusRef,_,_,_,_,_,_,hetsOpts,_) descr ab2dgNode dgraph = do
r <- lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph
case r of
Res.Result diags res -> do
showDiags hetsOpts diags
case res of
(Just (n, gth)) -> displayTheory "Theory" n dgraph gth
_ -> return ()
printTheory :: G_theory -> String
printTheory (G_theory lid sign sens) =
let shownsens = concatMap ((flip shows "\n\n") .
print_named lid emptyGlobalAnnos) sens
in showPretty sign "\n\n\n" ++ shownsens
displayTheory :: String -> Node -> DGraph -> G_theory
-> IO ()
displayTheory ext node dgraph gth =
let dgnode = lab' (context dgraph node)
str = printTheory (simplifyTh gth) in case dgnode of
(DGNode name (G_sign _ _) _ _ _ _) ->
let thname = showName name
title = ext ++ " of " ++ thname
in createTextSaveDisplay title (thname++".het") str
(DGRef _ _ _ _ _) -> error
"nodes of type dg_ref do not have a theory"
{- translate the theory of a node in a window;
used by the node menu defined in initializeGraph-}
translateTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode ->
DGraph -> IO()
translateTheoryOfNode gInfo@(proofStatusRef,_,_,_,_,_,_,opts,_) descr ab2dgNode dgraph = do
(_,libEnv,_) <- readIORef proofStatusRef
case (do
(_libname, node) <-
Res.maybeToResult nullPos ("Node "++show descr++" not found")
$ Map.lookup descr ab2dgNode
th <- computeTheory libEnv _libname dgraph node
return (node,th) ) of
Res.Result [] (Just (node,th)) -> do
Res.Result diags _ <- Res.ioresToIO(
do G_theory lid sign sens <- return th
-- find all comorphism paths starting from lid
let paths = findComorphismPaths logicGraph (sublogicOfTh th)
-- let the user choose one
sel <- Res.ioToIORes $ listBox "Choose a logic translation"
(map show paths)
i <- case sel of
Just j -> return j
_ -> Res.resToIORes $ Res.fatal_error "" nullPos
Comorphism cid <- return (paths!!i)
-- adjust lid's
let lidS = sourceLogic cid
lidT = targetLogic cid
sign' <- coerce lidS lid sign
sens' <- coerce lidS lid sens
-- translate theory along chosen comorphism
(sign'',sens1) <-
Res.resToIORes $ map_theory cid (sign',sens')
Res.ioToIORes $ displayTheory "Translated theory" node dgraph
(G_theory lidT sign'' sens1)
)
showDiags opts diags
return ()
Res.Result diags _ -> showDiags opts diags
{- outputs the sublogic of a node in a window;
used by the node menu defined in initializeGraph-}
getSublogicOfNode :: IORef ProofStatus -> Descr -> AGraphToDGraphNode -> DGraph -> IO()
getSublogicOfNode proofStatusRef descr ab2dgNode dgraph = do
(_,libEnv,_) <- readIORef proofStatusRef
case Map.lookup descr ab2dgNode of
Just (libname, node) ->
let dgnode = lab' (context dgraph node)
name = case dgnode of
(DGNode name _ _ _ _ _) -> name
_ -> emptyName
in case computeTheory libEnv libname dgraph node of
Res.Result _ (Just th) ->
let logstr = show $ sublogicOfTh th
title = "Sublogic of "++showName name
in createTextDisplay title logstr [size(30,10)]
Res.Result diags _ ->
error ("Could not compute theory for sublogic computation: "++
concatMap show diags)
Nothing -> error ("node with descriptor "
++ (show descr)
++ " has no corresponding node in the development graph")
{- prints the origin of the node -}
showOriginOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()
showOriginOfNode descr ab2dgNode dgraph =
case Map.lookup descr ab2dgNode of
Just (libname, node) ->
do let dgnode = lab' (context dgraph node)
case dgnode of
DGNode name _ _ _ _ orig ->
let title = "Origin of node "++showName name
in createTextDisplay title
(showPretty orig "") [size(30,10)]
DGRef _ _ _ _ _ -> error "showOriginOfNode: no DGNode"
Nothing -> error ("node with descriptor "
++ (show descr)
++ " has no corresponding node in the development graph")
{- start local theorem proving or consistency checking at a node -}
--proveAtNode :: Bool -> Descr -> AGraphToDGraphNode -> DGraph -> IO()
proveAtNode checkCons gInfo@(_,_,convRef,_,_,_,_,_,_) descr ab2dgNode dgraph =
case Map.lookup descr ab2dgNode of
Just libNode ->
do convMaps <- readIORef convRef
proofMenu gInfo (basicInferenceNode checkCons logicGraph libNode)
Nothing -> error ("node with descriptor "
++ (show descr)
++ " has no corresponding node in the development graph")
{- prints the morphism of the edge -}
showMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showMorphismOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Signature morphism"
((showPretty (dgl_morphism linklab) "")++hidingMorph) [size(150,50)]
where
hidingMorph = case (dgl_type linklab) of
(HidingThm morph _) -> "\n ++++++ \n"
++ (showPretty morph "")
_ -> ""
showMorphismOfEdge descr Nothing =
createTextDisplay "Error"
("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph") [size(30,10)]
{- prints the origin of the edge -}
showOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showOriginOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Origin of link"
(showPretty (dgl_origin linklab) "") [size(30,10)]
showOriginOfEdge descr Nothing =
createTextDisplay "Error"
("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph") [size(30,10)]
{- prints the proof base of the edge -}
showProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showProofStatusOfThm _ (Just ledge) =
createTextDisplay "Proof Status"
(show (getProofStatusOfThm ledge)) [size(30,10)]
showProofStatusOfThm descr Nothing =
putStrLn ("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph")
{- check consistency of the edge -}
checkconsistencyOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
checkconsistencyOfEdge _ (ref,_,_,_,_,_,_,opts,_)
(Just (source,target,linklab)) = do
(ln,libEnv,_) <- readIORef ref
let (_,_,dgraph) = maybe (error "checkconsistencyOfEdge") id
$ Map.lookup ln libEnv
dgtar = lab' (context dgraph target)
case dgtar of
DGNode name _ (G_l_sentence_list lid sens) _ _ _ ->
case dgl_morphism linklab of
GMorphism cid sign1 morphism2 -> do
let morphism2' = case coerce (targetLogic cid) lid morphism2 of
Just m -> m
_ -> error "checkconsistencyOfEdge: wrong logic"
let th = case computeTheory libEnv ln dgraph source of
Res.Result _ (Just th1) -> th1
_ -> error "checkconsistencyOfEdge: computeTheory"
G_theory lid1 sign1 sens1 <- return th
case coerce lid1 lid (sign1,sens1) of
Just (sign2, sens2) ->
let Res.Result diags res =
consCheck lid (sign2,sens2) morphism2' sens
showRes = case res of
Just(Just True) -> "The link is conservative"
Just(Just False) -> "The link is not conservative"
_ -> "Could not determine whether link is conservative"
showDiags = unlines (map show diags)
in createTextDisplay "Result of consistency check"
(showRes++"\n"++showDiags) [size(50,50)]
_ -> error "checkconsistencyOfEdge: wrong logic"
DGRef _ _ _ _ _ -> error "checkconsistencyOfEdge: no DGNode"
checkconsistencyOfEdge descr _ Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge "
++ "in the development graph") [size(30,10)]
getProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus
getProofStatusOfThm (_,_,label) =
case (dgl_type label) of
(LocalThm proofStatus _ _) -> proofStatus
(GlobalThm proofStatus _ _) -> proofStatus
(HidingThm _ proofStatus) -> proofStatus -- richtig?
-- (FreeThm GMorphism Bool) - keinen proofStatus?
_ -> error "the given edge is not a theorem"
{- converts the nodes of the development graph, if it has any,
and returns the resulting conversion maps
if the graph is empty the conversion maps are returned unchanged-}
convertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertNodes convMaps descr graphInfo dgraph libname
| isEmpty dgraph = do return convMaps
| otherwise = convertNodesAux convMaps
descr
graphInfo
(labNodes dgraph)
libname
{- auxiliar function for convertNodes if the given list of nodes is
emtpy, it returns the conversion maps unchanged otherwise it adds the
converted first node to the abstract graph and to the affected
conversion maps and afterwards calls itself with the remaining node
list -}
convertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps
convertNodesAux convMaps descr graphInfo [] libname = return convMaps
convertNodesAux convMaps descr graphInfo ((node,dgnode):lNodes) libname =
do let nodetype = getDGNodeType dgnode
Result newDescr err <- addnode descr
nodetype
(getDGNodeName dgnode)
graphInfo
convertNodesAux convMaps {dg2abstrNode = Map.insert (libname, node)
newDescr (dg2abstrNode convMaps),
abstr2dgNode = Map.insert newDescr
(libname, node) (abstr2dgNode convMaps)}
descr graphInfo lNodes libname
-- | gets the type of a development graph edge as a string
getDGNodeType :: DGNodeLab -> String
getDGNodeType dgnode =
(if locallyEmpty dgnode then "locallyEmpty_" else "")
++ case isDGRef dgnode of
True -> "dg_ref"
False -> if isInternalNode dgnode
then "internal"
else "spec"
getDGLinkType :: DGLinkLab -> String
getDGLinkType lnk = case dgl_type lnk of
GlobalDef ->
if hasIdComorphism $ dgl_morphism lnk then "globaldef"
else "hetdef"
HidingDef -> "hidingdef"
LocalThm thmLinkStatus _ _ -> "local" ++ getThmType thmLinkStatus ++ "thm"
GlobalThm thmLinkStatus _ _ -> getThmType thmLinkStatus ++ "thm"
HidingThm _ thmLinkStatus -> getThmType thmLinkStatus ++ "hidingthm"
FreeThm _ bool -> if bool then "proventhm" else "unproventhm"
_ -> "def" -- LocalDef, FreeDef, CofreeDef
getThmType :: ThmLinkStatus -> String
getThmType thmLinkStatus =
case thmLinkStatus of
Proven _ _ -> "proven"
Open -> "unproven"
{- converts the edges of the development graph
works the same way as convertNods does-}
convertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertEdges convMaps descr graphInfo dgraph libname
| isEmpty dgraph = do return convMaps
| otherwise = convertEdgesAux convMaps
descr
graphInfo
(labEdges dgraph)
libname
{- auxiliar function for convertEges --> not yet implemented! -}
convertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps
convertEdgesAux convMaps descr graphInfo [] libname = return convMaps
convertEdgesAux convMaps descr graphInfo ((ledge@(src,tar,edgelab)):lEdges)
libname =
do let srcnode = Map.lookup (libname,src) (dg2abstrNode convMaps)
tarnode = Map.lookup (libname,tar) (dg2abstrNode convMaps)
case (srcnode,tarnode) of
(Just s, Just t) -> do
Result newDescr err <- addlink descr (getDGLinkType edgelab)
"" (Just ledge) s t graphInfo
newConvMaps <- (convertEdgesAux
convMaps {dg2abstrEdge = Map.insert
(libname, (src,tar,show edgelab))
newDescr
(dg2abstrEdge convMaps),
abstr2dgEdge = Map.insert newDescr
(libname, (src,tar,show edgelab))
(abstr2dgEdge convMaps)}
descr graphInfo lEdges libname)
return newConvMaps
_ -> error "Cannot find nodes"
showReferencedLibrary :: IORef GraphMem -> Descr -> Descr -> GraphInfo
-> ConversionMaps -> HetcatsOpts -> IO (Descr, GraphInfo, ConversionMaps)
showReferencedLibrary graphMem descr abstractGraph graphInfo convMaps hetsOpts =
case Map.lookup descr (abstr2dgNode convMaps) of
Just (libname,node) ->
case Map.lookup libname libname2dgMap of
Just (_,_,dgraph) ->
do let (_,(DGRef _ refLibname refNode _ _)) =
labNode' (context dgraph node)
case Map.lookup refLibname libname2dgMap of
Just (_,refDgraph,_) ->
convertGraph graphMem refLibname (libname2dg convMaps) hetsOpts
Nothing -> error ("The referenced library ("
++ (show refLibname)
++ ") is unknown")
Nothing ->
error ("Selected node belongs to unknown library: "
++ (show libname))
Nothing ->
error ("there is no node with the descriptor "
++ show descr)
where libname2dgMap = libname2dg convMaps
showJustSubtree:: IORef GraphMem -> Descr -> Descr -> ConversionMaps
-> [[Node]]-> IO (Descr, [[Node]], Maybe String)
showJustSubtree ioRefGraphMem descr abstractGraph convMaps visibleNodes =
case Map.lookup descr (abstr2dgNode convMaps) of
Just (libname,parentNode) ->
case Map.lookup libname libname2dgMap of
Just (_,_,dgraph) ->
do let allNodes = getNodeDescriptors (head visibleNodes)
libname convMaps
dgNodesOfSubtree = nub (parentNode:(getNodesOfSubtree dgraph
(head visibleNodes) parentNode))
-- the selected node (parentNode) shall not be hidden either,
-- and we already know its descriptor (descr)
nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree
libname convMaps
nodesToHide = filter (notElemR nodesOfSubtree) allNodes
graphMem <- readIORef ioRefGraphMem
(Result eventDescr errorMsg) <- hidenodes abstractGraph
nodesToHide (graphInfo graphMem)
return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)
{- case errorMsg of
Just text -> return (-1,text)
Nothing -> return (eventDescr,
return convMaps-}
Nothing -> error
("showJustSubtree: Selected node belongs to unknown library: "
++ (show libname))
Nothing ->
error ("showJustSubtree: there is no node with the descriptor "
++ show descr)
where libname2dgMap = libname2dg convMaps
getNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]
getNodeDescriptors [] _ _ = []
getNodeDescriptors (node:nodelist) libname convMaps =
case Map.lookup (libname,node) (dg2abstrNode convMaps) of
Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)
Nothing -> error ("getNodeDescriptors: There is no descriptor for dgnode "
++ (show node))
getNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]
getNodesOfSubtree dgraph visibleNodes node =
(concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode))
++predOfNode
where predOfNode =
[n| n <- (pre dgraph node), elem n visibleNodes]
remainingVisibleNodes = [n| n <- visibleNodes, notElem n predOfNode]
elemR :: Eq a => [a] -> a -> Bool
elemR list element = elem element list
notElemR :: Eq a => [a] -> a -> Bool
notElemR list element = notElem element list
-- -- ################ einbindung von proofs.hs ############
applyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]
-> ConversionMaps
-> [([DGRule],[DGChange])]
-> IO (Descr, ConversionMaps)
applyChanges gid libname graphInfo eventDescr ioRefVisibleNodes
convMaps history =
case history of
[] -> return (eventDescr, convMaps)
(historyElem:list) ->
case snd historyElem of
[] -> return (eventDescr, convMaps)
changes@(x:xs) -> do
visibleNodes <- readIORef ioRefVisibleNodes
(newVisibleNodes, newEventDescr, newConvMaps) <-
applyChangesAux gid libname graphInfo visibleNodes
eventDescr convMaps changes
writeIORef ioRefVisibleNodes newVisibleNodes
return (newEventDescr, newConvMaps)
applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr
-> ConversionMaps -> [DGChange]
-> IO ([[Node]], Descr, ConversionMaps)
applyChangesAux _ _ _ visibleNodes eventDescr convMaps [] =
return (visibleNodes, eventDescr+1, convMaps)
applyChangesAux gid libname graphInfo visibleNodes eventDescr
convMaps (change:changes) =
case change of
InsertNode lnode@(node,nodelab) -> do
let nodetype = getDGNodeType nodelab
nodename = getDGNodeName nodelab
(Result descr err) <-
addnode gid nodetype nodename graphInfo
case err of
Nothing ->
do let dgNode = (libname,node)
newVisibleNodes = map (insertElem node) visibleNodes
newConvMaps =
convMaps {dg2abstrNode =
Map.insert dgNode descr (dg2abstrNode convMaps),
abstr2dgNode =
Map.insert descr dgNode (abstr2dgNode convMaps)}
applyChangesAux gid libname graphInfo newVisibleNodes (descr+1)
newConvMaps changes
Just msg ->
error ("applyChangesAux: could not add node " ++ (show node)
++" with name " ++ (show (nodename)) ++ "\n"
++ msg)
DeleteNode lnode@(node,nodelab) -> do
let nodename = getDGNodeName nodelab
dgnode = (libname,node)
case Map.lookup dgnode (dg2abstrNode convMaps) of
Just abstrNode -> do
(Result descr err) <- delnode gid abstrNode graphInfo
case err of
Nothing -> do
let newVisibleNodes = map (removeElem node) visibleNodes
newConvMaps =
convMaps {dg2abstrNode =
Map.delete dgnode (dg2abstrNode convMaps),
abstr2dgNode =
Map.delete abstrNode (abstr2dgNode convMaps)}
applyChangesAux gid libname graphInfo newVisibleNodes (descr+1)
newConvMaps changes
Just msg -> error ("applyChangesAux: could not delete node "
++ (show node) ++ " with name "
++ (show nodename) ++ "\n"
++ msg)
Nothing -> error ("applyChangesAux: could not delte node "
++ (show node) ++ " with name "
++ (show nodename) ++": " ++
"node does not exist in abstraction graph")
InsertEdge ledge@(src,tgt,edgelab) ->
do let dg2abstrNodeMap = dg2abstrNode convMaps
case (Map.lookup (libname,src) dg2abstrNodeMap,
Map.lookup (libname,tgt) dg2abstrNodeMap) of
(Just abstrSrc, Just abstrTgt) ->
do let dgEdge = (libname, (src,tgt,show edgelab))
(Result descr err) <-
addlink gid (getDGLinkType edgelab)
"" (Just ledge) abstrSrc abstrTgt graphInfo
case err of
Nothing ->
do let newConvMaps = convMaps
{dg2abstrEdge =
Map.insert dgEdge descr (dg2abstrEdge convMaps),
abstr2dgEdge =
Map.insert descr dgEdge (abstr2dgEdge convMaps)}
applyChangesAux gid libname graphInfo visibleNodes
(descr+1) newConvMaps changes
Just msg ->
error ("applyChangesAux: could not add link from "
++ (show src) ++ " to " ++ (show tgt) ++ ":\n"
++ (show msg))
_ ->
error ("applyChangesAux: could not add link " ++ (show src)
++ " to " ++ (show tgt) ++ ": illigal end nodes")
DeleteEdge (src,tgt,edgelab) ->
do let dgEdge = (libname, (src,tgt,show edgelab))
dg2abstrEdgeMap = dg2abstrEdge convMaps
case Map.lookup dgEdge dg2abstrEdgeMap of
Just abstrEdge ->
do (Result descr err) <- dellink gid abstrEdge graphInfo
case err of
Nothing ->
do let newConvMaps = convMaps
{dg2abstrEdge =
Map.delete dgEdge dg2abstrEdgeMap,
abstr2dgEdge =
Map.delete abstrEdge (abstr2dgEdge
convMaps)}
applyChangesAux gid libname graphInfo visibleNodes
(descr+1) newConvMaps changes
Just msg -> error ("applyChangesAux: could not delete edge "
++ (show abstrEdge) ++ ":\n"
++msg)
Nothing -> error ("applyChangesAux: deleted edge from "
++ (show src) ++ " to " ++ (show tgt)
++ " of type " ++ (show (dgl_type edgelab))
++ " and origin " ++ (show (dgl_origin edgelab))
++ " of development "
++ "graph does not exist in abstraction graph")
removeElem :: Eq a => a -> [a] -> [a]
removeElem element list = [e | e <- list, e /= element]
insertElem :: a -> [a] -> [a]
insertElem element list = element:list