Hets - the Heterogeneous Tool Set

Copyright(c) Igor Stassiy, DFKI Bremen 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Proofs.DGFlattening

Description

In this module we introduce flattening of the graph:

Flattening importings - deleting all inclusion links, and inserting a new node, with new computed theory (computeTheory).

Flattening non-disjoint unions - for each node with more than two importings modify importings in such a way that at each level, only non-disjoint signatures are imported.

Flattening renaming - deterimining renaming link, inserting a new node with the renaming morphism applied to theory of a source, deleting the link and setting a new inclusion link between a new node and the target node.

Flattening hiding links - for each compute normal form if there is such and eliminate hiding links.

Flattening heterogeneity - for each heterogeneous link, compute theory of a target node and eliminate heterogeneous link.

Documentation