hets -- a heterogenous Specification (CASL) tool set
Contents
Index
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