{-# 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.Map.Strict as M
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 forall a b. (a -> b) -> a -> b
$ 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 <- forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ 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
_
        } <- forall n e. Graph n e -> [Edge n e]
Graph.edges DotGraph
g
    ]
  , [Text
"}"]
  ]
  where
  show' :: Int -> Text
show' = String -> Text
L.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"m" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
BS.writeFile String
fp forall a b. (a -> b) -> a -> b
$ Text -> ByteString
E.encodeUtf8 forall a b. (a -> b) -> a -> b
$ DotGraph -> Text
renderDot DotGraph
dot