{-# 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 NodeId NodeId
dgNodeLabels :: Map NodeId L.Text
  , DotGraph -> Set (NodeId, NodeId)
dgEdges      :: Set (NodeId, NodeId)
  }

-- * Graph construction monad

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

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

initialDotState :: DotState n
initialDotState :: DotState n
initialDotState = DotState :: forall n. Map n NodeId -> [NodeId] -> DotGraph -> DotState n
DotState
  { dsNodeIds :: Map n NodeId
dsNodeIds      = Map n NodeId
forall k a. Map k a
M.empty
  , dsNodeIdSupply :: [NodeId]
dsNodeIdSupply = (Integer -> NodeId) -> [Integer] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map (String -> NodeId
L.pack (String -> NodeId) -> (Integer -> String) -> Integer -> NodeId
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 NodeId NodeId -> Set (NodeId, NodeId) -> DotGraph
DotGraph Map NodeId NodeId
forall a. Monoid a => a
mempty Set (NodeId, NodeId)
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 :: Env n -> DotM n x -> DotGraph
runDotM env :: Env n
env@Env{} = DotState n -> DotGraph
forall n. DotState n -> DotGraph
dsGraph (DotState n -> DotGraph)
-> (DotM n x -> DotState n) -> DotM n 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)
-> (DotM n x -> State (DotState n) x) -> DotM n x -> DotState n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DotM n x -> Env n -> State (DotState n) x)
-> Env n -> DotM n x -> State (DotState n) x
forall a b c. (a -> b -> c) -> b -> a -> c
flip DotM n 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 :: n -> DotM n NodeId
getLabel = (Env n -> n -> NodeId)
-> ReaderT (Env n) (State (DotState n)) (Env n)
-> ReaderT (Env n) (State (DotState n)) n
-> DotM n NodeId
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Env n -> n -> NodeId
forall n. Env n -> n -> NodeId
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 -> DotM n NodeId)
-> (n -> ReaderT (Env n) (State (DotState n)) n)
-> n
-> DotM n NodeId
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 :: n -> DotM n [n]
getConnections = (Env n -> n -> [n])
-> ReaderT (Env n) (State (DotState n)) (Env n)
-> ReaderT (Env n) (State (DotState n)) n
-> DotM 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 -> DotM n [n])
-> (n -> ReaderT (Env n) (State (DotState n)) n) -> n -> DotM 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 :: n -> DotM n (NodeId, Bool)
addEntity n
name = do
    s :: DotState n
s@(DotState Map n NodeId
nodeIds [NodeId]
nodeIdSupply DotGraph
graph) <- ReaderT (Env n) (State (DotState n)) (DotState n)
forall s (m :: * -> *). MonadState s m => m s
get
    case n -> Map n NodeId -> Maybe NodeId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup n
name Map n NodeId
nodeIds of
        Just NodeId
nodeId  -> (NodeId, Bool) -> DotM n (NodeId, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeId
nodeId, Bool
False)
        Maybe NodeId
Nothing -> do
            let NodeId
newNodeId:[NodeId]
remainingNodeIdSupply = [NodeId]
nodeIdSupply
            NodeId
label <- n -> DotM n NodeId
forall n. n -> DotM n NodeId
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 NodeId
dsNodeIds      = n -> NodeId -> Map n NodeId -> Map n NodeId
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert n
name NodeId
newNodeId Map n NodeId
nodeIds
              , dsNodeIdSupply :: [NodeId]
dsNodeIdSupply = [NodeId]
remainingNodeIdSupply
              , dsGraph :: DotGraph
dsGraph        = DotGraph
graph
                { dgNodeLabels :: Map NodeId NodeId
dgNodeLabels = NodeId -> NodeId -> Map NodeId NodeId -> Map NodeId NodeId
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert NodeId
newNodeId NodeId
label (Map NodeId NodeId -> Map NodeId NodeId)
-> (DotGraph -> Map NodeId NodeId) -> DotGraph -> Map NodeId NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Map NodeId NodeId
dgNodeLabels (DotGraph -> Map NodeId NodeId) -> DotGraph -> Map NodeId NodeId
forall a b. (a -> b) -> a -> b
$ DotGraph
graph
                }
              }
            (NodeId, Bool) -> DotM n (NodeId, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (NodeId
newNodeId, Bool
True)

-- | Add an arc from importer to imported.
addConnection :: NodeId -> NodeId -> DotM n ()
addConnection :: NodeId -> NodeId -> DotM n ()
addConnection NodeId
m1 NodeId
m2 = (DotState n -> DotState n) -> DotM n ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DotState n -> DotState n) -> DotM n ())
-> (DotState n -> DotState n) -> DotM 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 (NodeId, NodeId)
dgEdges = (NodeId, NodeId) -> Set (NodeId, NodeId) -> Set (NodeId, NodeId)
forall a. Ord a => a -> Set a -> Set a
S.insert (NodeId
m1, NodeId
m2) (Set (NodeId, NodeId) -> Set (NodeId, NodeId))
-> (DotState n -> Set (NodeId, NodeId))
-> DotState n
-> Set (NodeId, NodeId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Set (NodeId, NodeId)
dgEdges (DotGraph -> Set (NodeId, NodeId))
-> (DotState n -> DotGraph) -> DotState n -> Set (NodeId, NodeId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotState n -> DotGraph
forall n. DotState n -> DotGraph
dsGraph (DotState n -> Set (NodeId, NodeId))
-> DotState n -> Set (NodeId, NodeId)
forall a b. (a -> b) -> a -> b
$ DotState n
s
    }
  }

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

dottify' :: Ord n => n -> DotM n NodeId
dottify' :: n -> DotM n NodeId
dottify' n
entity = do
  (NodeId
nodeId, Bool
continue) <- n -> DotM n (NodeId, Bool)
forall n. Ord n => n -> DotM n (NodeId, 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
    [NodeId]
connectedNodeIds <- (n -> DotM n NodeId)
-> [n] -> ReaderT (Env n) (State (DotState n)) [NodeId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM n -> DotM n NodeId
forall n. Ord n => n -> DotM n NodeId
dottify' [n]
connectedEntities
    (NodeId -> ReaderT (Env n) (State (DotState n)) ())
-> [NodeId] -> ReaderT (Env n) (State (DotState n)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (NodeId -> NodeId -> ReaderT (Env n) (State (DotState n)) ()
forall n. NodeId -> NodeId -> DotM n ()
addConnection NodeId
nodeId) [NodeId]
connectedNodeIds
  NodeId -> DotM n NodeId
forall (m :: * -> *) a. Monad m => a -> m a
return NodeId
nodeId

-- * Graph rendering

renderDot :: DotGraph -> L.Text
renderDot :: DotGraph -> NodeId
renderDot DotGraph
g = [NodeId] -> NodeId
L.unlines ([NodeId] -> NodeId) -> [NodeId] -> NodeId
forall a b. (a -> b) -> a -> b
$ [[NodeId]] -> [NodeId]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [ NodeId
"digraph dependencies {" ]
  , [ [NodeId] -> NodeId
L.concat [NodeId
"   ", NodeId
nodeId, NodeId
"[label=\"", NodeId
label, NodeId
"\"];"]
    | (NodeId
nodeId, NodeId
label) <- Map NodeId NodeId -> [(NodeId, NodeId)]
forall k a. Map k a -> [(k, a)]
M.toList (DotGraph -> Map NodeId NodeId
dgNodeLabels DotGraph
g) ]
  , [ [NodeId] -> NodeId
L.concat [NodeId
"   ", NodeId
r1, NodeId
" -> ", NodeId
r2, NodeId
";"]
    | (NodeId
r1 , NodeId
r2) <- Set (NodeId, NodeId) -> [(NodeId, NodeId)]
forall a. Set a -> [a]
S.toList (DotGraph -> Set (NodeId, NodeId)
dgEdges DotGraph
g) ]
  , [NodeId
"}"]
  ]

renderDotToFile :: MonadIO m => DotGraph -> FilePath -> m ()
renderDotToFile :: 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
$ NodeId -> ByteString
E.encodeUtf8 (NodeId -> ByteString) -> NodeId -> ByteString
forall a b. (a -> b) -> a -> b
$ DotGraph -> NodeId
renderDot DotGraph
dot