0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtDescription : Gtk Module to enable disproving Theorems
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtCopyright : (c) Simon Ulbricht, Uni Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtMaintainer : tekknix@informatik.uni-bremen.de
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtStability : provisional
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtPortability : portable
0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtThis module provides a disproving module that checks consistency of inverted
9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maedermodule GUI.GtkDisprove (disproveAtNode) where
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified GUI.Glade.NodeChecker as ConsistencyChecker
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtimport GUI.GraphLogic hiding (openProofStatus)
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport Interfaces.GenericATPState (guiDefaultTimeLimit)
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtimport Interfaces.Utils (updateNodeProof)
9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maederimport qualified Common.OrderedMap as OMap
9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maederimport Control.Concurrent (forkIO, killThread)
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified Data.Map as Map
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder{- | this method holds the functionality to convert the nodes goals to the
65660c22133e6de16f9ece7b36ac6423014b20aaChristian MaederFNode datatype from GUI.GtkConsistencyChecker. The goals are being negated
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maederby negate_th and this theory is stored in FNodes DGNodeLab local and global
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtshowDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtshowDisproveGUI gi le dg (i, lbl) = case globalTheory lbl of
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht Nothing -> error "GtkDisprove.showDisproveGUI(no global theory found)"
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder Just gt@(G_theory _ _ _ _ sens _) -> let
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht fg g th = let
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht l = lbl { dgn_theory = th }
4f3a84cb1b7e55ce38df8f4ac71d06b574b23cb1mscodescu l' = l { globalTheory = computeLabelTheory le (libName gi) dg (i, l) }
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht no_cs = ConsistencyStatus CSUnchecked ""
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht stat = case OMap.lookup g sens of
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht Nothing -> no_cs
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht Just tm -> case thmStatus tm of
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht ts -> basicProofToConStatus $ maximum $ map snd ts
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder in FNode { name = g, node = (i, l'), sublogic = sublogicOfTh th,
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht cStatus = stat }
d8623e217fff016f9e1759b5603fc06b29fda62cChristian Maeder fgoals = foldr (\ (g, _) t -> case negate_th gt g of
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder Just nt -> fg g nt : t) []
d8623e217fff016f9e1759b5603fc06b29fda62cChristian Maeder $ getThGoals gt
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht in if null fgoals
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu errorDialogExt "Error (disprove)" "found no goals suitable for disprove function"
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht wait <- newEmptyMVar
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht showDisproveWindow wait (libName gi) le dg gt fgoals
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht res <- takeMVar wait
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder runDisproveAtNode gi (i, lbl) res
255f0ed47809d8fea6e177112139735ed8778359Till Mossakowski{- | negates a single sentence within a G_theory and returns a theory
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maedercontaining all axioms in addition to the one negated sentence. -}
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbrichtnegate_th :: G_theory -> String -> Maybe G_theory
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtnegate_th g_th goal = case g_th of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid1 syn (ExtSign sign symb) i1 sens _ ->
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht case OMap.lookup goal sens of
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht Nothing -> Nothing
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht case negation lid1 $ sentence sen of
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht Nothing -> Nothing
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht Just sen' -> let
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht negSen = sen { sentence = sen', isAxiom = True }
432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht sens' = OMap.insert goal negSen $ OMap.filter isAxiom sens
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder in Just $ G_theory lid1 syn (ExtSign sign symb) i1 sens' startThId
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder{- | this function is being called from outside and manages the locking-
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maedermechanism of the node being called upon. -}
a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtdisproveAtNode :: GInfo -> Int -> DGraph -> IO ()
a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtdisproveAtNode gInfo descr dgraph = do
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht lockedEnv <- ensureLockAtNode gInfo descr dgraph
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht case lockedEnv of
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder Nothing -> return ()
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht Just (dg, lbl, le) -> do
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht acquired <- tryLockLocal lbl
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht if acquired then do
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht showDisproveGUI gInfo le dg (descr, lbl)
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht unlockLocal lbl
e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht else errorDialogExt "Error" "Proof or disproof window already open"
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder{- | after results have been collected, this function is called to store
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maederthe results for this node within the dgraphs history. -}
6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtrunDisproveAtNode :: GInfo -> LNode DGNodeLab -> Result G_theory -> IO ()
abea93ed557b22ea833e1524ee5ca11afc12208aSimon UlbrichtrunDisproveAtNode gInfo (v, dgnode) (Result ds mres) = case mres of
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht let oldTh = dgn_theory dgnode in
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht unless (rTh == oldTh) $ do
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht showDiagMessAux 2 ds
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht lockGlobal gInfo
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht let ln = libName gInfo
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht iSt = intState gInfo
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht ost <- readIORef iSt
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht let (ost', hist) = updateNodeProof ln ost (v, dgnode) rTh
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht case i_state ost' of
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht Nothing -> return ()
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht writeIORef iSt ost'
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht runAndLock gInfo $ updateGraph gInfo hist
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht unlockGlobal gInfo
abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht _ -> return ()
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder{- | Displays a GUI to set TimeoutLimit and select the ConsistencyChecker
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maederand holds the functionality to call the ConsistencyChecker for the
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder(previously negated) selected Theorems. -}
65660c22133e6de16f9ece7b36ac6423014b20aaChristian MaedershowDisproveWindow :: MVar (Result G_theory) -> LibName -> LibEnv
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht -> DGraph -> G_theory -> [FNode] -> IO ()
a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtshowDisproveWindow res ln le dg g_th fgoals = postGUIAsync $ do
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht xml <- getGladeXML ConsistencyChecker.get
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -- get objects
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht window <- xmlGetWidget xml castToWindow "NodeChecker"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnClose <- xmlGetWidget xml castToButton "btnClose"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnResults <- xmlGetWidget xml castToButton "btnResults"
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht -- get goals view and buttons
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht trvGoals <- xmlGetWidget xml castToTreeView "trvNodes"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -- get checker view and buttons
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnCheck <- xmlGetWidget xml castToButton "btnCheck"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht btnStop <- xmlGetWidget xml castToButton "btnStop"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"
22a42cbea5bdf4b39b99794550b1403b3820b5e5Christian Maeder toolLabel <- xmlGetWidget xml castToLabel "label1"
22a42cbea5bdf4b39b99794550b1403b3820b5e5Christian Maeder labelSetLabel toolLabel "Pick disprover"
ea9768c548fe6ae05d275380869c2923c3392244Simon Ulbricht windowSetTitle window "Disprove"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht let widgets = [ toWidget sbTimeout
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget cbComorphism
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget lblSublogic ]
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht checkWidgets = widgets ++ [ toWidget btnClose
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnNodesAll
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnNodesNone
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnNodesInvert
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnNodesUnchecked
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnNodesTimeout
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht , toWidget btnResults ]
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht switch b = do
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnStop $ not b
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnCheck b
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnStop False
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnCheck False
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht threadId <- newEmptyMVar
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht wait <- newEmptyMVar
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mView <- newEmptyMVar
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -- setup data
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht listGoals <- setListData trvGoals show $ sort fgoals
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht listFinder <- setListData trvFinder fName []
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -- setup comorphism combobox
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht comboBoxSetModelText cbComorphism
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht shC <- after cbComorphism changed
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht $ setSelectedComorphism trvFinder listFinder cbComorphism
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -- setup view selection actions
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht let update = do
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mf <- getSelectedSingle trvFinder listFinder
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht updateComorphism trvFinder listFinder cbComorphism shC
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnCheck $ isJust mf
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht setListSelectorSingle trvFinder update
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht let upd = updateNodes trvGoals listGoals
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht labelSetLabel lblSublogic $ show s
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht updateFinder trvFinder listFinder b s)
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht labelSetLabel lblSublogic "No sublogic"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht listStoreClear listFinder
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht activate widgets False
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetSetSensitive btnCheck False)
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (activate widgets True >> widgetSetSensitive btnCheck True)
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht shN <- setListSelectorMultiple trvGoals btnNodesAll btnNodesNone
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht btnNodesInvert upd
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht let selectWithAux f u = do
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht signalBlock shN
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht sel <- treeViewGetSelection trvGoals
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht treeSelectionSelectAll sel
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht rs <- treeSelectionGetSelectedRows sel
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder mapM_ ( \ ~p@(row : []) -> do
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht fn <- listStoreGetValue listGoals row
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht signalUnblock shN
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht selectWith f = selectWithAux $ f . cStatus
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht onClicked btnNodesUnchecked
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht $ selectWith (== ConsistencyStatus CSUnchecked "") upd
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht onClicked btnResults $ showModelView mView "Models" listGoals []
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht onClicked btnClose $ widgetDestroy window
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht onClicked btnCheck $ do
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht activate checkWidgets False
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht timeout <- spinButtonGetValueAsInt sbTimeout
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht inclThms <- toggleButtonGetActive cbInclThms
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (updat, pexit) <- progressBar "Checking consistency" "please wait..."
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht goals' <- getSelectedMultiple trvGoals listGoals
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mf <- getSelectedSingle trvFinder listFinder
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht f <- case mf of
ea9768c548fe6ae05d275380869c2923c3392244Simon Ulbricht Nothing -> error "Disprove: internal error"
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht Just (_, f) -> return f
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht tid <- forkIO $ do
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- call the check function from GUI.GtkConsistencyChecker.
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder first argument means disprove-mode and leads the ConsistencyChecker
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder to mark consistent sentences as disproved (since consistent with
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder negated sentence) -}
987c9ee1092c7fd8b53242abefe4f3cf8e9a1011Simon Ulbricht check True inclThms ln le dg f timeout listGoals updat goals'
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht putMVar wait ()
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht putMVar threadId tid
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht takeMVar wait
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht postGUIAsync $ do
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht tryTakeMVar threadId
ea9768c548fe6ae05d275380869c2923c3392244Simon Ulbricht showModelView mView "Results of disproving" listGoals []
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht signalBlock shN
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht sortNodes trvGoals listGoals
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht signalUnblock shN
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht activate checkWidgets True
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder {- after window closes a new G_theory is created containing the results.
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder only successful disprove attempts are returned; for each one, a new
65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder BasicProof is created and set to disproved. -}
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht onDestroy window $ do
a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht fnodes' <- listStoreToList listGoals
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht maybe_F <- getSelectedSingle trvFinder listFinder
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht case maybe_F of
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht Just (_, f) -> case g_th of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid syn sig i1 sens _ -> let
3ac14720aa7f1e0715311bd1598e7d78c37dd3c6Simon Ulbricht sens' = foldr (\ fg t -> if (sType . cStatus) fg == CSInconsistent
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht ps = openProofStatus n' (fName f) (empty_proof_tree lid)
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht bp = BasicProof lid ps { goalStatus = Disproved }
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht c = comorphism f !! selected f
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht s' = s { senAttr = ThmStatus $ (c, bp) : thmStatus s } in
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht else t ) sens fnodes'
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder in putMVar res $ return (G_theory lid syn sig i1 sens' startThId)
53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht _ -> putMVar res $ return g_th
1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht selectWith (== ConsistencyStatus CSUnchecked "") upd
369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht widgetShow window