root/trunk/GUI/GraphMenu.hs @ 11229

Revision 11229, 20.1 kB (checked in by rpascanu, 11 months ago)

Changes to GUI to use common datatypes in Interfaces

  • Property svn:eol-style set to native
  • Property svn:keywords set to Author Date Id Revision
Line 
1{-# OPTIONS -cpp #-}
2{- |
3Module      :  $Header$
4Description :  Menu creation functions for the Graphdisplay
5Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2002-2008
6License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7
8Maintainer  :  raider@informatik.uni-bremen.de
9Stability   :  provisional
10Portability :  non-portable (imports Logic)
11
12Menu creation
13-}
14
15module GUI.GraphMenu
16  ( createGraph )
17  where
18
19import qualified GUI.GraphAbstraction as GA
20import GUI.GraphTypes
21import GUI.GraphLogic
22import GUI.ShowLogicGraph(showLogicGraph)
23import GUI.History
24import GUI.Utils
25#ifdef GTKGLADE
26import GUI.GtkLinkTypeChoice
27import GUI.GtkConsistencyChecker
28#endif
29
30import Data.IORef
31import qualified Data.Map as Map
32
33import Static.DevGraph
34import Static.PrintDevGraph
35
36import Proofs.EdgeUtils
37import Proofs.QualifyNames
38import Proofs.DGFlattening
39import Proofs.Automatic(automatic)
40import Proofs.Global(globSubsume, globDecomp)
41import Proofs.Local(localInference, locDecomp)
42import Proofs.Composition(composition, compositionCreatingEdges)
43import Proofs.HideTheoremShift(interactiveHideTheoremShift)
44import Proofs.TheoremHideShift(theoremHideShift, convertNodesToNf)
45import Proofs.ComputeColimit(computeColimit)
46
47import Common.DocUtils(showDoc)
48import Common.Result as Res
49
50import Driver.Options
51import Driver.ReadFn(libNameToFile)
52
53import GUI.UDGUtils
54import qualified GUI.HTkUtils as HTk
55
56import Control.Concurrent.MVar
57
58
59import Interfaces.DataTypes
60import Interfaces.History
61
62-- | Adds to the DGNodeType list style options for each type
63nodeTypes :: HetcatsOpts
64          -> [( DGNodeType -- Nodetype
65              , Shape GA.NodeValue -- Shape
66              , String -- Color
67              )]
68nodeTypes opts = map
69  ( (\ (n, s) -> case isLocallyEmpty n of -- Add color
70      True -> case nonRefType n of
71        NonRefType { isProvenCons = False }
72                -> (n, s, getColor opts Coral True  False)
73        _       -> (n, s, getColor opts Green True  False)
74      False -> case nonRefType n of
75        RefType -> (n, s, getColor opts Coral False False)
76        t       -> (n, s, getColor opts Coral False $ isProvenCons t)
77    )
78  . (\ n -> case nonRefType n of -- Add shape
79      RefType                               -> (n, Box)
80      NonRefType { isInternalSpec = True }  -> (n, Circle)
81      NonRefType { isInternalSpec = False } -> (n, Ellipse)
82    )
83  ) listDGNodeTypes
84
85-- | A Map of all nodetypes and their properties.
86mapNodeTypes :: HetcatsOpts -> Map.Map DGNodeType (Shape GA.NodeValue, String)
87mapNodeTypes opts = Map.fromList $ map (\ (n, s, c) -> (n, (s, c)))
88                                       $ nodeTypes opts
89
90-- | Adds to the DGEdgeType list style options for each type
91edgeTypes :: HetcatsOpts
92          -> [( DGEdgeType -- Edgetype
93              , EdgePattern GA.EdgeValue -- Lineformat
94              , String -- Color
95              , Bool -- Is theorem
96              , Bool -- Extra menu
97              )]
98edgeTypes opts = map
99  ( (\ (e, l, c) -> case edgeTypeModInc e of -- Add menu options
100      ThmType { thmEdgeType = HidingThmType } -> (e, l, c, True,  False)
101      ThmType _ _                             -> (e, l, c, True,  True)
102      _                                       -> (e, l, c, False, False)
103    )
104  . (\ (e, l) -> case edgeTypeModInc e of -- Add colors
105      HidingDefType   -> (e, l, getColor opts Blue   True  $ not $ isInc e)
106      FreeOrCofreeDef -> (e, l, getColor opts Blue   False $ not $ isInc e)
107      ThmType { thmEdgeType = thmType
108              , isProvenEdge = False } -> case thmType of
109        GlobalOrLocalThm { isLocalThmType = True, isHomThm = False }
110                      -> (e, l, getColor opts Coral  True  $ not $ isInc e)
111        HidingThmType -> (e, l, getColor opts Yellow False $ not $ isInc e)
112        _             -> (e, l, getColor opts Coral  False $ not $ isInc e)
113      ThmType { thmEdgeType = thmType
114              , isProvenEdge = True } -> case thmType of
115        GlobalOrLocalThm { isLocalThmType = True, isHomThm = False }
116                      -> (e, l, getColor opts Green  True  $ not $ isInc e)
117        HidingThmType -> (e, l, getColor opts Green  True  $ not $ isInc e)
118        _             -> (e, l, getColor opts Green  False $ not $ isInc e)
119      _               -> (e, l, getColor opts Black  False $ not $ isInc e)
120    )
121  . (\ e -> case edgeTypeModInc e of -- Add lineformat
122      ThmType { thmEdgeType = GlobalOrLocalThm { isLocalThmType = True
123                                               , isHomThm = True } }
124                   -> (e, Dashed)
125      ThmType { thmEdgeType = GlobalOrLocalThm { isHomThm = False } }
126                   -> (e, Double)
127      LocalDefType -> (e, Dashed)
128      HetGlobalDef -> (e, Double)
129      _            -> (e, Solid)
130    )
131  ) listDGEdgeTypes
132
133-- | A Map of all edgetypes and their properties.
134mapEdgeTypes :: HetcatsOpts
135             -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
136mapEdgeTypes opts = Map.fromList $ map (\ (e, l, c, _, _) -> (e, (l, c)))
137                                       $ edgeTypes opts
138
139-- | Creates the graph. Runs makegraph
140createGraph :: GInfo -> String -> ConvFunc -> LibFunc -> IO ()
141createGraph gInfo@(GInfo { gi_GraphInfo = actGraphInfo
142                         , gi_hetcatsOpts = opts
143                         }) title convGraph showLib = do
144 ost <- readIORef $ intState gInfo
145 case i_state ost of
146  Nothing -> return ()
147  Just ist -> do
148   let ln = i_ln ist
149       file = rmSuffix (libNameToFile opts ln) ++ prfSuffix
150   deselectEdgeTypes <- newIORef []
151   globMenu <- createGlobalMenu gInfo convGraph showLib deselectEdgeTypes
152   GA.makegraphExt actGraphInfo
153                  title
154                  (createOpen gInfo file convGraph showLib)
155                  (createSave gInfo file)
156                  (createSaveAs gInfo file)
157                  (createClose gInfo)
158                  (Just (createExit gInfo))
159                  globMenu
160                  (createNodeTypes gInfo convGraph showLib)
161                  (createEdgeTypes gInfo)
162
163-- | Returns the open-function
164createOpen :: GInfo -> FilePath -> ConvFunc -> LibFunc -> Maybe (IO ())
165createOpen gInfo file convGraph showLib = Just (
166  do
167    maybeFilePath <- fileOpenDialog file [ ("Proof", ["*.prf"])
168                                         , ("All Files", ["*"])] Nothing
169    case maybeFilePath of
170      Just filePath -> do
171        openProofStatus gInfo filePath convGraph showLib
172        return ()
173      Nothing -> fail "Could not open file."
174  )
175
176-- | Returns the save-function
177createSave :: GInfo -> FilePath -> Maybe (IO ())
178createSave gInfo file = Just (saveProofStatus gInfo file)
179
180-- | Returns the saveas-function
181createSaveAs :: GInfo -> FilePath -> Maybe (IO ())
182createSaveAs gInfo file = Just (
183  do
184    maybeFilePath <- fileSaveDialog file [ ("Proof", ["*.prf"])
185                                         , ("All Files", ["*"])] Nothing
186    case maybeFilePath of
187      Just filePath -> saveProofStatus gInfo filePath
188      Nothing -> fail "Could not save file."
189  )
190
191-- | Returns the save-function
192createClose :: GInfo -> IO Bool
193createClose gInfo@(GInfo { windowCount = wc
194                   , exitMVar = exit
195                   }) = do
196 ost <- readIORef $ intState gInfo
197 case i_state ost of
198  Nothing -> return False
199  Just ist -> do
200   let le = i_libEnv ist
201       ln = i_ln ist
202   case Map.lookup ln le of
203    Just dgraph -> do
204      case openlock dgraph of
205        Just lock -> do
206          notopen <- isEmptyMVar lock
207          case notopen of
208            True -> error "development graph seems to be closed already"
209            False ->  takeMVar lock
210        Nothing -> error $ "MVar of " ++ show ln ++ " not initialized"
211    Nothing -> error $ "development graph with libname " ++ show ln
212                       ++" does not exist"
213   count <- takeMVar wc
214   case count == 1 of
215    True -> putMVar exit ()
216    False -> putMVar wc $ count - 1
217   return True
218
219-- | Returns the save-function
220createExit :: GInfo -> IO ()
221createExit (GInfo {exitMVar = exit}) = do
222  putMVar exit ()
223
224-- | Creates the global menu
225createGlobalMenu :: GInfo -> ConvFunc -> LibFunc -> IORef [String]
226                 -> IO [GlobalMenu]
227createGlobalMenu gInfo@(GInfo { gi_hetcatsOpts = opts
228#ifdef GTKGLADE
229                              , gi_GraphInfo = gi
230                              }) convGraph showLib deselectEdgeTypes =
231#else
232                              }) convGraph showLib _ =
233#endif
234 do
235 ost <- readIORef $ intState gInfo
236 case i_state ost of
237  Nothing -> return []
238  Just ist -> do
239   let ral x = runAndLock gInfo x
240       ln = i_ln ist
241   return
242    [GlobalMenu (Menu Nothing
243     [ Button "Undo" $ ral $ undo gInfo True
244     , Button "Redo" $ ral $ undo gInfo False
245     , Button "Reload" $ ral $ reload gInfo
246     , Menu (Just "Unnamed nodes")
247        [ Button "Hide/show names" $ ral $ hideShowNames gInfo True
248        , Button "Hide nodes" $ ral $ hideNodes gInfo
249        , Button "Show nodes" $ ral $ showNodes gInfo
250      ]
251     , Button "Focus node" $ ral $ focusNode gInfo
252#ifdef GTKGLADE
253     , Button "Select Linktypes" $ showLinkTypeChoice deselectEdgeTypes
254                                $ (\ eList -> ral $ do
255                                    GA.showAll gi
256                                    GA.hideSetOfEdgeTypes gi eList
257                                    GA.redisplay gi
258                                  )
259#endif
260     , Menu (Just "Proofs") $ map (\ (str, cmd) ->
261       -- History ? or just some partial history in ch ?
262        Button str $ (ral $ performProofAction gInfo
263                  $ proofMenu gInfo $ return . return . cmd ln
264                  . Map.map undoRedo))
265        [ ("Automatic", automatic)
266        , ("Global Subsumption", globSubsume)
267        , ("Global Decomposition", globDecomp)
268        , ("Local Inference", localInference)
269        , ("Local Decomposition (merge of rules)", locDecomp)
270        , ("Composition (merge of rules)", composition)
271        , ("Composition - creating new links", compositionCreatingEdges)
272        ] ++
273        [Button "Hide Theorem Shift" $
274               -- (addMenuItemToHist ch "Hide Theorem Shift") >>
275               (ral $ performProofAction gInfo
276               $ proofMenu gInfo $ fmap return . interactiveHideTheoremShift ln)
277        ] ++
278        map (\ (str, cmd) ->
279               Button str $ -- (addMenuItemToHist ch str) >>
280                   (ral $ performProofAction gInfo
281                   $ proofMenu gInfo $ return . cmd ln))
282        [ ("Theorem Hide Shift", theoremHideShift)
283        , ("Compute Colimit", computeColimit)
284        , ("Compute normal forms", convertNodesToNf)
285        ] ++
286        [ Menu (Just "Flattening") $ map ( \ (str, cmd) ->
287           Button str $ ral $ performProofAction gInfo
288                      $ proofMenu gInfo $ return . cmd)
289              [ ("Importings", libEnv_flattening_imports)
290              , ("Disjoint unions", libEnv_flattening_dunions)
291              , ("Importings and renamings", libEnv_flattening_renamings)
292              , ("Hiding", libEnv_flattening_hiding)
293              , ("Heterogeneity", libEnv_flattening_heterogen)
294              , ("Qualify all names", qualifyLibEnv)]]
295     , Button "Dump LibEnv" $ do
296          let le = i_libEnv ist
297          print $ prettyLibEnv le
298     , Button "Translate Graph" $ ral $ translateGraph gInfo convGraph showLib
299     , Button "Show Logic Graph" $ ral $ showLogicGraph daVinciSort
300     , Button "Show Library Graph" $ ral $ showLibGraph gInfo showLib
301     , Button "Save Graph for uDrawGraph" $ ral
302              $ saveUDGraph gInfo (mapNodeTypes opts) $ mapEdgeTypes opts
303--     , Button "Save proof-script" $ ral
304--              $ askSaveProofScript (gi_GraphInfo gInfo) ch
305     ])
306    ]
307
308-- | A list of all Node Types
309createNodeTypes :: GInfo -> ConvFunc -> LibFunc
310                -> [(DGNodeType,DaVinciNodeTypeParms GA.NodeValue)]
311createNodeTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) cGraph showLib = map
312  (\ (n, s, c) ->
313    ( n
314    , case nonRefType n of
315        RefType -> createLocalMenuNodeTypeDgRef s c gInfo cGraph showLib
316        NonRefType { isInternalSpec = True }
317                -> createLocalMenuNodeTypeInternal s c gInfo
318        NonRefType { isInternalSpec = False }
319                -> createLocalMenuNodeTypeSpec s c gInfo
320    )
321  ) $ nodeTypes opts
322
323-- | the edge types (share strings to avoid typos)
324createEdgeTypes :: GInfo -> [(DGEdgeType,DaVinciArcTypeParms GA.EdgeValue)]
325createEdgeTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) =
326  map (\(title, look, color, thm, extra) ->
327        (title, look
328            $$$ Color color
329            $$$ (if thm then createLocalEdgeMenuThmEdge gInfo
330                  else createLocalEdgeMenu gInfo)
331            $$$ (if extra then createLocalMenuValueTitleShowConservativity
332                  $$$ emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue
333                  else
334                    emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue))
335      ) $ edgeTypes opts
336
337-- * methods to create the local menus of the different nodetypes
338
339createLocalMenuNode :: GInfo -> DaVinciNodeTypeParms GA.NodeValue
340createLocalMenuNode gInfo = LocalMenu (Menu (Just "node menu") $ map ($ gInfo)
341  [ createLocalMenuButtonShowNodeInfo
342  , createLocalMenuButtonShowTheory
343  , createLocalMenuButtonTranslateTheory
344  , createLocalMenuTaxonomy
345  , createLocalMenuButtonShowProofStatusOfNode
346  , createLocalMenuButtonProveAtNode
347#ifdef GTKGLADE
348  , createLocalMenuButtonConsistencyChecker
349#endif
350  , createLocalMenuButtonCCCAtNode ]) $$$ emptyNodeTypeParms
351
352-- | local menu for the nodetypes spec and locallyEmpty_spec
353createLocalMenuNodeTypeSpec :: Shape GA.NodeValue -> String -> GInfo
354                            -> DaVinciNodeTypeParms GA.NodeValue
355createLocalMenuNodeTypeSpec shape color gInfo =
356                 shape $$$ Color color
357                 $$$ ValueTitle (\ (s,_) -> return s)
358                 $$$ createLocalMenuNode gInfo
359
360-- | local menu for the nodetypes internal and locallyEmpty_internal
361createLocalMenuNodeTypeInternal :: Shape GA.NodeValue -> String -> GInfo
362                                -> DaVinciNodeTypeParms GA.NodeValue
363createLocalMenuNodeTypeInternal shape color
364               gInfo@(GInfo {internalNamesIORef = showInternalNames}) =
365                 shape $$$ Color color
366                 $$$ ValueTitleSource (\ (s,_) -> do
367                       b <- newSimpleBroadcaster ""
368                       intrn <- readIORef showInternalNames
369                       let upd = (s,applySimpleUpdate b)
370                       writeIORef showInternalNames
371                                  $ intrn {updater = upd:updater intrn}
372                       return $ toSimpleSource b)
373                 $$$ createLocalMenuNode gInfo
374
375-- | local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
376createLocalMenuNodeTypeDgRef :: Shape GA.NodeValue -> String -> GInfo
377                             -> ConvFunc -> LibFunc
378                             -> DaVinciNodeTypeParms GA.NodeValue
379createLocalMenuNodeTypeDgRef shape color gInfo convGraph showLib =
380                 shape $$$ Color color
381                 $$$ ValueTitle (\ (s,_) -> return s)
382                 $$$ LocalMenu (Menu (Just "node menu")
383                   [createLocalMenuButtonShowNodeInfo gInfo,
384                    createLocalMenuButtonShowTheory gInfo,
385                    createLocalMenuButtonShowProofStatusOfNode gInfo,
386                    createLocalMenuButtonProveAtNode gInfo,
387                    Button "Show referenced library"
388                     (\ (_, descr) -> do
389                       showReferencedLibrary descr gInfo convGraph showLib
390                       return ()
391                     )])
392                 $$$ emptyNodeTypeParms
393
394type ButtonMenu a = MenuPrim (Maybe String) (a -> IO ())
395
396-- | menu button for local menus
397createMenuButton :: String -> (Int -> DGraph -> IO ())
398                 -> GInfo -> ButtonMenu GA.NodeValue
399createMenuButton title menuFun gInfo =
400                    (Button title
401                      (\ (_, descr) ->
402                        do
403                         ost <- readIORef $ intState gInfo
404                         case i_state ost of
405                          Nothing -> return ()
406                          Just ist -> do
407                           let le = i_libEnv ist
408                               ln = i_ln ist
409                               dGraph = lookupDGraph ln le
410                           runAndLock gInfo $  menuFun descr dGraph
411                           return ()
412                       )
413                    )
414
415createLocalMenuButtonShowTheory :: GInfo -> ButtonMenu GA.NodeValue
416createLocalMenuButtonShowTheory gInfo =
417  createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo
418
419createLocalMenuButtonTranslateTheory :: GInfo -> ButtonMenu GA.NodeValue
420createLocalMenuButtonTranslateTheory gInfo =
421  createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo
422
423{- |
424   create a sub Menu for taxonomy visualisation
425   (added by KL)
426-}
427createLocalMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue
428createLocalMenuTaxonomy ginfo =
429  (Menu (Just "Taxonomy graphs")
430        [ createMenuButton "Subsort graph" (passTh displaySubsortGraph) ginfo
431        , createMenuButton "Concept graph" (passTh displayConceptGraph) ginfo
432        ])
433  where passTh displayFun descr _ =
434         do
435          ost <- readIORef $ intState ginfo
436          case i_state ost of
437           Nothing -> return ()
438           Just ist -> do
439             let ln = i_ln ist
440                 le = i_libEnv ist
441             r <- lookupTheoryOfNode le ln descr
442             case r of
443               Res.Result [] (Just (_le',n, gth)) ->
444                  displayFun (showDoc n "") gth
445          -- le is the changed LibEnv, have to modify
446               Res.Result ds _ -> showDiags defaultHetcatsOpts ds
447
448createLocalMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu GA.NodeValue
449createLocalMenuButtonShowProofStatusOfNode gInfo =
450  createMenuButton "Show proof status" (showProofStatusOfNode gInfo) gInfo
451
452createLocalMenuButtonProveAtNode :: GInfo -> ButtonMenu GA.NodeValue
453createLocalMenuButtonProveAtNode gInfo =
454  createMenuButton "Prove" (\descr dgraph -> performProofAction gInfo
455    (proveAtNode False gInfo descr dgraph)) gInfo
456
457#ifdef GTKGLADE
458createLocalMenuButtonConsistencyChecker :: GInfo -> ButtonMenu GA.NodeValue
459createLocalMenuButtonConsistencyChecker gInfo =
460  createMenuButton "Consistency checker"
461                   (showConsistencyChecker gInfo) gInfo
462#endif
463
464createLocalMenuButtonCCCAtNode :: GInfo -> ButtonMenu GA.NodeValue
465createLocalMenuButtonCCCAtNode gInfo =
466  createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo
467
468createLocalMenuButtonShowNodeInfo :: GInfo -> ButtonMenu GA.NodeValue
469createLocalMenuButtonShowNodeInfo gInfo =
470  createMenuButton "Show node info" showNodeInfo gInfo
471
472-- * methods to create the local menus for the edges
473
474createLocalEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue
475createLocalEdgeMenu gInfo =
476  LocalMenu (Menu (Just "edge menu")
477                  [ createLocalMenuButtonShowEdgeInfo gInfo
478                  , createLocalMenuButtonCheckconservativityOfEdge gInfo])
479
480createLocalEdgeMenuThmEdge :: GInfo -> LocalMenu GA.EdgeValue
481createLocalEdgeMenuThmEdge gInfo =
482  LocalMenu (Menu (Just "thm egde menu")
483                  [ createLocalMenuButtonShowEdgeInfo gInfo
484                  , createLocalMenuButtonCheckconservativityOfEdge gInfo])
485
486createLocalMenuButtonShowEdgeInfo :: GInfo -> ButtonMenu GA.EdgeValue
487createLocalMenuButtonShowEdgeInfo _ = Button "Show info"
488  (\ (_, (EdgeId descr), maybeLEdge) -> showEdgeInfo descr maybeLEdge)
489
490createLocalMenuButtonCheckconservativityOfEdge :: GInfo
491                                               -> ButtonMenu GA.EdgeValue
492createLocalMenuButtonCheckconservativityOfEdge gInfo =
493  Button "Check conservativity"
494    (\ (_, (EdgeId descr), maybeLEdge)  ->
495      checkconservativityOfEdge descr gInfo maybeLEdge)
496
497createLocalMenuValueTitleShowConservativity :: ValueTitle GA.EdgeValue
498createLocalMenuValueTitleShowConservativity = ValueTitle
499  (\ (_, _, maybeLEdge) -> case maybeLEdge of
500    Just (_,_,edgelab) -> case dgl_type edgelab of
501      GlobalThm _ c status -> return (showCons c status)
502      LocalThm _ c status -> return (showCons c status)
503      _ -> return ""
504    Nothing -> return "")
505  where
506    showCons :: Conservativity -> ThmLinkStatus -> String
507    showCons c status = case (c, status) of
508      (None, _) -> ""
509      (_, LeftOpen) -> show c ++ "?"
510      _ -> show c
Note: See TracBrowser for help on using the browser.