module Agda.Interaction.Highlighting.Dot.Base
( renderDotToFile
, renderDot
, DotGraph
) where
import Control.Monad.IO.Class
import qualified Data.Set as S
import qualified Data.Text.Lazy as L
import qualified Data.Text.Lazy.Encoding as E
import qualified Data.ByteString.Lazy as BS
import Agda.Utils.Graph.AdjacencyMap.Unidirectional
(Graph, WithUniqueInt)
import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph
type DotGraph = Graph (WithUniqueInt L.Text) ()
renderDot :: DotGraph -> L.Text
renderDot :: DotGraph -> Text
renderDot DotGraph
g = [Text] -> Text
L.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ Text
"digraph dependencies {" ]
, [ [Text] -> Text
L.concat [Text
" ", Int -> Text
show' Int
nodeId, Text
"[label=\"", Text
label, Text
"\"];"]
| Graph.WithUniqueInt Int
nodeId Text
label <- Set (WithUniqueInt Text) -> [WithUniqueInt Text]
forall a. Set a -> [a]
S.toList (Set (WithUniqueInt Text) -> [WithUniqueInt Text])
-> Set (WithUniqueInt Text) -> [WithUniqueInt Text]
forall a b. (a -> b) -> a -> b
$ DotGraph -> Set (WithUniqueInt Text)
forall n e. Graph n e -> Set n
Graph.nodes DotGraph
g
]
, [ [Text] -> Text
L.concat [Text
" ", Int -> Text
show' Int
r1, Text
" -> ", Int -> Text
show' Int
r2, Text
";"]
| Graph.Edge
{ source :: forall n e. Edge n e -> n
source = Graph.WithUniqueInt Int
r1 Text
_
, target :: forall n e. Edge n e -> n
target = Graph.WithUniqueInt Int
r2 Text
_
} <- DotGraph -> [Edge (WithUniqueInt Text) ()]
forall n e. Graph n e -> [Edge n e]
Graph.edges DotGraph
g
]
, [Text
"}"]
]
where
show' :: Int -> Text
show' = String -> Text
L.pack (String -> Text) -> (Int -> String) -> Int -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"m" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show
renderDotToFile :: MonadIO m => DotGraph -> FilePath -> m ()
renderDotToFile :: forall (m :: * -> *). MonadIO m => DotGraph -> String -> m ()
renderDotToFile DotGraph
dot String
fp = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
BS.writeFile String
fp (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
E.encodeUtf8 (Text -> ByteString) -> Text -> ByteString
forall a b. (a -> b) -> a -> b
$ DotGraph -> Text
renderDot DotGraph
dot