Copyright | (c) DFKI GmbH 2011 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Static.DgUtils
Contents
Description
- data XPathPart
- = ElemName String
- | ChildIndex Int
- data NodeName = NodeName {}
- readXPath :: Monad m => String -> m [XPathPart]
- readXPathComp :: Monad m => String -> m XPathPart
- isInternal :: NodeName -> Bool
- hasOpenConsStatus :: Bool -> ConsStatus -> Bool
- data DGNodeType = DGNodeType {
- isRefType :: Bool
- isProvenNode :: Bool
- isProvenCons :: Bool
- isInternalSpec :: Bool
- listDGNodeTypes :: [DGNodeType]
- data NodeMod = NodeMod {}
- unMod :: NodeMod
- delAxMod :: NodeMod
- delThMod :: NodeMod
- delSenMod :: NodeMod
- addSenMod :: NodeMod
- senMod :: NodeMod
- delSymMod :: NodeMod
- addSymMod :: NodeMod
- symMod :: NodeMod
- mergeNodeMod :: NodeMod -> NodeMod -> NodeMod
- newtype EdgeId = EdgeId {
- getEdgeNum :: Int
- incEdgeId :: EdgeId -> EdgeId
- startEdgeId :: EdgeId
- showEdgeId :: EdgeId -> String
- newtype ProofBasis = ProofBasis {
- proofBasis :: Set EdgeId
- data DGRule
- = DGRule String
- | DGRuleWithEdge String EdgeId
- | DGRuleLocalInference [(String, String)]
- | Composition [EdgeId]
- data ThmLinkStatus
- isProvenThmLinkStatus :: ThmLinkStatus -> Bool
- proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
- updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
- data Scope
- data LinkKind
- data FreeOrCofree
- fcList :: [FreeOrCofree]
- data ConsStatus = ConsStatus Conservativity Conservativity ThmLinkStatus
- isProvenConsStatusLink :: ConsStatus -> Bool
- mkConsStatus :: Conservativity -> ConsStatus
- getConsOfStatus :: ConsStatus -> Conservativity
- showConsStatus :: ConsStatus -> String
- getDGEdgeTypeName :: DGEdgeType -> String
- revertDGEdgeTypeName :: String -> DGEdgeType
- getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String
- data DGEdgeType = DGEdgeType {
- edgeTypeModInc :: DGEdgeTypeModInc
- isInc :: Bool
- data DGEdgeTypeModInc
- = GlobalDef
- | HetDef
- | HidingDef
- | LocalDef
- | FreeOrCofreeDef FreeOrCofree
- | ThmType {
- thmEdgeType :: ThmTypes
- isProvenEdge :: Bool
- isConservativ :: Bool
- isPending :: Bool
- data ThmTypes
- listDGEdgeTypes :: [DGEdgeType]
- isDefEdgeType :: DGEdgeType -> Bool
- data RTPointer
- mapRTNodes :: Map Int Int -> RTPointer -> RTPointer
- compPointer :: RTPointer -> RTPointer -> RTPointer
- refSource :: RTPointer -> Int
- data RTLeaves
- refTarget :: RTPointer -> RTLeaves
- emptyNodeName :: NodeName
- showExt :: NodeName -> String
- showName :: NodeName -> String
- makeRgName :: IRI -> Range -> NodeName
- makeName :: IRI -> NodeName
- setSrcRange :: Range -> NodeName -> NodeName
- parseNodeName :: String -> NodeName
- incBy :: Int -> NodeName -> NodeName
- inc :: NodeName -> NodeName
- extName :: String -> NodeName -> NodeName
- defaultEdgeId :: EdgeId
- emptyProofBasis :: ProofBasis
- nullProofBasis :: ProofBasis -> Bool
- addEdgeId :: ProofBasis -> EdgeId -> ProofBasis
- delEdgeId :: ProofBasis -> EdgeId -> ProofBasis
- updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis
- edgeInProofBasis :: EdgeId -> ProofBasis -> Bool
- topsortedLibsWithImports :: Rel LibName -> [LibName]
- getMapAndMaxIndex :: Ord k => k -> (b -> Map k a) -> b -> (Map k a, k)
- liftOr :: (a -> Bool) -> (a -> Bool) -> a -> Bool
node label types
Constructors
ElemName String | |
ChildIndex Int |
name of a node in a DG; auxiliary nodes may have extension string and non-zero number (for these, names are usually hidden).
Constructors
NodeName | |
readXPathComp :: Monad m => String -> m XPathPart Source #
isInternal :: NodeName -> Bool Source #
hasOpenConsStatus :: Bool -> ConsStatus -> Bool Source #
test if a conservativity is open, return input for None
data DGNodeType Source #
Constructors
DGNodeType | |
Fields
|
Instances
Eq DGNodeType Source # | |
Data DGNodeType Source # | |
Ord DGNodeType Source # | |
Show DGNodeType Source # | |
listDGNodeTypes :: [DGNodeType] Source #
node modifications
edge types
unique number for edges
Constructors
EdgeId | |
Fields
|
startEdgeId :: EdgeId Source #
the first edge in a graph
showEdgeId :: EdgeId -> String Source #
newtype ProofBasis Source #
a set of used edges
Constructors
ProofBasis | |
Fields
|
Instances
Eq ProofBasis Source # | |
Data ProofBasis Source # | |
Ord ProofBasis Source # | |
Show ProofBasis Source # | |
Rules in the development graph calculus, Sect. IV:4.4 of the CASL Reference Manual explains them in depth
Constructors
DGRule String | |
DGRuleWithEdge String EdgeId | |
DGRuleLocalInference [(String, String)] | |
Composition [EdgeId] |
data ThmLinkStatus Source #
proof status of a link
Constructors
LeftOpen | |
Proven DGRule ProofBasis |
Instances
Eq ThmLinkStatus Source # | |
Data ThmLinkStatus Source # | |
Ord ThmLinkStatus Source # | |
Show ThmLinkStatus Source # | |
isProvenThmLinkStatus :: ThmLinkStatus -> Bool Source #
Constructors
DefLink | |
ThmLink ThmLinkStatus |
data FreeOrCofree Source #
Instances
Bounded FreeOrCofree Source # | |
Enum FreeOrCofree Source # | |
Eq FreeOrCofree Source # | |
Data FreeOrCofree Source # | |
Ord FreeOrCofree Source # | |
Read FreeOrCofree Source # | |
Show FreeOrCofree Source # | |
fcList :: [FreeOrCofree] Source #
data ConsStatus Source #
required and proven conservativity (with a proof)
Constructors
ConsStatus Conservativity Conservativity ThmLinkStatus |
Instances
Eq ConsStatus Source # | |
Data ConsStatus Source # | |
Ord ConsStatus Source # | |
Show ConsStatus Source # | |
isProvenConsStatusLink :: ConsStatus -> Bool Source #
showConsStatus :: ConsStatus -> String Source #
to be displayed as edge label
getDGEdgeTypeName :: DGEdgeType -> String Source #
converts a DGEdgeType to a String
revertDGEdgeTypeName :: String -> DGEdgeType Source #
getDGEdgeTypeModIncName :: DGEdgeTypeModInc -> String Source #
data DGEdgeType Source #
Constructors
DGEdgeType | |
Fields
|
Instances
Eq DGEdgeType Source # | |
Data DGEdgeType Source # | |
Ord DGEdgeType Source # | |
Show DGEdgeType Source # | |
data DGEdgeTypeModInc Source #
Constructors
GlobalDef | |
HetDef | |
HidingDef | |
LocalDef | |
FreeOrCofreeDef FreeOrCofree | |
ThmType | |
Fields
|
Instances
Eq DGEdgeTypeModInc Source # | |
Data DGEdgeTypeModInc Source # | |
Ord DGEdgeTypeModInc Source # | |
Show DGEdgeTypeModInc Source # | |
Constructors
HidingThm | |
FreeOrCofreeThm FreeOrCofree | |
GlobalOrLocalThm | |
listDGEdgeTypes :: [DGEdgeType] Source #
Creates a list with all DGEdgeType types
isDefEdgeType :: DGEdgeType -> Bool Source #
check an EdgeType and see if its a definition link
datatypes for storing the nodes of the ref tree in the global env
mapRTNodes :: Map Int Int -> RTPointer -> RTPointer Source #
for node names
parseNodeName :: String -> NodeName Source #
handle edge numbers and proof bases
defaultEdgeId :: EdgeId Source #
create a default ID which has to be changed when inserting a certain edge.
nullProofBasis :: ProofBasis -> Bool Source #
addEdgeId :: ProofBasis -> EdgeId -> ProofBasis Source #
delEdgeId :: ProofBasis -> EdgeId -> ProofBasis Source #
updEdgeId :: ProofBasis -> EdgeId -> EdgeId -> ProofBasis Source #
edgeInProofBasis :: EdgeId -> ProofBasis -> Bool Source #
checks if the given edge is contained in the given proof basis..
utilities
getMapAndMaxIndex :: Ord k => k -> (b -> Map k a) -> b -> (Map k a, k) Source #