to abstract graphs of the graph display interface
share strings to avoid typos
hiding of internal nodes:
internal nodes that are not between named nodes should be kept
display inclusions and inter-logic links in special colour
try different graph layout algorithms for daVinci (dot?)
close program when all windows are closed
issue warning when theory cannot be flattened
different linktypes for local and hiding definition links
import
GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
import Broadcaster(newSimpleBroadcaster,applySimpleUpdate)
import Sources(toSimpleSource)
{- Maps used to track which node resp edge of the abstract graph
correspondes with which of the development graph and vice versa and
one Map to store which libname belongs to which development graph-}
data ConversionMaps = ConversionMaps {
dg2abstrNode :: DGraphToAGraphNode,
dg2abstrEdge :: DGraphToAGraphEdge,
abstr2dgNode :: AGraphToDGraphNode,
abstr2dgEdge :: AGraphToDGraphEdge,
instance PrettyPrint String where
printText0 ga c = ptext (take 25 c)
Pretty.$$ (printText0 ga $ dg2abstrNode convMaps)
Pretty.$$ ptext "dg2abstrEdge"
Pretty.$$ (printText0 ga $ dg2abstrEdge convMaps)
Pretty.$$ ptext "abstr2dgNode"
Pretty.$$ (printText0 ga $ abstr2dgNode convMaps)
Pretty.$$ ptext "abstr2dgEdge"
Pretty.$$ (printText0 ga $ abstr2dgEdge convMaps)
data GraphMem = GraphMem {
-- types of the Maps above
type DGraphToAGraphNode =
Map.Map (LIB_NAME,Node) Descr
type DGraphToAGraphEdge =
Map.Map (LIB_NAME,(Descr,Descr,String)) Descr
type AGraphToDGraphNode =
Map.Map Descr (LIB_NAME,Node)
type AGraphToDGraphEdge =
Map.Map Descr (LIB_NAME,(Descr,Descr,String))
InternalNames { showNames :: Bool,
updater :: [(String,(String -> String) -> IO ())] }
type GInfo = (IORef ProofStatus,
IORef InternalNames, -- show internal names?
initializeConverter :: IO (IORef GraphMem)
showLogicGraph daVinciSort
initGraphInfo <- initgraphs
graphMem <- (newIORef GraphMem{nextGraphId = 0,
graphInfo = initGraphInfo})
{- converts the development graph given by its libname into an abstract graph
and returns the descriptor of the latter, the graphInfo it is contained in
and the conversion maps (see above)-}
convertGraph :: IORef GraphMem -> LIB_NAME -> LibEnv -> HetcatsOpts
-> IO (Descr, GraphInfo, ConversionMaps)
convertGraph graphMem libname libEnv hetsOpts =
do let convMaps = ConversionMaps
{dg2abstrNode =
Map.empty::DGraphToAGraphNode,
abstr2dgNode =
Map.empty::AGraphToDGraphNode,
dg2abstrEdge =
Map.empty::DGraphToAGraphEdge,
abstr2dgEdge =
Map.empty::AGraphToDGraphEdge,
Just globContext@(_,_,dgraph) ->
do (abstractGraph,graphInfo,convRef) <-
initializeGraph graphMem libname dgraph convMaps globContext hetsOpts
return (abstractGraph, graphInfo,convMaps)
do newConvMaps <- convertNodes convMaps abstractGraph
finalConvMaps <- convertEdges newConvMaps abstractGraph
writeIORef convRef finalConvMaps
return (abstractGraph, graphInfo, finalConvMaps)
Nothing -> error ("development graph with libname "
{- initializes an empty abstract graph with the needed node and edge types,
return type equals the one of convertGraph -}
initializeGraph :: IORef GraphMem ->LIB_NAME -> DGraph -> ConversionMaps
-> GlobalContext -> HetcatsOpts
-> IO (Descr,GraphInfo,IORef ConversionMaps)
initializeGraph ioRefGraphMem ln dGraph convMaps globContext hetsOpts = do
graphMem <- readIORef ioRefGraphMem
convRef <- newIORef convMaps
showInternalNames <- newIORef (InternalNames False [])
let proofHistory =
Map.fromList [(key,[([]::[DGRule], []::[DGChange])])|
ioRefProofStatus <- newIORef (ln, libname2dg convMaps,proofHistory)
let gid = nextGraphId graphMem
actGraphInfo = graphInfo graphMem
let gInfo = (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, showInternalNames, hetsOpts, ioRefVisibleNodes)
makegraph ("Development graph for "++show ln)
(do currentPath <- getCurrentDirectory
event <- fileDialogStr "Open..." currentPath
maybeFilePath <- sync event
do openProofStatus filePath ioRefProofStatus convRef hetsOpts
do error ("Could not open file.")
(do proofStatus <- readIORef ioRefProofStatus
writeShATermFile ("./" ++ (show ln) ++ ".log") proofStatus)
-- action on "save as...:"
(do currentPath <- getCurrentDirectory
event <- newFileDialogStr "Save as..." currentPath
maybeFilePath <- sync event
proofStatus <- readIORef ioRefProofStatus
writeShATermFile filePath proofStatus
do error ("Could not save file.")
[GlobalMenu (Menu Nothing
[Menu (Just "Unnamed nodes")
(do (int::InternalNames) <- readIORef showInternalNames
let showThem = not $ showNames int
showIt s = if showThem then s else ""
mapM_ (\(s,upd) -> upd (\_ -> showIt s)) (updater int)
writeIORef showInternalNames (int {showNames = showThem})
redisplay gid actGraphInfo
(do Result descr msg <- hideSetOfNodeTypes gid
Nothing -> do redisplay gid actGraphInfo; return ()
(do descr <- readIORef event
showIt gid descr actGraphInfo
redisplay gid actGraphInfo
(proofMenu gInfo (fmap return . automatic)),
Button "Global Subsumption"
(proofMenu gInfo (fmap return . globSubsume)),
Button "Global Decomposition"
(proofMenu gInfo (fmap return . globDecomp)),
Button "Local Subsumption"
(proofMenu gInfo (fmap return . locSubsume)),
Button "Local Decomposition (merge of rules)"
(proofMenu gInfo (fmap return . locDecomp)),
Button "Hide Theorem Shift"
(proofMenu gInfo (fmap return .
(hideTheoremShift False))),
Button "Theorem Hide Shift"
(proofMenu gInfo (fmap return . theoremHideShift))
createLocalMenuNodeTypeSpec "Magenta" ioRefSubtreeEvents
actGraphInfo ioRefGraphMem gInfo
createLocalMenuNodeTypeSpec "Violet" ioRefSubtreeEvents
actGraphInfo ioRefGraphMem gInfo
createLocalMenuNodeTypeInternal "Grey" gInfo
("locallyEmpty_internal",
createLocalMenuNodeTypeInternal "LightGrey" gInfo
createLocalMenuNodeTypeDgRef "SteelBlue" actGraphInfo
ioRefGraphMem graphMem gInfo
createLocalMenuNodeTypeDgRef "LightSteelBlue"
actGraphInfo ioRefGraphMem graphMem gInfo
-- the link types (share strings to avoid typos)
$$$ createLocalEdgeMenu gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
Solid $$$ Color "Steelblue"
$$$ createLocalEdgeMenu gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
Solid $$$ Color "Lightblue"
$$$ createLocalEdgeMenu gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenu gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ createLocalMenuValueTitleShowConservativity
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ createLocalMenuValueTitleShowConservativity
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ createLocalMenuValueTitleShowConservativity
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ createLocalMenuValueTitleShowConservativity
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
Solid $$$ Color "Lightgreen"
$$$ createLocalEdgeMenuThmEdge gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue),
-- > ######### welche Farbe fuer reference ##########
$$$ createLocalEdgeMenu gInfo
$$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue)]
[("globaldef","globaldef","globaldef"),
("globaldef","def","def"),
("globaldef","hidingdef","hidingdef"),
("globaldef","hetdef","hetdef"),
("globaldef","proventhm","proventhm"),
("globaldef","unproventhm","unproventhm"),
("globaldef","localunproventhm","localunproventhm"),
("def","globaldef","def"),
("def","hidingdef","hidingdef"),
("def","hetdef","hetdef"),
("def","proventhm","proventhm"),
("def","unproventhm","unproventhm"),
("def","localunproventhm","localunproventhm"),
("hidingdef","globaldef","hidingdef"),
("hidingdef","def","def"),
("hidingdef","hidingdef","hidingdef"),
("hidingdef","hetdef","hetdef"),
("hidingdef","proventhm","proventhm"),
("hidingdef","unproventhm","unproventhm"),
("hidingdef","localunproventhm","localunproventhm"),
("hetdef","globaldef","hetdef"),
("hetdef","def","hetdef"),
("hetdef","hidingdef","hetdef"),
("hetdef","hetdef","hetdef"),
("hetdef","proventhm","proventhm"),
("hetdef","unproventhm","unproventhm"),
("hetdef","localunproventhm","localunproventhm"),
("proventhm","globaldef","proventhm"),
("proventhm","def","proventhm"),
("proventhm","hidingdef","proventhm"),
("proventhm","hetdef","proventhm"),
("proventhm","proventhm","proventhm"),
("proventhm","unproventhm","unproventhm"),
("proventhm","localunproventhm","localunproventhm"),
("unproventhm","globaldef","unproventhm"),
("unproventhm","def","unproventhm"),
("unproventhm","hidingdef","unproventhm"),
("unproventhm","hetdef","unproventhm"),
("unproventhm","proventhm","unproventhm"),
("unproventhm","unproventhm","unproventhm"),
("unproventhm","localunproventhm","localunproventhm"),
("localunproventhm","globaldef","localunproventhm"),
("localunproventhm","def","localunproventhm"),
("localunproventhm","hidingdef","localunproventhm"),
("localunproventhm","hetdef","localunproventhm"),
("localunproventhm","proventhm","localunproventhm"),
("localunproventhm","unproventhm","localunproventhm"),
("localunproventhm","localunproventhm","localunproventhm")]
writeIORef ioRefGraphMem graphMem{nextGraphId = gid+1}
graphMem'<- readIORef ioRefGraphMem
return (descr,graphInfo graphMem',convRef)
openProofStatus :: FilePath -> (IORef ProofStatus) -> (IORef ConversionMaps)
openProofStatus filename ioRefProofStatus convRef hetsOpts =
do resultProofStatus <- proofStatusFromShATerm filename
Nothing -> error ("Could not read proof status from file '"
++ (show filename) ++ "'")
Just proofStatus@(ln,libEnv',_) ->
do writeIORef ioRefProofStatus proofStatus
initGraphInfo <- initgraphs
graphMem' <- (newIORef GraphMem{nextGraphId = 0,
graphInfo = initGraphInfo})
(gid, actGraphInfo, convMaps)
<- convertGraph graphMem' ln libEnv' hetsOpts
writeIORef convRef convMaps
redisplay gid actGraphInfo
proofMenu (ioRefProofStatus, event, convRef, gid, ln, actGraphInfo, _, hOpts, ioRefVisibleNodes) proofFun
proofStatus <- readIORef ioRefProofStatus
putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
putIfVerbose hOpts 4 "Analyzing result of proof"
Nothing -> do sequence $ map (putStrLn . show) diags
Just newProofStatus@(ln,libEnv,proofHistory) -> do
writeIORef ioRefProofStatus newProofStatus
convMaps <- readIORef convRef
<- applyChanges gid ln actGraphInfo descr ioRefVisibleNodes
convMapsAux {libname2dg =
Map.insert ln newGlobContext (libname2dg convMapsAux)}
writeIORef event newDescr
writeIORef convRef newConvMaps
redisplay gid actGraphInfo
-> (ProofStatus -> ProofStatus)
proofMenuSef gInfo proofFun =
proofMenu gInfo (return . return . proofFun)
-- -------------------------------------------------------------
-- methods to create the local menus of the different nodetypes
-- -------------------------------------------------------------
-- local menu for the nodetypes spec and locallyEmpty_spec
createLocalMenuNodeTypeSpec color ioRefSubtreeEvents actGraphInfo
ioRefGraphMem gInfo@(_,_,convRef,_,_,_,_,_,ioRefVisibleNodes) =
$$$ ValueTitle (\ (s,_,_) -> return s)
$$$ LocalMenu (Menu (Just "node menu")
[createLocalMenuButtonShowSpec gInfo,
createLocalMenuButtonShowNumberOfNode,
createLocalMenuButtonShowSignature gInfo,
createLocalMenuButtonShowTheory gInfo,
createLocalMenuButtonTranslateTheory gInfo,
createLocalMenuTaxonomy gInfo,
createLocalMenuButtonShowSublogic gInfo,
createLocalMenuButtonShowNodeOrigin gInfo,
createLocalMenuButtonProveAtNode gInfo,
createLocalMenuButtonCCCAtNode gInfo,
createLocalMenuButtonShowJustSubtree ioRefSubtreeEvents
convRef ioRefVisibleNodes ioRefGraphMem
createLocalMenuButtonUndoShowJustSubtree ioRefVisibleNodes
ioRefSubtreeEvents actGraphInfo
]) -- ??? Should be globalized somehow
-- >$$$ LocalMenu (Button "xxx" undefined)
:: DaVinciNodeTypeParms (String,Int,Int)
-- local menu for the nodetypes internal and locallyEmpty_internal
createLocalMenuNodeTypeInternal color
gInfo@(_,_,convRef,_,_,_,showInternalNames,_,_) =
$$$ ValueTitleSource (\ (s,_,_) -> do
b <- newSimpleBroadcaster ""
int <- readIORef showInternalNames
let upd = (s,applySimpleUpdate b)
writeIORef showInternalNames (int {updater = upd:updater int})
return $ toSimpleSource b)
$$$ LocalMenu (Menu (Just "node menu")
[createLocalMenuButtonShowSpec gInfo,
createLocalMenuButtonShowNumberOfNode,
createLocalMenuButtonShowSignature gInfo,
createLocalMenuButtonShowTheory gInfo,
createLocalMenuButtonTranslateTheory gInfo,
createLocalMenuTaxonomy gInfo,
createLocalMenuButtonShowSublogic gInfo,
createLocalMenuButtonProveAtNode gInfo,
createLocalMenuButtonCCCAtNode gInfo,
createLocalMenuButtonShowNodeOrigin gInfo])
:: DaVinciNodeTypeParms (String,Int,Int)
-- local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
createLocalMenuNodeTypeDgRef color actGraphInfo
ioRefGraphMem graphMem (_,_,convRef,_,_,_,_,hetsOpts,_) =
$$$ ValueTitle (\ (s,_,_) -> return s)
$$$ LocalMenu (Button "Show referenced library"
do convMaps <- readIORef convRef
(refDescr, newGraphInfo, refConvMaps) <-
showReferencedLibrary ioRefGraphMem descr
--writeIORef convRef newConvMaps
graphMem{graphInfo = newGraphInfo,
nextGraphId = refDescr +1}
redisplay refDescr newGraphInfo
:: DaVinciNodeTypeParms (String,Int,Int)
-- menu button for local menus
createMenuButton title menuFun (ioProofStatus,_,convRef,_,_,_,_,_,_) =
do convMaps <- readIORef convRef
(ln,libEnv,_) <- readIORef ioProofStatus
createLocalMenuButtonShowSpec = createMenuButton "Show spec" showSpec
createLocalMenuButtonShowSignature =
createMenuButton "Show signature" getSignatureOfNode
createLocalMenuButtonShowTheory gInfo =
createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo
createLocalMenuButtonTranslateTheory gInfo =
createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo
create a sub Menu for taxonomy visualisation
--createLocalMenuTaxonomy :: IORef ProofStatus -> Descr -> AGraphToDGraphNode ->
createLocalMenuTaxonomy ginfo@(proofStatus,_,_,_,_,_,_,_,_) =
(Menu (Just "Taxonomy graphs")
[createMenuButton "Subsort graph"
(passTh displaySubsortGraph) ginfo,
createMenuButton "Concept graph"
(passTh displayConceptGraph) ginfo])
where passTh displayFun descr ab2dgNode dgraph =
do r <- lookupTheoryOfNode proofStatus
displayFun (showPretty n "") gth
showDiags defaultHetcatsOpts diags
createLocalMenuButtonShowSublogic gInfo@(proofStatus,_,_,_,_,_,_,_,_) =
createMenuButton "Show sublogic" (getSublogicOfNode proofStatus) gInfo
createLocalMenuButtonShowNodeOrigin =
createMenuButton "Show origin" showOriginOfNode
createLocalMenuButtonProveAtNode gInfo =
createMenuButton "Prove" (proveAtNode False gInfo) gInfo
createLocalMenuButtonCCCAtNode gInfo =
createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo
createLocalMenuButtonShowJustSubtree ioRefSubtreeEvents convRef
ioRefVisibleNodes ioRefGraphMem actGraphInfo =
(Button "Show just subtree"
do subtreeEvents <- readIORef ioRefSubtreeEvents
("it is already just the subtree of node "
++ (show descr) ++" shown")
do convMaps <- readIORef convRef
visibleNodes <- readIORef ioRefVisibleNodes
(eventDescr,newVisibleNodes,errorMsg) <-
showJustSubtree ioRefGraphMem
descr gid convMaps visibleNodes
Nothing -> do let newSubtreeEvents =
writeIORef ioRefSubtreeEvents
writeIORef ioRefVisibleNodes
redisplay gid actGraphInfo
Just text -> do putStrLn text
createLocalMenuButtonUndoShowJustSubtree ioRefVisibleNodes
ioRefSubtreeEvents actGraphInfo =
(Button "Undo show just subtree"
do visibleNodes <- readIORef ioRefVisibleNodes
case (tail visibleNodes) of
"Complete graph is already shown"
newVisibleNodes@(x:xs) ->
do subtreeEvents <- readIORef ioRefSubtreeEvents
do showIt gid hide_event actGraphInfo
writeIORef ioRefSubtreeEvents
writeIORef ioRefVisibleNodes
redisplay gid actGraphInfo
Nothing -> do putStrLn "undo not possible"
createLocalMenuButtonShowNumberOfNode =
(Button "Show number of node"
-- -------------------------------------------------------------
-- methods to create the local menus for the edges
-- -------------------------------------------------------------
createLocalEdgeMenu gInfo =
LocalMenu (Menu (Just "edge menu")
[createLocalMenuButtonShowMorphismOfEdge gInfo,
createLocalMenuButtonShowOriginOfEdge gInfo,
createLocalMenuButtonCheckconservativityOfEdge gInfo]
createLocalEdgeMenuThmEdge gInfo =
LocalMenu (Menu (Just "thm egde menu")
[createLocalMenuButtonShowMorphismOfEdge gInfo,
createLocalMenuButtonShowOriginOfEdge gInfo,
createLocalMenuButtonShowProofStatusOfThm gInfo,
createLocalMenuButtonCheckconservativityOfEdge gInfo]
createLocalMenuButtonShowMorphismOfEdge _ =
(\ (_,descr,maybeLEdge) ->
do showMorphismOfEdge descr maybeLEdge
createLocalMenuButtonShowOriginOfEdge _ =
(\ (_,descr,maybeLEdge) ->
do showOriginOfEdge descr maybeLEdge
createLocalMenuButtonCheckconservativityOfEdge gInfo =
(Button "Check conservativity (preliminary)"
(\ (ginfo,descr,maybeLEdge) ->
do checkconservativityOfEdge descr gInfo maybeLEdge
createLocalMenuButtonShowProofStatusOfThm _ =
(Button "Show proof status"
(\ (_,descr,maybeLEdge) ->
do showProofStatusOfThm descr maybeLEdge
createLocalMenuValueTitleShowConservativity =
GlobalThm _ c status -> return (showCons c status)
LocalThm _ c status -> return (showCons c status)
showCons :: Conservativity -> ThmLinkStatus -> String
(_,Open) -> (show c) ++ "?"
-- ------------------------------
-- end of local menu definitions
-- ------------------------------
showSpec descr convMap dgraph =
Just (libname,node) -> do
let sp = dgToSpec dgraph node
putStrLn (showPretty sp "")
{- auxiliary method for debugging. shows the number of the given node in the abstraction graph -}
getNumberOfNode :: Descr -> IO()
let title = "Number of node"
in createTextDisplay title (showPretty descr "") [size(10,10)]
{- outputs the signature of a node in a window;
used by the node menu defined in initializeGraph-}
getSignatureOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()
getSignatureOfNode descr ab2dgNode dgraph =
do let dgnode = lab' (context dgraph node)
(DGNode name (G_sign _ sig) _ _ _ _) ->
let title = "Signature of "++showName name
in createTextDisplay title (showPretty sig "") [size(80,50)]
(DGRef _ _ _ _ _) -> error
"nodes of type dg_ref do not have a signature"
Nothing -> error ("node with descriptor "
++ " has no corresponding node in the development graph")
fetches the theory from a node inside the IO Monad
(added by KL based on code in getTheoryOfNode) -}
lookupTheoryOfNode :: IORef ProofStatus -> Descr -> AGraphToDGraphNode ->
lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph = do
(ln,libEnv,_) <- readIORef proofStatusRef
gth <- computeTheory libEnv libNode
{- outputs the theory of a node in a window;
used by the node menu defined in initializeGraph-}
getTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode ->
getTheoryOfNode (proofStatusRef,_,_,_,_,_,_,hetsOpts,_) descr ab2dgNode dgraph = do
r <- lookupTheoryOfNode proofStatusRef descr ab2dgNode dgraph
(Just (n, gth)) -> displayTheory "Theory" n dgraph gth
displayTheory :: String -> Node -> DGraph -> G_theory
displayTheory ext node dgraph gth =
let dgnode = lab' (context dgraph node)
str = showPretty gth "\n" in case dgnode of
(DGNode name (G_sign _ _) _ _ _ _) ->
let thname = showName name
title = ext ++ " of " ++ thname
in createTextSaveDisplay title (thname++".het") str
(DGRef _ _ _ _ _) -> error
"nodes of type dg_ref do not have a theory"
{- translate the theory of a node in a window;
used by the node menu defined in initializeGraph-}
translateTheoryOfNode :: GInfo -> Descr -> AGraphToDGraphNode ->
translateTheoryOfNode gInfo@(proofStatusRef,_,_,_,_,_,_,opts,_) descr ab2dgNode dgraph = do
(_,libEnv,_) <- readIORef proofStatusRef
th <- computeTheory libEnv libNode
do G_theory lid sign sens <- return th
-- find all comorphism paths starting from lid
let paths = findComorphismPaths logicGraph (sublogicOfTh th)
-- let the user choose one
Comorphism cid <- return (paths!!i)
let lidS = sourceLogic cid
sign' <- coerce lidS lid sign
sens' <- coerce lidS lid sens
-- translate theory along chosen comorphism
(G_theory lidT sign'' sens1)
{- outputs the sublogic of a node in a window;
used by the node menu defined in initializeGraph-}
getSublogicOfNode :: IORef ProofStatus -> Descr -> AGraphToDGraphNode -> DGraph -> IO()
getSublogicOfNode proofStatusRef descr ab2dgNode dgraph = do
(_,libEnv,_) <- readIORef proofStatusRef
Just libNode@(_, node) ->
let dgnode = lab' (context dgraph node)
(DGNode name _ _ _ _ _) -> name
in case computeTheory libEnv libNode of
let logstr = show $ sublogicOfTh th
title = "Sublogic of "++showName name
in createTextDisplay title logstr [size(30,10)]
error ("Could not compute theory for sublogic computation: "++
Nothing -> error ("node with descriptor "
++ " has no corresponding node in the development graph")
{- prints the origin of the node -}
showOriginOfNode :: Descr -> AGraphToDGraphNode -> DGraph -> IO()
showOriginOfNode descr ab2dgNode dgraph =
do let dgnode = lab' (context dgraph node)
DGNode name _ _ _ _ orig ->
let title = "Origin of node "++showName name
in createTextDisplay title
(showPretty orig "") [size(30,10)]
DGRef _ _ _ _ _ -> error "showOriginOfNode: no DGNode"
Nothing -> error ("node with descriptor "
++ " has no corresponding node in the development graph")
{- start local theorem proving or consistency checking at a node -}
--proveAtNode :: Bool -> Descr -> AGraphToDGraphNode -> DGraph -> IO()
proveAtNode checkCons gInfo@(_,_,convRef,_,_,_,_,_,_) descr ab2dgNode dgraph =
do convMaps <- readIORef convRef
proofMenu gInfo (basicInferenceNode checkCons logicGraph libNode)
Nothing -> error ("node with descriptor "
++ " has no corresponding node in the development graph")
{- prints the morphism of the edge -}
showMorphismOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showMorphismOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Signature morphism"
((showPretty (dgl_morphism linklab) "")++hidingMorph) [size(150,50)]
hidingMorph = case (dgl_type linklab) of
(HidingThm morph _) -> "\n ++++++ \n"
showMorphismOfEdge descr Nothing =
createTextDisplay "Error"
("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph") [size(30,10)]
{- prints the origin of the edge -}
showOriginOfEdge :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showOriginOfEdge _ (Just (_,_,linklab)) =
createTextDisplay "Origin of link"
(showPretty (dgl_origin linklab) "") [size(30,10)]
showOriginOfEdge descr Nothing =
createTextDisplay "Error"
("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph") [size(30,10)]
{- prints the proof base of the edge -}
showProofStatusOfThm :: Descr -> Maybe (LEdge DGLinkLab) -> IO()
showProofStatusOfThm _ (Just ledge) =
createTextDisplay "Proof Status"
(show (getProofStatusOfThm ledge)) [size(30,10)]
showProofStatusOfThm descr Nothing =
putStrLn ("edge "++(show descr)++" has no corresponding edge"
++ "in the development graph")
{- check conservativity of the edge -}
checkconservativityOfEdge :: Descr -> GInfo -> Maybe (LEdge DGLinkLab) -> IO()
checkconservativityOfEdge _ (ref,_,_,_,_,_,_,opts,_)
(Just (source,target,linklab)) = do
(ln,libEnv,_) <- readIORef ref
let (_,_,dgraph) = maybe (error "checkconservativityOfEdge") id
dgtar = lab' (context dgraph target)
DGNode name _ (G_l_sentence_list lid sens) _ _ _ ->
case dgl_morphism linklab of
GMorphism cid sign1 morphism2 -> do
let morphism2' = case coerce (targetLogic cid) lid morphism2 of
_ -> error "checkconservativityOfEdge: wrong logic"
let th = case computeTheory libEnv (ln, source) of
_ -> error "checkconservativityOfEdge: computeTheory"
G_theory lid1 sign1 sens1 <- return th
case coerce lid1 lid (sign1,sens1) of
conservativityCheck lid (sign2,sens2) morphism2' sens
Just(Just True) -> "The link is conservative"
Just(Just False) -> "The link is not conservative"
_ -> "Could not determine whether link is conservative"
showDiags = unlines (map show diags)
in createTextDisplay "Result of consistency check"
(showRes++"\n"++showDiags) [size(50,50)]
_ -> error "checkconservativityOfEdge: wrong logic"
DGRef _ _ _ _ _ -> error "checkconservativityOfEdge: no DGNode"
checkconservativityOfEdge descr _ Nothing =
createTextDisplay "Error"
("edge " ++ show descr ++ " has no corresponding edge "
++ "in the development graph") [size(30,10)]
getProofStatusOfThm :: (LEdge DGLinkLab) -> ThmLinkStatus
getProofStatusOfThm (_,_,label) =
(LocalThm proofStatus _ _) -> proofStatus
(GlobalThm proofStatus _ _) -> proofStatus
(HidingThm _ proofStatus) -> proofStatus -- richtig?
-- (FreeThm GMorphism Bool) - keinen proofStatus?
_ -> error "the given edge is not a theorem"
{- converts the nodes of the development graph, if it has any,
and returns the resulting conversion maps
if the graph is empty the conversion maps are returned unchanged-}
convertNodes :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertNodes convMaps descr graphInfo dgraph libname
| isEmpty dgraph = do return convMaps
| otherwise = convertNodesAux convMaps
{- auxiliar function for convertNodes if the given list of nodes is
emtpy, it returns the conversion maps unchanged otherwise it adds the
converted first node to the abstract graph and to the affected
conversion maps and afterwards calls itself with the remaining node
convertNodesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LNode DGNodeLab] -> LIB_NAME -> IO ConversionMaps
convertNodesAux convMaps descr graphInfo [] libname = return convMaps
convertNodesAux convMaps descr graphInfo ((node,dgnode):lNodes) libname =
do let nodetype = getDGNodeType dgnode
Result newDescr err <- addnode descr
convertNodesAux convMaps {dg2abstrNode =
Map.insert (libname, node)
newDescr (dg2abstrNode convMaps),
(libname, node) (abstr2dgNode convMaps)}
descr graphInfo lNodes libname
-- | gets the type of a development graph edge as a string
getDGNodeType :: DGNodeLab -> String
(if locallyEmpty dgnode then "locallyEmpty_" else "")
++ case isDGRef dgnode of
False -> if isInternalNode dgnode
getDGLinkType :: DGLinkLab -> String
getDGLinkType lnk = case dgl_type lnk of
if hasIdComorphism $ dgl_morphism lnk then "globaldef"
LocalThm thmLinkStatus _ _ -> "local" ++ getThmType thmLinkStatus ++ "thm"
GlobalThm thmLinkStatus _ _ -> getThmType thmLinkStatus ++ "thm"
HidingThm _ thmLinkStatus -> getThmType thmLinkStatus ++ "hidingthm"
FreeThm _ bool -> if bool then "proventhm" else "unproventhm"
_ -> "def" -- LocalDef, FreeDef, CofreeDef
getThmType :: ThmLinkStatus -> String
getThmType thmLinkStatus =
{- converts the edges of the development graph
works the same way as convertNods does-}
convertEdges :: ConversionMaps -> Descr -> GraphInfo -> DGraph
-> LIB_NAME -> IO ConversionMaps
convertEdges convMaps descr graphInfo dgraph libname
| isEmpty dgraph = do return convMaps
| otherwise = convertEdgesAux convMaps
{- auxiliar function for convertEges --> not yet implemented! -}
convertEdgesAux :: ConversionMaps -> Descr -> GraphInfo ->
[LEdge DGLinkLab] -> LIB_NAME -> IO ConversionMaps
convertEdgesAux convMaps descr graphInfo [] libname = return convMaps
convertEdgesAux convMaps descr graphInfo ((ledge@(src,tar,edgelab)):lEdges)
do let srcnode =
Map.lookup (libname,src) (dg2abstrNode convMaps)
tarnode =
Map.lookup (libname,tar) (dg2abstrNode convMaps)
case (srcnode,tarnode) of
Result newDescr msg <- addlink descr (getDGLinkType edgelab)
"" (Just ledge) s t graphInfo
newConvMaps <- (convertEdgesAux
(libname, (src,tar,show edgelab))
(libname, (src,tar,show edgelab))
descr graphInfo lEdges libname)
_ -> error "Cannot find nodes"
showReferencedLibrary :: IORef GraphMem -> Descr -> Descr -> GraphInfo
-> ConversionMaps -> HetcatsOpts -> IO (Descr, GraphInfo, ConversionMaps)
showReferencedLibrary graphMem descr abstractGraph graphInfo convMaps hetsOpts =
do let (_,(DGRef _ refLibname refNode _ _)) =
labNode' (context dgraph node)
convertGraph graphMem refLibname (libname2dg convMaps) hetsOpts
Nothing -> error ("The referenced library ("
error ("Selected node belongs to unknown library: "
error ("there is no node with the descriptor "
where libname2dgMap = libname2dg convMaps
showJustSubtree:: IORef GraphMem -> Descr -> Descr -> ConversionMaps
-> [[Node]]-> IO (Descr, [[Node]], Maybe String)
showJustSubtree ioRefGraphMem descr abstractGraph convMaps visibleNodes =
Just (libname,parentNode) ->
do let allNodes = getNodeDescriptors (head visibleNodes)
dgNodesOfSubtree = nub (parentNode:(getNodesOfSubtree dgraph
(head visibleNodes) parentNode))
-- the selected node (parentNode) shall not be hidden either,
-- and we already know its descriptor (descr)
nodesOfSubtree = getNodeDescriptors dgNodesOfSubtree
nodesToHide = filter (notElemR nodesOfSubtree) allNodes
graphMem <- readIORef ioRefGraphMem
(Result eventDescr errorMsg) <- hidenodes abstractGraph
nodesToHide (graphInfo graphMem)
return (eventDescr, (dgNodesOfSubtree:visibleNodes), errorMsg)
Just text -> return (-1,text)
Nothing -> return (eventDescr,
("showJustSubtree: Selected node belongs to unknown library: "
error ("showJustSubtree: there is no node with the descriptor "
where libname2dgMap = libname2dg convMaps
getNodeDescriptors :: [Node] -> LIB_NAME -> ConversionMaps -> [Descr]
getNodeDescriptors [] _ _ = []
getNodeDescriptors (node:nodelist) libname convMaps =
case
Map.lookup (libname,node) (dg2abstrNode convMaps) of
Just descr -> descr:(getNodeDescriptors nodelist libname convMaps)
Nothing -> error ("getNodeDescriptors: There is no descriptor for dgnode "
getNodesOfSubtree :: DGraph -> [Node] -> Node -> [Node]
getNodesOfSubtree dgraph visibleNodes node =
(concat (map (getNodesOfSubtree dgraph remainingVisibleNodes) predOfNode))
[n| n <- (pre dgraph node), elem n visibleNodes]
remainingVisibleNodes = [n| n <- visibleNodes, notElem n predOfNode]
elemR :: Eq a => [a] -> a -> Bool
elemR list element = elem element list
notElemR :: Eq a => [a] -> a -> Bool
notElemR list element = notElem element list
-- -- ################ einbindung von
proofs.hs ############
applyChanges :: Descr -> LIB_NAME -> GraphInfo -> Descr -> IORef [[Node]]
-> [([DGRule],[DGChange])]
-> IO (Descr, ConversionMaps)
applyChanges gid libname graphInfo eventDescr ioRefVisibleNodes
[] -> return (eventDescr, convMaps)
[] -> return (eventDescr, convMaps)
visibleNodes <- readIORef ioRefVisibleNodes
(newVisibleNodes, newEventDescr, newConvMaps) <-
applyChangesAux gid libname graphInfo visibleNodes
eventDescr convMaps changes
writeIORef ioRefVisibleNodes newVisibleNodes
return (newEventDescr, newConvMaps)
applyChangesAux :: Descr -> LIB_NAME -> GraphInfo -> [[Node]] -> Descr
-> ConversionMaps -> [DGChange]
-> IO ([[Node]], Descr, ConversionMaps)
applyChangesAux _ _ _ visibleNodes eventDescr convMaps [] =
return (visibleNodes, eventDescr+1, convMaps)
applyChangesAux gid libname graphInfo visibleNodes eventDescr
convMaps (change:changes) =
InsertNode lnode@(node,nodelab) -> do
let nodetype = getDGNodeType nodelab
nodename = getDGNodeName nodelab
addnode gid nodetype nodename graphInfo
do let dgNode = (libname,node)
newVisibleNodes = map (insertElem node) visibleNodes
applyChangesAux gid libname graphInfo newVisibleNodes (descr+1)
error ("applyChangesAux: could not add node " ++ (show node)
++" with name " ++ (show (nodename)) ++ "\n"
DeleteNode lnode@(node,nodelab) -> do
let nodename = getDGNodeName nodelab
(Result descr err) <- delnode gid abstrNode graphInfo
let newVisibleNodes = map (removeElem node) visibleNodes
applyChangesAux gid libname graphInfo newVisibleNodes (descr+1)
Just msg -> error ("applyChangesAux: could not delete node "
++ (show node) ++ " with name "
++ (show nodename) ++ "\n"
Nothing -> error ("applyChangesAux: could not delte node "
++ (show node) ++ " with name "
++ (show nodename) ++": " ++
"node does not exist in abstraction graph")
InsertEdge ledge@(src,tgt,edgelab) ->
do let dg2abstrNodeMap = dg2abstrNode convMaps
(Just abstrSrc, Just abstrTgt) ->
do let dgEdge = (libname, (src,tgt,show edgelab))
addlink gid (getDGLinkType edgelab)
"" (Just ledge) abstrSrc abstrTgt graphInfo
do let newConvMaps = convMaps
applyChangesAux gid libname graphInfo visibleNodes
(descr+1) newConvMaps changes
error ("applyChangesAux: could not add link from "
++ (show src) ++ " to " ++ (show tgt) ++ ":\n"
error ("applyChangesAux: could not add link " ++ (show src)
++ " to " ++ (show tgt) ++ ": illigal end nodes")
DeleteEdge (src,tgt,edgelab) ->
do let dgEdge = (libname, (src,tgt,show edgelab))
dg2abstrEdgeMap = dg2abstrEdge convMaps
do (Result descr err) <- dellink gid abstrEdge graphInfo
do let newConvMaps = convMaps
applyChangesAux gid libname graphInfo visibleNodes
(descr+1) newConvMaps changes
Just msg -> error ("applyChangesAux: could not delete edge "
++ (show abstrEdge) ++ ":\n"
Nothing -> error ("applyChangesAux: deleted edge from "
++ (show src) ++ " to " ++ (show tgt)
++ " of type " ++ (show (dgl_type edgelab))
++ " and origin " ++ (show (dgl_origin edgelab))
++ "graph does not exist in abstraction graph")
removeElem :: Eq a => a -> [a] -> [a]
removeElem element list = [e | e <- list, e /= element]
insertElem :: a -> [a] -> [a]
insertElem element list = element:list