Context Navigation

GraphLogic.hs @ 11173

Revision 11173, 42.1 kB (checked in by maeder, 11 months ago)
support uni version 2 with hierarchical module names
Property svn:eol-style set to `native` Property svn:keywords set to `Author Date Id Revision`

Line
1	{-# OPTIONS -cpp #-}
2	{- \|
3	Module : $Header$
4	Description : Logic for manipulating the graph in the Central GUI
5	Copyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
6	License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7
8	Maintainer : till@informatik.uni-bremen.de
9	Stability : provisional
10	Portability : non-portable (imports Logic)
11
12	This module provides functions for all the menus in the Hets GUI.
13	These are then assembled to the GUI in "GUI.GraphMenu".
14	-}
15
16	module GUI.GraphLogic
17	( undo
18	, reload
19	, performProofAction
20	, openProofStatus
21	, saveProofStatus
22	, nodeErr
23	, proofMenu
24	, showReferencedLibrary
25	, getTheoryOfNode
26	, translateTheoryOfNode
27	, displaySubsortGraph
28	, displayConceptGraph
29	, lookupTheoryOfNode
30	, showProofStatusOfNode
31	, proveAtNode
32	, showNodeInfo
33	, showEdgeInfo
34	, checkconservativityOfEdge
35	, convert
36	, hideNodes
37	, getLibDeps
38	, hideShowNames
39	, showNodes
40	, translateGraph
41	, showLibGraph
42	, runAndLock
43	, saveUDGraph
44	, focusNode
45	, applyChanges
46	) where
47
48	import Logic.Logic(conservativityCheck,map_sen, comp)
49	import Logic.Coerce(coerceSign, coerceMorphism)
50	import Logic.Grothendieck
51	import Logic.Comorphism
52	import Logic.Prover
53	import Comorphisms.LogicGraph(logicGraph)
54
55	import Static.GTheory
56	import Static.DevGraph
57	import Static.PrintDevGraph
58	import Static.DGTranslation(libEnv_translation)
59
60	import Proofs.EdgeUtils
61	import Proofs.InferBasic(basicInferenceNode)
62	import Proofs.StatusUtils(lookupHistory, removeContraryChanges)
63	import Proofs.TheoremHideShift
64
65	import GUI.Taxonomy (displayConceptGraph,displaySubsortGraph)
66	import GUI.DGTranslation(getDGLogic)
67	import GUI.GraphTypes
68	import qualified GUI.GraphAbstraction as GA
69	import GUI.Utils
70
71	#ifdef UNIVERSION2
72	import Graphs.GraphConfigure
73	import Reactor.InfoBus(encapsulateWaitTermAct)
74	import HTk.Toolkit.DialogWin (useHTk)
75	#else
76	import GraphConfigure
77	import InfoBus(encapsulateWaitTermAct)
78	import DialogWin (useHTk)
79	#endif
80	import qualified GUI.HTkUtils as HTk
81
82	import Common.DocUtils (showDoc)
83	import Common.AS_Annotation (isAxiom)
84	import Common.Consistency
85	import Common.ExtSign
86	import Common.LibName
87	import Common.Result as Res
88	import qualified Common.OrderedMap as OMap
89	import qualified Common.Lib.Rel as Rel
90	import qualified Common.Lib.SizedList as SizedList
91
92	import Driver.Options
93	import Driver.WriteLibDefn(writeShATermFile)
94	import Driver.ReadFn(libNameToFile, readVerbose)
95	import Driver.AnaLib(anaLibExt, anaLib)
96
97	import System.Directory(getModificationTime)
98
99	import Data.IORef
100	import Data.Char(toLower)
101	import Data.List(partition)
102	import Data.Graph.Inductive.Graph (Node, LEdge, LNode)
103	import qualified Data.Map as Map
104
105	import Control.Monad
106	import Control.Concurrent (forkIO)
107	import Control.Concurrent.MVar
108
109	-- \| Locks the global lock and runs function
110	runAndLock :: GInfo -> IO () -> IO ()
111	runAndLock (GInfo { functionLock = lock
112	, gi_GraphInfo = actGraphInfo
113	}) function = do
114	locked <- tryPutMVar lock ()
115	case locked of
116	True -> do
117	GA.deactivateGraphWindow actGraphInfo
118	function
119	takeMVar lock
120	GA.redisplay actGraphInfo
121	GA.layoutImproveAll actGraphInfo
122	GA.activateGraphWindow actGraphInfo
123	False ->
124	GA.showTemporaryMessage actGraphInfo
125	$ "an other function is still working ... please wait ..."
126
127	-- \| Undo one step of the History
128	undo :: GInfo -> Bool -> IO ()
129	undo gInfo@(GInfo { globalHist = gHist
130	, gi_GraphInfo = actGraph
131	}) isUndo = do
132	(guHist, grHist) <- takeMVar gHist
133	case if isUndo then guHist else grHist of
134	[] -> do
135	GA.showTemporaryMessage actGraph "History is empty..."
136	putMVar gHist (guHist, grHist)
137	lns : gHist' -> do
138	undoDGraphs gInfo isUndo lns
139	putMVar gHist $ if isUndo then (gHist', reverse lns : grHist)
140	else (reverse lns : guHist, gHist')
141
142	undoDGraphs :: GInfo -> Bool -> [LIB_NAME] -> IO ()
143	undoDGraphs g u = mapM_ $ undoDGraph g u
144
145	undoDGraph :: GInfo -> Bool -> LIB_NAME -> IO ()
146	undoDGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
147	, gi_GraphInfo = actGraph
148	}) isUndo ln = do
149	GA.showTemporaryMessage actGraph $
150	(if isUndo then "Un" else "Re") ++ "do last change to "
151	++ show ln ++ "..."
152	lockGlobal gInfo
153	le <- readIORef ioRefProofStatus
154	let
155	dg = lookupDGraph ln le
156	(dg', changes) = (if isUndo then undoHistStep else redoHistStep) dg
157	writeIORef ioRefProofStatus $ Map.insert ln dg' le
158	case openlock dg' of
159	Nothing -> return ()
160	Just lock -> do
161	mvar <- tryTakeMVar lock
162	case mvar of
163	Nothing -> return ()
164	Just applyHist -> do
165	applyHist changes
166	putMVar lock applyHist
167	unlockGlobal gInfo
168
169	-- \| reloads the Library of the DevGraph
170	reload :: GInfo -> IO()
171	reload gInfo@(GInfo { libEnvIORef = ioRefProofStatus
172	, gi_LIB_NAME = ln
173	, gi_hetcatsOpts = opts
174	, gi_GraphInfo = actGraphInfo
175	}) = do
176	lockGlobal gInfo
177	oldle <- readIORef ioRefProofStatus
178	let
179	libdeps = Rel.toList $ Rel.intransKernel $ Rel.transClosure $ Rel.fromList
180	$ getLibDeps oldle
181	ioruplibs <- newIORef ([] :: [LIB_NAME])
182	writeIORef ioruplibs []
183	reloadLibs ioRefProofStatus opts libdeps ioruplibs ln
184	unlockGlobal gInfo
185	libs <- readIORef ioruplibs
186	case libs of
187	[] -> GA.showTemporaryMessage actGraphInfo "Reload not needed!"
188	_ -> remakeGraph gInfo
189
190	-- \| Creates a list of all LIB_NAME pairs, which have a dependency
191	getLibDeps :: LibEnv -> [(LIB_NAME, LIB_NAME)]
192	getLibDeps le =
193	concat $ map (\ ln -> getDep ln le) $ Map.keys le
194
195	-- \| Creates a list of LIB_NAME pairs for the fist argument
196	getDep :: LIB_NAME -> LibEnv -> [(LIB_NAME, LIB_NAME)]
197	getDep ln le = map (\ (_, x) -> (ln, dgn_libname x)) $
198	filter (isDGRef . snd) $ labNodesDG $ lookupDGraph ln le
199
200	-- \| Reloads a library
201	reloadLib :: IORef LibEnv -> HetcatsOpts -> IORef [LIB_NAME] -> LIB_NAME
202	-> IO ()
203	reloadLib iorle opts ioruplibs ln = do
204	mfile <- existsAnSource opts {intype = GuessIn}
205	$ rmSuffix $ libNameToFile opts ln
206	case mfile of
207	Nothing -> return ()
208	Just file -> do
209	le <- readIORef iorle
210	mFunc <- case openlock $ lookupDGraph ln le of
211	Just lock -> tryTakeMVar lock
212	Nothing -> return Nothing
213	let
214	le' = Map.delete ln le
215	mres <- anaLibExt opts file le'
216	case mres of
217	Just (_, newle) -> do
218	uplibs <- readIORef ioruplibs
219	writeIORef ioruplibs $ ln:uplibs
220	case mFunc of
221	Just func -> case openlock $ lookupDGraph ln newle of
222	Just lock -> putMVar lock func
223	Nothing -> errorDialog "Error"
224	"Reload: Can't set openlock in DevGraph"
225	Nothing -> return ()
226	writeIORef iorle $ newle
227	Nothing ->
228	errorDialog "Error" $ "Error when reloading file " ++ show file
229
230	-- \| Reloads libraries if nessesary
231	reloadLibs :: IORef LibEnv -> HetcatsOpts -> [(LIB_NAME, LIB_NAME)]
232	-> IORef [LIB_NAME] -> LIB_NAME -> IO Bool
233	reloadLibs iorle opts deps ioruplibs ln = do
234	uplibs <- readIORef ioruplibs
235	case elem ln uplibs of
236	True -> return True
237	False -> do
238	let
239	deps' = map (snd) $ filter (\ (ln',_) -> ln == ln') deps
240	res <- mapM (reloadLibs iorle opts deps ioruplibs) deps'
241	let
242	libupdate = foldl (\ u r -> if r then True else u) False res
243	case libupdate of
244	True -> do
245	reloadLib iorle opts ioruplibs ln
246	return True
247	False -> do
248	le <- readIORef iorle
249	let
250	newln:_ = filter (ln ==) $ Map.keys le
251	mfile <- existsAnSource opts $ rmSuffix $ libNameToFile opts ln
252	case mfile of
253	Nothing -> return False
254	Just file -> do
255	newmt <- getModificationTime file
256	let
257	libupdate' = (getModTime $ getLIB_ID newln) < newmt
258	case libupdate' of
259	False -> return False
260	True -> do
261	reloadLib iorle opts ioruplibs ln
262	return True
263
264	-- \| Deletes the old edges and nodes of the Graph and makes new ones
265	remakeGraph :: GInfo -> IO ()
266	remakeGraph gInfo@(GInfo { libEnvIORef = ioRefProofStatus
267	, gi_LIB_NAME = ln
268	, gi_GraphInfo = actGraphInfo
269	}) = do
270	le <- readIORef ioRefProofStatus
271	let
272	dgraph = lookupDGraph ln le
273	showNodes gInfo
274	GA.clear actGraphInfo
275	convert actGraphInfo dgraph
276	hideNodes gInfo
277
278	-- \| Toggles to display internal node names
279	hideShowNames :: GInfo -> Bool -> IO ()
280	hideShowNames (GInfo { internalNamesIORef = showInternalNames
281	}) toggle = do
282	(intrn::InternalNames) <- readIORef showInternalNames
283	let showThem = if toggle then not $ showNames intrn else showNames intrn
284	showItrn s = if showThem then s else ""
285	mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
286	writeIORef showInternalNames $ intrn {showNames = showThem}
287
288	-- \| shows all hidden nodes and edges
289	showNodes :: GInfo -> IO ()
290	showNodes gInfo@(GInfo { gi_GraphInfo = actGraphInfo
291	}) = do
292	hhn <- GA.hasHiddenNodes actGraphInfo
293	case hhn of
294	True -> do
295	GA.showTemporaryMessage actGraphInfo "Revealing hidden nodes ..."
296	GA.showAll actGraphInfo
297	hideShowNames gInfo False
298	False -> do
299	GA.showTemporaryMessage actGraphInfo "No hidden nodes found ..."
300
301	-- \| hides all unnamed internal nodes that are proven
302	hideNodes :: GInfo -> IO ()
303	hideNodes (GInfo { libEnvIORef = ioRefProofStatus
304	, gi_LIB_NAME = ln
305	, gi_GraphInfo = actGraphInfo
306	}) = do
307	hhn <- GA.hasHiddenNodes actGraphInfo
308	case hhn of
309	True ->
310	GA.showTemporaryMessage actGraphInfo "Nodes already hidden ..."
311	False -> do
312	GA.showTemporaryMessage actGraphInfo "Hiding unnamed nodes..."
313	le <- readIORef ioRefProofStatus
314	let dg = lookupDGraph ln le
315	nodes = selectNodesByType dg [DGNodeType
316	{nonRefType = NonRefType
317	{isProvenCons = True
318	, isInternalSpec = True}
319	, isLocallyEmpty = True}]
320	edges = getCompressedEdges dg nodes
321	GA.hideNodes actGraphInfo nodes edges
322
323	-- \| selects all nodes of a type with outgoing edges
324	selectNodesByType :: DGraph -> [DGNodeType] -> [Node]
325	selectNodesByType dg types =
326	filter (\ n -> outDG dg n /= []) $ map fst
327	$ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg
328
329	-- \| compresses a list of types to the highest one
330	compressTypes :: [DGEdgeType] -> DGEdgeType
331	compressTypes [] = error "compressTypes: wrong usage"
332	compressTypes (t:[]) = t
333	compressTypes (t1:t2:r) = case t1 > t2 of
334	True -> compressTypes (t1:r)
335	False -> compressTypes (t2:r)
336
337	-- \| returns a list of compressed edges
338	getCompressedEdges :: DGraph -> [Node] -> [(Node,Node,DGEdgeType)]
339	getCompressedEdges dg hidden =
340	filterDuplicates $ getShortPaths $ concat
341	$ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden [])
342	inEdges
343	where
344	inEdges = filter (\ (_,t,_) -> elem t hidden)
345	$ concat $ map (outDG dg)
346	$ foldr (\ n i -> if elem n hidden
347	\|\| elem n i then i else n:i) []
348	$ map (\ (s,_,_) -> s) $ concat $ map (innDG dg) hidden
349
350	-- \| filter duplicate paths
351	filterDuplicates :: [(Node,Node,DGEdgeType)]
352	-> [(Node,Node,DGEdgeType)]
353	filterDuplicates [] = []
354	filterDuplicates ((s,t,et):r) = edge:filterDuplicates others
355	where
356	(same,others) = partition (\ (s',t',_) -> s == s' && t == t') r
357	edge = (s,t,compressTypes $ et:map (\ (_,_,et') -> et') same)
358
359	-- \| returns the pahts of a given node through hidden nodes
360	getPaths :: DGraph -> Node -> [Node] -> [Node] -> [[LEdge DGLinkLab]]
361	getPaths dg node hidden seen' = case elem node hidden of
362	True -> case edges /= [] of
363	True -> concat $ map (\ e@(_,t,_) -> map (e:) $ getPaths dg t hidden seen)
364	edges
365	False -> []
366	False -> [[]]
367	where
368	seen = node:seen'
369	edges = filter (\ (_,t,_) -> notElem t seen) $ outDG dg node
370
371	-- \| returns source and target node of a path with the compressed type
372	getShortPaths :: [[LEdge DGLinkLab]]
373	-> [(Node,Node,DGEdgeType)]
374	getShortPaths [] = []
375	getShortPaths (p:r) =
376	((s,t,compressTypes $ map (\ (_,_,e) -> getRealDGLinkType e) p))
377	: getShortPaths r
378	where
379	(s,_,_) = head p
380	(_,t,_) = last p
381
382	-- \| Let the user select a Node to focus
383	focusNode :: GInfo -> IO ()
384	focusNode GInfo { libEnvIORef = ioRefProofStatus
385	, gi_LIB_NAME = ln
386	, gi_GraphInfo = grInfo } = do
387	le <- readIORef ioRefProofStatus
388	idsnodes <- filterM (fmap not . GA.isHiddenNode grInfo . fst)
389	$ labNodesDG $ lookupDGraph ln le
390	selection <- listBox "Select a node to focus"
391	$ map (\ (n, l) -> shows n " " ++ getDGNodeName l) idsnodes
392	case selection of
393	Just idx -> GA.focusNode grInfo $ fst $ idsnodes !! idx
394	Nothing -> return ()
395
396	translateGraph :: GInfo -> ConvFunc -> LibFunc -> IO ()
397	translateGraph (GInfo {libEnvIORef = ioRefProofStatus,
398	gi_LIB_NAME = ln,
399	gi_hetcatsOpts = opts
400	}) convGraph showLib = do
401	le <- readIORef ioRefProofStatus
402	openTranslateGraph le ln opts (getDGLogic le) convGraph showLib
403
404	showLibGraph :: GInfo -> LibFunc -> IO ()
405	showLibGraph gInfo showLib = do
406	showLib gInfo
407	return ()
408
409	{- \| it tries to perform the given action to the given graph.
410	If part of the given graph is not hidden, then the action can
411	be performed directly; otherwise the graph will be shown completely
412	firstly, and then the action will be performed, and after that the graph
413	will be hidden again.
414	-}
415	performProofAction :: GInfo -> IO () -> IO ()
416	performProofAction gInfo@(GInfo { gi_GraphInfo = actGraphInfo
417	}) proofAction = do
418	let actionWithMessage = do
419	GA.showTemporaryMessage actGraphInfo
420	"Applying development graph calculus proof rule..."
421	proofAction
422	hhn <- GA.hasHiddenNodes actGraphInfo
423	case hhn of
424	True -> do
425	showNodes gInfo
426	actionWithMessage
427	hideNodes gInfo
428	False -> actionWithMessage
429	GA.showTemporaryMessage actGraphInfo
430	"Development graph calculus proof rule finished."
431
432	saveProofStatus :: GInfo -> FilePath -> IO ()
433	saveProofStatus (GInfo { libEnvIORef = ioRefProofStatus
434	, gi_LIB_NAME = ln
435	, gi_hetcatsOpts = opts
436	}) file = encapsulateWaitTermAct $ do
437	proofStatus <- readIORef ioRefProofStatus
438	writeShATermFile file (ln, lookupHistory ln proofStatus)
439	putIfVerbose opts 2 $ "Wrote " ++ file
440
441	-- \| implementation of open menu, read in a proof status
442	openProofStatus :: GInfo -> FilePath -> ConvFunc -> LibFunc
443	-> IO ()
444	openProofStatus gInfo@(GInfo { libEnvIORef = ioRefProofStatus
445	, gi_LIB_NAME = ln
446	, gi_hetcatsOpts = opts
447	}) file convGraph showLib = do
448	mh <- readVerbose opts ln file
449	case mh of
450	Nothing -> errorDialog "Error" $ "Could not read proof status from file '"
451	++ file ++ "'"
452	Just h -> do
453	let libfile = libNameToFile opts ln
454	m <- anaLib opts { outtypes = [] } libfile
455	case m of
456	Nothing -> errorDialog "Error"
457	$ "Could not read original development graph from '"
458	++ libfile ++ "'"
459	Just (_, libEnv) -> case Map.lookup ln libEnv of
460	Nothing -> errorDialog "Error" $ "Could not get original"
461	++ "development graph for '" ++ showDoc ln "'"
462	Just dg -> do
463	lockGlobal gInfo
464	oldEnv <- readIORef ioRefProofStatus
465	let proofStatus = Map.insert ln
466	(applyProofHistory h dg) oldEnv
467	writeIORef ioRefProofStatus proofStatus
468	unlockGlobal gInfo
469	gInfo' <- copyGInfo gInfo ln
470	convGraph gInfo' "Proof Status " showLib
471	let actGraphInfo = gi_GraphInfo gInfo
472	GA.deactivateGraphWindow actGraphInfo
473	GA.redisplay actGraphInfo
474	GA.layoutImproveAll actGraphInfo
475	GA.activateGraphWindow actGraphInfo
476
477	-- \| apply a rule of the development graph calculus
478	proofMenu :: GInfo
479	-> (LibEnv -> IO (Res.Result LibEnv))
480	-> IO ()
481	proofMenu gInfo@(GInfo { libEnvIORef = ioRefProofStatus
482	, gi_LIB_NAME = ln
483	, gi_GraphInfo = actGraphInfo
484	, gi_hetcatsOpts = hOpts
485	, proofGUIMVar = guiMVar
486	, globalHist = gHist
487	}) proofFun = do
488	filled <- tryPutMVar guiMVar Nothing
489	if not filled
490	then readMVar guiMVar >>=
491	(maybe (putIfVerbose hOpts 0 "proofMenu: ignored Nothing")
492	(\ w -> do
493	putIfVerbose hOpts 4 $
494	"proofMenu: Ignored Proof command; " ++
495	"maybe a proof window is still open?"
496	HTk.putWinOnTop w))
497	else do
498	lockGlobal gInfo
499	proofStatus <- readIORef ioRefProofStatus
500	putIfVerbose hOpts 4 "Proof started via \"Proofs\" menu"
501	Res.Result ds res <- proofFun proofStatus
502	putIfVerbose hOpts 4 "Analyzing result of proof"
503	case res of
504	Nothing -> do
505	unlockGlobal gInfo
506	printDiags 2 ds
507	Just newProofStatus -> do
508	let newGr = lookupDGraph ln newProofStatus
509	history = snd $ splitHistory (lookupDGraph ln proofStatus) newGr
510	(guHist, grHist) <- takeMVar gHist
511	doDump hOpts "PrintHistory" $ do
512	putStrLn "History"
513	print $ prettyHistory history
514	putMVar gHist
515	(calcGlobalHistory proofStatus newProofStatus : guHist, grHist)
516	applyChanges actGraphInfo $ reverse
517	$ flatHistory history
518	writeIORef ioRefProofStatus newProofStatus
519	unlockGlobal gInfo
520	hideShowNames gInfo False
521	mGUIMVar <- tryTakeMVar guiMVar
522	maybe (fail $ "should be filled with Nothing after proof attempt")
523	(const $ return ())
524	mGUIMVar
525
526	calcGlobalHistory :: LibEnv -> LibEnv -> [LIB_NAME]
527	calcGlobalHistory old new = let
528	length' = \ ln -> SizedList.size . proofHistory . lookupDGraph ln
529	changes = filter (\ ln -> length' ln old < length' ln new) $ Map.keys old
530	in concatMap (\ ln -> replicate (length' ln new - length' ln old) ln) changes
531
532	nodeErr :: Int -> IO ()
533	nodeErr descr = error $ "node with descriptor " ++ show descr
534	++ " has no corresponding node in the development graph"
535
536	showNodeInfo :: Int -> DGraph -> IO ()
537	showNodeInfo descr dgraph = do
538	let dgnode = labDG dgraph descr
539	title = (if isDGRef dgnode then ("reference " ++) else
540	if isInternalNode dgnode then ("internal " ++) else id)
541	"node " ++ getDGNodeName dgnode ++ " " ++ show descr
542	createTextDisplay title (title ++ "\n" ++ showDoc dgnode "")
543
544	{- \|
545	fetches the theory from a node inside the IO Monad
546	(added by KL based on code in getTheoryOfNode) -}
547	lookupTheoryOfNode :: IORef LibEnv -> LIB_NAME -> Int
548	-> IO (Res.Result (LibEnv, Node, G_theory))
549	lookupTheoryOfNode proofStatusRef ln descr = do
550	libEnv <- readIORef proofStatusRef
551	return $ do
552	(libEnv', gth) <- computeTheory True libEnv ln descr
553	return (libEnv', descr, gth)
554
555	showDiagMess :: HetcatsOpts -> [Diagnosis] -> IO ()
556	showDiagMess opts ds = let es = Res.filterDiags (verbose opts) ds in
557	if null es then return () else
558	(if hasErrors es then errorDialog "Error" else infoDialog "Info") $ unlines
559	$ map show es
560
561	{- \| outputs the theory of a node in a window;
562	used by the node menu defined in initializeGraph-}
563	getTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
564	getTheoryOfNode gInfo@(GInfo { gi_LIB_NAME = ln
565	, gi_GraphInfo = actGraphInfo
566	, libEnvIORef = le
567	}) descr dgraph = do
568	r <- lookupTheoryOfNode le ln descr
569	case r of
570	Res.Result ds res -> do
571	showDiagMess (gi_hetcatsOpts gInfo) ds
572	case res of
573	(Just (le', n, gth)) -> do
574	lockGlobal gInfo
575	displayTheoryWithWarning "Theory" (getNameOfNode n dgraph)
576	(addHasInHidingWarning dgraph n) gth
577	let newGr = lookupDGraph ln le'
578	libEnv <- readIORef le
579	let history = snd $ splitHistory (lookupDGraph ln libEnv) newGr
580	applyChanges actGraphInfo $ reverse $ flatHistory history
581	writeIORef le le'
582	unlockGlobal gInfo
583	_ -> return ()
584
585	{- \| translate the theory of a node in a window;
586	used by the node menu defined in initializeGraph-}
587	translateTheoryOfNode :: GInfo -> Int -> DGraph -> IO ()
588	translateTheoryOfNode
589	gInfo@(GInfo {gi_hetcatsOpts = opts, libEnvIORef = le}) node dgraph = do
590	libEnv <- readIORef le
591	let Res.Result ds mEnv = computeTheory False libEnv (gi_LIB_NAME gInfo) node
592	case mEnv of
593	Just (_, th@(G_theory lid sign _ sens _)) -> do
594	-- find all comorphism paths starting from lid
595	let paths = findComorphismPaths logicGraph (sublogicOfTh th)
596	-- let the user choose one
597	sel <- listBox "Choose a node logic translation" $ map show paths
598	case sel of
599	Nothing -> errorDialog "Error" "no node logic translation chosen"
600	Just i -> do
601	Comorphism cid <- return (paths!!i)
602	-- adjust lid's
603	let lidS = sourceLogic cid
604	lidT = targetLogic cid
605	sign' <- coerceSign lid lidS "" sign
606	sens' <- coerceThSens lid lidS "" sens
607	-- translate theory along chosen comorphism
608	let Result es mTh = wrapMapTheory cid
609	(plainSign sign', toNamedList sens')
610	case mTh of
611	Nothing -> showDiagMess opts es
612	Just (sign'', sens1) -> displayTheoryWithWarning
613	"Translated Theory" (getNameOfNode node dgraph)
614	(addHasInHidingWarning dgraph node)
615	(G_theory lidT (mkExtSign sign'') startSigId
616	(toThSens sens1) startThId)
617	Nothing -> showDiagMess opts ds
618
619	-- \| Show proof status of a node
620	showProofStatusOfNode :: GInfo -> Int -> DGraph -> IO ()
621	showProofStatusOfNode _ descr dgraph = do
622	let dgnode = labDG dgraph descr
623	stat = showStatusAux dgnode
624	title = "Proof status of node "++showName (dgn_name dgnode)
625	createTextDisplay title stat
626
627	showStatusAux :: DGNodeLab -> String
628	showStatusAux dgnode =
629	case dgn_theory dgnode of
630	G_theory _ _ _ sens _ ->
631	let goals = OMap.filter (not . isAxiom) sens
632	(proven,open) = OMap.partition isProvenSenStatus goals
633	consGoal = "\nconservativity of this node"
634	in "Proven proof goals:\n"
635	++ showDoc proven ""
636	++ if not $ hasOpenConsStatus True dgnode
637	then consGoal
638	else ""
639	++ "\nOpen proof goals:\n"
640	++ showDoc open ""
641	++ if hasOpenConsStatus False dgnode
642	then consGoal
643	else ""
644
645	-- \| start local theorem proving or consistency checking at a node
646	proveAtNode :: Bool -> GInfo -> Int -> DGraph -> IO ()
647	proveAtNode checkCons gInfo@(GInfo { libEnvIORef = ioRefProofStatus
648	, gi_LIB_NAME = ln
649	, commandHist = ch }) descr dgraph = do
650	let dgn = labDG dgraph descr
651	libNode = (ln,descr)
652	(dgraph',dgn') <- case hasLock dgn of
653	True -> return (dgraph, dgn)
654	False -> do
655	lockGlobal gInfo
656	le <- readIORef ioRefProofStatus
657	(dgraph',dgn') <- initLocking (lookupDGraph ln le) (descr, dgn)
658	writeIORef ioRefProofStatus $ Map.insert ln dgraph' le
659	unlockGlobal gInfo
660	return (dgraph',dgn')
661	locked <- tryLockLocal dgn'
662	case locked of
663	False -> do
664	errorDialog "Error" "Proofwindow already open"
665	True -> do
666	let action = do
667	le <- readIORef ioRefProofStatus
668	guiMVar <- newMVar Nothing
669	res <- basicInferenceNode checkCons logicGraph libNode ln
670	guiMVar le ch
671	runProveAtNode checkCons gInfo (descr, dgn') res
672	unlockLocal dgn'
673	case checkCons \|\| not (hasIncomingHidingEdge dgraph' $ snd libNode) of
674	True -> do
675	forkIO action
676	return ()
677	False -> do
678	b <- warningDialog "Warning"
679	"This node has incoming hiding links!\n Prove anyway?"
680	$ Just action
681	unless b $ unlockLocal dgn'
682	return ()
683
684	runProveAtNode :: Bool -> GInfo -> LNode DGNodeLab
685	-> Res.Result (LibEnv, Res.Result G_theory) -> IO ()
686	runProveAtNode checkCons gInfo (v, dgnode) res = case maybeResult res of
687	Just (le, tres) -> do
688	let nodetext = getDGNodeName dgnode ++ " node: " ++ show v
689	when checkCons $ case maybeResult tres of
690	Just gth -> createTextSaveDisplay
691	("Model for " ++ nodetext)
692	"model.log" $ showDoc gth ""
693	Nothing -> case diags tres of
694	ds -> infoDialog nodetext
695	$ unlines $ "could not (re-)construct a model" : map diagString ds
696	proofMenu gInfo $ mergeDGNodeLab gInfo
697	(v, labDG (lookupDGraph (gi_LIB_NAME gInfo) le) v)
698	Nothing -> return ()
699
700	mergeDGNodeLab :: GInfo -> LNode DGNodeLab -> LibEnv -> IO (Res.Result LibEnv)
701	mergeDGNodeLab (GInfo{gi_LIB_NAME = ln}) (v, new_dgn) le = do
702	let dg = lookupDGraph ln le
703	old_dgn = labDG dg v
704	return $ do
705	theory <- joinG_sentences (dgn_theory old_dgn) $ dgn_theory new_dgn
706	let new_dgn' = old_dgn { dgn_theory = theory }
707	dg'' = changeDGH dg $ SetNodeLab old_dgn (v, new_dgn')
708	return $ Map.insert ln dg'' le
709
710	-- \| print the id, origin, type, proof-status and morphism of the edge
711	showEdgeInfo :: Int -> Maybe (LEdge DGLinkLab) -> IO ()
712	showEdgeInfo descr me = case me of
713	Just e@(_, _, l) -> let estr = showLEdge e in
714	infoDialog ("Info of " ++ estr)
715	(estr ++ "\n" ++ showDoc l "")
716	Nothing -> errorDialog "Error"
717	("edge " ++ show descr ++ " has no corresponding edge"
718	++ "in the development graph")
719
720	conservativityRule :: DGRule
721	conservativityRule = DGRule "ConservativityCheck"
722
723	-- \| check conservativity of the edge
724	checkconservativityOfEdge :: Int -> GInfo -> Maybe (LEdge DGLinkLab) -> IO ()
725	checkconservativityOfEdge _ gInfo@(GInfo{gi_LIB_NAME = ln,
726	gi_GraphInfo = _actGraphInfo,
727	libEnvIORef = le})
728	(Just (source,target,linklab)) = do
729	lockGlobal gInfo
730	libEnv <- readIORef $ libEnvIORef gInfo
731	let libEnv' = case convertToNf ln libEnv target of
732	Result _ (Just lE) -> lE
733	_ -> error "checkconservativityOfEdge: convertToNf"
734	let (_, thTar) =
735	case computeTheory True libEnv' ln target of
736	Res.Result _ (Just th1) -> th1
737	_ -> error "checkconservativityOfEdge: computeTheory"
738	G_theory lid _sign _ sensTar _ <- return thTar
739	GMorphism cid _ _ morphism2 _ <- return $ dgl_morphism linklab
740	Just (GMorphism cid' _ _ morphism3 _) <- return $
741	dgn_sigma $ labDG (lookupDGraph ln libEnv') target
742	morphism2' <- coerceMorphism (targetLogic cid) lid
743	"checkconservativityOfEdge2" morphism2
744	morphism3' <- coerceMorphism (targetLogic cid') lid
745	"checkconservativityOfEdge3" morphism3
746	let compMor = case comp morphism2' morphism3' of
747	Res.Result _ (Just phi) -> phi
748	_ -> error "checkconservativtiyOfEdge: comp"
749	let (_le', thSrc) =
750	case computeTheory False libEnv' (gi_LIB_NAME gInfo) source of
751	Res.Result _ (Just th1) -> th1
752	_ -> error "checkconservativityOfEdge: computeTheory"
753	G_theory lid1 sign1 _ sensSrc1 _ <- return thSrc
754	sign2 <- coerceSign lid1 lid "checkconservativityOfEdge.coerceSign" sign1
755	sensSrc2 <- coerceThSens lid1 lid "checkconservativityOfEdge1" sensSrc1
756	let transSensSrc = propagateErrors
757	$ mapThSensValueM (map_sen lid compMor) sensSrc2
758	if length (conservativityCheck lid) < 1
759	then
760	do
761	infoDialog "Result of conservativity check"
762	"No conservativity checkers available"
763	writeIORef le libEnv'
764	unlockGlobal gInfo
765	else
766	do
767	checkerR <- conservativityChoser $ conservativityCheck lid
768	if Res.hasErrors $ Res.diags checkerR
769	then
770	do
771	infoDialog "Result of conservativity check"
772	"No conservativity checker chosen"
773	writeIORef le libEnv'
774	unlockGlobal gInfo
775	else
776	do
777	let chCons = checkConservativity $
778	maybe (error "checkconservativityOfEdge4") id
779	$ Res.maybeResult $ checkerR
780	let Res.Result ds res =
781	chCons
782	(plainSign sign2, toNamedList sensSrc2)
783	compMor $ toNamedList
784	(sensTar `OMap.difference` transSensSrc)
785	showObls [] = ""
786	showObls obls = ", provided that the following proof obligations "
787	++ "can be discharged:\n"
788	++ concatMap (flip showDoc "\n") obls
789	showRes = case res of
790	Just (Just (cst, obls)) -> "The link is "
791	++ showConsistencyStatus cst ++ showObls obls
792	_ -> "Could not determine whether link is conservative"
793	myDiags = showRelDiags 2 ds
794	createTextDisplay "Result of conservativity check"
795	(showRes ++ "\n" ++ myDiags)
796	let
797	consShow = case res of
798	Just (Just (cst, _)) -> cst
799	_ -> Unknown "Unknown"
800	GlobalThm proven conserv _ = dgl_type linklab
801	consNew = if ((show conserv) == (showToComply consShow))
802	then
803	Proven conservativityRule emptyProofBasis
804	else
805	LeftOpen
806	provenEdge = (source
807	,target
808	,linklab
809	{
810	dgl_type = GlobalThm proven conserv consNew
811	}
812	)
813	changes = [ DeleteEdge (source,target,linklab)
814	, InsertEdge provenEdge ]
815	let newGr = lookupDGraph ln libEnv'
816	nextGr = changesDGH newGr changes
817	newLibEnv = Map.insert ln
818	(groupHistory newGr conservativityRule nextGr) libEnv'
819	-- applyChanges actGraphInfo history
820	writeIORef le newLibEnv
821	unlockGlobal gInfo
822
823	checkconservativityOfEdge descr _ Nothing =
824	errorDialog "Error"
825	("edge " ++ show descr ++ " has no corresponding edge "
826	++ "in the development graph")
827
828	-- \| Graphical choser for conservativity checkers
829	conservativityChoser :: [ConservativityChecker sign sentence morphism]
830	-> IO
831	(Res.Result (ConservativityChecker
832	sign sentence morphism))
833	conservativityChoser checkers =
834	case length $ checkers of
835	0 -> return $ fail "No conservativity checkers available"
836	1 -> return $ return $ head $ checkers
837	_ ->
838	do
839	chosenOne <- listBox "Pick a conservativity checker"
840	$ map checker_id checkers
841	case chosenOne of
842	Nothing -> return $ fail "No conservativity checker chosen"
843	Just i -> return $ return $ (checkers !! i)
844
845	-- \| converts a DGraph
846	convert :: GA.GraphInfo -> DGraph -> IO ()
847	convert ginfo dgraph = do
848	convertNodes ginfo dgraph
849	convertEdges ginfo dgraph
850
851	{- \| converts the nodes of the development graph, if it has any,
852	and returns the resulting conversion maps
853	if the graph is empty the conversion maps are returned unchanged-}
854	convertNodes :: GA.GraphInfo -> DGraph -> IO ()
855	convertNodes ginfo = mapM_ (convertNodesAux ginfo) .labNodesDG
856
857	{- \| auxiliary function for convertNodes if the given list of nodes is
858	emtpy, it returns the conversion maps unchanged otherwise it adds the
859	converted first node to the abstract graph and to the affected
860	conversion maps and afterwards calls itself with the remaining node
861	list -}
862	convertNodesAux :: GA.GraphInfo -> LNode DGNodeLab -> IO ()
863	convertNodesAux ginfo (node, dgnode) =
864	GA.addNode ginfo node (getRealDGNodeType dgnode) $ getDGNodeName dgnode
865
866	{- \| converts the edges of the development graph
867	works the same way as convertNods does-}
868	convertEdges :: GA.GraphInfo -> DGraph -> IO ()
869	convertEdges ginfo = mapM_ (convertEdgesAux ginfo) . labEdgesDG
870
871	-- \| auxiliary function for convertEges
872	convertEdgesAux :: GA.GraphInfo -> LEdge DGLinkLab -> IO ()
873	convertEdgesAux ginfo e@(src, tar, lbl) =
874	GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tar "" $ Just e
875
876	-- \| show library referened by a DGRef node (=node drawn as a box)
877	showReferencedLibrary :: Int -> GInfo -> ConvFunc -> LibFunc -> IO ()
878	showReferencedLibrary descr gInfo@(GInfo { libEnvIORef = ioRefProofStatus
879	, gi_LIB_NAME = ln })
880	convGraph showLib = do
881	le <- readIORef ioRefProofStatus
882	let refNode = labDG (lookupDGraph ln le) descr
883	refLibname = if isDGRef refNode then dgn_libname refNode
884	else error "showReferencedLibrary"
885	case Map.lookup refLibname le of
886	Just _ -> do
887	gInfo' <- copyGInfo gInfo refLibname
888	convGraph gInfo' "development graph" showLib
889	let gv = gi_GraphInfo gInfo'
890	GA.deactivateGraphWindow gv
891	hideNodes gInfo'
892	GA.redisplay gv
893	GA.layoutImproveAll gv
894	GA.showTemporaryMessage gv "Development Graph initialized."
895	GA.activateGraphWindow gv
896	return ()
897	Nothing -> error $ "The referenced library (" ++ show refLibname
898	++ ") is unknown"
899
900	-- \| apply the changes of first history item (computed by proof rules,
901	-- see folder Proofs) to the displayed development graph
902	applyChanges :: GA.GraphInfo -> [DGChange] -> IO ()
903	applyChanges ginfo = mapM_ (applyChangesAux ginfo) . removeContraryChanges
904
905	-- \| auxiliary function for applyChanges
906	applyChangesAux :: GA.GraphInfo -> DGChange -> IO ()
907	applyChangesAux ginfo change =
908	case change of
909	SetNodeLab _ (node, newLab) ->
910	GA.changeNodeType ginfo node $ getRealDGNodeType newLab
911	InsertNode (node, nodelab) ->
912	GA.addNode ginfo node (getRealDGNodeType nodelab) $ getDGNodeName nodelab
913	DeleteNode (node, _) ->
914	GA.delNode ginfo node
915	InsertEdge e@(src, tgt, lbl) ->
916	GA.addEdge ginfo (dgl_id lbl) (getRealDGLinkType lbl) src tgt "" $ Just e
917	DeleteEdge (_, _, lbl) ->
918	GA.delEdge ginfo $ dgl_id lbl
919
920	-- \| display a window of translated graph with maximal sublogic.
921	openTranslateGraph :: LibEnv -> LIB_NAME -> HetcatsOpts
922	-> Res.Result G_sublogics -> ConvFunc -> LibFunc -> IO ()
923	openTranslateGraph libEnv ln opts (Res.Result diagsSl mSublogic) convGraph
924	showLib =
925	-- if an error existed by the search of maximal sublogicn
926	-- (see GUI.DGTranslation.getDGLogic), the process need not to go on.
927	let myErrMess = showDiagMess opts in
928	if hasErrors diagsSl then myErrMess diagsSl else case mSublogic of
929	Nothing -> errorDialog "Error" "the maximal sublogic is not found."
930	Just sublogic -> do
931	let paths = findComorphismPaths logicGraph sublogic
932	if null paths then
933	errorDialog "Error" "This graph has no comorphism to translation."
934	else do
935	-- the user choose one
936	sel <- listBox "Choose a logic translation"
937	$ map show paths
938	case sel of
939	Nothing -> errorDialog "Error" "no logic translation chosen"
940	Just j -> do
941	-- graph translation.
942	let Res.Result diagsTrans mLEnv =
943	libEnv_translation libEnv $ paths !! j
944	case mLEnv of
945	Just newLibEnv -> do
946	showDiagMess opts $ diagsSl ++ diagsTrans
947	dg_showGraphAux
948	(\gI@(GInfo{libEnvIORef = iorLE}) -> do
949	writeIORef iorLE newLibEnv
950	convGraph (gI{ gi_LIB_NAME = ln
951	, gi_hetcatsOpts = opts})
952	"translation Graph" showLib)
953	Nothing -> myErrMess $ diagsSl ++ diagsTrans
954
955	dg_showGraphAux :: (GInfo -> IO ()) -> IO ()
956	dg_showGraphAux convFct = do
957	useHTk -- All messages are displayed in TK dialog windows
958	-- from this point on
959	gInfo <- emptyGInfo
960	convFct gInfo
961	let actGraphInfo = gi_GraphInfo gInfo
962	GA.deactivateGraphWindow actGraphInfo
963	GA.redisplay actGraphInfo
964	GA.layoutImproveAll actGraphInfo
965	GA.activateGraphWindow actGraphInfo
966
967	-- DaVinciGraph to String
968	-- Functions to convert a DaVinciGraph to a String to store as a .udg file
969
970	-- \| saves the uDrawGraph graph to a file
971	saveUDGraph :: GInfo -> Map.Map DGNodeType (Shape value, String)
972	-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String) -> IO ()
973	saveUDGraph gInfo@(GInfo { gi_GraphInfo = graphInfo
974	, gi_LIB_NAME = ln
975	, gi_hetcatsOpts = opts
976	}) nodemap linkmap = do
977	maybeFilePath <- fileSaveDialog ((rmSuffix $ libNameToFile opts ln) ++ ".udg")
978	[ ("uDrawGraph",["*.udg"])
979	, ("All Files", ["*"])] Nothing
980	case maybeFilePath of
981	Just filepath -> do
982	GA.showTemporaryMessage graphInfo "Converting graph..."
983	nstring <- nodes2String gInfo nodemap linkmap
984	writeFile filepath nstring
985	GA.showTemporaryMessage graphInfo $ "Graph stored to " ++ filepath ++ "!"
986	Nothing -> GA.showTemporaryMessage graphInfo $ "Aborted!"
987
988	-- \| Converts the nodes of the graph to String representation
989	nodes2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
990	-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
991	-> IO String
992	nodes2String gInfo@(GInfo { gi_GraphInfo = graphInfo
993	, gi_LIB_NAME = ln
994	, libEnvIORef = ioRefProofStatus
995	}) nodemap linkmap = do
996	le <- readIORef ioRefProofStatus
997	nodes <- filterM (\(n,_) -> do b <- GA.isHiddenNode graphInfo n
998	return $ not b)
999	$ labNodesDG $ lookupDGraph ln le
1000	nstring <- foldM (\s node -> do
1001	s' <- (node2String gInfo nodemap linkmap node)
1002	return $ s ++ (if s /= "" then ",\n " else "") ++ s')
1003	"" nodes
1004	return $ "[" ++ nstring ++ "]"
1005
1006	-- \| Converts a node to String representation
1007	node2String :: GInfo -> Map.Map DGNodeType (Shape value, String)
1008	-> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
1009	-> LNode DGNodeLab -> IO String
1010	node2String gInfo nodemap linkmap (nid, dgnode) = do
1011	label <- getNodeLabel gInfo dgnode
1012	let ntype = getRealDGNodeType dgnode
1013	(shape, color) <- case Map.lookup ntype nodemap of
1014	Nothing -> error $ "SaveGraph: can't lookup nodetype: " ++ show ntype
1015	Just (s, c) -> return (s, c)
1016	let
1017	object = "a(\"OBJECT\",\"" ++ label ++ "\"),"
1018	color' = "a(\"COLOR\",\"" ++ color ++ "\"),"
1019	shape' = "a(\"_GO\",\"" ++ (map toLower $ show shape) ++ "\")"
1020	links <- links2String gInfo linkmap nid
1021	return $ "l(\"" ++ (show nid) ++ "\",n(\"" ++ show ntype ++ "\","
1022	++ "[" ++ object ++ color' ++ shape' ++ "],"
1023	++ "\n [" ++ links ++ "]))"
1024
1025	-- \| Converts all links of a node to String representation
1026	links2String :: GInfo -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
1027	-> Int -> IO String
1028	links2String (GInfo { gi_GraphInfo = graphInfo
1029	, gi_LIB_NAME = ln
1030	, libEnvIORef = ioRefProofStatus
1031	}) linkmap nodeid = do
1032	le <- readIORef ioRefProofStatus
1033	edges <- filterM (\(src,_,edge) -> do
1034	let eid = dgl_id edge
1035	b <- GA.isHiddenEdge graphInfo eid
1036	return $ (not b) && src == nodeid)
1037	$ labEdgesDG $ lookupDGraph ln le
1038	foldM (\s edge -> do
1039	s' <- link2String linkmap edge
1040	return $ s ++ (if s /= "" then ",\n " else "") ++ s') "" edges
1041
1042	-- \| Converts a link to String representation
1043	link2String :: Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
1044	-> LEdge DGLinkLab -> IO String
1045	link2String linkmap (nodeid1, nodeid2, edge) = do
1046	let (EdgeId linkid) = dgl_id edge
1047	ltype = getRealDGLinkType edge
1048	(line, color) <- case Map.lookup ltype linkmap of
1049	Nothing -> error $ "SaveGraph: can't lookup linktype: " ++ show ltype
1050	Just (l, c) -> return (l, c)
1051	let
1052	name = "\"" ++ (show linkid) ++ ":" ++ (show nodeid1) ++ "->"
1053	++ (show nodeid2) ++ "\""
1054	color' = "a(\"EDGECOLOR\",\"" ++ color ++ "\"),"
1055	line' = "a(\"EDGEPATTERN\",\"" ++ (map toLower $ show line) ++ "\")"
1056	return $ "l(" ++ name ++ ",e(\"" ++ show ltype ++ "\","
1057	++ "[" ++ color' ++ line' ++"],"
1058	++ "r(\"" ++ (show nodeid2) ++ "\")))"
1059
1060	-- \| Returns the name of the Node
1061	getNodeLabel :: GInfo -> DGNodeLab -> IO String
1062	getNodeLabel (GInfo {internalNamesIORef = ioRefInternal}) dgnode = do
1063	internal <- readIORef ioRefInternal
1064	let ntype = getDGNodeType dgnode
1065	return $ if (not $ showNames internal) &&
1066	elem ntype ["open_cons__internal"
1067	, "proven_cons__internal"
1068	, "locallyEmpty__open_cons__internal"
1069	, "locallyEmpty__proven_cons__internal"]
1070	then "" else getDGNodeName dgnode

Note: See TracBrowser for help on using the browser.

Hets

Context Navigation

root/trunk/GUI/GraphLogic.hs @ 11173

Download in other formats: