data ConversionMaps = ConversionMaps {} |
|
data GraphMem = GraphMem {} |
|
type DGraphToAGraphNode = Map (LIB_NAME, Node) Descr |
|
type DGraphToAGraphEdge = Map (LIB_NAME, (Descr, Descr, String)) Descr |
|
type AGraphToDGraphNode = Map Descr (LIB_NAME, Node) |
|
type AGraphToDGraphEdge = Map Descr (LIB_NAME, (Descr, Descr, String)) |
|
initializeConverter :: IO (IORef GraphMem) |
|
convertGraph :: IORef GraphMem -> LIB_NAME -> LibEnv -> IO (Descr, GraphInfo, ConversionMaps) |
|
initializeGraph :: IORef GraphMem -> LIB_NAME -> DGraph -> ConversionMaps -> GlobalContext -> IO (Descr, GraphInfo, IORef ConversionMaps) |
|
getSignatureOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO () |
|
getSublogicOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO () |
|
showOriginOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO () |
|
showMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO () |
|
showOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO () |
|
showProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO () |
|
getProofStatusOfThm :: LEdge DGLinkLab -> ThmLinkStatus |
|
convertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME -> IO ConversionMaps |
|
convertNodesAux :: ConversionMaps -> Descr -> GraphInfo -> [LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps |
|
getDGNodeName :: DGNodeLab -> String |
|
getDGNodeType :: DGNodeLab -> IO String |
|
getDGNodeTypeAux :: DGNodeLab -> String |
|
getDGLinkType :: DGLinkType -> String |
|
getThmType :: ThmLinkStatus -> String |
|
convertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph -> LIB_NAME -> IO ConversionMaps |
|
invContext :: DGraph -> Node -> Context DGNodeLab DGLinkLab |
|
convertEdgesAux :: ConversionMaps -> Descr -> GraphInfo -> [LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps |
|
showReferencedLibrary :: IORef GraphMem -> Descr -> Descr -> GraphInfo -> ConversionMaps -> IO (Descr, GraphInfo, ConversionMaps) |
|
showJustSubtree :: IORef GraphMem -> Descr -> Descr -> ConversionMaps -> [[Node]] -> IO (Descr, [[Node]], Maybe String) |
|
getNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr] |
|
getNodesOfSubtree :: DGraph -> [[Node]] -> Node -> [Node] |
|
elemR :: Eq a => [a] -> a -> Bool |
|
notElemR :: Eq a => [a] -> a -> Bool |
|
applyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> ConversionMaps -> [([DGRule], [DGChange])] -> IO (Descr, ConversionMaps) |
|
applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> Descr -> ConversionMaps -> [DGChange] -> IO (Descr, ConversionMaps) |