Copyright	(c) Maciek Makowski Warsaw University 2004-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-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 Haskell	None

Static.ArchDiagram

Contents

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

Description

Synopsis

emptyDiag :: Diag
data DiagNodeSig = Diag_node_sig Node NodeSig
data MaybeDiagNode
- = JustDiagNode DiagNodeSig
- | EmptyDiagNode AnyLogic
toMaybeNode :: MaybeDiagNode -> MaybeNode
getSigFromDiag :: DiagNodeSig -> NodeSig
data BasedUnitSig
- = Based_unit_sig DiagNodeSig RefSig
- | Based_par_unit_sig MaybeDiagNode RefSig
- | Based_lambda_unit_sig [DiagNodeSig] RefSig
type StBasedUnitCtx = Map IRI BasedUnitSig
emptyStBasedUnitCtx :: StBasedUnitCtx
type ExtStUnitCtx = (StBasedUnitCtx, Diag)
emptyExtStUnitCtx :: ExtStUnitCtx
printDiag :: a -> String -> Diag -> Result a
ctx :: ExtStUnitCtx -> RefStUnitCtx
insInclusionEdges :: LogicGraph -> Diag -> [DiagNodeSig] -> DiagNodeSig -> Result Diag
insInclusionEdgesRev :: LogicGraph -> Diag -> DiagNodeSig -> [DiagNodeSig] -> Result Diag
extendDiagramIncl :: LogicGraph -> Diag -> [DiagNodeSig] -> NodeSig -> String -> Result (DiagNodeSig, Diag)
extendDGraph :: DGraph -> NodeSig -> GMorphism -> IRI -> DGOrigin -> Result (NodeSig, DGraph)
extendDGraphRev :: DGraph -> NodeSig -> GMorphism -> IRI -> DGOrigin -> Result (NodeSig, DGraph)
extendDGraphRevHide :: DGraph -> NodeSig -> GMorphism -> IRI -> DGOrigin -> Result (NodeSig, DGraph)
extendDiagramWithMorphismRevHide :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> IRI -> String -> DGOrigin -> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphism :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> IRI -> String -> DGOrigin -> Result (DiagNodeSig, Diag, DGraph)
extendDiagramWithMorphismRev :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> String -> IRI -> DGOrigin -> Result (DiagNodeSig, Diag, DGraph)
extendDiagram :: Diag -> DiagNodeSig -> GMorphism -> NodeSig -> String -> Result (DiagNodeSig, Diag)
homogeniseDiagram :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Diag -> Result (Gr sign (Int, morphism))
diagDesc :: Diag -> Gr String String
inclusionSink :: LogicGraph -> [DiagNodeSig] -> NodeSig -> Result [(Node, GMorphism)]
extendDiagramWithEdge :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> DiagNodeSig -> GMorphism -> DGLinkOrigin -> Result (Diag, DGraph)
matchDiagram :: Node -> Diag -> (MContext DiagNodeLab DiagLinkLab, Diag)
copyDiagram :: LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node)
copyEdges :: [Node] -> Diag -> Map Node Node -> Map Edge Bool -> (Map Edge Bool, Diag)
copyEdge :: Diag -> Map Node Node -> LEdge DiagLinkLab -> Map Edge Bool -> (Map Edge Bool, Diag)
copyDiagramAux :: Map Node Node -> LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node)
insertFormalParamAndVerifCond :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> NodeSig -> DiagNodeSig -> GMorphism -> String -> DGOrigin -> Result (Diag, DGraph)

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

emptyDiag :: Diag Source #

data DiagNodeSig Source #

Constructors

Diag_node_sig Node NodeSig

Instances

Instances details

Show DiagNodeSig Source #
Instance details Defined in Static.ArchDiagram Methods showsPrec :: Int -> DiagNodeSig -> ShowS show :: DiagNodeSig -> String showList :: [DiagNodeSig] -> ShowS

data MaybeDiagNode Source #

Constructors

JustDiagNode DiagNodeSig
EmptyDiagNode AnyLogic

Instances

Instances details

Show MaybeDiagNode Source #
Instance details Defined in Static.ArchDiagram Methods showsPrec :: Int -> MaybeDiagNode -> ShowS show :: MaybeDiagNode -> String showList :: [MaybeDiagNode] -> ShowS

toMaybeNode :: MaybeDiagNode -> MaybeNode Source #

getSigFromDiag :: DiagNodeSig -> NodeSig Source #

Return a signature stored within given diagram node sig

data BasedUnitSig Source #

Constructors

Based_unit_sig DiagNodeSig RefSig
Based_par_unit_sig MaybeDiagNode RefSig
Based_lambda_unit_sig [DiagNodeSig] RefSig

Instances

Instances details

Show BasedUnitSig Source #
Instance details Defined in Static.ArchDiagram Methods showsPrec :: Int -> BasedUnitSig -> ShowS show :: BasedUnitSig -> String showList :: [BasedUnitSig] -> ShowS

type StBasedUnitCtx = Map IRI BasedUnitSig Source #

emptyStBasedUnitCtx :: StBasedUnitCtx Source #

type ExtStUnitCtx = (StBasedUnitCtx, Diag) Source #

emptyExtStUnitCtx :: ExtStUnitCtx Source #

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

matchDiagram :: Node -> Diag -> (MContext DiagNodeLab DiagLinkLab, Diag) Source #

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

Pretty Diag Source #
Instance details Methods pretty :: Diag -> Doc Source # pretties :: [Diag] -> Doc Source #