Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Static.DevGraph

Contents

Description

Central datastructures for development graphs Follows Sect. IV:4.2 of the CASL Reference Manual.

We also provide functions for constructing and modifying development graphs. However note that these changes need to be propagated to the GUI if they also shall be visible in the displayed development graph.

Synopsis

types for structured specification analysis

basic types

data NodeSig Source #

Node with signature in a DG

Constructors

NodeSig 

Fields

Instances

Eq NodeSig Source # 

Methods

(==) :: NodeSig -> NodeSig -> Bool

(/=) :: NodeSig -> NodeSig -> Bool

Show NodeSig Source # 

Methods

showsPrec :: Int -> NodeSig -> ShowS

show :: NodeSig -> String

showList :: [NodeSig] -> ShowS

data MaybeNode Source #

NodeSig or possibly the empty sig in a logic (but since we want to avoid lots of vsacuous nodes with empty sig, we do not assign a real node in the DG here)

Instances

Eq MaybeNode Source # 

Methods

(==) :: MaybeNode -> MaybeNode -> Bool

(/=) :: MaybeNode -> MaybeNode -> Bool

Show MaybeNode Source # 

Methods

showsPrec :: Int -> MaybeNode -> ShowS

show :: MaybeNode -> String

showList :: [MaybeNode] -> ShowS

newtype Renamed Source #

a wrapper for renamings with a trivial Ord instance

Constructors

Renamed RENAMING 

Instances

Eq Renamed Source # 

Methods

(==) :: Renamed -> Renamed -> Bool

(/=) :: Renamed -> Renamed -> Bool

Ord Renamed Source # 

Methods

compare :: Renamed -> Renamed -> Ordering

(<) :: Renamed -> Renamed -> Bool

(<=) :: Renamed -> Renamed -> Bool

(>) :: Renamed -> Renamed -> Bool

(>=) :: Renamed -> Renamed -> Bool

max :: Renamed -> Renamed -> Renamed

min :: Renamed -> Renamed -> Renamed

Show Renamed Source # 

Methods

showsPrec :: Int -> Renamed -> ShowS

show :: Renamed -> String

showList :: [Renamed] -> ShowS

data DGOrigin Source #

Data type indicating the origin of nodes and edges in the input language This is not used in the DG calculus, only may be used in the future for reconstruction of input and management of change.

Instances

Eq DGOrigin Source # 

Methods

(==) :: DGOrigin -> DGOrigin -> Bool

(/=) :: DGOrigin -> DGOrigin -> Bool

Ord DGOrigin Source # 

Methods

compare :: DGOrigin -> DGOrigin -> Ordering

(<) :: DGOrigin -> DGOrigin -> Bool

(<=) :: DGOrigin -> DGOrigin -> Bool

(>) :: DGOrigin -> DGOrigin -> Bool

(>=) :: DGOrigin -> DGOrigin -> Bool

max :: DGOrigin -> DGOrigin -> DGOrigin

min :: DGOrigin -> DGOrigin -> DGOrigin

Show DGOrigin Source # 

Methods

showsPrec :: Int -> DGOrigin -> ShowS

show :: DGOrigin -> String

showList :: [DGOrigin] -> ShowS

data DGNodeInfo Source #

node content or reference to another library's node

Constructors

DGNode 
DGRef 

Fields

Instances

Eq DGNodeInfo Source # 

Methods

(==) :: DGNodeInfo -> DGNodeInfo -> Bool

(/=) :: DGNodeInfo -> DGNodeInfo -> Bool

Show DGNodeInfo Source # 

Methods

showsPrec :: Int -> DGNodeInfo -> ShowS

show :: DGNodeInfo -> String

showList :: [DGNodeInfo] -> ShowS

data DGNodeLab Source #

node inscriptions in development graphs. Nothing entries indicate "not computed yet"

Constructors

DGNodeLab 

Fields

Instances

Show DGNodeLab Source # 

Methods

showsPrec :: Int -> DGNodeLab -> ShowS

show :: DGNodeLab -> String

showList :: [DGNodeLab] -> ShowS

sensWithKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> G_theory -> [String] Source #

hasSenKind :: (forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool) -> DGNodeLab -> Bool Source #

hasOpenGoals :: DGNodeLab -> Bool Source #

test if a given node label has local open goals

isInternalNode :: DGNodeLab -> Bool Source #

check if the node has an internal name

getNodeConservativity :: LNode DGNodeLab -> Conservativity Source #

returns the Conservativity if the given node has one, otherwise none

hasOpenNodeConsStatus :: Bool -> DGNodeLab -> Bool Source #

test if a node conservativity is open, return input for refs or nodes with normal forms

getRealDGNodeType :: DGNodeLab -> DGNodeType Source #

creates a DGNodeType from a DGNodeLab

newtype Fitted Source #

a wrapper for fitting morphisms with a trivial Eq instance

Constructors

Fitted [G_mapping] 

Instances

Eq Fitted Source # 

Methods

(==) :: Fitted -> Fitted -> Bool

(/=) :: Fitted -> Fitted -> Bool

Show Fitted Source # 

Methods

showsPrec :: Int -> Fitted -> ShowS

show :: Fitted -> String

showList :: [Fitted] -> ShowS

data DGLinkType Source #

Link types of development graphs, Sect. IV:4.2 of the CASL Reference Manual explains them in depth.

Instances

Eq DGLinkType Source # 

Methods

(==) :: DGLinkType -> DGLinkType -> Bool

(/=) :: DGLinkType -> DGLinkType -> Bool

Show DGLinkType Source # 

Methods

showsPrec :: Int -> DGLinkType -> ShowS

show :: DGLinkType -> String

showList :: [DGLinkType] -> ShowS

thmLinkStatus :: DGLinkType -> Maybe ThmLinkStatus Source #

extract theorem link status from link type

thmProofBasis :: DGLinkType -> ProofBasis Source #

extract proof basis from link type

data DGLinkLab Source #

link inscriptions in development graphs

Constructors

DGLink 

Instances

Eq DGLinkLab Source # 

Methods

(==) :: DGLinkLab -> DGLinkLab -> Bool

(/=) :: DGLinkLab -> DGLinkLab -> Bool

Show DGLinkLab Source # 

Methods

showsPrec :: Int -> DGLinkLab -> ShowS

show :: DGLinkLab -> String

showList :: [DGLinkLab] -> ShowS

nameDGLink :: String -> DGLinkLab -> DGLinkLab Source #

name a link

getDGLinkType :: DGLinkLab -> String Source #

describe the link type of the label

getRealDGLinkType :: DGLinkLab -> DGEdgeType Source #

creates a DGEdgeType from a DGLinkLab

getProofBasis :: DGLinkLab -> ProofBasis Source #

return the proof basis of the given linklab

setProof :: ThmLinkStatus -> DGLinkType -> DGLinkType Source #

set proof for theorem links

methods to check the type of an edge

hasOutgoingFreeEdge :: DGraph -> Node -> Bool Source #

types for global environments

data GenSig Source #

import, formal parameters and united signature of formal params

Instances

Show GenSig Source # 

Methods

showsPrec :: Int -> GenSig -> ShowS

show :: GenSig -> String

showList :: [GenSig] -> ShowS

getGenSigNodes :: GenSig -> Set Node Source #

data ExtGenSig Source #

genericity and body

Constructors

ExtGenSig 

Instances

Show ExtGenSig Source # 

Methods

showsPrec :: Int -> ExtGenSig -> ShowS

show :: ExtGenSig -> String

showList :: [ExtGenSig] -> ShowS

data ExtViewSig Source #

source, morphism, parameterized target

Instances

Show ExtViewSig Source # 

Methods

showsPrec :: Int -> ExtViewSig -> ShowS

show :: ExtViewSig -> String

showList :: [ExtViewSig] -> ShowS

types for architectural and unit specification analysis (as defined for basic static semantics in Chap. III:5.1)

data UnitSig Source #

Constructors

UnitSig [NodeSig] NodeSig (Maybe NodeSig) 

Instances

Eq UnitSig Source # 

Methods

(==) :: UnitSig -> UnitSig -> Bool

(/=) :: UnitSig -> UnitSig -> Bool

Show UnitSig Source # 

Methods

showsPrec :: Int -> UnitSig -> ShowS

show :: UnitSig -> String

showList :: [UnitSig] -> ShowS

data RefSig Source #

Instances

Eq RefSig Source # 

Methods

(==) :: RefSig -> RefSig -> Bool

(/=) :: RefSig -> RefSig -> Bool

Show RefSig Source # 

Methods

showsPrec :: Int -> RefSig -> ShowS

show :: RefSig -> String

showList :: [RefSig] -> ShowS

getRefSigNodes :: RefSig -> Set Node Source #

data BranchSig Source #

Instances

Eq BranchSig Source # 

Methods

(==) :: BranchSig -> BranchSig -> Bool

(/=) :: BranchSig -> BranchSig -> Bool

Show BranchSig Source # 

Methods

showsPrec :: Int -> BranchSig -> ShowS

show :: BranchSig -> String

showList :: [BranchSig] -> ShowS

data GlobalEntry Source #

an entry of the global environment

Instances

Show GlobalEntry Source # 

Methods

showsPrec :: Int -> GlobalEntry -> ShowS

show :: GlobalEntry -> String

showList :: [GlobalEntry] -> ShowS

change and history types

data DGChange Source #

the edit operations of the DGraph

Instances

Show DGChange Source # 

Methods

showsPrec :: Int -> DGChange -> ShowS

show :: DGChange -> String

showList :: [DGChange] -> ShowS

data RTNodeType Source #

Constructors

RTPlain UnitSig 
RTRef Node 

Instances

Eq RTNodeType Source # 

Methods

(==) :: RTNodeType -> RTNodeType -> Bool

(/=) :: RTNodeType -> RTNodeType -> Bool

Show RTNodeType Source # 

Methods

showsPrec :: Int -> RTNodeType -> ShowS

show :: RTNodeType -> String

showList :: [RTNodeType] -> ShowS

data RTNodeLab Source #

Constructors

RTNodeLab 

Fields

Instances

Eq RTNodeLab Source # 

Methods

(==) :: RTNodeLab -> RTNodeLab -> Bool

(/=) :: RTNodeLab -> RTNodeLab -> Bool

Show RTNodeLab Source # 

Methods

showsPrec :: Int -> RTNodeLab -> ShowS

show :: RTNodeLab -> String

showList :: [RTNodeLab] -> ShowS

data RTLinkType Source #

Constructors

RTRefine 
RTComp 

Instances

Eq RTLinkType Source # 

Methods

(==) :: RTLinkType -> RTLinkType -> Bool

(/=) :: RTLinkType -> RTLinkType -> Bool

Show RTLinkType Source # 

Methods

showsPrec :: Int -> RTLinkType -> ShowS

show :: RTLinkType -> String

showList :: [RTLinkType] -> ShowS

data RTLinkLab Source #

Constructors

RTLink 

Fields

Instances

Eq RTLinkLab Source # 

Methods

(==) :: RTLinkLab -> RTLinkLab -> Bool

(/=) :: RTLinkLab -> RTLinkLab -> Bool

Show RTLinkLab Source # 

Methods

showsPrec :: Int -> RTLinkLab -> ShowS

show :: RTLinkLab -> String

showList :: [RTLinkLab] -> ShowS

addNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph) Source #

addSpecNodeRT :: DGraph -> UnitSig -> String -> (Node, DGraph) Source #

updateNodeNameRT :: DGraph -> Node -> Bool -> String -> DGraph Source #

updateNodeNameSpecRT :: DGraph -> Node -> String -> DGraph Source #

copySubTree :: DGraph -> Node -> Maybe Node -> (DGraph, Map Node Node) Source #

copySubTreeN :: DGraph -> [Node] -> Map Node Node -> (DGraph, Map Node Node) Source #

copyNode :: Node -> (DGraph, Map Node Node) -> LNode RTLinkLab -> (DGraph, Map Node Node) Source #

addRefEdgeRT :: DGraph -> Node -> Node -> DGraph Source #

addEdgesToNodeRT :: DGraph -> [Node] -> Node -> DGraph Source #

data DiagNodeLab Source #

Constructors

DiagNode 

Fields

Instances

Show DiagNodeLab Source # 

Methods

showsPrec :: Int -> DiagNodeLab -> ShowS

show :: DiagNodeLab -> String

showList :: [DiagNodeLab] -> ShowS

data DiagLinkLab Source #

Constructors

DiagLink 

Fields

Instances

Show DiagLinkLab Source # 

Methods

showsPrec :: Int -> DiagLinkLab -> ShowS

show :: DiagLinkLab -> String

showList :: [DiagLinkLab] -> ShowS

data Diag Source #

Constructors

Diagram 

Instances

Show Diag Source # 

Methods

showsPrec :: Int -> Diag -> ShowS

show :: Diag -> String

showList :: [Diag] -> ShowS

data DGraph Source #

the actual development graph with auxiliary information. A G_sign should be stored in sigMap under its gSignSelfIdx. The same applies to G_morphism with morMap and gMorphismSelfIdx resp. G_theory with thMap and gTheorySelfIdx.

Constructors

DGraph 

Fields

Instances

Show DGraph Source # 

Methods

showsPrec :: Int -> DGraph -> ShowS

show :: DGraph -> String

showList :: [DGraph] -> ShowS

emptyLibEnv :: LibEnv Source #

an empty environment

utility functions

for node signatures

accessing node label

dgn_origin :: DGNodeLab -> DGOrigin Source #

get the origin of a non-reference node (partial)

dgn_libname :: DGNodeLab -> LibName Source #

get the referenced library (partial)

dgn_node :: DGNodeLab -> Node Source #

get the referenced node (partial)

dgn_sign :: DGNodeLab -> G_sign Source #

get the signature of a node's theory (total)

getDGNodeName :: DGNodeLab -> String Source #

gets the name of a development graph node as a string (total)

globOrLocTh :: DGNodeLab -> G_theory Source #

get the global theory of a node or the local one if missing

creating node content and label

newNodeInfo :: DGOrigin -> DGNodeInfo Source #

create default content

newRefInfo :: LibName -> Node -> DGNodeInfo Source #

create a reference node part

newInfoNodeLab :: NodeName -> DGNodeInfo -> G_theory -> DGNodeLab Source #

create a new node label

newNodeLab :: NodeName -> DGOrigin -> G_theory -> DGNodeLab Source #

create a new node label using newNodeInfo and newInfoNodeLab

handle the lock of a node

treatNodeLock :: (MVar () -> a) -> DGNodeLab -> a Source #

wrapper to access the maybe lock

tryLockLocal :: DGNodeLab -> IO Bool Source #

Tries to acquire the local lock. Return False if already acquired.

unlockLocal :: DGNodeLab -> IO () Source #

Releases the local lock.

hasLock :: DGNodeLab -> Bool Source #

checks if locking MVar is initialized

edge label equalities

eqDGLinkLabContent :: DGLinkLab -> DGLinkLab -> Bool Source #

equality without comparing the edge ids

eqDGLinkLabById :: DGLinkLab -> DGLinkLab -> Bool Source #

equality comparing ids only

setting index maps

looking up in index maps

getting index maps and their maximal index

lookup other graph parts

lookupInAllRefNodesDG :: DGNodeInfo -> DGraph -> Maybe Node Source #

lookup a reference node for a given libname and node

lookup nodes by their names or other properties

lookupNodeByName :: String -> DGraph -> [LNode DGNodeLab] Source #

lookup a node in the graph by its name, using showName to convert nodenames.

lookupUniqueNodeByName :: String -> DGraph -> Maybe (LNode DGNodeLab) Source #

filterLocalNodesByName :: String -> DGraph -> [LNode DGNodeLab] Source #

filters all local nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

filterRefNodesByName :: String -> LibName -> DGraph -> [LNode DGNodeLab] Source #

filter all ref nodes in the graph by their names, using showName to convert nodenames. See also lookupNodeByName.

lookupLocalNodeByNameInEnv :: LibEnv -> String -> Maybe (DGraph, LNode DGNodeLab) Source #

Given a LibEnv we search each DGraph in it for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNodeByName :: LibEnv -> DGraph -> String -> Maybe (DGraph, LNode DGNodeLab) Source #

We search only the given DGraph for a (maybe referenced) node with the given name. We return the labeled node and the Graph where this node resides as local node. See also lookupLocalNode.

lookupLocalNode :: LibEnv -> DGraph -> Node -> (DGraph, LNode DGNodeLab) Source #

Given a Node and a DGraph we follow the node to the graph where it is defined as a local node.

lookupRefNode :: LibEnv -> LibName -> DGraph -> Node -> (LibName, DGraph, LNode DGNodeLab) Source #

Given a Node and a DGraph we follow the node to the graph where it is defined .

lookupRefNodeM :: LibEnv -> Maybe LibName -> DGraph -> Node -> (Maybe LibName, DGraph, LNode DGNodeLab) Source #

accessing the actual graph

getNewNodeDG :: DGraph -> Node Source #

get the next available node id

labNodesDG :: DGraph -> [LNode DGNodeLab] Source #

get all the nodes

labEdgesDG :: DGraph -> [LEdge DGLinkLab] Source #

get all the edges

isEmptyDG :: DGraph -> Bool Source #

checks if a DG is empty or not.

gelemDG :: Node -> DGraph -> Bool Source #

checks if a given node belongs to a given DG

innDG :: DGraph -> Node -> [LEdge DGLinkLab] Source #

get all the incoming ledges of the given node in a given DG

outDG :: DGraph -> Node -> [LEdge DGLinkLab] Source #

get all the outgoing ledges of the given node in a given DG

nodesDG :: DGraph -> [Node] Source #

get all the nodes of the given DG

labDG :: DGraph -> Node -> DGNodeLab Source #

tries to get the label of the given node in a given DG

labRT :: DGraph -> Node -> RTNodeLab Source #

tries to get the label of the given node in a given RT

getNameOfNode :: Node -> DGraph -> String Source #

get the name of a node from the number of node

newNodesDG :: Int -> DGraph -> [Node] Source #

gets the given number of new node-ids in a given DG.

safeContextDG :: String -> DGraph -> Node -> Context DGNodeLab DGLinkLab Source #

get the context and throw input string as error message

manipulate graph

labelNodeDG :: LNode DGNodeLab -> DGraph -> (DGraph, DGNodeLab) Source #

sets the node with new label and returns the new graph and the old label

delNodeDG :: Node -> DGraph -> DGraph Source #

delete the node out of the given DG

delNodesDG :: [Node] -> DGraph -> DGraph Source #

delete a list of nodes out of the given DG

insNodeDG :: LNode DGNodeLab -> DGraph -> DGraph Source #

insert a new node into given DGraph

insLNodeDG :: LNode DGNodeLab -> DGraph -> DGraph Source #

inserts a lnode into a given DG

insNodesDG :: [LNode DGNodeLab] -> DGraph -> DGraph Source #

insert a new node with the given node content into a given DGraph

delLEdgeDG :: LEdge DGLinkLab -> DGraph -> DGraph Source #

delete a labeled edge out of the given DG

insInclEdgeDG :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> Result DGraph Source #

inserts an edge between two nodes, labelled with inclusion

insLEdgeDG :: LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph) Source #

insert a labeled edge into a given DG, return possibly new id of edge

insLEdgeNubDG :: LEdge DGLinkLab -> DGraph -> DGraph Source #

tries to insert a labeled edge into a given DG, but if this edge already exists, then does nothing.

insEdgeAsIs :: LEdge DGLinkLab -> DGraph -> DGraph Source #

inserts a new edge into the DGraph using it's own edgeId. ATTENTION: the caller must ensure that an edgeId is not used twice

insEdgesDG :: [LEdge DGLinkLab] -> DGraph -> DGraph Source #

insert a list of labeled edge into a given DG

mkGraphDG :: [LNode DGNodeLab] -> [LEdge DGLinkLab] -> DGraph -> DGraph Source #

merge a list of lnodes and ledges into a given DG

getDGLinksById :: EdgeId -> DGraph -> [LEdge DGLinkLab] Source #

get links by id (inefficiently)

lookupUniqueLink :: Monad m => Node -> EdgeId -> DGraph -> m (LEdge DGLinkLab) Source #

find a unique link given its source node and edgeId

top-level functions

initLocking :: DGraph -> LNode DGNodeLab -> IO (DGraph, DGNodeLab) Source #

initializes the MVar for locking if nessesary

lookupDGraph :: LibName -> LibEnv -> DGraph Source #

returns the DGraph that belongs to the given library name

computeLocalTheory :: Monad m => LibEnv -> LibName -> Node -> m G_theory Source #

compute the theory of a given node. If this node is a DGRef, the referenced node is looked up first.

computeLocalNodeTheory :: Monad m => LibEnv -> DGraph -> Node -> m G_theory Source #

test link types

liftE :: (DGLinkType -> a) -> LEdge DGLinkLab -> a Source #

create link types

link conservativity

getConservativity :: LEdge DGLinkLab -> Conservativity Source #

returns the Conservativity if the given edge has one, otherwise none

getConservativityOfPath :: [LEdge DGLinkLab] -> Conservativity Source #

returns the conservativity of the given path

bottom up traversal

getLibDepRel :: LibEnv -> Rel LibName Source #

Creates a LibName relation wrt dependencies via reference nodes

dependentLibs :: LibName -> LibEnv -> [LibName] Source #

Get imported libs in topological order, i.e. lib(s) without imports first. The input lib-name will be last