~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Interaction/Highlighting/Dot.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
1
1
{-# LANGUAGE CPP #-}
 
2
 
 
3
-- | Generate an import dependency graph for a given module.
 
4
 
2
5
module Agda.Interaction.Highlighting.Dot where
3
6
 
4
7
import Control.Applicative
12
15
import qualified Data.Set as S
13
16
import Data.Set (Set)
14
17
 
15
 
import System.Directory
16
 
import System.FilePath
17
 
 
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
24
21
 
25
 
import Agda.Utils.FileName
26
 
 
27
 
 
28
22
#include "../../undefined.h"
29
23
import Agda.Utils.Impossible
30
24
 
 
25
-- | Internal module identifiers for construction of dependency graph.
 
26
type ModuleId = String
 
27
 
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.
35
36
  }
36
37
 
37
38
initialDotState :: DotState
43
44
 
44
45
type DotM = StateT DotState TCM
45
46
 
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)
47
51
addModule m = do
48
52
    s <- get
49
53
    case M.lookup m (dsModules s) of
56
60
              }
57
61
            return (newName, True)
58
62
 
59
 
 
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)}
62
66
 
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
64
70
dottify inter = do
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.
68
76
    when continue $ do
 
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
71
81
    return name
72
82
 
73
 
 
 
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
77
89
        dottify inter
78
 
    mfile <- optDependencyGraph <$> commandLineOptions
79
 
    case mfile of
80
 
        Nothing -> __IMPOSSIBLE__
81
 
        Just fp -> liftIO $ writeFile fp $ mkDot state
 
90
    fp <- fromMaybe __IMPOSSIBLE__ . optDependencyGraph <$> commandLineOptions
 
91
    liftIO $ writeFile fp $ mkDot state
82
92
  where
83
93
    mkDot :: DotState -> String
84
94
    mkDot st = unlines $