1010N/A{-

1879N/AModule : $Header$

1379N/ACopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2004

1010N/ALicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

1010N/A

1010N/AMaintainer : hets@tzi.de

1010N/AStability : provisional

1010N/APortability : non-portable (imports Logic)

1010N/A

1010N/A Conversion of development graphs from Logic.DevGraph

1010N/A to abstract graphs of the graph display interface

1010N/A

1010N/A todo:

1010N/A hiding of internal nodes:

1010N/A internal nodes that are not between named nodes should be kept

1010N/A display inclusions and inter-logic links in special colour

1010N/A try different graph layout algorithms for daVinci (dot?)

1010N/A close program when all windows are closed

1010N/A-}

1472N/A

1472N/Amodule GUI.ConvertDevToAbstractGraph where

1472N/A

1010N/Aimport Logic.Logic

1010N/Aimport Logic.Comorphism

1010N/Aimport Logic.Grothendieck

1879N/Aimport Comorphisms.LogicGraph

1879N/A

1879N/Aimport Static.DevGraph

1879N/Aimport Static.DGToSpec

1879N/Aimport Proofs.Proofs

1010N/A

1010N/Aimport GUI.AbstractGraphView

1010N/Aimport DaVinciGraph

1010N/Aimport GraphDisp

1010N/Aimport GraphConfigure

1010N/Aimport TextDisplay

1379N/Aimport Configuration

1379N/Aimport qualified HTk

1379N/A

1010N/Aimport qualified Common.Lib.Map as Map hiding (isEmpty)

1010N/Aimport Common.Lib.Graph

1379N/Aimport Common.Id

1379N/Aimport Common.PrettyPrint

1379N/Aimport qualified Common.Lib.Pretty as Pretty

1010N/Aimport Common.AS_Annotation

1010N/Aimport qualified Common.Result as Res

1010N/Aimport Syntax.AS_Library

1010N/Aimport Syntax.Print_HetCASL

1010N/A

1431N/Aimport Data.IORef

1431N/Aimport List(nub)

1010N/A

1010N/A

1010N/A{- Maps used to track which node resp edge of the abstract graph

1010N/Acorrespondes with which of the development graph and vice versa and

1010N/Aone Map to store which libname belongs to which development graph-}

1010N/A

1010N/Adata ConversionMaps = ConversionMaps {

1010N/A dg2abstrNode :: DGraphToAGraphNode,

1010N/A dg2abstrEdge :: DGraphToAGraphEdge,

1010N/A abstr2dgNode :: AGraphToDGraphNode,

1010N/A abstr2dgEdge :: AGraphToDGraphEdge,

1010N/A libname2dg :: LibEnv}

1010N/A

1010N/Adata GraphMem = GraphMem {

1010N/A graphInfo :: GraphInfo,

1010N/A nextGraphId :: Descr}

1010N/A

1010N/A-- types of the Maps above

1010N/Atype DGraphToAGraphNode = Map.Map (LIB_NAME,Node) Descr

1010N/Atype DGraphToAGraphEdge = Map.Map (LIB_NAME,(Descr,Descr,String)) Descr

1010N/Atype AGraphToDGraphNode = Map.Map Descr (LIB_NAME,Node)

1010N/Atype AGraphToDGraphEdge = Map.Map Descr (LIB_NAME,(Descr,Descr,String))

1010N/A

1010N/AinitializeConverter :: IO (IORef GraphMem)

1010N/AinitializeConverter =

1431N/A do HTk.initHTk [HTk.withdrawMainWin]

1431N/A initGraphInfo <- initgraphs

1431N/A graphMem <- (newIORef GraphMem{nextGraphId = 0,

1010N/A graphInfo = initGraphInfo})

1010N/A return graphMem

1010N/A

1010N/A{- converts the development graph given by its libname into an abstract graph

1010N/Aand returns the descriptor of the latter, the graphInfo it is contained in

1010N/Aand the conversion maps (see above)-}

1010N/A

1010N/AconvertGraph :: IORef GraphMem -> LIB_NAME -> LibEnv

1010N/A -> IO (Descr, GraphInfo, ConversionMaps)

1010N/AconvertGraph graphMem libname libEnv =

1010N/A do --nextGraphId <- newIORef 0

1010N/A let convMaps = ConversionMaps

1010N/A {dg2abstrNode = Map.empty::DGraphToAGraphNode,

1010N/A abstr2dgNode = Map.empty::AGraphToDGraphNode,

1010N/A dg2abstrEdge = Map.empty::DGraphToAGraphEdge,

1010N/A abstr2dgEdge = Map.empty::AGraphToDGraphEdge,

1010N/A libname2dg = libEnv}

1010N/A

1010N/A case Map.lookup libname libEnv of

1379N/A

1379N/A Just globContext@(_,_,dgraph) ->

1379N/A if (isEmpty dgraph) then

1431N/A do (abstractGraph,graphInfo,convRef) <-

1379N/A initializeGraph graphMem libname dgraph convMaps globContext

1379N/A return (abstractGraph, graphInfo,convMaps)

1379N/A else

1379N/A do (abstractGraph,graphInfo,convRef) <-

1379N/A initializeGraph graphMem libname dgraph convMaps globContext

1010N/A newConvMaps <- convertNodes convMaps abstractGraph

1425N/A graphInfo dgraph libname

1425N/A finalConvMaps <- convertEdges newConvMaps abstractGraph

1425N/A graphInfo dgraph libname

1010N/A writeIORef convRef finalConvMaps

1010N/A return (abstractGraph, graphInfo, finalConvMaps)

1010N/A

1010N/A Nothing -> error ("development graph with libname "

1010N/A ++ (show libname)

1010N/A ++ " does not exist")

1010N/A

1010N/A

1010N/A{- initializes an empty abstract graph with the needed node and edge types,

1010N/Areturn type equals the one of convertGraph -}

1010N/AinitializeGraph :: IORef GraphMem ->LIB_NAME -> DGraph -> ConversionMaps

1010N/A -> GlobalContext

1010N/A -> IO (Descr,GraphInfo,IORef ConversionMaps)

1010N/AinitializeGraph ioRefGraphMem ln dGraph convMaps globContext = do

1010N/A graphMem <- readIORef ioRefGraphMem

1010N/A event <- newIORef 0

1010N/A convRef <- newIORef convMaps

1010N/A ioRefProofStatus <- newIORef (globContext,

1010N/A [([]::[DGRule], []::[DGChange])],

1010N/A dGraph)

1010N/A ioRefSubtreeEvents <- newIORef (Map.empty::(Map.Map Descr Descr))

1010N/A ioRefVisibleNodes <- newIORef [(Common.Lib.Graph.nodes dGraph)]

1010N/A let gid = nextGraphId graphMem -- newIORef (nextGraphId convMaps)

1010N/A actGraphInfo = graphInfo graphMem

1010N/A-- graphId <- newIORef 0

1010N/A let gInfo = (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo)

1010N/A Result descr _ <-

1010N/A makegraph ("Development graph for "++show ln)

1010N/A [GlobalMenu (Menu Nothing

1010N/A [Menu (Just "Unnamed nodes")

1010N/A [Button "Hide"

1010N/A (do --gid <- readIORef graphId

1010N/A Result descr _ <- hideSetOfNodeTypes gid

1010N/A ["internal",

1010N/A "locallyEmpty_internal"]

1010N/A actGraphInfo

1010N/A writeIORef event descr

1010N/A redisplay gid actGraphInfo

1010N/A return () ),

1010N/A

1010N/A Button "Show"

1010N/A (do --gid <- readIORef graphId

1010N/A descr <- readIORef event

1010N/A showIt gid descr actGraphInfo

1010N/A redisplay gid actGraphInfo

1010N/A return () )],

1010N/A

1010N/A Menu (Just "Proofs")

1010N/A [Button "Global Subsumption"

1010N/A (proofMenuSef gInfo globSubsume),

1010N/A Button "Local Decomposition (merge of rules)"

1010N/A (proofMenuSef gInfo locDecomp),

1010N/A Button "Global Decomposition"

1010N/A (proofMenuSef gInfo globDecomp)

1010N/A ]])]

1010N/A [("spec",

1010N/A createLocalMenuNodeTypeSpec "Magenta" convRef dGraph

1010N/A ioRefSubtreeEvents ioRefVisibleNodes

1010N/A actGraphInfo ioRefGraphMem gInfo

1010N/A ),

1010N/A ("locallyEmpty_spec",

1010N/A createLocalMenuNodeTypeSpec "Violet" convRef dGraph

1010N/A ioRefSubtreeEvents ioRefVisibleNodes

1010N/A actGraphInfo ioRefGraphMem gInfo),

1010N/A ("internal",

1010N/A createLocalMenuNodeTypeInternal "Grey" convRef dGraph gInfo

1010N/A ),

1010N/A ("locallyEmpty_internal",

1010N/A createLocalMenuNodeTypeInternal "LightGrey" convRef dGraph gInfo),

1010N/A ("dg_ref",

1010N/A createLocalMenuNodeTypeDgRef "SteelBlue" convRef actGraphInfo

1010N/A ioRefGraphMem graphMem

1010N/A ),

1010N/A ("locallyEmpty_dg_ref",

1010N/A createLocalMenuNodeTypeDgRef "LightSteelBlue" convRef

1010N/A actGraphInfo ioRefGraphMem graphMem

1010N/A ) ]

1010N/A [("globaldef",

1010N/A Solid

1010N/A $$$ createLocalEdgeMenu

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A ("def",

1010N/A Solid $$$ Color "Steelblue"

1010N/A $$$ createLocalEdgeMenu

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A ("proventhm",

1010N/A Solid $$$ Color "Green"

1010N/A $$$ createLocalEdgeMenuThmEdge

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A ("unproventhm",

1010N/A Solid $$$ Color "Red"

1010N/A $$$ createLocalEdgeMenuThmEdge

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A ("localproventhm",

1010N/A Dashed $$$ Color "Green"

1010N/A $$$ createLocalEdgeMenuThmEdge

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A ("localunproventhm",

1010N/A Dashed $$$ Color "Red"

1010N/A $$$ createLocalEdgeMenuThmEdge

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),

1010N/A -- > ######### welche Farbe fuer reference ##########

1010N/A ("reference",

1010N/A Dotted $$$ Color "Grey"

1010N/A $$$ createLocalEdgeMenu

1010N/A $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue)]

1010N/A [("globaldef","globaldef","globaldef"),

1010N/A ("globaldef","def","def"),

1010N/A ("globaldef","proventhm","proventhm"),

1010N/A ("globaldef","unproventhm","unproventhm"),

1010N/A ("def","globaldef","def"),

1010N/A ("def","def","def"),

1010N/A ("def","proventhm","proventhm"),

1879N/A ("def","unproventhm","unproventhm"),

1879N/A ("proventhm","globaldef","proventhm"),

("proventhm","def","proventhm"),

("proventhm","proventhm","proventhm"),

("proventhm","unproventhm","unproventhm"),

("unproventhm","globaldef","unproventhm"),

("unproventhm","def","unproventhm"),

("unproventhm","proventhm","unproventhm"),

("unproventhm","unproventhm","unproventhm")]

actGraphInfo

writeIORef ioRefGraphMem graphMem{nextGraphId = gid+1}

graphMem'<- readIORef ioRefGraphMem

return (descr,graphInfo graphMem',convRef)

--proofMenu :: (ProofStatus -> IO ProofStatus) -> IO ()

proofMenu (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo) proofFun

= do

proofStatus <- readIORef ioRefProofStatus

Res.Result diags res <- proofFun proofStatus

case res of

Nothing -> do sequence $ map (putStrLn . show) diags

return ()

Just newProofStatus@(_,history,_) -> do

writeIORef ioRefProofStatus newProofStatus

descr <- readIORef event

convMaps <- readIORef convRef

(newDescr,newConvMaps)

<- applyChanges gid ln actGraphInfo descr convMaps history

writeIORef event newDescr

writeIORef convRef newConvMaps

redisplay gid actGraphInfo

return ()

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 convRef dGraph ioRefSubtreeEvents

ioRefVisibleNodes actGraphInfo ioRefGraphMem gInfo =

Ellipse $$$ Color color

$$$ ValueTitle (\ (s,_,_) -> return s)

$$$ LocalMenu (Menu (Just "node menu")

[--createLocalMenuButtonShowSpec convRef dGraph,

createLocalMenuButtonShowSignature convRef dGraph,

createLocalMenuButtonShowTheory convRef dGraph,

createLocalMenuButtonShowSublogic convRef dGraph,

createLocalMenuButtonShowNodeOrigin convRef dGraph,

createLocalMenuButtonProveAtNode gInfo convRef dGraph,

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 convRef dGraph gInfo =

Ellipse $$$ Color color

$$$ ValueTitle (\ (s,_,_) -> return "")

$$$ LocalMenu (Menu (Just "node menu")

[--createLocalMenuButtonShowSpec convRef dGraph,

createLocalMenuButtonShowSignature convRef dGraph,

createLocalMenuButtonShowTheory convRef dGraph,

createLocalMenuButtonShowSublogic convRef dGraph,

createLocalMenuButtonProveAtNode gInfo convRef dGraph,

createLocalMenuButtonShowNodeOrigin convRef dGraph])

$$$ emptyNodeTypeParms

:: DaVinciNodeTypeParms (String,Int,Int)

-- local menu for the nodetypes dg_ref and locallyEmpty_dg_ref

createLocalMenuNodeTypeDgRef color convRef actGraphInfo

ioRefGraphMem graphMem =

Box $$$ Color color

$$$ ValueTitle (\ (s,_,_) -> return s)

$$$ LocalMenu (Button "Show referenced library"

(\ (name,descr,gid) ->

do convMaps <- readIORef convRef

--g <- readIORef graphId

(refDescr, newGraphInfo, refConvMaps) <-

showReferencedLibrary ioRefGraphMem descr

gid

actGraphInfo

convMaps

--writeIORef convRef newConvMaps

writeIORef ioRefGraphMem

graphMem{graphInfo = newGraphInfo,

nextGraphId = refDescr +1}

redisplay refDescr newGraphInfo

-- redisplay gid graphInfo

return ()

))

$$$ emptyNodeTypeParms

:: DaVinciNodeTypeParms (String,Int,Int)

-- menu button for local menus

createMenuButton title menuFun convRef dGraph =

(Button title

(\ (name,descr,gid) ->

do convMaps <- readIORef convRef

menuFun descr

(abstr2dgNode convMaps)

dGraph

return ()

)

)

createLocalMenuButtonShowSpec = createMenuButton "Show spec" showSpec

createLocalMenuButtonShowSignature =

createMenuButton "Show signature" getSignatureOfNode

createLocalMenuButtonShowTheory =

createMenuButton "Show theory" getTheoryOfNode

createLocalMenuButtonShowSublogic =

createMenuButton "Show sublogic" getSublogicOfNode

createLocalMenuButtonShowNodeOrigin =

createMenuButton "Show origin" showOriginOfNode

createLocalMenuButtonProveAtNode gInfo =

createMenuButton "Prove" (proveAtNode 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()

)

)

-- -------------------------------------------------------------

-- methods to create the local menus for the edges

-- -------------------------------------------------------------

createLocalEdgeMenu =

LocalMenu (Menu (Just "edge menu")

[createLocalMenuButtonShowMorphismOfEdge,

createLocalMenuButtonShowOriginOfEdge]

)

createLocalEdgeMenuThmEdge =

LocalMenu (Menu (Just "thm egde menu")

[createLocalMenuButtonShowMorphismOfEdge,

createLocalMenuButtonShowOriginOfEdge,

createLocalMenuButtonShowProofStatusOfThm]

)

createLocalMenuButtonShowMorphismOfEdge =

(Button "Show morphism"

(\ (_,descr,maybeLEdge) ->

do showMorphismOfEdge descr maybeLEdge

return ()

))

createLocalMenuButtonShowOriginOfEdge =

(Button "Show origin"

(\ (_,descr,maybeLEdge) ->

do showOriginOfEdge descr maybeLEdge

return ()

))

createLocalMenuButtonShowProofStatusOfThm =

(Button "Show proof status"

(\ (_,descr,maybeLEdge) ->

do showProofStatusOfThm descr maybeLEdge

return ()

))

-- ------------------------------

-- 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 (show (printText0_eGA sp))

{- 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 node dgraph)

case dgnode of

(DGNode name (G_sign _ sig) _ _) ->

let title = case name of

Nothing -> "Signature"

Just n -> "Signature of "++showPretty n ""

in createTextDisplay title (showPretty sig "") [size(50,50)]

--putStrLn ((showPretty sig) "\n")

(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")

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

used by the node menu defined in initializeGraph-}

getTheoryOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()

getTheoryOfNode descr ab2dgNode dgraph = case (do

(libname, node) <-

Res.maybeToResult nullPos ("Node "++show descr++" not found")

$ Map.lookup descr ab2dgNode

(G_sign lid sign,G_l_sentence_list lid' sens) <-

computeTheory dgraph node

let shownsens = concat $ map ((++"\n") . flip showPretty "") sens

return (node,showPretty sign "\n\naxioms\n" ++ shownsens)

) of

Res.Result [] (Just (node,str)) ->

do let dgnode = lab' (context node dgraph)

case dgnode of

(DGNode name (G_sign _ sig) _ _) ->

let title = case name of

Nothing -> "Theory"

Just n -> "Theory of "++showPretty n ""

in createTextDisplay title str [size(100,50)]

--putStrLn ((showPretty sig) "\n")

(DGRef _ _ _) -> error

"nodes of type dg_ref do not have a theory"

Res.Result diags _ -> do

sequence $ map (putStrLn . show) diags

return ()

{- outputs the sublogic of a node in a window;

used by the node menu defined in initializeGraph-}

getSublogicOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()

getSublogicOfNode descr ab2dgNode dgraph =

case Map.lookup descr ab2dgNode of

Just (libname, node) ->

do let dgnode = lab' (context node dgraph)

case dgnode of

(DGNode name _ _ _) ->

case (dgn_sign dgnode) of

G_sign lid sigma ->

let logstr = (language_name lid ++ "."

++ head (sublogic_names lid

(min_sublogic_sign lid sigma)))

title = case name of

Nothing -> "Sublogic"

Just n -> "Sublogic of "++showPretty n ""

in createTextDisplay title logstr [size(30,10)]

(DGRef _ _ _) -> error "nodes of type dg_ref do not have a sublogic"

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 node dgraph)

case dgnode of

(DGNode name _ _ orig) ->

let title = case name of

Nothing -> "Origin of node"

Just n -> "Origin of node "++showPretty n ""

in createTextDisplay title

(showPretty orig "") [size(30,10)]

Nothing -> error ("node with descriptor "

++ (show descr)

++ " has no corresponding node in the development graph")

{- start local theorem proving at a node -}

--proveAtNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()

proveAtNode gInfo descr ab2dgNode dgraph =

case Map.lookup descr ab2dgNode of

Just libNode -> proofMenu gInfo (basicInferenceNode 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) "") [size(150,50)]

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) =

putStrLn (show (getProofStatusOfThm ledge))

showProofStatusOfThm descr Nothing =

putStrLn ("edge "++(show descr)++" has no corresponding edge"

++ "in the development graph")

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?

otherwise -> 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 nodetype <- (getDGNodeType dgnode)

Result newDescr err <- addnode descr

nodetype

(getDGNodeName dgnode)

graphInfo

--putStrLn (maybe "" id err)

newConvMaps <- (convertNodesAux

convMaps {dg2abstrNode = Map.insert (libname, node)

newDescr (dg2abstrNode convMaps),

abstr2dgNode = Map.insert newDescr

(libname, node) (abstr2dgNode convMaps)}

descr graphInfo lNodes libname)

return newConvMaps

-- gets the name of a development graph node as a string

getDGNodeName :: DGNodeLab -> String

getDGNodeName dgnode =

case get_dgn_name dgnode of

Just simpleId -> tokStr simpleId

Nothing -> ""

-- gets the type of a development graph edge as a string

getDGNodeType :: DGNodeLab -> IO String

getDGNodeType dgnode =

do let nodetype = getDGNodeTypeAux dgnode

case (isDGRef dgnode) of

True -> return (nodetype++"dg_ref")

False -> case get_dgn_name dgnode of

Just _ -> return (nodetype++"spec")

Nothing -> return (nodetype++"internal")

getDGNodeTypeAux :: DGNodeLab -> String

getDGNodeTypeAux dgnode = if (locallyEmpty dgnode) then "locallyEmpty_"

else ""

getDGLinkType :: DGLinkType -> String

getDGLinkType LocalDef = "def"

getDGLinkType GlobalDef = "globaldef"

getDGLinkType HidingDef = "def"

getDGLinkType (FreeDef _) = "def"

getDGLinkType (CofreeDef _) = "def"

getDGLinkType (LocalThm thmLinkStatus _ _) =

"local"++(getThmType thmLinkStatus)

getDGLinkType (GlobalThm thmLinkStatus _ _) = getThmType thmLinkStatus

getDGLinkType (HidingThm _ thmLinkStatus) = getThmType thmLinkStatus

getDGLinkType (FreeThm _ bool) = if bool then "proventhm" else "unproventhm"

getThmType :: ThmLinkStatus -> String

getThmType thmLinkStatus =

case thmLinkStatus of

Proven _ -> "proventhm"

Open -> "unproventhm"

{- 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

-- function context from Graph.hs with inverse arguments

invContext :: DGraph -> Node -> Context DGNodeLab DGLinkLab

invContext dgraph node = context node dgraph

{- 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 (dgl_type 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

otherwise -> error "Cannot find nodes"

showReferencedLibrary :: IORef GraphMem -> Descr -> Descr -> GraphInfo

-> ConversionMaps -> IO (Descr, GraphInfo, ConversionMaps)

showReferencedLibrary graphMem descr abstractGraph graphInfo convMaps =

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 node dgraph)

case Map.lookup refLibname libname2dgMap of

Just (_,refDgraph,_) ->

convertGraph graphMem refLibname (libname2dg convMaps)

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

-- --------------------------

-- returntype festlegen

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 -- allDgNodes = Common.Lib.Graph.nodes dgraph

allNodes = getNodeDescriptors (head visibleNodes)

libname convMaps -- allDgNodes libname convMaps

dgNodesOfSubtree = nub (parentNode:(getNodesOfSubtree dgraph

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 visibleNodes) predOfNode))

++predOfNode

where predOfNode = filter (elemR (head visibleNodes)) (pre dgraph node)

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 -> ConversionMaps

-> [([DGRule],[DGChange])]

-> IO (Descr, ConversionMaps)

applyChanges gid libname graphInfo eventDescr convMaps history =

case history of

[] -> return (eventDescr, convMaps)

(historyElem:list) ->

case snd historyElem of

[] -> return (eventDescr, convMaps)

changes@(x:xs) ->

applyChangesAux gid libname graphInfo eventDescr convMaps changes

applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> Descr

-> ConversionMaps -> [DGChange]

-> IO (Descr, ConversionMaps)

applyChangesAux _ _ _ eventDescr convMaps [] = return (eventDescr+1, convMaps)

applyChangesAux gid libname graphInfo eventDescr convMaps (change:changes) =

case change of

InsertNode lNode -> error "insert node not yet implemented"

DeleteNode node -> error "delete node not yet implemented"

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 (dgl_type 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 (descr+1)

newConvMaps changes

Just _ ->

-- -- ##### was machen, wenn Einf�gen nicht erfolgreich?! ###

-- Momentane L�sung: ignorieren...

applyChangesAux gid libname graphInfo eventDescr

convMaps changes

otherwise ->

-- -- ##### was machen, wenn Einf�gen nicht erfolgreich?! ###

-- Momentane L�sung: ignorieren...

applyChangesAux gid libname graphInfo eventDescr

convMaps changes

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 (descr+1)

newConvMaps changes

-- -- @@@ was machen, wenn Entfernen nicht erfolgreich?! @@@

-- Momentane L�sung: abbrechen...

Just _ -> error ("applyChangesAux: could not delete edge "

++ (show abstrEdge))

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")