{-# LANGUAGE CPP #-}
module Agda.Interaction.Highlighting.Dot where
import Control.Monad.State
import qualified Data.Map as M
import Data.Map(Map)
import Data.Maybe
import Data.Monoid
import qualified Data.Set as S
import Data.Set (Set)
import Agda.Interaction.Options
import Agda.Syntax.Abstract
import Agda.TypeChecking.Monad
#include "undefined.h"
import Agda.Utils.Impossible
type ModuleId = String
data DotState = DotState
{ dsModules :: Map ModuleName ModuleId
, dsNameSupply :: [ModuleId]
, dsConnection :: Set (ModuleId, ModuleId)
}
initialDotState :: DotState
initialDotState = DotState
{ dsModules = mempty
, dsNameSupply = map (('m':) . show) [0..]
, dsConnection = mempty
}
type DotM = StateT DotState TCM
addModule :: ModuleName -> DotM (ModuleId, Bool)
addModule m = do
s <- get
case M.lookup m (dsModules s) of
Just r -> return (r, False)
Nothing -> do
let newName:nameSupply = dsNameSupply s
put s
{ dsModules = M.insert m newName (dsModules s)
, dsNameSupply = nameSupply
}
return (newName, True)
addConnection :: ModuleId -> ModuleId -> DotM ()
addConnection m1 m2 = modify $ \s -> s {dsConnection = S.insert (m1,m2) (dsConnection s)}
dottify :: Interface -> DotM ModuleId
dottify inter = do
let curModule = iModuleName inter
(name, continue) <- addModule curModule
when continue $ do
importsifs <- lift $ map miInterface . catMaybes <$>
mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules inter)
imports <- mapM dottify importsifs
mapM_ (addConnection name) imports
return name
generateDot :: Interface -> TCM ()
generateDot inter = do
(top, state) <- flip runStateT initialDotState $ do
dottify inter
fp <- fromMaybe __IMPOSSIBLE__ . optDependencyGraph <$> commandLineOptions
liftIO $ writeFile fp $ mkDot state
where
mkDot :: DotState -> String
mkDot st = unlines $
[ "digraph dependencies {"
] ++ [" " ++ repr ++ "[label=\"" ++ show (mnameToConcrete modulename) ++ "\"];"
| (modulename, repr) <- M.toList (dsModules st)]
++ [" " ++ r1 ++ " -> " ++ r2 ++ ";"
| (r1 , r2) <- S.toList (dsConnection st) ]
++ ["}"]