ConvertDevToAbstractGraph.hs revision ba904a15082557e939db689fcfba0c68c9a4f740
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport DaVinciGraph
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederimport GraphDisp
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport GraphConfigure
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport FiniteMap
dba1eafdf5b025161058f973c44b2c880e6b8241Christian Maederpretty x = show $ printText0 emptyGlobalAnnos x
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder{- FiniteMaps used to track which node resp edge of the abstract graph correspondes with which of the development graph and vice versa
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederand one FiniteMap to store which libname belongs to which development graph-}
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederdata ConversionMaps = ConversionMaps {
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder dg2abstrNode :: DGraphToAGraphNode,
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder dg2abstrEdge :: DGraphToAGraphEdge,
c35d75c97d5257326d24e40fdc0ac6486f63ab55Christian Maeder abstr2dgNode :: AGraphToDGraphNode,
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder abstr2dgEdge :: AGraphToDGraphEdge,
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder libname2dg :: LibEnv
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder-- types of the FiniteMaps above
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskitype DGraphToAGraphNode = FiniteMap (LIB_NAME,Node) Descr
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maedertype DGraphToAGraphEdge = FiniteMap (LIB_NAME,Edge) Descr
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maedertype AGraphToDGraphNode = FiniteMap Descr (LIB_NAME,Node)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedertype AGraphToDGraphEdge = FiniteMap Descr (LIB_NAME,Edge)
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder{- converts the development graph given by its libname into an abstract graph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederand returns the descriptor of the latter, the graphInfo it is contained in and the conversion maps (see above)-}
2e2094a642e3775b0d76b890556407941d3a53b6Christian MaederconvertGraph :: LIB_NAME -> LibEnv -> IO (Descr, GraphInfo, ConversionMaps)
2e2094a642e3775b0d76b890556407941d3a53b6Christian MaederconvertGraph libname libEnv =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder do let convMaps = ConversionMaps
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder {dg2abstrNode = emptyFM::DGraphToAGraphNode,
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder abstr2dgNode = emptyFM::AGraphToDGraphNode,
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder dg2abstrEdge = emptyFM::DGraphToAGraphEdge,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder abstr2dgEdge = emptyFM::AGraphToDGraphEdge,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder libname2dg = libEnv}
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder case lookupFM libEnv libname of
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Just (_,dgraph,_) -> if (isEmpty dgraph) then
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder do (abstractGraph,graphInfo,convRef) <- initializeGraph libname dgraph convMaps
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder return (abstractGraph, graphInfo,convMaps)
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder else do (abstractGraph,graphInfo,convRef) <- initializeGraph libname dgraph convMaps
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder newConvMaps <- convertNodes convMaps abstractGraph graphInfo dgraph libname
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder finalConvMaps <- convertEdges newConvMaps abstractGraph graphInfo dgraph libname
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder writeIORef convRef finalConvMaps
57a2436f9d44e37042498a3b3dfacd301d91bb6dChristian Maeder return (abstractGraph, graphInfo, finalConvMaps)
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder Nothing -> error ("development graph with libname "
d4892fa7401ceef014ea59d2d900773eaf88fcbdChristian Maeder ++ (show libname)
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder ++ "does not exist")
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maeder{- initializes an empty abstract graph with the needed node and edge types,
eee4b2ee739f163e09d6af6e45c025681e6c01a0Christian Maederreturn type equals the one of convertGraph -}
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus LuettichinitializeGraph :: LIB_NAME -> DGraph -> ConversionMaps -> IO (Descr,GraphInfo,IORef ConversionMaps)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederinitializeGraph ln dGraph convMaps = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder graphInfo <- initgraphs
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder event <- newIORef 0
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder convRef <- newIORef convMaps
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Result descr _ <-
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder makegraph ("Development graph for "++show ln)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [GlobalMenu(Menu (Just "internal nodes")
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder [Button "Hide"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (do Result descr _ <- hidenodetype 0 "internal" graphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder writeIORef event descr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder redisplay 0 graphInfo
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder Button "Show"
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (do descr <- readIORef event
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder showIt 0 descr graphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder redisplay 0 graphInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder return () )])]
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski Ellipse $$$ Color "Magenta" $$$ ValueTitle (\ (s,_,_) -> return s)
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich $$$ LocalMenu
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (Button "Show spec"
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (\ (name,descr,gid) -> do convMaps <- readIORef convRef
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski showSpec descr (abstr2dgNode convMaps) dGraph
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder $$$ emptyNodeTypeParms :: DaVinciNodeTypeParms (String,Int,Int)),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Ellipse $$$ Color "Grey" $$$ ValueTitle (\ (s,_,_) -> return "")
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder $$$ LocalMenu
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (Button "Show spec"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (\ (name,descr,gid) -> do convMaps <- readIORef convRef
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showSpec descr (abstr2dgNode convMaps) dGraph
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder $$$ emptyNodeTypeParms :: DaVinciNodeTypeParms (String,Int,Int)),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Box $$$ Color "SteelBlue" $$$ ValueTitle (\ (s,_,_) -> return s)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder $$$ emptyNodeTypeParms :: DaVinciNodeTypeParms (String,Int,Int)) ]
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder Solid $$$ emptyArcTypeParms :: DaVinciArcTypeParms (String,Int)),
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder ("proventhm",
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Solid $$$ Color "Green" $$$ emptyArcTypeParms :: DaVinciArcTypeParms (String,Int)),
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder ("unproventhm",
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder Solid $$$ Color "Red" $$$ emptyArcTypeParms :: DaVinciArcTypeParms (String,Int))]
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder [("def","def","def"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("def","proventhm","proventhm"),
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ("def","unproventhm","unproventhm"),
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder ("proventhm","def","proventhm"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("proventhm","proventhm","proventhm"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("proventhm","unproventhm","unproventhm"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("unproventhm","def","unproventhm"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("unproventhm","proventhm","unproventhm"),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ("unproventhm","unproventhm","unproventhm")] graphInfo
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return (descr,graphInfo,convRef)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedershowSpec descr convMap dgraph =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case lookupFM convMap descr of
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Nothing -> return ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (libname,node) -> do
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder let sp = dgToSpec dgraph node
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putStrLn (show (printText0_eGA sp))
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder{- returns the signature of a node as a(n IO) string
62ea3d19927e5ce1318d62931a8427d8930f1576Christian Maederused by the node menu defined in initializeGraph-}
62ea3d19927e5ce1318d62931a8427d8930f1576Christian MaedergetSignatureOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO String
4017ebc0f692820736d796af3110c3b3018c108aChristian MaedergetSignatureOfNode descr ab2dgNode dgraph =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder case lookupFM ab2dgNode descr of
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder Just (libname, node) -> do let dgnode = lab' (context node dgraph)
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder return (show (dgn_sign dgnode))
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Nothing -> error ("node with descriptor "
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder ++ (show descr)
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder ++ " has no corresponding node in the development graph")
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder{- converts the nodes of the development graph, if it has any,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederand returns the resulting conversion maps
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederif the graph is empty the conversion maps are returned unchanged-}
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederconvertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME -> IO ConversionMaps
88318aafc287e92931dceffbb943d58a9310001dChristian MaederconvertNodes convMaps descr graphInfo dgraph libname
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder | isEmpty dgraph = do return convMaps
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder | otherwise = convertNodesAux convMaps descr graphInfo (labNodes dgraph) libname
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- auxiliar function for convertNodes
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederif the given list of nodes is emtpy, it returns the conversion maps unchanged
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederotherwise it adds the converted first node to the abstract graph and to the affected conversion maps
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederand afterwards calls itself with the remaining node list -}
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederconvertNodesAux :: ConversionMaps -> Descr -> GraphInfo -> [LNode DGNode] -> LIB_NAME -> IO ConversionMaps
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederconvertNodesAux convMaps descr graphInfo [] libname = return convMaps
4017ebc0f692820736d796af3110c3b3018c108aChristian MaederconvertNodesAux convMaps descr graphInfo ((node,dgnode):lNodes) libname =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder do Result newDescr err <- addnode descr (getDGNodeType dgnode) (getDGNodeName dgnode) graphInfo
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich --putStrLn (maybe "" id err)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder newConvMaps <- (convertNodesAux
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder convMaps {dg2abstrNode = addToFM (dg2abstrNode convMaps) (libname, node) newDescr,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder abstr2dgNode = addToFM (abstr2dgNode convMaps) newDescr (libname, node)}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder descr graphInfo lNodes libname)
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder return newConvMaps
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- gets the name of a development graph node as a string
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergetDGNodeName :: DGNode -> String
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergetDGNodeName dgnode =
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder case get_dgn_name dgnode of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just simpleId -> pretty simpleId
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> ""
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- gets the type of a development graph edge as a string
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedergetDGNodeType :: DGNode -> String
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedergetDGNodeType dgnode =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case isDGRef dgnode of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder True -> "dg_ref"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder False -> case get_dgn_name dgnode of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Just _ -> "spec"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> "internal"
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedergetDGLinkType :: DGLinkType -> String
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergetDGLinkType LocalDef = "def"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergetDGLinkType GlobalDef = "def"
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian MaedergetDGLinkType HidingDef = "def"
431d34c7007a787331c4e5ec997badb0f8190fc7Christian MaedergetDGLinkType (FreeDef _) = "def"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedergetDGLinkType (CofreeDef _) = "def"
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedergetDGLinkType (LocalThm bool) = getThmType bool
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus LuettichgetDGLinkType (GlobalThm bool) = getThmType bool
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetDGLinkType (HidingThm _ bool) = getThmType bool
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergetDGLinkType (FreeThm _ bool) = getThmType bool
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaedergetThmType :: Bool -> String
6b6773cf587b74259178641d811746a235faf056Christian MaedergetThmType bool = case bool of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder True -> "proventhm"
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder False -> "unproventhm"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder{- converts the edges of the development graph
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederworks the same way as convertNods does-}
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederconvertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME -> IO ConversionMaps
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederconvertEdges convMaps descr graphInfo dgraph libname
d272062059eea4d7479e1c6e8517469f02f61287Christian Maeder | isEmpty dgraph = do return convMaps
0cfef6179a1bfec4f07f460686dd629a27b4b778Christian Maeder | otherwise = convertEdgesAux convMaps descr graphInfo dgraph (labEdges dgraph) libname
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder-- function context from Graph.hs with inverse arguments
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederinvContext :: DGraph -> Node -> Context DGNode DGLink
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederinvContext dgraph node = context node dgraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder{- auxiliar function for convertEges --> not yet implemented! -}
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederconvertEdgesAux :: ConversionMaps -> Descr -> GraphInfo -> DGraph ->
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [LEdge DGLink] -> LIB_NAME -> IO ConversionMaps
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederconvertEdgesAux convMaps descr graphInfo dgraph [] libname = return convMaps
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederconvertEdgesAux convMaps descr graphInfo dgraph ((src,tar,edge):lEdges) libname =
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder do let srcnode = lookupFM (dg2abstrNode convMaps) (libname,src)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers tarnode = lookupFM (dg2abstrNode convMaps) (libname,tar)
010c56c4cf12dd7977ca36efe85219b91e265ee3Christian Maeder case (srcnode,tarnode) of
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich (Just s, Just t) -> do
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski Result newDescr err <- addlink descr (getDGLinkType (dgl_type edge)) "" s t graphInfo
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder --putStrLn (maybe "" id err)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers --putStrLn ("Adding link" ++ show descr)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder newConvMaps <- (convertEdgesAux
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder convMaps {dg2abstrEdge = addToFM (dg2abstrEdge convMaps) (libname, (src,tar)) newDescr,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder abstr2dgEdge = addToFM (abstr2dgEdge convMaps) newDescr (libname, (src,tar))}
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder descr graphInfo dgraph lEdges libname)
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers return newConvMaps
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder otherwise -> error "Cannot find nodes"