GtkDisprove.hs revision 65660c22133e6de16f9ece7b36ac6423014b20aa
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
a530dde7009b0a808300c420def741354a4d13d2Martin KühlDescription : Gtk Module to enable disproving Theorems
a530dde7009b0a808300c420def741354a4d13d2Martin KühlCopyright : (c) Simon Ulbricht, Uni Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a530dde7009b0a808300c420def741354a4d13d2Martin KühlMaintainer : tekknix@informatik.uni-bremen.de
a530dde7009b0a808300c420def741354a4d13d2Martin KühlStability : provisional
a530dde7009b0a808300c420def741354a4d13d2Martin KühlPortability : portable
a530dde7009b0a808300c420def741354a4d13d2Martin KühlThis module provides a disproving module that checks consistency of inverted
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescomodule GUI.GtkDisprove (disproveAtNode) where
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified GUI.Glade.NodeChecker as ConsistencyChecker
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport GUI.GraphLogic hiding (openProofStatus)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport Interfaces.GenericATPState (guiDefaultTimeLimit)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport Interfaces.Utils (updateNodeProof)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Common.OrderedMap as OMap
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescoimport Common.LibName (LibName)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riescoimport Control.Concurrent (forkIO, killThread)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport qualified Data.Map as Map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco{- | this method holds the functionality to convert the nodes goals to the
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoFNode datatype from GUI.GtkConsistencyChecker. The goals are being negated
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoby negate_th and this theory is stored in FNodes DGNodeLab local and global
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoshowDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedershowDisproveGUI gi le dg (i, lbl) = case globalTheory lbl of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Nothing -> error "GtkDisprove.showDisproveGUI(no global theory found)"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just gt@(G_theory _ _ _ sens _) -> let
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder fg g th = let
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco l = lbl { dgn_theory = th }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder l' = l { globalTheory = computeLabelTheory le dg (i, l) }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder no_cs = ConsistencyStatus CSUnchecked ""
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco stat = case OMap.lookup g sens of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Nothing -> no_cs
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Just tm -> case thmStatus tm of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ts -> basicProofToConStatus $ maximum $ map snd ts
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder in FNode { name = g, node = (i, l'), sublogic = sublogicOfTh th,
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder cStatus = stat }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco fgoals = foldr (\ g t -> case negate_th gt g of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just nt -> fg g nt : t) []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco $ OMap.keys $ OMap.filter (not . isAxiom) sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in if null fgoals
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco errorDialogExt "Error (disprove)"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco "found no goals suitable for disprove function"
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco wait <- newEmptyMVar
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco showDisproveWindow wait (libName gi) le dg gt fgoals
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco res <- takeMVar wait
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco runDisproveAtNode gi (i, lbl) res
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco{- | negates a single sentence within a G_theory and returns a theorie
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riescocontaining all axioms in addition to the one negated sentence. -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesconegate_th :: G_theory -> String -> Maybe G_theory
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesconegate_th g_th goal = case g_th of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco G_theory lid1 (ExtSign sign symb) i1 sens i2 ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco case OMap.lookup goal sens of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco case negation lid1 $ sentence sen of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just sen' -> let
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder negSen = sen { sentence = sen', isAxiom = True }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder sens' = OMap.insert goal negSen $ OMap.filter isAxiom sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in Just $ G_theory lid1 (ExtSign sign symb) i1 sens' i2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | this function is being called from outside and manages the locking-
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomechanism of the node being called upon. -}
a74f814d3b445eadad6f68737a98a7a303698affChristian MaederdisproveAtNode :: GInfo -> Int -> DGraph -> IO ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescodisproveAtNode gInfo descr dgraph = do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco lockedEnv <- ensureLockAtNode gInfo descr dgraph
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco case lockedEnv of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Nothing -> return ()
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Just (dg, lbl, le) -> do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco acquired <- tryLockLocal lbl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco if acquired then do
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder showDisproveGUI gInfo le dg (descr, lbl)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder unlockLocal lbl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else errorDialogExt "Error" "Proof or disproof window already open"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | after results have been collected, this function is called to store
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthe results for this node within the dgraphs history. -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederrunDisproveAtNode :: GInfo -> LNode DGNodeLab -> Result G_theory -> IO ()
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederrunDisproveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
6e121321775373fe11161d23c541437456df19b4Adrián Riesco let oldTh = dgn_theory dgnode in
6e121321775373fe11161d23c541437456df19b4Adrián Riesco unless (rTh == oldTh) $ do
6e121321775373fe11161d23c541437456df19b4Adrián Riesco showDiagMessAux 2 ds
6e121321775373fe11161d23c541437456df19b4Adrián Riesco lockGlobal gInfo
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let ln = libName gInfo
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder iSt = intState gInfo
6e121321775373fe11161d23c541437456df19b4Adrián Riesco ost <- readIORef iSt
6e121321775373fe11161d23c541437456df19b4Adrián Riesco let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder case i_state ost' of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Nothing -> return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder writeIORef iSt ost'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder runAndLock gInfo $ updateGraph gInfo hist
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco unlockGlobal gInfo
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> return ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco{- | Displays a GUI to set TimeoutLimit and select the ConsistencyChecker
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoand holds the functionality to call the ConsistencyChecker for the
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco(previously negated) selected Theorems. -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoshowDisproveWindow :: MVar (Result G_theory) -> LibName -> LibEnv
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> DGraph -> G_theory -> [FNode] -> IO ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoshowDisproveWindow res ln le dg g_th fgoals = postGUIAsync $ do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco xml <- getGladeXML ConsistencyChecker.get
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- get objects
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder window <- xmlGetWidget xml castToWindow "NodeChecker"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnClose <- xmlGetWidget xml castToButton "btnClose"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnResults <- xmlGetWidget xml castToButton "btnResults"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder -- get goals view and buttons
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder trvGoals <- xmlGetWidget xml castToTreeView "trvNodes"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -- get checker view and buttons
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder btnCheck <- xmlGetWidget xml castToButton "btnCheck"
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco btnStop <- xmlGetWidget xml castToButton "btnStop"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco windowSetTitle window "Disprove"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let widgets = [ toWidget sbTimeout
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , toWidget cbComorphism
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder , toWidget lblSublogic ]
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder checkWidgets = widgets ++ [ toWidget btnClose
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder , toWidget btnNodesAll
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco , toWidget btnNodesNone
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , toWidget btnNodesInvert
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , toWidget btnNodesUnchecked
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , toWidget btnNodesTimeout
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco , toWidget btnResults ]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco switch b = do
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco widgetSetSensitive btnStop $ not b
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco widgetSetSensitive btnCheck b
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco widgetSetSensitive btnStop False
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco widgetSetSensitive btnCheck False
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco threadId <- newEmptyMVar
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco wait <- newEmptyMVar
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mView <- newEmptyMVar
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco -- setup data
5eb747ed1f9cb3d902d4277badfc2a42f9f98b0cAdrián Riesco listGoals <- setListData trvGoals show $ sort fgoals
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco listFinder <- setListData trvFinder fName []
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco -- setup comorphism combobox
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco comboBoxSetModelText cbComorphism
3f8cdebaede9921402318d525b57a9af8f9279d3Adrián Riesco shC <- after cbComorphism changed
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco $ setSelectedComorphism trvFinder listFinder cbComorphism
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco -- setup view selection actions
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let update = do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mf <- getSelectedSingle trvFinder listFinder
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco updateComorphism trvFinder listFinder cbComorphism shC
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco widgetSetSensitive btnCheck $ isJust mf
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco setListSelectorSingle trvFinder update
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let upd = updateNodes trvGoals listGoals
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder labelSetLabel lblSublogic $ show s
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco updateFinder trvFinder listFinder b s)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco labelSetLabel lblSublogic "No sublogic"
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco listStoreClear listFinder
0f593bb6e3f0bc82abf3d6d3c76ef222a43d0476Adrián Riesco activate widgets False
0f593bb6e3f0bc82abf3d6d3c76ef222a43d0476Adrián Riesco widgetSetSensitive btnCheck False)
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco (activate widgets True >> widgetSetSensitive btnCheck True)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco shN <- setListSelectorMultiple trvGoals btnNodesAll btnNodesNone
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco btnNodesInvert upd
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco let selectWithAux f u = do
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco signalBlock shN
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco sel <- treeViewGetSelection trvGoals
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco treeSelectionSelectAll sel
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco rs <- treeSelectionGetSelectedRows sel
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco mapM_ ( \ ~p@(row : []) -> do
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco fn <- listStoreGetValue listGoals row
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco (if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco signalUnblock shN
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco selectWith f = selectWithAux $ f . cStatus
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco onClicked btnNodesUnchecked
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder $ selectWith (== ConsistencyStatus CSUnchecked "") upd
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder onClicked btnResults $ showModelView mView "Models" listGoals []
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder onClicked btnClose $ widgetDestroy window
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco onClicked btnCheck $ do
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco activate checkWidgets False
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco timeout <- spinButtonGetValueAsInt sbTimeout
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco inclThms <- toggleButtonGetActive cbInclThms
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco (updat, pexit) <- progressBar "Checking consistency" "please wait..."
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco goals' <- getSelectedMultiple trvGoals listGoals
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco mf <- getSelectedSingle trvFinder listFinder
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco f <- case mf of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco Nothing -> error "Disprove: internal error"
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco Just (_, f) -> return f
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco tid <- forkIO $ do
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco {- call the check function from GUI.GtkConsistencyChecker.
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco first argument means disprove-mode and leads the ConsistencyChecker
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco to mark consistent sentences as disproved (since consistent with
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco negated sentence) -}
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco check True inclThms ln le dg f timeout listGoals updat goals'
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco putMVar wait ()
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco putMVar threadId tid
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco takeMVar wait
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco postGUIAsync $ do
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco tryTakeMVar threadId
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder showModelView mView "Results of disproving" listGoals []
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder signalBlock shN
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco sortNodes trvGoals listGoals
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco signalUnblock shN
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco activate checkWidgets True
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco {- after window closes a new G_theory is created containing the results.
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco only successful disprove attempts are returned; for each one, a new
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco BasicProof is created and set to disproved. -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder onDestroy window $ do
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco fnodes' <- listStoreToList listGoals
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco maybe_F <- getSelectedSingle trvFinder listFinder
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco case maybe_F of
cffa214f1ca524a65075ab26339df7040fe36032Christian Maeder Just (_, f) -> case g_th of
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco G_theory lid _s _i1 sens _i2 -> let
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco sens' = foldr (\ fg t -> if (sType . cStatus) fg == CSInconsistent
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco ps = openProofStatus n' (fName f) (empty_proof_tree lid)
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco bp = BasicProof lid ps { goalStatus = Disproved }
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco c = comorphism f !! selected f
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco s' = s { senAttr = ThmStatus $ (c, bp) : thmStatus s } in
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco else t ) sens fnodes'
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco in putMVar res $ return (G_theory lid _s _i1 sens' _i2)
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco _ -> putMVar res $ return g_th
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder selectWith (== ConsistencyStatus CSUnchecked "") upd
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco widgetShow window