{-# LANGUAGE GADTs #-}
-- | Generate an import dependency graph for a given module.

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

-- | Graph structure
type DotGraph = Graph (WithUniqueInt L.Text) ()

-- * Graph rendering

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