dcbd586414fbe6a9b4355081269912c864b72991Simon UlbrichtDescription : Gtk GUI for automatic proving procedure of multiple nodes
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon UlbrichtCopyright : (c) Simon Ulbricht, Uni Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon UlbrichtMaintainer : tekknix@informatik.uni-bremen.de
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtStability : provisional
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtPortability : portable
d6d21a06b12c5d5be318a722e3cec4cac50618c7Simon UlbrichtThis module provides a GUI for the automatic proofs module.
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht (showAutomaticProofs, Finder (..))
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport qualified GUI.Glade.NodeChecker as ConsistencyChecker
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport Interfaces.GenericATPState (guiDefaultTimeLimit)
8969a00d3fa8a33b08c85afd50ab675a56ee6f84Christian Maederimport Logic.Comorphism (AnyComorphism (..))
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport Comorphisms.LogicGraph (logicGraph)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport Common.LibName (LibName)
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon Ulbrichtimport Control.Concurrent (forkIO, killThread)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport Control.Monad (foldM_, join, when)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtimport qualified Data.Map as Map
dcbd586414fbe6a9b4355081269912c864b72991Simon Ulbricht-- | Data structure for saving the user-selected prover and comorphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Finder = Finder { fName :: String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , finder :: G_prover
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , comorphism :: [AnyComorphism]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , selected :: Int }
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbrichtinstance Eq Finder where
0425e5ed787f937a67a33d20c263fa72409bfe73Simon Ulbricht f1 == f2 = fName f1 == fName f2 && comorphism f1 == comorphism f2
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Displays the consistency checker window
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtshowAutomaticProofs :: GInfo -> LibEnv -> IO (Result LibEnv)
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela DiaconushowAutomaticProofs ginf@(GInfo { libName = ln }) le = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht wait <- newEmptyMVar
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela Diaconu showProverWindow ginf wait ln le
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht le' <- takeMVar wait
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht return $ Result [] $ Just le'
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Displays the consistency checker window
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela DiaconushowProverWindow :: GInfo -> MVar LibEnv -> LibName -> LibEnv -> IO ()
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela DiaconushowProverWindow ginf res ln le = postGUIAsync $ do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder xml <- getGladeXML ConsistencyChecker.get
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- get objects
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder window <- xmlGetWidget xml castToWindow "NodeChecker"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnClose <- xmlGetWidget xml castToButton "btnClose"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnResults <- xmlGetWidget xml castToButton "btnResults"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- get nodes view and buttons
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- get checker view and buttons
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnCheck <- xmlGetWidget xml castToButton "btnCheck"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder btnStop <- xmlGetWidget xml castToButton "btnStop"
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht -- btnFineGrained <- xmlGetWidget xml castToButton "btnFineGrained"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder toolLabel <- xmlGetWidget xml castToLabel "label1"
a25ddb094b360b2553307dca7c7be34ade82c614Christian Maeder labelSetLabel toolLabel "Pick prover"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht windowSetTitle window "AutomaticProofs"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht let widgets = [ toWidget sbTimeout
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget cbComorphism
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget lblSublogic ]
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht checkWidgets = widgets ++ [ toWidget btnClose
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnNodesAll
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnNodesNone
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnNodesInvert
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnNodesUnchecked
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnNodesTimeout
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht , toWidget btnResults ]
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht switch b = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSensitive btnStop $ not b
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSensitive btnCheck b
24483f2ee2ecec569b06242055078638df627177Simon Ulbricht toggleButtonSetActive cbInclThms False
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSensitive btnStop False
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSensitive btnCheck False
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht threadId <- newEmptyMVar
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder wait <- newEmptyMVar
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mView <- newEmptyMVar
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let dg = lookupDGraph ln le
dcbd586414fbe6a9b4355081269912c864b72991Simon Ulbricht nodes = initFNodes $ labNodesDG dg
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup data
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder listNodes <- setListData trvNodes show $ sort nodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht listFinder <- setListData trvFinder fName []
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup comorphism combobox
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht comboBoxSetModelText cbComorphism
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht shC <- after cbComorphism changed
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht $ setSelectedComorphism trvFinder listFinder cbComorphism
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup view selection actions
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht let update = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mf <- getSelectedSingle trvFinder listFinder
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht updateComorphism trvFinder listFinder cbComorphism shC
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSensitive btnCheck $ isJust mf
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht setListSelectorSingle trvFinder update
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht let upd = updateNodes trvNodes listNodes
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht labelSetLabel lblSublogic $ show s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder updateFinder trvFinder listFinder s )
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht labelSetLabel lblSublogic "No sublogic"
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht listStoreClear listFinder
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht activate widgets False
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht widgetSetSensitive btnCheck False)
761eb2b535a763e518887d72cf276f781304cf0eSimon Ulbricht (activate widgets True >> widgetSetSensitive btnCheck True)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht shN <- setListSelectorMultiple trvNodes btnNodesAll btnNodesNone
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht btnNodesInvert upd
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- this function handles the selction of nodes, getting as input parameter
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder a function f (FNode -> Bool). -}
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht let selectWith f u = do
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht signalBlock shN
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht sel <- treeViewGetSelection trvNodes
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht treeSelectionSelectAll sel
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht rs <- treeSelectionGetSelectedRows sel
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder mapM_ ( \ ~p@(row : []) -> do
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht fn <- listStoreGetValue listNodes row
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht (if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht signalUnblock shN
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht onClicked btnNodesUnchecked
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht $ selectWith unchecked upd
5a81c9ef37269e5c5bca9e3b8e4e230f293a585dSimon Ulbricht onClicked btnNodesTimeout $ selectWith timedout upd
c8dd144f13de2667bf3fddea71b0b22d4aa25ff1Simon Ulbricht onClicked btnResults $ showModelView mView "Models" listNodes []
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onClicked btnClose $ widgetDestroy window
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onClicked btnCheck $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht activate checkWidgets False
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht timeout <- spinButtonGetValueAsInt sbTimeout
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht inclThms <- toggleButtonGetActive cbInclThms
23f5a785aa582c89a0eac4e3c03fae932e8c197aSimon Ulbricht (prgBar, exit) <- progressBar "Proving" "please wait..."
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes' <- getSelectedMultiple trvNodes listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mf <- getSelectedSingle trvFinder listFinder
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht f <- case mf of
0425e5ed787f937a67a33d20c263fa72409bfe73Simon Ulbricht Nothing -> error "Automatic Proofs: internal error"
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht Just (_, f) -> return f
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht tid <- forkIO $ do
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela Diaconu performAutoProof ginf inclThms timeout prgBar f listNodes nodes'
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht putMVar wait ()
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht putMVar threadId tid
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht takeMVar wait
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht postGUIAsync $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht tryTakeMVar threadId
c8dd144f13de2667bf3fddea71b0b22d4aa25ff1Simon Ulbricht showModelView mView "Results of automatic proofs" listNodes []
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht signalBlock shN
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sortNodes trvNodes listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht signalUnblock shN
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht activate checkWidgets True
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- after window is closed, the results are written back into the DGraph.
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder for each node a DGChange object is created and applied to the DGraph. -}
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onDestroy window $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes' <- listStoreToList listNodes
af14ce5114c39c964531ebba25cbd46cf70ecd7fSimon Ulbricht let dg' = foldl (\ cs fn ->
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- where the proving did not return anything, the node is
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder not updated -}
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht if unchecked fn then cs
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu else updateLabelTheory le ln cs (node fn) (results fn)
af1369c2b9ce0cb2a290e499b1719441917c0196Simon Ulbricht putMVar res $ Map.insert ln (groupHistory dg (DGRule "autoproof") dg') le
663e95bc1a04e039893e2a5a0815358cda1170eeChristian Maeder -- setting up the selected items at startup
5a81c9ef37269e5c5bca9e3b8e4e230f293a585dSimon Ulbricht selectWith (not . allProved) upd
663e95bc1a04e039893e2a5a0815358cda1170eeChristian Maeder -- TODO select SPASS Prover if possible
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetShow window
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela DiaconuperformAutoProof :: GInfo
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela Diaconu -- include proven Theorems in subsequent proofs
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -- Timeout (sec)
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -- Progress bar
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder -> (Double -> String -> IO ())
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -- selcted Prover and Comorphism
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -- Display function for node selection box
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder -> ListStore FNode
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -- selected nodes
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht -> [(Int, FNode)]
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- no return value, since results are stored by changing
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder FNode data -}
46b5fe38c0c8cd7b8a92ccb44e683e4996aea19cLoredana Mihaela DiaconuperformAutoProof gi inclThms timeout update (Finder _ pr cs i) listNodes nodes =
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht let count' = fromIntegral $ length nodes
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht in foldM_ (\ count (row, fn) -> do
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht postGUISync $ update (count / count') $ name fn
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht res <- maybe (return Nothing) (\ g_th -> do
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht Result ds ms <- runResultT
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa (a, b) <- autoProofAtNode inclThms timeout [] [] g_th
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder liftIO $ addCommandHistoryToState (intState gi)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (fst b) (Just (pr, c)) (snd b) (name fn)
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder (True, timeout)
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht maybe (fail $ showRelDiags 1 ds) (return . Just . fst) ms)
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht $ globalTheory $ snd $ node fn
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder Just gt -> postGUISync $ listStoreSetValue listNodes row
af14ce5114c39c964531ebba25cbd46cf70ecd7fSimon Ulbricht fn { results = propagateProofs (results fn) gt }
af14ce5114c39c964531ebba25cbd46cf70ecd7fSimon Ulbricht Nothing -> return ()
7295fc55bb16da7bc967fdf6d63cdfd03b061127Simon Ulbricht return $ count + 1) 0 nodes
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtsortNodes :: TreeView -> ListStore FNode -> IO ()
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtsortNodes trvNodes listNodes = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sel <- getSelectedMultiple trvNodes listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes <- listStoreToList listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht let sn = sort nodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht updateListData listNodes sn
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht selector <- treeViewGetSelection trvNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mapM_ (\ (_, FNode { name = n }) -> treeSelectionSelectPath selector
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht [fromMaybe (error "Node not found!") $ findIndex ((n ==) . name) sn]
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Called when node selection is changed. Updates finder list
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon UlbrichtupdateNodes :: TreeView -> ListStore FNode -> (G_sublogics -> IO ())
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -> IO () -> IO () -> IO ()
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtupdateNodes view listNodes update lock unlock = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes <- getSelectedMultiple view listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht if null nodes then lock
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht else let sls = map (sublogic . snd) nodes in
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon Ulbricht maybe lock (\ sl -> unlock >> update sl)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht $ foldl (\ ma b -> case ma of
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Just a -> joinSublogics b a
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Nothing -> Nothing) (Just $ head sls) $ tail sls
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Update the list of finder
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon UlbrichtupdateFinder :: TreeView -> ListStore Finder -> G_sublogics -> IO ()
d6865474d3248c1d8ed080c221c4a9548b0a4bb3Simon UlbrichtupdateFinder view list sl = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht old <- listStoreToList list
cddd87cd39be9d031348ef95051c4d14067e1646cmaeder ps <- getUsableProvers ProveCMDLautomatic sl logicGraph
af1369c2b9ce0cb2a290e499b1719441917c0196Simon Ulbricht let new = Map.elems $ foldr (\ (pr, c) m ->
abee46762c1663b85c6f18d934cd11df83828f6eChristian Maeder let n = getProverName pr
af1369c2b9ce0cb2a290e499b1719441917c0196Simon Ulbricht f = Map.findWithDefault (Finder n pr [] 0) n m
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht in Map.insert n (f { comorphism = c : comorphism f}) m) Map.empty
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht when (old /= new) $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- update list and try to select previous finder
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht selected' <- getSelectedSingle view list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sel <- treeViewGetSelection view
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht listStoreClear list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mapM_ (listStoreAppend list) $ mergeFinder old new
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht maybe (selectFirst view)
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht (\ (_, f) -> let i = findIndex ((fName f ==) . fName) new in
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht maybe (selectFirst view) (treeSelectionSelectPath sel . (: [])) i
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Try to select previous selected comorphism if possible
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtmergeFinder :: [Finder] -> [Finder] -> [Finder]
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtmergeFinder old new = let m' = Map.fromList $ map (\ f -> (fName f, f)) new in
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Map.elems $ foldl (\ m (Finder { fName = n, comorphism = cc, selected = i}) ->
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Just f@(Finder { comorphism = cc' }) -> let c = cc !! i in
22a42cbea5bdf4b39b99794550b1403b3820b5e5Christian Maeder Map.insert n (f { selected = fromMaybe 0 $ elemIndex c cc' }) m
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtupdateComorphism :: TreeView -> ListStore Finder -> ComboBox
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -> ConnectId ComboBox -> IO ()
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtupdateComorphism view list cbComorphism sh = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht signalBlock sh
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht model <- comboBoxGetModelText cbComorphism
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht listStoreClear model
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mfinder <- getSelectedSingle view list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht case mfinder of
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Just (_, f) -> do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mapM_ (comboBoxAppendText cbComorphism) $ expand f
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht comboBoxSetActive cbComorphism $ selected f
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Nothing -> return ()
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht signalUnblock sh
3c39e5cbfd4e6d547e2f7a9505a5d39c32118186cmaederexpand :: Finder -> [ComboBoxText]
c0b7a54447004864480a70752e2b3deca8e8be2ecmaederexpand = toComboBoxText . comorphism
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtsetSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtsetSelectedComorphism view list cbComorphism = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mfinder <- getSelectedSingle view list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht case mfinder of
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Just (i, f) -> do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sel <- comboBoxGetActive cbComorphism
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht listStoreSetValue list i f { selected = sel }
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Nothing -> return ()
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Displays the model view window
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtshowModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode]
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtshowModelViewAux lock title list other = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder xml <- getGladeXML ConsistencyChecker.get
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- get objects
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder window <- xmlGetWidget xml castToWindow "ModelView"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht btnClose <- xmlGetWidget xml castToButton "btnResClose"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder frNodes <- xmlGetWidget xml castToFrame "frResNodes"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht trvNodes <- xmlGetWidget xml castToTreeView "trvResNodes"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder tvModel <- xmlGetWidget xml castToTextView "tvResModel"
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht windowSetTitle window title
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup text view
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht buffer <- textViewGetBuffer tvModel
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht textBufferInsertAtCursor buffer ""
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht tagTable <- textBufferGetTagTable buffer
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht font <- textTagNew Nothing
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht set font [ textTagFont := "FreeMono" ]
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht textTagTableAdd tagTable font
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht start <- textBufferGetStartIter buffer
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht end <- textBufferGetEndIter buffer
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht textBufferApplyTag buffer font start end
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup list view
af1369c2b9ce0cb2a290e499b1719441917c0196Simon Ulbricht let filterNodes = id
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes <- listStoreToList list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht listNodes <- setListData trvNodes show $ sort $ filterNodes $ other ++ nodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht setListSelectorSingle trvNodes $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht mn <- getSelectedSingle trvNodes listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht Nothing -> textBufferSetText buffer ""
faa53f457a1847053529e6cdeda3586329815392Simon Ulbricht Just (_, n) -> textBufferSetText buffer $ showStatus n
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht -- setup actions
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onClicked btnClose $ widgetDestroy window
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht onDestroy window $ takeMVar lock >>= const (return ())
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht putMVar lock $ do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sel' <- getSelectedSingle trvNodes listNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht sel <- treeViewGetSelection trvNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht nodes'' <- listStoreToList list
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht let nodes' = sort $ filterNodes nodes''
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht updateListData listNodes $ sort (other ++ nodes')
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht maybe (selectFirst trvNodes) (treeSelectionSelectPath sel . (: []))
dd0d471630e5a700970dd61448de1a0b930c5981Simon Ulbricht $ maybe Nothing (\ (_, n) -> findIndex ((name n ==) . name) nodes') sel'
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht selectFirst trvNodes
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSizeRequest window 800 600
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetSetSizeRequest frNodes 250 (-1)
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht widgetShow window
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht-- | Displays the model view window
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtshowModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()
366c3a899de56473bd4e714c5079d7a873411605Simon UlbrichtshowModelView lock title list other = do
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht isNotOpen <- isEmptyMVar lock
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht if isNotOpen then showModelViewAux lock title list other
366c3a899de56473bd4e714c5079d7a873411605Simon Ulbricht else join (readMVar lock)