    -- | 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