Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.Dot

Description

Generate an import dependency graph for a given module.

Synopsis

- type ModuleId = String
- data DotState = DotState {
  - dsModules :: Map ModuleName ModuleId
  - dsNameSupply :: [ModuleId]
  - dsConnection :: Set (ModuleId, ModuleId)
  }
- initialDotState :: DotState
- type DotM = StateT DotState TCM
- addModule :: ModuleName -> DotM (ModuleId, Bool)
- addConnection :: ModuleId -> ModuleId -> DotM ()
- dottify :: Interface -> DotM ModuleId
- generateDot :: Interface -> TCM ()

# Documentation

type ModuleId = String Source #

Internal module identifiers for construction of dependency graph.

data DotState Source #

Constructors

DotState |

Fields

- dsModules :: Map ModuleName ModuleId

  Records already processed modules and maps them to an internal identifier.

- dsNameSupply :: [ModuleId]

  Supply of internal identifiers.

- dsConnection :: Set (ModuleId, ModuleId)

  Edges of dependency graph.

initialDotState :: DotState Source #

type DotM = StateT DotState TCM Source #

addModule :: ModuleName -> DotM (ModuleId, Bool) Source #

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.

addConnection :: ModuleId -> ModuleId -> DotM () Source #

Add an arc from importer to imported.

dottify :: Interface -> DotM ModuleId Source #

Recursively build import graph, starting from given `Interface`. Modifies the state in `DotM` and returns the `ModuleId` of the `Interface`.

generateDot :: Interface -> TCM () Source #

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.