df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski{- |

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiModule : $Header$

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiDescription : Gtk Module to enable disproving Theorems

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Simon Ulbricht, Uni Bremen 2010

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiMaintainer : tekknix@informatik.uni-bremen.de

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : provisional

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : portable

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiThis module provides a disproving module that checks consistency of inverted

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitheorems.

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-}

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskimodule GUI.GtkDisprove (disproveAtNode) where

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Graphics.UI.Gtk

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Graphics.UI.Gtk.Glade

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport GUI.GtkUtils as GtkUtils

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified GUI.Glade.NodeChecker as ConsistencyChecker

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport GUI.GraphTypes

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport GUI.GtkConsistencyChecker

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Proofs.ConsistencyCheck

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maederimport Interfaces.GenericATPState (guiDefaultTimeLimit)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Interfaces.DataTypes

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Logic.Logic

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Logic.Prover

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Static.DevGraph

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Static.GTheory

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Static.ComputeTheory

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Common.OrderedMap as OMap

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.AS_Annotation

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.LibName (LibName)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.Result

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Common.ExtSign

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Control.Concurrent (forkIO, killThread)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Control.Concurrent.MVar

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.Graph.Inductive.Graph (LNode)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.IORef

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport qualified Data.Map as Map

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.List

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiimport Data.Maybe

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskishowDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskishowDisproveGUI gi le dg (i,lbl) = case globalTheory lbl of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> error "GtkDisprove.showDisproveGUI"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just gt@(G_theory _ _ _ sens _) -> let

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski fgoal g = let th = negate_th gt g

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski l = lbl { dgn_theory = th }

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski l' = l { globalTheory = computeLabelTheory le dg (i, l) }

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in FNode { name = g, node = (i,l'), sublogic = sublogicOfTh th,

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski cStatus = ConsistencyStatus CSUnchecked "" }

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski fgoals = map fgoal $ OMap.keys $ OMap.filter (not . isAxiom) sens

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in do

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski wait <- newEmptyMVar

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski showDisproveWindow wait (libName gi) le dg gt fgoals

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski res <- takeMVar wait

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski return ()

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskinegate_th :: G_theory -> String -> G_theory

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskinegate_th g_th goal = case g_th of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski G_theory lid1 (ExtSign sign symb) i1 sens i2 ->

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let axs = OMap.filter isAxiom sens

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder negSen = case OMap.lookup goal sens of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> error "GtkDisprove.disproveThmSingle(1)"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just sen ->

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski case negation lid1 $ sentence sen of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> error "GtkDisprove.disproveThmSingle(2)"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just sen' -> sen { sentence = sen', isAxiom = True }

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sens' = OMap.insert goal negSen axs

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski in G_theory lid1 (ExtSign sign symb) i1 sens' i2

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskidisproveAtNode :: GInfo -> Int -> DGraph -> IO ()

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskidisproveAtNode gInfo descr dgraph = do

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let iSt = intState gInfo

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ost <- readIORef iSt

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski case i_state ost of

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Nothing -> return ()

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Just ist -> do

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let le = i_libEnv ist

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski dgn = labDG dgraph descr

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski showDisproveGUI gInfo le dgraph (descr, dgn)

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- | Displays a GUI to set TimeoutLimit and select the ConsistencyChecker

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- and holds the functionality to call the ConsistencyChecker for the

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- (previously negated) selected Theorems.

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- TODO proveAtNode anschauen, nach hasLock (..), tryLockLocal,

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- MVar auf LNode DGNodeLab

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- TODO rueckgabe von G_theory (Result ..) und einbingung in GraphLogic

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskishowDisproveWindow :: MVar (Result G_theory) -> LibName -> LibEnv

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -> DGraph -> G_theory -> [FNode] -> IO ()

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskishowDisproveWindow res ln le dg g_th fgoals = postGUIAsync $ do

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski xml <- getGladeXML ConsistencyChecker.get

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- get objects

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski window <- xmlGetWidget xml castToWindow "NodeChecker"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnClose <- xmlGetWidget xml castToButton "btnClose"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnResults <- xmlGetWidget xml castToButton "btnResults"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- get goals view and buttons

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski trvGoals <- xmlGetWidget xml castToTreeView "trvNodes"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder -- get checker view and buttons

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnCheck <- xmlGetWidget xml castToButton "btnCheck"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski btnStop <- xmlGetWidget xml castToButton "btnStop"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski windowSetTitle window "Consistency Checker"

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski let widgets = [ toWidget sbTimeout

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget cbComorphism

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget lblSublogic ]

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski checkWidgets = widgets ++ [ toWidget btnClose

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget btnNodesAll

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget btnNodesNone

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget btnNodesInvert

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget btnNodesUnchecked

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski , toWidget btnNodesTimeout

, toWidget btnResults ]

switch b = do

widgetSetSensitive btnStop $ not b

widgetSetSensitive btnCheck b

widgetSetSensitive btnStop False

widgetSetSensitive btnCheck False

threadId <- newEmptyMVar

wait <- newEmptyMVar

mView <- newEmptyMVar

-- setup data

listGoals <- setListData trvGoals show $ sort fgoals

listFinder <- setListData trvFinder fName []

-- setup comorphism combobox

comboBoxSetModelText cbComorphism

shC <- after cbComorphism changed

$ setSelectedComorphism trvFinder listFinder cbComorphism

-- setup view selection actions

let update = do

mf <- getSelectedSingle trvFinder listFinder

updateComorphism trvFinder listFinder cbComorphism shC

widgetSetSensitive btnCheck $ isJust mf

setListSelectorSingle trvFinder update

let upd = updateNodes trvGoals listGoals

(\ b s -> do

labelSetLabel lblSublogic $ show s

updateFinder trvFinder listFinder b s)

(do

labelSetLabel lblSublogic "No sublogic"

listStoreClear listFinder

activate widgets False

widgetSetSensitive btnCheck False)

(activate widgets True >> widgetSetSensitive btnCheck True)

shN <- setListSelectorMultiple trvGoals btnNodesAll btnNodesNone

btnNodesInvert upd

-- bindings

let selectWithAux f u = do

signalBlock shN

sel <- treeViewGetSelection trvGoals

treeSelectionSelectAll sel

rs <- treeSelectionGetSelectedRows sel

mapM_ ( \ p@(row : []) -> do

fn <- listStoreGetValue listGoals row

(if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)

sel p) rs

signalUnblock shN

u

selectWith f = selectWithAux $ f . cStatus

onClicked btnNodesUnchecked

$ selectWith (== ConsistencyStatus CSUnchecked "") upd

onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd

onClicked btnResults $ showModelView mView "Models" listGoals []

onClicked btnClose $ widgetDestroy window

onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait

onClicked btnCheck $ do

activate checkWidgets False

timeout <- spinButtonGetValueAsInt sbTimeout

inclThms <- toggleButtonGetActive cbInclThms

(updat, pexit) <- progressBar "Checking consistency" "please wait..."

goals' <- getSelectedMultiple trvGoals listGoals

mf <- getSelectedSingle trvFinder listFinder

f <- case mf of

Nothing -> error "Consistency checker: internal error"

Just (_, f) -> return f

switch False

tid <- forkIO $ do

check inclThms ln le dg f timeout listGoals updat goals'

putMVar wait ()

putMVar threadId tid

forkIO_ $ do

takeMVar wait

postGUIAsync $ do

switch True

tryTakeMVar threadId

showModelView mView "Results of consistency check" listGoals []

signalBlock shN

sortNodes trvGoals listGoals

signalUnblock shN

upd

activate checkWidgets True

pexit

-- TODO if FNode is Consistent, it must be set to Disproved in DGraph!

onDestroy window $ do

fnodes' <- listStoreToList listGoals

Just (_, f) <- getSelectedSingle trvFinder listFinder

case g_th of

G_theory lid _s _i1 sens _i2 -> let

sens' = foldr (\ fg t -> if (sType . cStatus) fg == CSConsistent

then let

n' = name fg

es = Map.findWithDefault (error

"GtkDisprove.showDisproveWindow") n' t

s = OMap.ele es

ps = openProofStatus n' (fName f) (empty_proof_tree lid)

bp = BasicProof lid ps { goalStatus = Disproved }

c = comorphism f !! selected f

s' = s { senAttr = ThmStatus $ (c, bp) : thmStatus s }

in Map.insert n' es { OMap.ele = s' } t

else t ) sens fnodes'

in putMVar res $ return (G_theory lid _s _i1 sens' _i2)

selectWith (== ConsistencyStatus CSUnchecked "") upd

widgetShow window