Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
FreeC.IR.DependencyGraph
Contents
Description
This module contains functions to construct dependency graphs of
declarations and modules of the intermediate language. A dependency graph
is a directed graph whose nodes are labeled with declarations. There is an
edge from node A
to B
if the declaration of A
depends on the
declaration of B
(i.e. in Coq B
has to be defined before A
or both
have to be declared in the same sentence). The module dependency graph
contains an edge from node A
to B
if the module of A
contains an
import
declaration for the module of B
.
The dependency graph does only contain defined top-level declarations
(i.e. there are no nodes for imported or built-in data types or operations
and there are no nodes for local variables such as function parameters or
variable patterns). However, the entries of the dependency graph contain
keys for predefined functions (but not local variables) as well as the
special functions error
and undefined
that are used in error terms.
We distinguish between the type and value dependency graph. This is because function declarations and type declarations live in separate scopes but we want to avoid name conflicts. Since we assume all type declarations to precede function declarations in the generated Coq code, this separation of the dependency graphs should not be a problem. For the same reason, the value dependency graph does not include nodes for constructors (as always, the keys of used constructors are still present).
The construction of a dependency graph does not fail even if there are are undefined identifiers. The dependency graph does not know about the environment, it only knows which (type) constructors and (type) variables occur freely in the declarations. Most importantly, that means that it does not know about the module system. Thus, dependency analysis should not be performed before all references have been resolved to their original (qualified) identifiers.
For debugging purposes, dependency graphs can be converted to the DOT format such that they can be visualized using Graphviz (See https://www.graphviz.org/).
Synopsis
- type DGKey = QName
- type DGEntry node = (node, DGKey, [DGKey])
- data DependencyGraph node = DependencyGraph {
- dgGraph :: Graph
- dgGetEntry :: Vertex -> DGEntry node
- dgGetVertex :: DGKey -> Maybe Vertex
- dgEntries :: DependencyGraph node -> [DGEntry node]
- dependsDirectlyOn :: DependencyGraph node -> DGKey -> DGKey -> Bool
- typeDependencyGraph :: (HasRefs node, HasDeclIdent node) => [node] -> DependencyGraph node
- valueDependencyGraph :: (HasRefs node, HasDeclIdent node) => [node] -> DependencyGraph node
- moduleDependencyGraph :: [ModuleOf decls] -> DependencyGraph (ModuleOf decls)
- data DependencyComponent decl
- = NonRecursive decl
- | Recursive [decl]
- unwrapComponent :: DependencyComponent decl -> [decl]
- dependencyComponents :: DependencyGraph a -> [DependencyComponent a]
- typeDependencyComponents :: (HasRefs node, HasDeclIdent node) => [node] -> [DependencyComponent node]
- valueDependencyComponents :: (HasRefs node, HasDeclIdent node) => [node] -> [DependencyComponent node]
- groupModules :: [ModuleOf decls] -> [DependencyComponent (ModuleOf decls)]
- mapComponent :: ([decl] -> [decl']) -> DependencyComponent decl -> DependencyComponent decl'
- mapComponentM :: MonadFail m => ([decl] -> m [decl']) -> DependencyComponent decl -> m (DependencyComponent decl')
- mapComponentM_ :: MonadFail m => ([decl] -> m a) -> DependencyComponent decl -> m ()
Dependency Graph
Every node of the dependency graph is uniquely identified by a key. We use their qualified original name to identify declarations.
type DGEntry node = (node, DGKey, [DGKey]) Source #
Every node (i.e., declaration) in a dependency graph is associated with a unique key (its qualified original name) and a list of keys that identify the nodes this node depends on (adjacency list).
data DependencyGraph node Source #
A dependency graph is a directed graph whose nodes are declarations
(Usually TypeDecl
or FuncDecl
). There is an edge from node
A
to node B
if the declaration of A
depends on B
.
Nodes are identified by their qualified original name (See DGKey
).
Internally, nodes are identified by a number (See Vertex
).
In addition to the actual Graph
that stores the adjacency matrix
of the internal identifiers, this data type contains functions to convert
between the internal and high level representation.
Constructors
DependencyGraph | |
Fields
|
Instances
Pretty (DependencyGraph node) Source # | Pretty instance that converts a dependency graph to the DOT format. |
Defined in FreeC.IR.DependencyGraph |
Getters
dgEntries :: DependencyGraph node -> [DGEntry node] Source #
Gets the entries of the given dependency graph.
Predicates
Arguments
:: DependencyGraph node | The dependency graph. |
-> DGKey | The key of the first node. |
-> DGKey | The key of the second node. |
-> Bool |
Tests whether two nodes (identified by the given keys) of the dependency graph depend on each other directly (i.e., there is an edge from the first node to the second node).
Returns False
if one of the nodes does not exist.
Constructors
typeDependencyGraph :: (HasRefs node, HasDeclIdent node) => [node] -> DependencyGraph node Source #
Creates the type dependency graph for a list of nodes.
valueDependencyGraph :: (HasRefs node, HasDeclIdent node) => [node] -> DependencyGraph node Source #
Creates the dependency graph for a list of function declarations.
moduleDependencyGraph :: [ModuleOf decls] -> DependencyGraph (ModuleOf decls) Source #
Creates the dependency graph for the given modules.
Strongly Connected Components
data DependencyComponent decl Source #
A strongly connected component of the dependency graph.
All declarations that mutually depend on each other are in the same strongly connected component.
The only difference to
is that the constructors have been
renamed to be more explanatory in the context of dependency analysis.SCC
decl
Constructors
NonRecursive decl | A single non-recursive declaration. |
Recursive [decl] | A list of mutually recursive declarations. |
Instances
Show decl => Show (DependencyComponent decl) Source # | |
Defined in FreeC.IR.DependencyGraph | |
Pretty decl => Pretty (DependencyComponent decl) Source # | Pretty instance that pretty prints the declarations of a strongly connected component. Each declaration is on its own line and indented by two spaces. The first line of the document indicates whether the component was recursive or not. |
Defined in FreeC.IR.DependencyGraph |
unwrapComponent :: DependencyComponent decl -> [decl] Source #
Gets the declarations wrapped by the given strongly connected component.
Constructors
dependencyComponents :: DependencyGraph a -> [DependencyComponent a] Source #
Computes the strongly connected components of the given dependency graph.
Each strongly connected component corresponds either to a set of mutually recursive declarations or a single non-recursive declaration.
The returned list of strongly connected components is in reverse
topological order, i.e. if any declaration in a strongly connected
component B
depends on a declaration in a strongly connected component
A
, then A
precedes B
in the returned list.
If two components do not depend on each other, they are in reverse alphabetical order.
typeDependencyComponents :: (HasRefs node, HasDeclIdent node) => [node] -> [DependencyComponent node] Source #
Combines the construction of the type dependency graph with the computation of strongly connected components.
valueDependencyComponents :: (HasRefs node, HasDeclIdent node) => [node] -> [DependencyComponent node] Source #
Combines the construction of the value dependency graph with the computation of strongly connected components.
groupModules :: [ModuleOf decls] -> [DependencyComponent (ModuleOf decls)] Source #
Combines the construction of the dependency graph for the given
modules (See moduleDependencyGraph
) with the computation of strongly
connected components.
Since cyclic module dependencies are not allowed, all
DependencyComponent
s in the returned list should be NonRecursive
.
Otherwise, there is a module dependency error.
Manipulating
mapComponent :: ([decl] -> [decl']) -> DependencyComponent decl -> DependencyComponent decl' Source #
Applies the given function to the declarations in the given strongly connected component of the dependency graph.
In case of a NonRecursive
component, the function is given a singleton
list. The given function must not change the number of declarations in the
component.
mapComponentM :: MonadFail m => ([decl] -> m [decl']) -> DependencyComponent decl -> m (DependencyComponent decl') Source #
Monadic version of mapComponent
.
There must be a MonadFail
instance since this function fails if the
given function changes the number of declarations in a non-recursive
strongly connected component.
mapComponentM_ :: MonadFail m => ([decl] -> m a) -> DependencyComponent decl -> m () Source #
Like mapComponentM
but discards the result.