-- | Generate an import dependency graph for a given module.

module Agda.Interaction.Highlighting.Dot where

import Control.Monad.State

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

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

import Agda.Interaction.Options
import Agda.Syntax.Abstract
import Agda.TypeChecking.Monad

import Agda.Utils.Impossible

-- | Internal module identifiers for construction of dependency graph.
type ModuleId = String

data DotState = DotState
  { DotState -> Map ModuleName ModuleId
dsModules    :: Map ModuleName ModuleId
    -- ^ Records already processed modules
    --   and maps them to an internal identifier.
  , DotState -> [ModuleId]
dsNameSupply :: [ModuleId]
    -- ^ Supply of internal identifiers.
  , DotState -> Set (ModuleId, ModuleId)
dsConnection :: Set (ModuleId, ModuleId)
    -- ^ Edges of dependency graph.
  }

initialDotState :: DotState
initialDotState :: DotState
initialDotState = DotState :: Map ModuleName ModuleId
-> [ModuleId] -> Set (ModuleId, ModuleId) -> DotState
DotState
  { dsModules :: Map ModuleName ModuleId
dsModules    = Map ModuleName ModuleId
forall a. Monoid a => a
mempty
  , dsNameSupply :: [ModuleId]
dsNameSupply = (Integer -> ModuleId) -> [Integer] -> [ModuleId]
forall a b. (a -> b) -> [a] -> [b]
map ((Char
'm'Char -> ModuleId -> ModuleId
forall a. a -> [a] -> [a]
:) (ModuleId -> ModuleId)
-> (Integer -> ModuleId) -> Integer -> ModuleId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ModuleId
forall a. Show a => a -> ModuleId
show) [Integer
0..]
  , dsConnection :: Set (ModuleId, ModuleId)
dsConnection = Set (ModuleId, ModuleId)
forall a. Monoid a => a
mempty
  }

type DotM = StateT DotState TCM

-- | Translate a 'ModuleName' to an internal 'ModuleId'.
--   Returns @True@ if the 'ModuleName' is new, i.e., has not been
--   encountered before and is thus added to the map of processed modules.
addModule :: ModuleName -> DotM (ModuleId, Bool)
addModule :: ModuleName -> DotM (ModuleId, Bool)
addModule ModuleName
m = do
    DotState
s <- StateT DotState TCM DotState
forall s (m :: * -> *). MonadState s m => m s
get
    case ModuleName -> Map ModuleName ModuleId -> Maybe ModuleId
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ModuleName
m (DotState -> Map ModuleName ModuleId
dsModules DotState
s) of
        Just ModuleId
r  -> (ModuleId, Bool) -> DotM (ModuleId, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleId
r, Bool
False)
        Maybe ModuleId
Nothing -> do
            let ModuleId
newName:[ModuleId]
nameSupply = DotState -> [ModuleId]
dsNameSupply DotState
s
            DotState -> StateT DotState TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put DotState
s
              { dsModules :: Map ModuleName ModuleId
dsModules = ModuleName
-> ModuleId -> Map ModuleName ModuleId -> Map ModuleName ModuleId
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ModuleName
m ModuleId
newName (DotState -> Map ModuleName ModuleId
dsModules DotState
s)
              , dsNameSupply :: [ModuleId]
dsNameSupply = [ModuleId]
nameSupply
              }
            (ModuleId, Bool) -> DotM (ModuleId, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleId
newName, Bool
True)

-- | Add an arc from importer to imported.
addConnection :: ModuleId -> ModuleId -> DotM ()
addConnection :: ModuleId -> ModuleId -> StateT DotState TCM ()
addConnection ModuleId
m1 ModuleId
m2 = (DotState -> DotState) -> StateT DotState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DotState -> DotState) -> StateT DotState TCM ())
-> (DotState -> DotState) -> StateT DotState TCM ()
forall a b. (a -> b) -> a -> b
$ \DotState
s -> DotState
s {dsConnection :: Set (ModuleId, ModuleId)
dsConnection = (ModuleId, ModuleId)
-> Set (ModuleId, ModuleId) -> Set (ModuleId, ModuleId)
forall a. Ord a => a -> Set a -> Set a
S.insert (ModuleId
m1,ModuleId
m2) (DotState -> Set (ModuleId, ModuleId)
dsConnection DotState
s)}

-- | Recursively build import graph, starting from given 'Interface'.
--   Modifies the state in 'DotM' and returns the 'ModuleId' of the 'Interface'.
dottify :: Interface -> DotM ModuleId
dottify :: Interface -> DotM ModuleId
dottify Interface
inter = do
    let curModule :: ModuleName
curModule = Interface -> ModuleName
iModuleName Interface
inter
    (ModuleId
name, Bool
continue) <- ModuleName -> DotM (ModuleId, Bool)
addModule ModuleName
curModule
    -- If we have not visited this interface yet,
    -- process its imports recursively and
    -- add them as connections to the graph.
    Bool -> StateT DotState TCM () -> StateT DotState TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
continue (StateT DotState TCM () -> StateT DotState TCM ())
-> StateT DotState TCM () -> StateT DotState TCM ()
forall a b. (a -> b) -> a -> b
$ do
        [Interface]
importsifs <- TCMT IO [Interface] -> StateT DotState TCM [Interface]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [Interface] -> StateT DotState TCM [Interface])
-> TCMT IO [Interface] -> StateT DotState TCM [Interface]
forall a b. (a -> b) -> a -> b
$ (ModuleInfo -> Interface) -> [ModuleInfo] -> [Interface]
forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface ([ModuleInfo] -> [Interface])
-> ([Maybe ModuleInfo] -> [ModuleInfo])
-> [Maybe ModuleInfo]
-> [Interface]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe ModuleInfo] -> [ModuleInfo]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ModuleInfo] -> [Interface])
-> TCMT IO [Maybe ModuleInfo] -> TCMT IO [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          ((ModuleName, Hash) -> TCMT IO (Maybe ModuleInfo))
-> [(ModuleName, Hash)] -> TCMT IO [Maybe ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
getVisitedModule (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo))
-> ((ModuleName, Hash) -> TopLevelModuleName)
-> (ModuleName, Hash)
-> TCMT IO (Maybe ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ((ModuleName, Hash) -> ModuleName)
-> (ModuleName, Hash)
-> TopLevelModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst) (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
inter)
        [ModuleId]
imports    <- (Interface -> DotM ModuleId)
-> [Interface] -> StateT DotState TCM [ModuleId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Interface -> DotM ModuleId
dottify [Interface]
importsifs
        (ModuleId -> StateT DotState TCM ())
-> [ModuleId] -> StateT DotState TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ModuleId -> ModuleId -> StateT DotState TCM ()
addConnection ModuleId
name) [ModuleId]
imports
    ModuleId -> DotM ModuleId
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleId
name

-- | Generate a .dot file for the import graph starting with the
--   given 'Interface' and write it to the file specified by the
--   command line option.
generateDot :: Interface -> TCM ()
generateDot :: Interface -> TCM ()
generateDot Interface
inter = do
    (ModuleId
top, DotState
state) <- (DotM ModuleId -> DotState -> TCM (ModuleId, DotState))
-> DotState -> DotM ModuleId -> TCM (ModuleId, DotState)
forall a b c. (a -> b -> c) -> b -> a -> c
flip DotM ModuleId -> DotState -> TCM (ModuleId, DotState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT DotState
initialDotState (DotM ModuleId -> TCM (ModuleId, DotState))
-> DotM ModuleId -> TCM (ModuleId, DotState)
forall a b. (a -> b) -> a -> b
$ do
        Interface -> DotM ModuleId
dottify Interface
inter
    ModuleId
fp <- ModuleId -> Maybe ModuleId -> ModuleId
forall a. a -> Maybe a -> a
fromMaybe ModuleId
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ModuleId -> ModuleId)
-> (CommandLineOptions -> Maybe ModuleId)
-> CommandLineOptions
-> ModuleId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe ModuleId
optDependencyGraph (CommandLineOptions -> ModuleId)
-> TCMT IO CommandLineOptions -> TCMT IO ModuleId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
    IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleId -> ModuleId -> IO ()
writeFile ModuleId
fp (ModuleId -> IO ()) -> ModuleId -> IO ()
forall a b. (a -> b) -> a -> b
$ DotState -> ModuleId
mkDot DotState
state
  where
    mkDot :: DotState -> String
    mkDot :: DotState -> ModuleId
mkDot DotState
st = [ModuleId] -> ModuleId
unlines ([ModuleId] -> ModuleId) -> [ModuleId] -> ModuleId
forall a b. (a -> b) -> a -> b
$
        [ ModuleId
"digraph dependencies {"
        ] [ModuleId] -> [ModuleId] -> [ModuleId]
forall a. [a] -> [a] -> [a]
++ [ModuleId
"   " ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
repr ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
"[label=\"" ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ QName -> ModuleId
forall a. Show a => a -> ModuleId
show (ModuleName -> QName
mnameToConcrete ModuleName
modulename) ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
"\"];"
             | (ModuleName
modulename, ModuleId
repr) <- Map ModuleName ModuleId -> [(ModuleName, ModuleId)]
forall k a. Map k a -> [(k, a)]
M.toList (DotState -> Map ModuleName ModuleId
dsModules DotState
st)]
          [ModuleId] -> [ModuleId] -> [ModuleId]
forall a. [a] -> [a] -> [a]
++ [ModuleId
"   " ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
r1 ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
" -> " ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
r2 ModuleId -> ModuleId -> ModuleId
forall a. [a] -> [a] -> [a]
++ ModuleId
";"
             | (ModuleId
r1 , ModuleId
r2) <- Set (ModuleId, ModuleId) -> [(ModuleId, ModuleId)]
forall a. Set a -> [a]
S.toList (DotState -> Set (ModuleId, ModuleId)
dsConnection DotState
st) ]
          [ModuleId] -> [ModuleId] -> [ModuleId]
forall a. [a] -> [a] -> [a]
++ [ModuleId
"}"]