Static.DgUtils

Contents

• node label types
• edge types
• datatypes for storing the nodes of the ref tree in the global env
  • for node names
  • handle edge numbers and proof bases
• utilities

Description

Synopsis

• data XPathPart
  • = ElemName String
  • | ChildIndex Int
• data NodeName = NodeName {
  • getName :: IRI
  • extString :: String
  • extIndex :: Int
  • xpath :: [XPathPart]
  • srcRange :: Range
  }
• 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 {
  • delAx :: Bool
  • delTh :: Bool
  • addSen :: Bool
  • delSym :: Bool
  • addSym :: Bool
  }
• 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
  • = LeftOpen
  • | Proven DGRule ProofBasis
• isProvenThmLinkStatus :: ThmLinkStatus -> Bool
• proofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis
• updProofBasisOfThmLinkStatus :: ThmLinkStatus -> ProofBasis -> ThmLinkStatus
• data Scope
  • = Local
  • | Global
• data LinkKind
  • = DefLink
  • | ThmLink ThmLinkStatus
• data FreeOrCofree
  • = Free
  • | Cofree
  • | NPFree
  • | Minimize
• 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
  • = HidingThm
  • | FreeOrCofreeThm FreeOrCofree
  • | GlobalOrLocalThm {
    • thmScope :: Scope
    • isHomThm :: Bool
    }
• listDGEdgeTypes :: [DGEdgeType]
• isDefEdgeType :: DGEdgeType -> Bool
• data RTPointer
  • = RTNone
  • | NPUnit Int
  • | NPBranch Int (Map IRI RTPointer)
  • | NPRef Int Int
  • | NPComp (Map IRI RTPointer)
• mapRTNodes :: Map Int Int -> RTPointer -> RTPointer
• compPointer :: RTPointer -> RTPointer -> RTPointer
• refSource :: RTPointer -> Int
• data RTLeaves
  • = RTLeaf Int
  • | RTLeaves (Map IRI 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

edge types

datatypes for storing the nodes of the ref tree in the global env

for node names

handle edge numbers and proof bases

utilities