Static.XGraph

Description

Synopsis

• data XGraph = XGraph {
  • libName :: LibName
  • globAnnos :: GlobalAnnos
  • nextLinkId :: EdgeId
  • thmLinks :: [XLink]
  • startNodes :: [XNode]
  • xg_body :: XTree
  }
• type XTree = [[([XLink], XNode)]]
• type EdgeMap = Map String (Map String [XLink])
• data XNode
  • = XNode {
    • nodeName :: NodeName
    • logicName :: String
    • symbs :: (Bool, String)
    • specs :: String
    • nd_cons :: Conservativity
    }
  • | XRef {
    • nodeName :: NodeName
    • refNode :: String
    • refLib :: String
    • specs :: String
    }
• data XLink = XLink {
  • source :: String
  • target :: String
  • edgeId :: EdgeId
  • lType :: DGEdgeType
  • rule :: DGRule
  • cons :: Conservativity
  • prBasis :: ProofBasis
  • mr_name :: String
  • mr_source :: Maybe String
  • mapping :: String
  }
• insertXLink :: XLink -> EdgeMap -> EdgeMap
• mkEdgeMap :: [XLink] -> EdgeMap
• xGraph :: Element -> Result XGraph
• builtXGraph :: Monad m => Set String -> EdgeMap -> Map String XNode -> XTree -> m XTree
• extractXNodes :: Monad m => Element -> m [XNode]
• extractXLinks :: Monad m => Element -> m [XLink]
• mkXNode :: Monad m => Element -> m XNode
• extractNodeName :: Monad m => Element -> m NodeName
• mkXLink :: Monad m => Element -> m XLink
• readCons :: Element -> Conservativity
• extractEdgeId :: Monad m => Element -> m EdgeId
• readEdgeId :: String -> EdgeId
• deepSearch :: [String] -> Element -> [Element]
• extractGlobalAnnos :: Element -> Result GlobalAnnos
• parseAnnotations :: Element -> Result GlobalAnnos

Documentation