Hets - the Heterogeneous Tool Set

Copyright(c) Maciek Makowski Warsaw University 2004-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (Logic) Data types and functions for architectural diagrams Follows the CASL Reference Manual, section III.5.6. Extended to the new rules for lambda expressions(WADT2010).
Safe HaskellNone

Static.ArchDiagram

Contents

Description

 

Synopsis

Types (as defined for extended static semantics in Chap. III:5.6.1)

data DiagNodeSig Source #

Constructors

Diag_node_sig Node NodeSig 

Instances

Show DiagNodeSig Source # 

Methods

showsPrec :: Int -> DiagNodeSig -> ShowS

show :: DiagNodeSig -> String

showList :: [DiagNodeSig] -> ShowS

data MaybeDiagNode Source #

Instances

Show MaybeDiagNode Source # 

Methods

showsPrec :: Int -> MaybeDiagNode -> ShowS

show :: MaybeDiagNode -> String

showList :: [MaybeDiagNode] -> ShowS

getSigFromDiag :: DiagNodeSig -> NodeSig Source #

Return a signature stored within given diagram node sig

Functions

printDiag :: a -> String -> Diag -> Result a Source #

return the diagram

ctx :: ExtStUnitCtx -> RefStUnitCtx Source #

A mapping from extended to basic static unit context

insInclusionEdges Source #

Arguments

:: LogicGraph 
-> Diag

the diagram to insert edges to

-> [DiagNodeSig]

the source nodes

-> DiagNodeSig

the target node

-> Result Diag

the diagram with edges inserted

Insert the edges from given source nodes to given target node into the given diagram. The edges are labelled with inclusions.

insInclusionEdgesRev Source #

Arguments

:: LogicGraph 
-> Diag

the diagram to insert edges to

-> DiagNodeSig

the source node

-> [DiagNodeSig]

the target nodes

-> Result Diag

the diagram with edges inserted

Insert the edges from given source node to given target nodes into the given diagram. The edges are labelled with inclusions.

extendDiagramIncl Source #

Arguments

:: LogicGraph 
-> Diag

the diagram to be extended

-> [DiagNodeSig]

the nodes which should be linked to the new node

-> NodeSig

the signature with which the new node should be labelled

-> String

the node description (for diagnostics)

-> Result (DiagNodeSig, Diag) 

Build a diagram that extends given diagram with a node containing given signature and with edges from given set of nodes to the new node. The new edges are labelled with sigature inclusions.

returns the new node and the extended diagram

extendDGraph Source #

Arguments

:: DGraph

the development graph to be extended

-> NodeSig

the NodeSig from which the morphism originates

-> GMorphism

the morphism to be inserted

-> IRI

the name of the node to be inserted

-> DGOrigin 
-> Result (NodeSig, DGraph) 

Extend the development graph with given morphism originating from given NodeSig

returns the target signature of the morphism and the resulting DGraph

extendDGraphRev Source #

Arguments

:: DGraph

the development graph to be extended

-> NodeSig

the NodeSig to which the morphism points

-> GMorphism

the morphism to be inserted

-> IRI

the name of the node to be inserted

-> DGOrigin 
-> Result (NodeSig, DGraph) 

Extend the development graph with given morphism pointing to given NodeSig

returns the source signature of the morphism and the resulting DGraph

extendDGraphRevHide Source #

Arguments

:: DGraph

the development graph to be extended

-> NodeSig

the NodeSig to which the morphism points

-> GMorphism

the morphism to be inserted

-> IRI

the name of the node to be inserted

-> DGOrigin 
-> Result (NodeSig, DGraph) 

Extend the development graph with given morphism pointing to given NodeSig

returns the source signature of the morphism and the resulting DGraph

extendDiagramWithMorphismRevHide Source #

Arguments

:: Range

the position (for diagnostics)

-> LogicGraph 
-> Diag

the diagram to be extended

-> DGraph

the development graph

-> DiagNodeSig

the node to which the edge should point

-> GMorphism

the morphism as label for the new edge

-> IRI

the name of the node to be inserted

-> String

a diagnostic node description

-> DGOrigin

the origin of the new node

-> Result (DiagNodeSig, Diag, DGraph) 

returns the new node, the extended diagram and extended development graph

extendDiagramWithMorphism Source #

Arguments

:: Range

the position (for diagnostics)

-> LogicGraph 
-> Diag

the diagram to be extended

-> DGraph

the development graph

-> DiagNodeSig

the node from which the edge should originate

-> GMorphism

the morphism as label for the new edge

-> IRI

the name of the node to be inserted

-> String

the node description (for diagnostics)

-> DGOrigin

the origin of the new node

-> Result (DiagNodeSig, Diag, DGraph) 

Build a diagram that extends the given diagram with a node and an edge to that node. The edge is labelled with a given signature morphism and the node contains the target of this morphism. Extends the development graph with the given morphism as well.

returns the new node, the extended diagram and extended development graph

extendDiagramWithMorphismRev Source #

Arguments

:: Range

the position (for diagnostics)

-> LogicGraph 
-> Diag

the diagram to be extended

-> DGraph

the development graph

-> DiagNodeSig

the node to which the edge should point

-> GMorphism

the morphism as label for the new edge

-> String

a diagnostic node description

-> IRI

the name of the node to be inserted

-> DGOrigin

the origin of the new node

-> Result (DiagNodeSig, Diag, DGraph) 

Build a diagram that extends a given diagram with a node and an edge from that node. The edge is labelled with a given signature morphism and the node contains the source of this morphism. Extends the development graph with the given morphism as well.

returns the new node, the extended diagram and extended development graph

extendDiagram Source #

Arguments

:: Diag

the diagram to be extended

-> DiagNodeSig

the node from which morphism originates

-> GMorphism

the morphism as label for the new edge

-> NodeSig

the signature as label for the new node

-> String

the node description (for diagnostics)

-> Result (DiagNodeSig, Diag) 

Build a diagram that extends given diagram with a node containing given signature and with edge from given nodes to the new node. The new edge is labelled with given signature morphism.

returns the new node and the extended diagram

homogeniseDiagram Source #

Arguments

:: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree 
=> lid

the target logic to be coerced to

-> Diag

the diagram to be homogenised

-> Result (Gr sign (Int, morphism)) 

Convert a homogeneous diagram to a simple diagram where all the signatures in nodes and morphism on the edges are coerced to a common logic.

diagDesc :: Diag -> Gr String String Source #

Create a graph containing descriptions of nodes and edges.

inclusionSink Source #

Arguments

:: LogicGraph 
-> [DiagNodeSig]

the source nodes

-> NodeSig

the target signature

-> Result [(Node, GMorphism)] 

Create a sink consisting of incusion morphisms between signatures from given set of nodes and given signature.

returns the diagram with edges inserted

extendDiagramWithEdge Source #

Arguments

:: Range

the position (for diagnostics)

-> LogicGraph 
-> Diag

the diagram to be extended

-> DGraph

the development graph

-> DiagNodeSig

the node from which the edge should originate

-> DiagNodeSig

the target node of the edge

-> GMorphism

the morphism as label for the new edge

-> DGLinkOrigin

the origin of the new edge

-> Result (Diag, DGraph) 

Build a diagram that extends the given diagram with an edge between existing nodes. The edge is labelled with a given signature morphism. Extends the development graph with the given morphism as well.

returns the extended diagram and extended development graph

copyDiagram :: LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node) Source #

copyEdges :: [Node] -> Diag -> Map Node Node -> Map Edge Bool -> (Map Edge Bool, Diag) Source #

copyEdge :: Diag -> Map Node Node -> LEdge DiagLinkLab -> Map Edge Bool -> (Map Edge Bool, Diag) Source #

copyDiagramAux :: Map Node Node -> LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node) Source #

insertFormalParamAndVerifCond Source #

Arguments

:: Range

the position (for diagnostics)

-> LogicGraph 
-> Diag

the diagram to be extended

-> DGraph

the development graph

-> DiagNodeSig

the node to which the edge should point

-> NodeSig

the dg node where the param is based

-> DiagNodeSig

the union of the params

-> GMorphism

the morphism as label for the new edge

-> String

a diagnostic node description

-> DGOrigin

the origin of the new node

-> Result (Diag, DGraph) 

returns the new node, the extended diagram and extended development graph

Orphan instances