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

    module Agda.Interaction.Highlighting.Dot.Base
      ( dottify
      , renderDotToFile
      , renderDot
      , DotGraph (..)
      , Env(..)
      ) where

    import Control.Monad          (liftM2, when)
    import Control.Monad.IO.Class (MonadIO(..))
    import Control.Monad.Reader   (ReaderT, runReaderT, ask)
    import Control.Monad.State    (State, execState, get, modify, put)

    import qualified Data.Map as M
    import Data.Map(Map)

    import qualified Data.Set as S
    import Data.Set (Set)

    import qualified Data.Text.Lazy as L
    import qualified Data.Text.Lazy.Encoding as E
    import qualified Data.ByteString.Lazy as BS

    -- | Internal module identifiers for construction of dependency graph.
    type NodeId = L.Text

    -- | Graph structure
    data DotGraph = DotGraph
      { DotGraph -> Map Text Text
    dgNodeLabels :: Map NodeId L.Text
      , DotGraph -> Set (Text, Text)
    dgEdges      :: Set (NodeId, NodeId)
      }

    -- * Graph construction monad

    -- Read-only environment when constructing the graph.
    data Env n where
      Env :: Ord n =>
        { forall n. Env n -> n -> [n]
    deConnections :: n -> [n]
        -- ^ Names connected to an entity
        , forall n. Env n -> n -> Text
    deLabel       :: n -> L.Text
        -- ^ Rendering that entity's name to a label
        } -> Env n

    data DotState n = DotState
      { forall n. DotState n -> Map n Text
    dsNodeIds      :: Map n NodeId
        -- ^ Records already processed entities
        --   and maps them to an internal identifier.
      , forall n. DotState n -> [Text]
    dsNodeIdSupply :: [NodeId]
        -- ^ Supply of internal identifiers.
      , forall n. DotState n -> DotGraph
    dsGraph        :: DotGraph
      }

    initialDotState :: DotState n
    initialDotState :: forall n. DotState n
    initialDotState = DotState :: forall n. Map n Text -> [Text] -> DotGraph -> DotState n
    DotState
      { dsNodeIds :: Map n Text
    dsNodeIds      = Map n Text
    forall k a. Map k a
    M.empty
      , dsNodeIdSupply :: [Text]
    dsNodeIdSupply = (Integer -> Text) -> [Integer] -> [Text]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Text
    L.pack (String -> Text) -> (Integer -> String) -> Integer -> Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char
    'm'Char -> String -> String
    forall a. a -> [a] -> [a]
    :) (String -> String) -> (Integer -> String) -> Integer -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> String
    forall a. Show a => a -> String
    show) [Integer
    0..]
      , dsGraph :: DotGraph
    dsGraph        = Map Text Text -> Set (Text, Text) -> DotGraph
    DotGraph Map Text Text
    forall a. Monoid a => a
    mempty Set (Text, Text)
    forall a. Monoid a => a
    mempty
      }

    type DotM n a = ReaderT (Env n) (State (DotState n)) a

    runDotM :: Env n -> DotM n x -> DotGraph
    runDotM :: forall n x. Env n -> DotM n x -> DotGraph
    runDotM env :: Env n
    env@Env{} = DotState n -> DotGraph
    forall n. DotState n -> DotGraph
    dsGraph (DotState n -> DotGraph)
    -> (ReaderT (Env n) (StateT (DotState n) Identity) x -> DotState n)
    -> ReaderT (Env n) (StateT (DotState n) Identity) x
    -> DotGraph
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (State (DotState n) x -> DotState n -> DotState n)
    -> DotState n -> State (DotState n) x -> DotState n
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip State (DotState n) x -> DotState n -> DotState n
    forall s a. State s a -> s -> s
    execState DotState n
    forall n. DotState n
    initialDotState (State (DotState n) x -> DotState n)
    -> (ReaderT (Env n) (StateT (DotState n) Identity) x
        -> State (DotState n) x)
    -> ReaderT (Env n) (StateT (DotState n) Identity) x
    -> DotState n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ReaderT (Env n) (StateT (DotState n) Identity) x
     -> Env n -> State (DotState n) x)
    -> Env n
    -> ReaderT (Env n) (StateT (DotState n) Identity) x
    -> State (DotState n) x
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ReaderT (Env n) (StateT (DotState n) Identity) x
    -> Env n -> State (DotState n) x
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT Env n
    env

    getLabel :: n -> DotM n L.Text
    getLabel :: forall n. n -> DotM n Text
    getLabel = (Env n -> n -> Text)
    -> ReaderT (Env n) (State (DotState n)) (Env n)
    -> ReaderT (Env n) (State (DotState n)) n
    -> ReaderT (Env n) (State (DotState n)) Text
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Env n -> n -> Text
    forall n. Env n -> n -> Text
    deLabel ReaderT (Env n) (State (DotState n)) (Env n)
    forall r (m :: * -> *). MonadReader r m => m r
    ask (ReaderT (Env n) (State (DotState n)) n
     -> ReaderT (Env n) (State (DotState n)) Text)
    -> (n -> ReaderT (Env n) (State (DotState n)) n)
    -> n
    -> ReaderT (Env n) (State (DotState n)) Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . n -> ReaderT (Env n) (State (DotState n)) n
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    getConnections :: n -> DotM n [n]
    getConnections :: forall n. n -> DotM n [n]
    getConnections = (Env n -> n -> [n])
    -> ReaderT (Env n) (State (DotState n)) (Env n)
    -> ReaderT (Env n) (State (DotState n)) n
    -> ReaderT (Env n) (State (DotState n)) [n]
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Env n -> n -> [n]
    forall n. Env n -> n -> [n]
    deConnections ReaderT (Env n) (State (DotState n)) (Env n)
    forall r (m :: * -> *). MonadReader r m => m r
    ask (ReaderT (Env n) (State (DotState n)) n
     -> ReaderT (Env n) (State (DotState n)) [n])
    -> (n -> ReaderT (Env n) (State (DotState n)) n)
    -> n
    -> ReaderT (Env n) (State (DotState n)) [n]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . n -> ReaderT (Env n) (State (DotState n)) n
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

    -- | Translate an entity name into an internal 'NodeId'.
    --   Returns @True@ if the 'ModuleName' is new, i.e., has not been
    --   encountered before and is thus added to the map of processed modules.
    addEntity :: Ord n => n -> DotM n (NodeId, Bool)
    addEntity :: forall n. Ord n => n -> DotM n (Text, Bool)
    addEntity n
    name = do
        s :: DotState n
    s@(DotState Map n Text
    nodeIds [Text]
    nodeIdSupply DotGraph
    graph) <- ReaderT (Env n) (State (DotState n)) (DotState n)
    forall s (m :: * -> *). MonadState s m => m s
    get
        case n -> Map n Text -> Maybe Text
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup n
    name Map n Text
    nodeIds of
            Just Text
    nodeId  -> (Text, Bool) -> DotM n (Text, Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    nodeId, Bool
    False)
            Maybe Text
    Nothing -> do
                let Text
    newNodeId:[Text]
    remainingNodeIdSupply = [Text]
    nodeIdSupply
                Text
    label <- n -> DotM n Text
    forall n. n -> DotM n Text
    getLabel n
    name
                DotState n -> ReaderT (Env n) (State (DotState n)) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put DotState n
    s
                  { dsNodeIds :: Map n Text
    dsNodeIds      = n -> Text -> Map n Text -> Map n Text
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert n
    name Text
    newNodeId Map n Text
    nodeIds
                  , dsNodeIdSupply :: [Text]
    dsNodeIdSupply = [Text]
    remainingNodeIdSupply
                  , dsGraph :: DotGraph
    dsGraph        = DotGraph
    graph
                    { dgNodeLabels :: Map Text Text
    dgNodeLabels = Text -> Text -> Map Text Text -> Map Text Text
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert Text
    newNodeId Text
    label (Map Text Text -> Map Text Text)
    -> (DotGraph -> Map Text Text) -> DotGraph -> Map Text Text
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotGraph -> Map Text Text
    dgNodeLabels (DotGraph -> Map Text Text) -> DotGraph -> Map Text Text
    forall a b. (a -> b) -> a -> b
    $ DotGraph
    graph
                    }
                  }
                (Text, Bool) -> DotM n (Text, Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text
    newNodeId, Bool
    True)

    -- | Add an arc from importer to imported.
    addConnection :: NodeId -> NodeId -> DotM n ()
    addConnection :: forall n. Text -> Text -> DotM n ()
    addConnection Text
    m1 Text
    m2 = (DotState n -> DotState n)
    -> ReaderT (Env n) (State (DotState n)) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((DotState n -> DotState n)
     -> ReaderT (Env n) (State (DotState n)) ())
    -> (DotState n -> DotState n)
    -> ReaderT (Env n) (State (DotState n)) ()
    forall a b. (a -> b) -> a -> b
    $ \DotState n
    s -> DotState n
    s
      { dsGraph :: DotGraph
    dsGraph = (DotState n -> DotGraph
    forall n. DotState n -> DotGraph
    dsGraph DotState n
    s)
        { dgEdges :: Set (Text, Text)
    dgEdges = (Text, Text) -> Set (Text, Text) -> Set (Text, Text)
    forall a. Ord a => a -> Set a -> Set a
    S.insert (Text
    m1, Text
    m2) (Set (Text, Text) -> Set (Text, Text))
    -> (DotState n -> Set (Text, Text))
    -> DotState n
    -> Set (Text, Text)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotGraph -> Set (Text, Text)
    dgEdges (DotGraph -> Set (Text, Text))
    -> (DotState n -> DotGraph) -> DotState n -> Set (Text, Text)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DotState n -> DotGraph
    forall n. DotState n -> DotGraph
    dsGraph (DotState n -> Set (Text, Text)) -> DotState n -> Set (Text, Text)
    forall a b. (a -> b) -> a -> b
    $ DotState n
    s
        }
      }

    dottify :: Ord n => Env n -> n -> DotGraph
    dottify :: forall n. Ord n => Env n -> n -> DotGraph
    dottify Env n
    env n
    root = Env n -> DotM n Text -> DotGraph
    forall n x. Env n -> DotM n x -> DotGraph
    runDotM Env n
    env (n -> DotM n Text
    forall n. Ord n => n -> DotM n Text
    dottify' n
    root)

    dottify' :: Ord n => n -> DotM n NodeId
    dottify' :: forall n. Ord n => n -> DotM n Text
    dottify' n
    entity = do
      (Text
    nodeId, Bool
    continue) <- n -> DotM n (Text, Bool)
    forall n. Ord n => n -> DotM n (Text, Bool)
    addEntity n
    entity
      -- If we have not visited this interface yet,
      -- process its imports recursively and
      -- add them as connections to the graph.
      Bool
    -> ReaderT (Env n) (State (DotState n)) ()
    -> ReaderT (Env n) (State (DotState n)) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    continue (ReaderT (Env n) (State (DotState n)) ()
     -> ReaderT (Env n) (State (DotState n)) ())
    -> ReaderT (Env n) (State (DotState n)) ()
    -> ReaderT (Env n) (State (DotState n)) ()
    forall a b. (a -> b) -> a -> b
    $ do
        [n]
    connectedEntities <- n -> DotM n [n]
    forall n. n -> DotM n [n]
    getConnections n
    entity
        [Text]
    connectedNodeIds <- (n -> DotM n Text)
    -> [n] -> ReaderT (Env n) (State (DotState n)) [Text]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM n -> DotM n Text
    forall n. Ord n => n -> DotM n Text
    dottify' [n]
    connectedEntities
        (Text -> ReaderT (Env n) (State (DotState n)) ())
    -> [Text] -> ReaderT (Env n) (State (DotState n)) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Text -> Text -> ReaderT (Env n) (State (DotState n)) ()
    forall n. Text -> Text -> DotM n ()
    addConnection Text
    nodeId) [Text]
    connectedNodeIds
      Text -> DotM n Text
    forall (m :: * -> *) a. Monad m => a -> m a
    return Text
    nodeId

    -- * 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
    "   ", Text
    nodeId, Text
    "[label=\"", Text
    label, Text
    "\"];"]
        | (Text
    nodeId, Text
    label) <- Map Text Text -> [(Text, Text)]
    forall k a. Map k a -> [(k, a)]
    M.toList (DotGraph -> Map Text Text
    dgNodeLabels DotGraph
    g) ]
      , [ [Text] -> Text
    L.concat [Text
    "   ", Text
    r1, Text
    " -> ", Text
    r2, Text
    ";"]
        | (Text
    r1 , Text
    r2) <- Set (Text, Text) -> [(Text, Text)]
    forall a. Set a -> [a]
    S.toList (DotGraph -> Set (Text, Text)
    dgEdges DotGraph
    g) ]
      , [Text
    "}"]
      ]

    renderDotToFile :: MonadIO m => DotGraph -> FilePath -> m ()
    renderDotToFile :: forall (m :: * -> *). MonadIO m => DotGraph -> String -> m ()
    renderDotToFile DotGraph
    dot String
    fp = IO () -> m ()
    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