12
15
import qualified Data.Set as S
13
16
import Data.Set (Set)
15
import System.Directory
16
import System.FilePath
18
import qualified Agda.Syntax.Concrete.Name as CN
19
import Agda.Interaction.FindFile
20
18
import Agda.Interaction.Options
21
19
import Agda.Syntax.Abstract
22
import Agda.Syntax.Abstract.Name
23
20
import Agda.TypeChecking.Monad
25
import Agda.Utils.FileName
28
22
#include "../../undefined.h"
29
23
import Agda.Utils.Impossible
25
-- | Internal module identifiers for construction of dependency graph.
26
type ModuleId = String
31
28
data DotState = DotState
32
{ dsModules :: Map ModuleName String
33
, dsNameSupply :: [String]
34
, dsConnection :: Set (String, String)
29
{ dsModules :: Map ModuleName ModuleId
30
-- ^ Records already processed modules
31
-- and maps them to an internal identifier.
32
, dsNameSupply :: [ModuleId]
33
-- ^ Supply of internal identifiers.
34
, dsConnection :: Set (ModuleId, ModuleId)
35
-- ^ Edges of dependency graph.
37
38
initialDotState :: DotState
44
45
type DotM = StateT DotState TCM
46
addModule :: ModuleName -> DotM (String, Bool)
47
-- | Translate a 'ModuleName' to an internal 'ModuleId'.
48
-- Returns @True@ if the 'ModuleName' is new, i.e., has not been
49
-- encountered before and is thus added to the map of processed modules.
50
addModule :: ModuleName -> DotM (ModuleId, Bool)
49
53
case M.lookup m (dsModules s) of
57
61
return (newName, True)
60
addConnection :: String -> String -> DotM ()
63
-- | Add an arc from importer to imported.
64
addConnection :: ModuleId -> ModuleId -> DotM ()
61
65
addConnection m1 m2 = modify $ \s -> s {dsConnection = S.insert (m1,m2) (dsConnection s)}
63
dottify :: Interface -> DotM String
67
-- | Recursively build import graph, starting from given 'Interface'.
68
-- Modifies the state in 'DotM' and returns the 'ModuleId' of the 'Interface'.
69
dottify :: Interface -> DotM ModuleId
65
71
let curModule = iModuleName inter
66
72
(name, continue) <- addModule curModule
67
importsifs <- lift $ map miInterface . catMaybes <$> mapM (getVisitedModule . toTopLevelModuleName) (iImportedModules inter)
73
-- If we have not visited this interface yet,
74
-- process its imports recursively and
75
-- add them as connections to the graph.
77
importsifs <- lift $ map miInterface . catMaybes <$>
78
mapM (getVisitedModule . toTopLevelModuleName . fst) (iImportedModules inter)
69
79
imports <- mapM dottify importsifs
70
80
mapM_ (addConnection name) imports
83
-- | Generate a .dot file for the import graph starting with the
84
-- given 'Interface' and write it to the file specified by the
85
-- command line option.
74
86
generateDot :: Interface -> TCM ()
75
87
generateDot inter = do
76
88
(top, state) <- flip runStateT initialDotState $ do
78
mfile <- optDependencyGraph <$> commandLineOptions
80
Nothing -> __IMPOSSIBLE__
81
Just fp -> liftIO $ writeFile fp $ mkDot state
90
fp <- fromMaybe __IMPOSSIBLE__ . optDependencyGraph <$> commandLineOptions
91
liftIO $ writeFile fp $ mkDot state
83
93
mkDot :: DotState -> String
84
94
mkDot st = unlines $