e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Display of development graphs using Graphviz\/dot
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederCopyright : (c) Till Mossakowski, Klaus Luettich Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable(Logic)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDisplay of development graphs using Graphviz\/dot
f409ea7e4a6a1fee58595481759fcd2e839ce152Christian Maedermodule Static.DotGraph (dotGraph) where
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian MaederedgeAttributes :: DGEdgeType -> String
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian MaederedgeAttributes ety = concatMap (", " ++)
52405236a950dca8f5904b771ec5440d802ec626Christian Maeder $ (if isInc ety then ["arrowsize=0.5"] else ["style=bold"])
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder ++ case edgeTypeModInc ety of
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder GlobalDef -> []
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder HetDef -> ["color=" ++ doubleColor "black"]
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder HidingDef -> ["color=blue"]
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder LocalDef -> ["style=dashed"]
5c9d9c85e0aac314175d6804a994993aabbd1a89Simon Ulbricht FreeOrCofreeDef _ -> ["color=blue"]
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder { thmEdgeType = thTy
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder , isProvenEdge = isProv
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder , isConservativ = isCons
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder , isPending = isPend }
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder hc = ["color=" ++ if isPend then "cyan" else
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder if isProv then "green" else "blue"]
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder in case thTy of
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder HidingThm -> "style=dashed" : hc
6991b9cb29b2d8f106642e547fee727aeac5e52bSimon Ulbricht FreeOrCofreeThm _ -> "style=dotted" : hc
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder cl c = if isHomThm th then c else doubleColor c
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder rc = if isProv then
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder if isCons then
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder if isPend then "yellow" else show "/green"
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder else "orange"
fb5b958b07a002f7f6daa0ac032976979c63b7c3Christian Maeder in ("color=" ++ cl rc) : case thmScope th of
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder Local -> ["style=dashed"]
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian MaederdoubleColor :: String -> String
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian MaederdoubleColor s = show $ s ++ ':' : s
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaederdotEdge :: String -> LEdge DGLinkLab -> String
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaederdotEdge url (n1, n2, link) = let
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder cs = showConsStatus (getEdgeConsStatus link)
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder es = showEdgeId (dgl_id link)
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder in show n1 ++ " -> " ++ show n2
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ " [id=" ++ es
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ (if null url then "" else ", URL=" ++ show (url ++ "?edge=" ++ es))
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ (if null cs then "" else
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ", fontname=Helvetica, fontsize=10, label=" ++ show cs)
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ edgeAttributes (getRealDGLinkType link)
0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus LuettichnodeAttribute :: Bool -> DGNodeLab -> String
3ffc0010fb6bb89aaef9c08e29b9ec336b4d1d4bChristian MaedernodeAttribute showInternal la = concatMap (", " ++)
3ffc0010fb6bb89aaef9c08e29b9ec336b4d1d4bChristian Maeder (inter la : ["shape=box" | isDGRef la]
3ffc0010fb6bb89aaef9c08e29b9ec336b4d1d4bChristian Maeder ++ [ "style=filled"
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder , "fontsize=12"
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder , "fontname=Helvetica"
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder , "fillcolor=" ++ if hasOpenGoals la then "red" else
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder if hasOpenNodeConsStatus False la then "yellow" else show "/green" ])
0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettich where inter l = if isInternalNode l && not showInternal
a873000c712a1a7e5ca6afe46b7ef6df6e6af6b3Christian Maeder then "label=\"\", height=0.1, width=0.2"
224210bd9cffd3375eca29aba6ed57e0d860142eChristian Maeder else "label=\"" ++ getDGNodeName la ++ "\""
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaederdotNode :: Bool -> String -> LNode DGNodeLab -> String
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaederdotNode showInternal url (n, ncontents) = let ns = show n in
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ns ++ " [id=" ++ ns
4b06b558d824fdc970e8c6be4e4386bf18ef911dSimon Ulbricht ++ (if null url then "" else ", URL=" ++ show (url ++ "?theory=" ++ ns))
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ nodeAttribute showInternal ncontents ++ "];"
0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettich-- | Generate a dot term representation out of a development graph
9b3aefff51492156e8e7f7f6a57986dac35a55fcChristian MaederdotGraph :: FilePath
9b3aefff51492156e8e7f7f6a57986dac35a55fcChristian Maeder -> Bool -- ^ True means show internal node labels
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder -> String -- ^ URL for node and edge links
0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettich -> DGraph -> String
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian MaederdotGraph f showInternalNodeLabels url dg = unlines $
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ["digraph " ++ show f ++ " {" ]
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ map (dotNode showInternalNodeLabels url) (labNodesDG dg)
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder ++ map (dotEdge url) (labEdgesDG dg)