{- |
Module      :  ./Static/DotGraph.hs
Description :  Display of development graphs using Graphviz\/dot
Copyright   :  (c) Till Mossakowski, Klaus Luettich Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

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

Display of development graphs using Graphviz\/dot
-}

module Static.DotGraph (dotGraph) where

import Data.Graph.Inductive.Graph

import Static.DgUtils
import Static.DevGraph

edgeAttributes :: DGEdgeType -> String
edgeAttributes :: DGEdgeType -> String
edgeAttributes ety :: DGEdgeType
ety = (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (", " String -> String -> String
forall a. [a] -> [a] -> [a]
++)
  ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (if DGEdgeType -> Bool
isInc DGEdgeType
ety then ["arrowsize=0.5"] else ["style=bold"])
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ case DGEdgeType -> DGEdgeTypeModInc
edgeTypeModInc DGEdgeType
ety of
    GlobalDef -> []
    HetDef -> ["color=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
doubleColor "black"]
    HidingDef -> ["color=blue"]
    LocalDef -> ["style=dashed"]
    FreeOrCofreeDef _ -> ["color=blue"]
    ThmType
      { thmEdgeType :: DGEdgeTypeModInc -> ThmTypes
thmEdgeType = ThmTypes
thTy
      , isProvenEdge :: DGEdgeTypeModInc -> Bool
isProvenEdge = Bool
isProv
      , isConservativ :: DGEdgeTypeModInc -> Bool
isConservativ = Bool
isCons
      , isPending :: DGEdgeTypeModInc -> Bool
isPending = Bool
isPend }
      -> let
      hc :: [String]
hc = ["color=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool
isPend then "cyan" else
             if Bool
isProv then "green" else "blue"]
      in case ThmTypes
thTy of
      HidingThm -> "style=dashed" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
hc
      FreeOrCofreeThm _ -> "style=dotted" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
hc
      th :: ThmTypes
th -> let
        cl :: String -> String
cl c :: String
c = if ThmTypes -> Bool
isHomThm ThmTypes
th then String
c else String -> String
doubleColor String
c
        rc :: String
rc = if Bool
isProv then
               if Bool
isCons then
                 if Bool
isPend then "yellow" else String -> String
forall a. Show a => a -> String
show "/green"
               else "orange"
             else "red"
        in ("color=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
cl String
rc) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: case ThmTypes -> Scope
thmScope ThmTypes
th of
        Global -> []
        Local -> ["style=dashed"]

doubleColor :: String -> String
doubleColor :: String -> String
doubleColor s :: String
s = String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ':' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s

dotEdge :: String -> LEdge DGLinkLab -> String
dotEdge :: String -> LEdge DGLinkLab -> String
dotEdge url :: String
url (n1 :: Node
n1, n2 :: Node
n2, link :: DGLinkLab
link) = let
  cs :: String
cs = ConsStatus -> String
showConsStatus (DGLinkLab -> ConsStatus
getEdgeConsStatus DGLinkLab
link)
  es :: String
es = EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
link)
  in Node -> String
forall a. Show a => a -> String
show Node
n1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Node -> String
forall a. Show a => a -> String
show Node
n2
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [id=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
es
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
url then "" else ", URL=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ "?edge=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
es))
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
cs then "" else
        ", fontname=Helvetica, fontsize=10, label=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
cs)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGEdgeType -> String
edgeAttributes (DGLinkLab -> DGEdgeType
getRealDGLinkType DGLinkLab
link)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ "];"

nodeAttribute :: Bool -> DGNodeLab -> String
nodeAttribute :: Bool -> DGNodeLab -> String
nodeAttribute showInternal :: Bool
showInternal la :: DGNodeLab
la = (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (", " String -> String -> String
forall a. [a] -> [a] -> [a]
++)
  (DGNodeLab -> String
inter DGNodeLab
la String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ["shape=box" | DGNodeLab -> Bool
isDGRef DGNodeLab
la]
   [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "style=filled"
      , "fontsize=12"
      , "fontname=Helvetica"
      , "fillcolor=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ if DGNodeLab -> Bool
hasOpenGoals DGNodeLab
la then "red" else
        if Bool -> DGNodeLab -> Bool
hasOpenNodeConsStatus Bool
False DGNodeLab
la then "yellow" else String -> String
forall a. Show a => a -> String
show "/green" ])
 where inter :: DGNodeLab -> String
inter l :: DGNodeLab
l = if DGNodeLab -> Bool
isInternalNode DGNodeLab
l Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
showInternal
                    then "label=\"\", height=0.1, width=0.2"
                    else "label=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGNodeLab -> String
getDGNodeName DGNodeLab
la String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""

dotNode :: Bool -> String -> LNode DGNodeLab -> String
dotNode :: Bool -> String -> LNode DGNodeLab -> String
dotNode showInternal :: Bool
showInternal url :: String
url (n :: Node
n, ncontents :: DGNodeLab
ncontents) = let ns :: String
ns = Node -> String
forall a. Show a => a -> String
show Node
n in
  String
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [id=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ns
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
url then "" else ", URL=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (String
url String -> String -> String
forall a. [a] -> [a] -> [a]
++ "?theory=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ns))
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> DGNodeLab -> String
nodeAttribute Bool
showInternal DGNodeLab
ncontents String -> String -> String
forall a. [a] -> [a] -> [a]
++ "];"

-- | Generate a dot term representation out of a development graph
dotGraph :: FilePath
    -> Bool -- ^ True means show internal node labels
    -> String -- ^ URL for node and edge links
    -> DGraph -> String
dotGraph :: String -> Bool -> String -> DGraph -> String
dotGraph f :: String
f showInternalNodeLabels :: Bool
showInternalNodeLabels url :: String
url dg :: DGraph
dg = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
  ["digraph " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " {" ]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (LNode DGNodeLab -> String) -> [LNode DGNodeLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> String -> LNode DGNodeLab -> String
dotNode Bool
showInternalNodeLabels String
url) (DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
dg)
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (LEdge DGLinkLab -> String) -> [LEdge DGLinkLab] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> LEdge DGLinkLab -> String
dotEdge String
url) (DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dg)
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["}"]