{- |
Module      :  ./GUI/GtkDisprove.hs
Description :  Gtk Module to enable disproving Theorems
Copyright   :  (c) Simon Ulbricht, Uni Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  tekknix@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

This module provides a disproving module that checks consistency of inverted
theorems.
-}

module GUI.GtkDisprove (disproveAtNode) where

import Graphics.UI.Gtk

import GUI.GtkUtils
import qualified GUI.Glade.NodeChecker as ConsistencyChecker
import GUI.GraphTypes
import GUI.GraphLogic hiding (openProofStatus)
import GUI.GtkConsistencyChecker

import Proofs.ConsistencyCheck

import Interfaces.GenericATPState (guiDefaultTimeLimit)
import Interfaces.DataTypes
import Interfaces.Utils (updateNodeProof)

import Logic.Logic
import Logic.Prover

import Static.DevGraph
import Static.GTheory
import Static.ComputeTheory

import qualified Common.OrderedMap as OMap
import Common.AS_Annotation
import Common.LibName (LibName)
import Common.Result
import Common.ExtSign

import Control.Concurrent (forkIO, killThread)
import Control.Concurrent.MVar
import Control.Monad (unless)

import Data.Graph.Inductive.Graph (LNode)
import Data.IORef
import qualified Data.Map as Map
import Data.List
import Data.Maybe

{- | this method holds the functionality to convert the nodes goals to the
FNode datatype from GUI.GtkConsistencyChecker. The goals are being negated
by negate_th and this theory is stored in FNodes DGNodeLab local and global
theory. -}
showDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
showDisproveGUI :: GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
showDisproveGUI gi :: GInfo
gi le :: LibEnv
le dg :: DGraph
dg (i :: Node
i, lbl :: DGNodeLab
lbl) = case DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl of
  Nothing -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error "GtkDisprove.showDisproveGUI(no global theory found)"
  Just gt :: G_theory
gt@(G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) -> let
    fg :: [Char] -> G_theory -> FNode
fg g :: [Char]
g th :: G_theory
th = let
      l :: DGNodeLab
l = DGNodeLab
lbl { dgn_theory :: G_theory
dgn_theory = G_theory
th }
      l' :: DGNodeLab
l' = DGNodeLab
l { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
le (GInfo -> LibName
libName GInfo
gi) DGraph
dg (Node
i, DGNodeLab
l) }
      no_cs :: ConsistencyStatus
no_cs = SType -> [Char] -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked ""
      stat :: ConsistencyStatus
stat = case [Char]
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenStatus sentence (AnyComorphism, BasicProof))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup [Char]
g ThSens sentence (AnyComorphism, BasicProof)
sens of
        Nothing -> ConsistencyStatus
no_cs
        Just tm :: SenStatus sentence (AnyComorphism, BasicProof)
tm -> case SenStatus sentence (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenStatus sentence (AnyComorphism, BasicProof)
tm of
          [] -> ConsistencyStatus
no_cs
          ts :: [(AnyComorphism, BasicProof)]
ts -> BasicProof -> ConsistencyStatus
basicProofToConStatus (BasicProof -> ConsistencyStatus)
-> BasicProof -> ConsistencyStatus
forall a b. (a -> b) -> a -> b
$ [BasicProof] -> BasicProof
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([BasicProof] -> BasicProof) -> [BasicProof] -> BasicProof
forall a b. (a -> b) -> a -> b
$ ((AnyComorphism, BasicProof) -> BasicProof)
-> [(AnyComorphism, BasicProof)] -> [BasicProof]
forall a b. (a -> b) -> [a] -> [b]
map (AnyComorphism, BasicProof) -> BasicProof
forall a b. (a, b) -> b
snd [(AnyComorphism, BasicProof)]
ts
      in FNode :: [Char]
-> LNode DGNodeLab -> G_sublogics -> ConsistencyStatus -> FNode
FNode { name :: [Char]
name = [Char]
g, node :: LNode DGNodeLab
node = (Node
i, DGNodeLab
l'), sublogic :: G_sublogics
sublogic = G_theory -> G_sublogics
sublogicOfTh G_theory
th,
                 cStatus :: ConsistencyStatus
cStatus = ConsistencyStatus
stat }
    fgoals :: [FNode]
fgoals = (([Char], Maybe BasicProof) -> [FNode] -> [FNode])
-> [FNode] -> [([Char], Maybe BasicProof)] -> [FNode]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (g :: [Char]
g, _) t :: [FNode]
t -> case G_theory -> [Char] -> Maybe G_theory
negate_th G_theory
gt [Char]
g of
      Nothing -> [FNode]
t
      Just nt :: G_theory
nt -> [Char] -> G_theory -> FNode
fg [Char]
g G_theory
nt FNode -> [FNode] -> [FNode]
forall a. a -> [a] -> [a]
: [FNode]
t) []
        ([([Char], Maybe BasicProof)] -> [FNode])
-> [([Char], Maybe BasicProof)] -> [FNode]
forall a b. (a -> b) -> a -> b
$ G_theory -> [([Char], Maybe BasicProof)]
getThGoals G_theory
gt
    in if [FNode] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FNode]
fgoals
      then
          [Char] -> [Char] -> IO ()
errorDialogExt "Error (disprove)" "found no goals suitable for disprove function"
      else do
        MVar (Result G_theory)
wait <- IO (MVar (Result G_theory))
forall a. IO (MVar a)
newEmptyMVar
        MVar (Result G_theory)
-> LibName -> LibEnv -> DGraph -> G_theory -> [FNode] -> IO ()
showDisproveWindow MVar (Result G_theory)
wait (GInfo -> LibName
libName GInfo
gi) LibEnv
le DGraph
dg G_theory
gt [FNode]
fgoals
        Result G_theory
res <- MVar (Result G_theory) -> IO (Result G_theory)
forall a. MVar a -> IO a
takeMVar MVar (Result G_theory)
wait
        GInfo -> LNode DGNodeLab -> Result G_theory -> IO ()
runDisproveAtNode GInfo
gi (Node
i, DGNodeLab
lbl) Result G_theory
res

{- | negates a single sentence within a G_theory and returns a theory
containing all axioms in addition to the one negated sentence. -}
negate_th :: G_theory -> String -> Maybe G_theory
negate_th :: G_theory -> [Char] -> Maybe G_theory
negate_th g_th :: G_theory
g_th goal :: [Char]
goal = case G_theory
g_th of
  G_theory lid1 :: lid
lid1 syn :: Maybe IRI
syn (ExtSign sign :: sign
sign symb :: Set symbol
symb) i1 :: SigId
i1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ ->
    case [Char]
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenStatus sentence (AnyComorphism, BasicProof))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup [Char]
goal ThSens sentence (AnyComorphism, BasicProof)
sens of
      Nothing -> Maybe G_theory
forall a. Maybe a
Nothing
      Just sen :: SenStatus sentence (AnyComorphism, BasicProof)
sen ->
        case lid -> sentence -> Maybe sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sentence -> Maybe sentence
negation lid
lid1 (sentence -> Maybe sentence) -> sentence -> Maybe sentence
forall a b. (a -> b) -> a -> b
$ SenStatus sentence (AnyComorphism, BasicProof) -> sentence
forall s a. SenAttr s a -> s
sentence SenStatus sentence (AnyComorphism, BasicProof)
sen of
          Nothing -> Maybe G_theory
forall a. Maybe a
Nothing
          Just sen' :: sentence
sen' -> let
            negSen :: SenStatus sentence (AnyComorphism, BasicProof)
negSen = SenStatus sentence (AnyComorphism, BasicProof)
sen { sentence :: sentence
sentence = sentence
sen', isAxiom :: Bool
isAxiom = Bool
True }
            sens' :: ThSens sentence (AnyComorphism, BasicProof)
sens' = [Char]
-> SenStatus sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => k -> a -> OMap k a -> OMap k a
OMap.insert [Char]
goal SenStatus sentence (AnyComorphism, BasicProof)
negSen (ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens
            in G_theory -> Maybe G_theory
forall a. a -> Maybe a
Just (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid1 Maybe IRI
syn (sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sign Set symbol
symb) SigId
i1 ThSens sentence (AnyComorphism, BasicProof)
sens' ThId
startThId

{- | this function is being called from outside and manages the locking-
mechanism of the node being called upon. -}
disproveAtNode :: GInfo -> Int -> DGraph -> IO ()
disproveAtNode :: GInfo -> Node -> DGraph -> IO ()
disproveAtNode gInfo :: GInfo
gInfo descr :: Node
descr dgraph :: DGraph
dgraph = do
  Maybe (DGraph, DGNodeLab, LibEnv)
lockedEnv <- GInfo -> Node -> DGraph -> IO (Maybe (DGraph, DGNodeLab, LibEnv))
ensureLockAtNode GInfo
gInfo Node
descr DGraph
dgraph
  case Maybe (DGraph, DGNodeLab, LibEnv)
lockedEnv of
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just (dg :: DGraph
dg, lbl :: DGNodeLab
lbl, le :: LibEnv
le) -> do
      Bool
acquired <- DGNodeLab -> IO Bool
tryLockLocal DGNodeLab
lbl
      if Bool
acquired then do
        GInfo -> LibEnv -> DGraph -> LNode DGNodeLab -> IO ()
showDisproveGUI GInfo
gInfo LibEnv
le DGraph
dg (Node
descr, DGNodeLab
lbl)
        DGNodeLab -> IO ()
unlockLocal DGNodeLab
lbl
      else [Char] -> [Char] -> IO ()
errorDialogExt "Error" "Proof or disproof window already open"

{- | after results have been collected, this function is called to store
the results for this node within the dgraphs history. -}
runDisproveAtNode :: GInfo -> LNode DGNodeLab -> Result G_theory -> IO ()
runDisproveAtNode :: GInfo -> LNode DGNodeLab -> Result G_theory -> IO ()
runDisproveAtNode gInfo :: GInfo
gInfo (v :: Node
v, dgnode :: DGNodeLab
dgnode) (Result ds :: [Diagnosis]
ds mres :: Maybe G_theory
mres) = case Maybe G_theory
mres of
  Just rTh :: G_theory
rTh ->
    let oldTh :: G_theory
oldTh = DGNodeLab -> G_theory
dgn_theory DGNodeLab
dgnode in
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (G_theory
rTh G_theory -> G_theory -> Bool
forall a. Eq a => a -> a -> Bool
== G_theory
oldTh) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      Node -> [Diagnosis] -> IO ()
showDiagMessAux 2 [Diagnosis]
ds
      GInfo -> IO ()
lockGlobal GInfo
gInfo
      let ln :: LibName
ln = GInfo -> LibName
libName GInfo
gInfo
          iSt :: IORef IntState
iSt = GInfo -> IORef IntState
intState GInfo
gInfo
      IntState
ost <- IORef IntState -> IO IntState
forall a. IORef a -> IO a
readIORef IORef IntState
iSt
      let (ost' :: IntState
ost', hist :: [DGChange]
hist) = LibName
-> IntState
-> LNode DGNodeLab
-> G_theory
-> (IntState, [DGChange])
updateNodeProof LibName
ln IntState
ost (Node
v, DGNodeLab
dgnode) G_theory
rTh
      case IntState -> Maybe IntIState
i_state IntState
ost' of
        Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just _ -> do
          IORef IntState -> IntState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef IntState
iSt IntState
ost'
          GInfo -> IO () -> IO ()
runAndLock GInfo
gInfo (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ GInfo -> [DGChange] -> IO ()
updateGraph GInfo
gInfo [DGChange]
hist
      GInfo -> IO ()
unlockGlobal GInfo
gInfo
  _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{- | Displays a GUI to set TimeoutLimit and select the ConsistencyChecker
and holds the functionality to call the ConsistencyChecker for the
(previously negated) selected Theorems. -}
showDisproveWindow :: MVar (Result G_theory) -> LibName -> LibEnv
                   -> DGraph -> G_theory -> [FNode] -> IO ()
showDisproveWindow :: MVar (Result G_theory)
-> LibName -> LibEnv -> DGraph -> G_theory -> [FNode] -> IO ()
showDisproveWindow res :: MVar (Result G_theory)
res ln :: LibName
ln le :: LibEnv
le dg :: DGraph
dg g_th :: G_theory
g_th fgoals :: [FNode]
fgoals = IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  Builder
builder <- ([Char], [Char]) -> IO Builder
getGTKBuilder ([Char], [Char])
ConsistencyChecker.get
  -- get objects
  Window
window <- Builder -> (GObject -> Window) -> [Char] -> IO Window
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Window
forall obj. GObjectClass obj => obj -> Window
castToWindow "NodeChecker"
  Button
btnClose <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnClose"
  Button
btnResults <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnResults"
  -- get goals view and buttons
  TreeView
trvGoals <- Builder -> (GObject -> TreeView) -> [Char] -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvNodes"
  Button
btnNodesAll <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesAll"
  Button
btnNodesNone <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesNone"
  Button
btnNodesInvert <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesInvert"
  Button
btnNodesUnchecked <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesUnchecked"
  Button
btnNodesTimeout <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnNodesTimeout"
  CheckButton
cbInclThms <- Builder -> (GObject -> CheckButton) -> [Char] -> IO CheckButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> CheckButton
forall obj. GObjectClass obj => obj -> CheckButton
castToCheckButton "cbInclThms"
  -- get checker view and buttons
  ComboBox
cbComorphism <- Builder -> (GObject -> ComboBox) -> [Char] -> IO ComboBox
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> ComboBox
forall obj. GObjectClass obj => obj -> ComboBox
castToComboBox "cbComorphism"
  Label
lblSublogic <- Builder -> (GObject -> Label) -> [Char] -> IO Label
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Label
forall obj. GObjectClass obj => obj -> Label
castToLabel "lblSublogic"
  SpinButton
sbTimeout <- Builder -> (GObject -> SpinButton) -> [Char] -> IO SpinButton
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> SpinButton
forall obj. GObjectClass obj => obj -> SpinButton
castToSpinButton "sbTimeout"
  Button
btnCheck <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnCheck"
  Button
btnStop <- Builder -> (GObject -> Button) -> [Char] -> IO Button
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Button
forall obj. GObjectClass obj => obj -> Button
castToButton "btnStop"
  TreeView
trvFinder <- Builder -> (GObject -> TreeView) -> [Char] -> IO TreeView
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> TreeView
forall obj. GObjectClass obj => obj -> TreeView
castToTreeView "trvFinder"
  Label
toolLabel <- Builder -> (GObject -> Label) -> [Char] -> IO Label
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Label
forall obj. GObjectClass obj => obj -> Label
castToLabel "label1"
  Label -> [Char] -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
toolLabel "Pick disprover"
  Window -> [Char] -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window "Disprove"
  SpinButton -> Double -> IO ()
forall self. SpinButtonClass self => self -> Double -> IO ()
spinButtonSetValue SpinButton
sbTimeout (Double -> IO ()) -> Double -> IO ()
forall a b. (a -> b) -> a -> b
$ Node -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Node
guiDefaultTimeLimit

  let widgets :: [Widget]
widgets = [ SpinButton -> Widget
forall o. WidgetClass o => o -> Widget
toWidget SpinButton
sbTimeout
                , ComboBox -> Widget
forall o. WidgetClass o => o -> Widget
toWidget ComboBox
cbComorphism
                , Label -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Label
lblSublogic ]
      checkWidgets :: [Widget]
checkWidgets = [Widget]
widgets [Widget] -> [Widget] -> [Widget]
forall a. [a] -> [a] -> [a]
++ [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnClose
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesAll
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesNone
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesInvert
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesUnchecked
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnNodesTimeout
                                , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnResults ]
      switch :: Bool -> IO ()
switch b :: Bool
b = do
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
b

  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop Bool
False
  Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False

  MVar ThreadId
threadId <- IO (MVar ThreadId)
forall a. IO (MVar a)
newEmptyMVar
  MVar ()
wait <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  MVar (IO ())
mView <- IO (MVar (IO ()))
forall a. IO (MVar a)
newEmptyMVar

  -- setup data
  ListStore FNode
listGoals <- TreeView -> (FNode -> [Char]) -> [FNode] -> IO (ListStore FNode)
forall a. TreeView -> (a -> [Char]) -> [a] -> IO (ListStore a)
setListData TreeView
trvGoals FNode -> [Char]
forall a. Show a => a -> [Char]
show ([FNode] -> IO (ListStore FNode))
-> [FNode] -> IO (ListStore FNode)
forall a b. (a -> b) -> a -> b
$ [FNode] -> [FNode]
forall a. Ord a => [a] -> [a]
sort [FNode]
fgoals
  ListStore Finder
listFinder <- TreeView -> (Finder -> [Char]) -> [Finder] -> IO (ListStore Finder)
forall a. TreeView -> (a -> [Char]) -> [a] -> IO (ListStore a)
setListData TreeView
trvFinder Finder -> [Char]
fName []

  -- setup comorphism combobox
  ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxSetModelText ComboBox
cbComorphism
  ConnectId ComboBox
shC <- ComboBox
-> Signal ComboBox (IO ()) -> IO () -> IO (ConnectId ComboBox)
forall object callback.
object
-> Signal object callback -> callback -> IO (ConnectId object)
after ComboBox
cbComorphism Signal ComboBox (IO ())
forall self. ComboBoxClass self => Signal self (IO ())
changed
    (IO () -> IO (ConnectId ComboBox))
-> IO () -> IO (ConnectId ComboBox)
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore Finder -> ComboBox -> IO ()
setSelectedComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism

  -- setup view selection actions
  let update :: IO ()
update = do
        Maybe (Node, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Node, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Node, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
        TreeView
-> ListStore Finder -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism TreeView
trvFinder ListStore Finder
listFinder ComboBox
cbComorphism ConnectId ComboBox
shC
        Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe (Node, Finder) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (Node, Finder)
mf
  TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvFinder IO ()
update

  let upd :: IO ()
upd = TreeView
-> ListStore FNode
-> (Bool -> G_sublogics -> IO ())
-> IO ()
-> IO ()
-> IO ()
updateNodes TreeView
trvGoals ListStore FNode
listGoals
        (\ b :: Bool
b s :: G_sublogics
s -> do
           Label -> [Char] -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ G_sublogics -> [Char]
forall a. Show a => a -> [Char]
show G_sublogics
s
           TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()
updateFinder TreeView
trvFinder ListStore Finder
listFinder Bool
b G_sublogics
s)
        (do
          Label -> [Char] -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblSublogic "No sublogic"
          ListStore Finder -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore Finder
listFinder
          [Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
False
          Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
False)
        ([Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
True IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnCheck Bool
True)

  ConnectId TreeSelection
shN <- TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvGoals Button
btnNodesAll Button
btnNodesNone
    Button
btnNodesInvert IO ()
upd

  -- bindings
  let selectWithAux :: (FNode -> Bool) -> IO b -> IO b
selectWithAux f :: FNode -> Bool
f u :: IO b
u = do
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvGoals
        TreeSelection -> IO ()
forall self. TreeSelectionClass self => self -> IO ()
treeSelectionSelectAll TreeSelection
sel
        [TreePath]
rs <- TreeSelection -> IO [TreePath]
forall self. TreeSelectionClass self => self -> IO [TreePath]
treeSelectionGetSelectedRows TreeSelection
sel
        (TreePath -> IO ()) -> [TreePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ ~p :: TreePath
p@(row :: Node
row : []) -> do
          FNode
fn <- ListStore FNode -> Node -> IO FNode
forall a. ListStore a -> Node -> IO a
listStoreGetValue ListStore FNode
listGoals Node
row
          (if FNode -> Bool
f FNode
fn then TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath else TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionUnselectPath)
            TreeSelection
sel TreePath
p) [TreePath]
rs
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO b
u
      selectWith :: (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith f :: ConsistencyStatus -> Bool
f = (FNode -> Bool) -> IO b -> IO b
forall b. (FNode -> Bool) -> IO b -> IO b
selectWithAux ((FNode -> Bool) -> IO b -> IO b)
-> (FNode -> Bool) -> IO b -> IO b
forall a b. (a -> b) -> a -> b
$ ConsistencyStatus -> Bool
f (ConsistencyStatus -> Bool)
-> (FNode -> ConsistencyStatus) -> FNode -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> ConsistencyStatus
cStatus

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesUnchecked
    (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (ConsistencyStatus -> Bool) -> IO () -> IO ()
forall b. (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith (ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> [Char] -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked "") IO ()
upd
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnNodesTimeout (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ (ConsistencyStatus -> Bool) -> IO () -> IO ()
forall b. (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith (ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> [Char] -> ConsistencyStatus
ConsistencyStatus SType
CSTimeout "") IO ()
upd

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnResults (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar (IO ()) -> [Char] -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Models" ListStore FNode
listGoals []
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnClose (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnStop (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar ThreadId -> IO ThreadId
forall a. MVar a -> IO a
takeMVar MVar ThreadId
threadId IO ThreadId -> (ThreadId -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ThreadId -> IO ()
killThread IO () -> (() -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait

  Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnCheck (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
    [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
False
    Node
timeout <- SpinButton -> IO Node
forall self. SpinButtonClass self => self -> IO Node
spinButtonGetValueAsInt SpinButton
sbTimeout
    Bool
inclThms <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbInclThms
    (updat :: Double -> [Char] -> IO ()
updat, pexit :: IO ()
pexit) <- [Char] -> [Char] -> IO (Double -> [Char] -> IO (), IO ())
progressBar "Checking consistency" "please wait..."
    [(Node, FNode)]
goals' <- TreeView -> ListStore FNode -> IO [(Node, FNode)]
forall a. TreeView -> ListStore a -> IO [(Node, a)]
getSelectedMultiple TreeView
trvGoals ListStore FNode
listGoals
    Maybe (Node, Finder)
mf <- TreeView -> ListStore Finder -> IO (Maybe (Node, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Node, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
    Finder
f <- case Maybe (Node, Finder)
mf of
      Nothing -> [Char] -> IO Finder
forall a. HasCallStack => [Char] -> a
error "Disprove: internal error"
      Just (_, f :: Finder
f) -> Finder -> IO Finder
forall (m :: * -> *) a. Monad m => a -> m a
return Finder
f
    Bool -> IO ()
switch Bool
False
    ThreadId
tid <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
      {- call the check function from GUI.GtkConsistencyChecker.
      first argument means disprove-mode and leads the ConsistencyChecker
      to mark consistent sentences as disproved (since consistent with
      negated sentence) -}
      Bool
-> Bool
-> LibName
-> LibEnv
-> DGraph
-> Finder
-> Node
-> ListStore FNode
-> (Double -> [Char] -> IO ())
-> [(Node, FNode)]
-> IO ()
check Bool
True Bool
inclThms LibName
ln LibEnv
le DGraph
dg Finder
f Node
timeout ListStore FNode
listGoals Double -> [Char] -> IO ()
updat [(Node, FNode)]
goals'
      MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait ()
    MVar ThreadId -> ThreadId -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ThreadId
threadId ThreadId
tid
    IO () -> IO ()
forkIO_ (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
wait
      IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Bool -> IO ()
switch Bool
True
        MVar ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ThreadId
threadId
        MVar (IO ()) -> [Char] -> ListStore FNode -> [FNode] -> IO ()
showModelView MVar (IO ())
mView "Results of disproving" ListStore FNode
listGoals []
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shN
        TreeView -> ListStore FNode -> IO ()
sortNodes TreeView
trvGoals ListStore FNode
listGoals
        ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shN
        IO ()
upd
        [Widget] -> Bool -> IO ()
activate [Widget]
checkWidgets Bool
True
        IO ()
pexit

  {- after window closes a new G_theory is created containing the results.
  only successful disprove attempts are returned; for each one, a new
  BasicProof is created and set to disproved. -}
  Window -> IO () -> IO (ConnectId Window)
forall w. WidgetClass w => w -> IO () -> IO (ConnectId w)
onDestroy Window
window (IO () -> IO (ConnectId Window)) -> IO () -> IO (ConnectId Window)
forall a b. (a -> b) -> a -> b
$ do
    [FNode]
fnodes' <- ListStore FNode -> IO [FNode]
forall a. ListStore a -> IO [a]
listStoreToList ListStore FNode
listGoals
    Maybe (Node, Finder)
maybe_F <- TreeView -> ListStore Finder -> IO (Maybe (Node, Finder))
forall a. TreeView -> ListStore a -> IO (Maybe (Node, a))
getSelectedSingle TreeView
trvFinder ListStore Finder
listFinder
    case Maybe (Node, Finder)
maybe_F of
      Just (_, f :: Finder
f) -> case G_theory
g_th of
        G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig i1 :: SigId
i1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> let
          sens' :: ThSens sentence (AnyComorphism, BasicProof)
sens' = (FNode
 -> ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> [FNode]
-> ThSens sentence (AnyComorphism, BasicProof)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ fg :: FNode
fg t :: ThSens sentence (AnyComorphism, BasicProof)
t -> if (ConsistencyStatus -> SType
sType (ConsistencyStatus -> SType)
-> (FNode -> ConsistencyStatus) -> FNode -> SType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FNode -> ConsistencyStatus
cStatus) FNode
fg SType -> SType -> Bool
forall a. Eq a => a -> a -> Bool
== SType
CSInconsistent
            then let
              n' :: [Char]
n' = FNode -> [Char]
name FNode
fg
              es :: ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
es = ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> [Char]
-> ThSens sentence (AnyComorphism, BasicProof)
-> ElemWOrd
     (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char]
-> ElemWOrd
     (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall a. HasCallStack => [Char] -> a
error
                   "GtkDisprove.showDisproveWindow") [Char]
n' ThSens sentence (AnyComorphism, BasicProof)
t
              s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s = ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
es
              ps :: ProofStatus proof_tree
ps = [Char] -> [Char] -> proof_tree -> ProofStatus proof_tree
forall pt. Ord pt => [Char] -> [Char] -> pt -> ProofStatus pt
openProofStatus [Char]
n' (Finder -> [Char]
fName Finder
f) (lid -> proof_tree
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> proof_tree
empty_proof_tree lid
lid)
              bp :: BasicProof
bp = lid -> ProofStatus proof_tree -> BasicProof
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ProofStatus proof_tree -> BasicProof
BasicProof lid
lid ProofStatus proof_tree
ps { goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved }
              c :: AnyComorphism
c = Finder -> [AnyComorphism]
comorphism Finder
f [AnyComorphism] -> Node -> AnyComorphism
forall a. [a] -> Node -> a
!! Finder -> Node
selected Finder
f
              s' :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s' = SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s { senAttr :: ThmStatus (AnyComorphism, BasicProof)
senAttr = [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a. [a] -> ThmStatus a
ThmStatus ([(AnyComorphism, BasicProof)]
 -> ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ (AnyComorphism
c, BasicProof
bp) (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a. a -> [a] -> [a]
: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s } in
              [Char]
-> ElemWOrd
     (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
n' ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
es { ele :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
OMap.ele = SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s' } ThSens sentence (AnyComorphism, BasicProof)
t
            else ThSens sentence (AnyComorphism, BasicProof)
t ) ThSens sentence (AnyComorphism, BasicProof)
sens [FNode]
fnodes'
          in MVar (Result G_theory) -> Result G_theory -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (Result G_theory)
res (Result G_theory -> IO ()) -> Result G_theory -> IO ()
forall a b. (a -> b) -> a -> b
$ G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sig SigId
i1 ThSens sentence (AnyComorphism, BasicProof)
sens' ThId
startThId)
      _ -> MVar (Result G_theory) -> Result G_theory -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (Result G_theory)
res (Result G_theory -> IO ()) -> Result G_theory -> IO ()
forall a b. (a -> b) -> a -> b
$ G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return G_theory
g_th

  (ConsistencyStatus -> Bool) -> IO () -> IO ()
forall b. (ConsistencyStatus -> Bool) -> IO b -> IO b
selectWith (ConsistencyStatus -> ConsistencyStatus -> Bool
forall a. Eq a => a -> a -> Bool
== SType -> [Char] -> ConsistencyStatus
ConsistencyStatus SType
CSUnchecked "") IO ()
upd
  Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window