hets -- a heterogenous Specification (CASL) tool setContentsIndex
Static.DevGraph
Portability non-portable(Logic)
Stability provisional
Maintainer hets@tzi.de
Description
Central data structure for development graphs.
Synopsis
data DGNodeLab
= DGNode {
dgn_name :: (Maybe SIMPLE_ID)
dgn_sign :: G_sign
dgn_sens :: G_l_sentence_list
dgn_origin :: DGOrigin
}
| DGRef {
dgn_renamed :: (Maybe SIMPLE_ID)
dgn_libname :: LIB_NAME
dgn_node :: Node
}
isDGRef :: DGNodeLab -> Bool
locallyEmpty :: DGNodeLab -> Bool
data DGLinkLab = DGLink {
dgl_morphism :: GMorphism
dgl_type :: DGLinkType
dgl_origin :: DGOrigin
}
data ThmLinkStatus
= Open
| Proven [DGLinkLab]
data DGLinkType
= LocalDef
| GlobalDef
| HidingDef
| FreeDef NodeSig
| CofreeDef NodeSig
| LocalThm ThmLinkStatus Conservativity ThmLinkStatus
| GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
| HidingThm GMorphism ThmLinkStatus
| FreeThm GMorphism Bool
data Conservativity
= None
| Cons
| Mono
| Def
data DGOrigin
= DGBasic
| DGExtension
| DGTranslation
| DGUnion
| DGHiding
| DGRevealing
| DGRevealTranslation
| DGFree
| DGCofree
| DGLocal
| DGClosed
| DGClosedLenv
| DGFormalParams
| DGImports
| DGSpecInst SIMPLE_ID
| DGFitSpec
| DGView SIMPLE_ID
| DGFitView SIMPLE_ID
| DGFitViewImp SIMPLE_ID
| DGFitViewA SIMPLE_ID
| DGFitViewAImp SIMPLE_ID
| DGProof
type DGraph = Graph DGNodeLab DGLinkLab
data NodeSig
= NodeSig (Node, G_sign)
| EmptyNode AnyLogic
data ExtNodeSig
= ExtNodeSig (Node, G_ext_sign)
| ExtEmptyNode AnyLogic
type ExtGenSig = (NodeSig, [NodeSig], G_sign, NodeSig)
type ExtViewSig = (NodeSig, GMorphism, ExtGenSig)
type ArchSig = ()
type UnitSig = ()
data GlobalEntry
= SpecEntry ExtGenSig
| ViewEntry ExtViewSig
| ArchEntry ArchSig
| UnitEntry UnitSig
type GlobalEnv = Map SIMPLE_ID GlobalEntry
type GlobalContext = (GlobalAnnos, GlobalEnv, DGraph)
type LibEnv = Map LIB_NAME GlobalContext
emptyLibEnv :: LibEnv
get_dgn_name :: DGNodeLab -> Maybe SIMPLE_ID
Produced by Haddock version 0.6