| 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
Description
- emptyDiag :: Diag
- data DiagNodeSig = Diag_node_sig Node NodeSig
- data MaybeDiagNode
- toMaybeNode :: MaybeDiagNode -> MaybeNode
- getSigFromDiag :: DiagNodeSig -> NodeSig
- data BasedUnitSig
- 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 -> DGOrigin -> Result (NodeSig, DGraph)
- extendDGraphRev :: DGraph -> NodeSig -> GMorphism -> DGOrigin -> Result (NodeSig, DGraph)
- extendDGraphRevHide :: DGraph -> NodeSig -> GMorphism -> DGOrigin -> Result (NodeSig, DGraph)
- extendDiagramWithMorphismRevHide :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> String -> DGOrigin -> Result (DiagNodeSig, Diag, DGraph)
- extendDiagramWithMorphism :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> String -> DGOrigin -> Result (DiagNodeSig, Diag, DGraph)
- extendDiagramWithMorphismRev :: Range -> LogicGraph -> Diag -> DGraph -> DiagNodeSig -> GMorphism -> String -> 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)
getSigFromDiag :: DiagNodeSig -> NodeSig
Return a signature stored within given diagram node sig
data BasedUnitSig
Constructors
| Based_unit_sig DiagNodeSig RefSig | |
| Based_par_unit_sig MaybeDiagNode RefSig | |
| Based_lambda_unit_sig [DiagNodeSig] RefSig |
Instances
type StBasedUnitCtx = Map IRI BasedUnitSig
type ExtStUnitCtx = (StBasedUnitCtx, Diag)
Functions
ctx :: ExtStUnitCtx -> RefStUnitCtx
A mapping from extended to basic static unit context
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.
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.
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
Arguments
| :: DGraph | the development graph to be extended |
| -> NodeSig | the NodeSig from which the morphism originates |
| -> GMorphism | the morphism 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
Arguments
| :: DGraph | the development graph to be extended |
| -> NodeSig | the NodeSig to which the morphism points |
| -> GMorphism | the morphism 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
Arguments
| :: DGraph | the development graph to be extended |
| -> NodeSig | the NodeSig to which the morphism points |
| -> GMorphism | the morphism 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
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 |
| -> DGOrigin | the origin of the new node |
| -> Result (DiagNodeSig, Diag, DGraph) |
returns the new node, the extended diagram and extended development graph
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 |
| -> 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
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 |
| -> 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
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
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.
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
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)
copyDiagram :: LogicGraph -> [Node] -> Diag -> Result (Diag, Map Node Node)
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