Safe Haskell	Safe
Language	Haskell2010

FreeC.IR.DependencyGraph

Contents

Dependency Graph
Strongly Connected Components
- Constructors
- Manipulating

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

type DGKey = QName Source #

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 dgGraph :: Graph The actual graph. dgGetEntry :: Vertex -> DGEntry node Gets an entry for a vertex of the graph. dgGetVertex :: DGKey -> Maybe Vertex Gets the vertex of a node with the given key.

Instances

Pretty (DependencyGraph node) Source #	Pretty instance that converts a dependency graph to the DOT format.
Instance details Defined in FreeC.IR.DependencyGraph Methods pretty :: DependencyGraph node -> Doc # prettyList :: [DependencyGraph node] -> Doc #

Getters

dgEntries :: DependencyGraph node -> [DGEntry node] Source #

Gets the entries of the given dependency graph.

Predicates

dependsDirectlyOn Source #

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 SCC decl is that the constructors have been renamed to be more explanatory in the context of dependency analysis.

Constructors

NonRecursive decl	A single non-recursive declaration.
Recursive [decl]	A list of mutually recursive declarations.

Instances

Show decl => Show (DependencyComponent decl) Source #
Instance details Defined in FreeC.IR.DependencyGraph Methods showsPrec :: Int -> DependencyComponent decl -> ShowS Source # show :: DependencyComponent decl -> String Source # showList :: [DependencyComponent decl] -> ShowS Source #
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.
Instance details Defined in FreeC.IR.DependencyGraph Methods pretty :: DependencyComponent decl -> Doc # prettyList :: [DependencyComponent decl] -> Doc #

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 DependencyComponents 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.