hets -- a heterogenous Specification (CASL) tool setContentsIndex
GUI.ConvertDevToAbstractGraph
Synopsis
data ConversionMaps = ConversionMaps {
dg2abstrNode :: DGraphToAGraphNode
dg2abstrEdge :: DGraphToAGraphEdge
abstr2dgNode :: AGraphToDGraphNode
abstr2dgEdge :: AGraphToDGraphEdge
libname2dg :: LibEnv
}
data GraphMem = GraphMem {
graphInfo :: GraphInfo
nextGraphId :: Descr
}
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)
Produced by Haddock version 0.6