fcc3093f7b872846234fe62496fad4feddf8dd27trawick{- |

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickModule : $Header$

fcc3093f7b872846234fe62496fad4feddf8dd27trawickDescription : Gtk Module to enable disproving Theorems

c76b9f9f0feb93458a61875e0c4f7aa36fac8cf5jimCopyright : (c) Simon Ulbricht, Uni Bremen 2010

fcc3093f7b872846234fe62496fad4feddf8dd27trawickLicense : GPLv2 or higher, see LICENSE.txt

fcc3093f7b872846234fe62496fad4feddf8dd27trawick

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickMaintainer : tekknix@informatik.uni-bremen.de

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickStability : provisional

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickPortability : portable

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickThis module provides a disproving module that checks consistency of inverted

125681776870ca1c5f5db07ae7b32540ee44e2f9trawicktheorems.

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick-}

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickmodule GUI.GtkDisprove (showDisproveGUI) where

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Graphics.UI.Gtk

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Graphics.UI.Gtk.Glade

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport GUI.GtkUtils as GtkUtils

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport qualified GUI.Glade.NodeChecker as ConsistencyChecker

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport GUI.GraphTypes

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Static.DevGraph

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport Static.PrintDevGraph ()

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport Static.GTheory

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Static.History

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport Static.ComputeTheory

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickimport Interfaces.GenericATPState (guiDefaultTimeLimit)

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Logic.Logic

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Logic.Coerce

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickimport Logic.Grothendieck

fcc3093f7b872846234fe62496fad4feddf8dd27trawickimport Logic.Comorphism

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Logic.Prover

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Comorphisms.LogicGraph (logicGraph)

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Comorphisms.KnownProvers

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport qualified Common.OrderedMap as OMap

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Common.AS_Annotation

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Common.LibName (LibName)

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Common.Result

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Common.ExtSign

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Common.Utils

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Control.Concurrent (forkIO, killThread)

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Control.Concurrent.MVar

8f234296a4f049d42dfc15e1e3544b4c788242b8trawickimport Control.Monad (foldM_, join, when)

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Proofs.AbstractState

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Data.Graph.Inductive.Graph (LNode)

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport qualified Data.Map as Map

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Data.List

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickimport Data.Maybe

8f234296a4f049d42dfc15e1e3544b4c788242b8trawick

176e4ecfb3dba2ce74bf21c657738755efe3899etrawickdata Finder = Finder { fName :: String

176e4ecfb3dba2ce74bf21c657738755efe3899etrawick , finder :: G_cons_checker

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick , comorphism :: [AnyComorphism]

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick , selected :: Int }

efda5b91e5449985bbee6c3e3aa5d8d87b496310trawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickdata FGoal = FGoal { name :: String

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick , neg_th :: G_theory }

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick -- checkers :: [(G_Cons_Checker, [AnyComorphism])] }

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick

125681776870ca1c5f5db07ae7b32540ee44e2f9trawickshowDisproveGUI :: LNode DGNodeLab -> ProofState lid sentence

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick -> IO (ProofState lid sentence)

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawickshowDisproveGUI (_,lbl) pstate = case globalTheory lbl of

fcc3093f7b872846234fe62496fad4feddf8dd27trawick Nothing -> error "GtkDisprove.showDisproveGUI"

fcc3093f7b872846234fe62496fad4feddf8dd27trawick Just gt@(G_theory lid1 (ExtSign sign symb) _ sens _) -> let

fcc3093f7b872846234fe62496fad4feddf8dd27trawick goals = OMap.keys $ OMap.filter (not . isAxiom) sens

fcc3093f7b872846234fe62496fad4feddf8dd27trawick neg_theories = map (negate_th gt) goals

fcc3093f7b872846234fe62496fad4feddf8dd27trawick consCheckers = concatMap (\th -> getConsCheckers $

fcc3093f7b872846234fe62496fad4feddf8dd27trawick findComorphismPaths logicGraph $

fcc3093f7b872846234fe62496fad4feddf8dd27trawick sublogicOfTh th) neg_theories

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick fgoals = zipWith (\ a b -> FGoal {name = a, neg_th = b}) goals neg_theories

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick in do

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick wait <- newEmptyMVar

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick showDisproveWindow gt pstate fgoals consCheckers wait

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick st' <- takeMVar wait

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick return st'

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawicknegate_th :: G_theory -> String -> G_theory

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawicknegate_th g_th goal = case g_th of

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

125681776870ca1c5f5db07ae7b32540ee44e2f9trawick let axs = OMap.filter isAxiom sens

69c7cb9eeb0d965849dbc65e06a4a734f17fd7eftrawick negSen = case OMap.lookup goal sens of

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

Just sen ->

case negation lid1 $ sentence sen of

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

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

sens' = OMap.insert goal negSen axs

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

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

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

-- (previously negated) selected Theorems.

-- TODO

showDisproveWindow :: G_theory -> ProofState lid sentence -> [FGoal]

-> [(G_cons_checker, AnyComorphism)]

-> MVar (ProofState lid sentence) -> IO ()

showDisproveWindow g_th st fgoals finders res = postGUIAsync $ do

xml <- getGladeXML ConsistencyChecker.get

-- get objects

window <- xmlGetWidget xml castToWindow "NodeChecker"

btnClose <- xmlGetWidget xml castToButton "btnClose"

btnResults <- xmlGetWidget xml castToButton "btnResults"

-- get nodes view and buttons

trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"

btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"

btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"

btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"

btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"

btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"

cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"

-- get checker view and buttons

cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"

lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"

btnCheck <- xmlGetWidget xml castToButton "btnCheck"

btnStop <- xmlGetWidget xml castToButton "btnStop"

trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"

windowSetTitle window "Consistency Checker"

spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit

let widgets = [ toWidget sbTimeout

, toWidget cbComorphism

, toWidget lblSublogic ]

checkWidgets = widgets ++ [ toWidget btnClose

, toWidget btnNodesAll

, toWidget btnNodesNone

, toWidget btnNodesInvert

, toWidget btnNodesUnchecked

, 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

let toFinder (gc,c) = Finder { fName = getPName gc, finder = gc,

comorphism = [c], selected = 1 }

listNodes <- setListData trvNodes name fgoals

listFinder <- setListData trvFinder fName [toFinder (head finders)]

-- 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

update' s' = do

return s'

setListSelectorSingle trvFinder update

{- let upd = updateNodes trvNodes listNodes

(\ 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 trvNodes btnNodesAll btnNodesNone

-- btnNodesInvert

-- bindings

let selectWith f = do

-- signalBlock shN

sel <- treeViewGetSelection trvNodes

treeSelectionSelectAll sel

rs <- treeSelectionGetSelectedRows sel

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

fn <- listStoreGetValue listNodes row

(if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)

sel p) rs

-- signalUnblock shN

onClicked btnNodesUnchecked

$ selectWith (\ a -> True)

onClicked btnNodesTimeout $ selectWith (\ a -> True)

-- onClicked btnResults $ showModelView mView "Models" listNodes emptyNodes

--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 trvNodes listNodes

mf <- getSelectedSingle trvFinder listFinder

f <- case mf of

Nothing -> error "Consistency checker: internal error"

Just (_, f) -> return f

switch False

tid <- forkIO $ do

let count' = fromIntegral $ length goals

-- c = comorphism f !! selected f

foldM_ (\ count fg -> do

postGUISync $ updat (count / count') $ name fg

s' <- takeMVar res

s'' <- disproveThmSingle fg f timeout s'

--postGUISync $ listStoreSetValue listNodes row fn { status = res }

putMVar res =<< update' s''

return $ count + 1) 0 fgoals

putMVar wait ()

putMVar threadId tid

forkIO_ $ do

takeMVar wait

postGUIAsync $ do

switch True

tryTakeMVar threadId

--showModelView mView "Results of consistency check" listNodes emptyNodes

--signalBlock shN

--sortNodes trvNodes listNodes

--signalUnblock shN

--upd

activate checkWidgets True

pexit

--onDestroy window $ do

{-nodes' <- listStoreToList listNodes

let changes = foldl (\ cs (FNode { node = (i, l), status = s }) ->

if (\ st -> st /= CSConsistent && st /= CSInconsistent)

$ sType s then cs

else

let n = (i, if sType s == CSInconsistent then

markNodeInconsistent "" l

else markNodeConsistent "" l)

in SetNodeLab l n : cs

) [] nodes'

dg' = changesDGH dg changes -}

--putMVar res $ Map.insert ln (groupHistory dg (DGRule "Consistency") dg') le

putMVar res =<< update' st

selectWith (\ a -> False)

widgetShow window

updateComorphism :: TreeView -> ListStore Finder -> ComboBox

-> ConnectId ComboBox -> IO ()

updateComorphism view list cbComorphism sh = do

signalBlock sh

model <- comboBoxGetModelText cbComorphism

listStoreClear model

mfinder <- getSelectedSingle view list

case mfinder of

Just (_, f) -> do

mapM_ (comboBoxAppendText cbComorphism) $ expand f

comboBoxSetActive cbComorphism $ selected f

Nothing -> return ()

signalUnblock sh

expand :: Finder -> [String]

expand = map show . comorphism

setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()

setSelectedComorphism view list cbComorphism = do

mfinder <- getSelectedSingle view list

case mfinder of

Just (i, f) -> do

sel <- comboBoxGetActive cbComorphism

listStoreSetValue list i f { selected = sel }

Nothing -> return ()

disproveThmSingle :: FGoal

-> Finder

-> Int -- ^ timeout limit

-> ProofState lid sentence

-> IO (ProofState lid sentence)

disproveThmSingle (FGoal n th) fdr t'' state = undefined {-

let info s = infoDialog ("Disprove " ++ selGoal) s in

case globalTheory lbl of

Nothing -> info "Disprove failed: No global Theory"

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

case OMap.lookup selGoal sens of

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

Just sen -> case negation lid1 $ sentence sen of

Nothing -> info "Disprove failed: negation is not defined"

Just s' -> do

let negSen = sen { sentence = s', isAxiom = True }

axs = OMap.filter isAxiom sens

sens' = OMap.insert selGoal negSen axs

g_th = G_theory lid1 (ExtSign sign symb) i1 sens' i2

subL = sublogicOfTh g_th

lcc = getConsCheckers $ findComorphismPaths logicGraph subL

case find (\ (p, _) -> getPName p == selPr) lcc of

Nothing ->

info $ "failed to find Consistency Checker for the selected prover\n\n"

++ "possible ConsCheckers are:\n" ++ intercalate "\n"

(nubOrd $ map (getPName . fst) lcc)

Just (G_cons_checker lid4 cc, Comorphism cid) -> do

let lidS = sourceLogic cid

lidT = targetLogic cid

res = do

bTh' <- coerceBasicTheory lid1 lidS "" (sign, toNamedList sens')

(sig2, sens2) <- wrapMapTheory cid bTh'

incl <- subsig_inclusion lidT (empty_signature lidT) sig2

return TheoryMorphism

{ tSource = emptyTheory lidT

, tTarget = Theory sig2 $ toThSens sens2

, tMorphism = incl }

case maybeResult res of

Nothing ->

info "Disprove failed: TheoryMorphism could not be constructed"

Just mor -> do

let thName = getDGNodeName lbl

ts = TacticScript $ if ccNeedsTimer cc then "" else show t''

cc' <- coerceConsChecker lid4 lidT "" cc

ccS <- (if ccNeedsTimer cc' then timeoutSecs t'' else ((return . Just) =<<))

(ccAutomatic cc' thName ts mor [])

case ccS of

Just ccStatus -> do

info $ "the ConsistencyChecker " ++ ccName cc' ++ " has returned "

++ "the following " ++ case ccResult ccStatus of

Nothing -> ""

Just b -> if b then "consistent" else "inconsistent"

++ " results:\n" ++ show (ccProofTree ccStatus)

Nothing -> do

info $ "the ConsistencyChecker has not returned any results\n"

++ "ConsistencyChecker used: " ++ ccName cc'

-}