{- |
Module      :  ./GUI/GtkProverGUI.hs
Description :  Gtk GUI for the prover
Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

This module provides a GUI for the prover.
-}

module GUI.GtkProverGUI ( showProverGUI ) where

import Graphics.UI.Gtk

import GUI.GtkUtils
import qualified GUI.Glade.ProverGUI as ProverGUI
import GUI.HTkProofDetails -- not implemented in Gtk

import Common.AS_Annotation as AS_Anno
import qualified Common.Doc as Pretty
import Common.Result
import qualified Common.OrderedMap as OMap
import Common.ExtSign
import Common.GtkGoal
import Common.Utils

import Control.Concurrent.MVar

import Proofs.AbstractState

import Logic.Comorphism
import Logic.Logic
import Logic.Prover

import qualified Comorphisms.KnownProvers as KnownProvers

import Static.GTheory

import qualified Data.Map as Map
import Data.List
import Data.Maybe (fromMaybe, isJust )

data GProver = GProver
  { GProver -> String
pName :: String
  , GProver -> [AnyComorphism]
comorphism :: [AnyComorphism]
  , GProver -> Int
selected :: Int }

-- ProverGUI

-- | Displays the consistency checker window
showProverGUI :: ProofActions -- ^ record of possible GUI actions
  -> String -- ^ theory name
  -> String -- ^ warning information
  -> G_theory -- ^ theory
  -> KnownProvers.KnownProversMap -- ^ map of known provers
  -> [(G_prover, AnyComorphism)]
     -- ^ list of suitable comorphisms to provers for sublogic of G_theory
  -> IO (Result G_theory)
showProverGUI :: ProofActions
-> String
-> String
-> G_theory
-> KnownProversMap
-> [(G_prover, AnyComorphism)]
-> IO (Result G_theory)
showProverGUI prGuiAcs :: ProofActions
prGuiAcs thName :: String
thName warn :: String
warn th :: G_theory
th knownProvers :: KnownProversMap
knownProvers comorphList :: [(G_prover, AnyComorphism)]
comorphList = do
  ProofState
initState <- ProofActions -> ProofState -> IO ProofState
recalculateSublogicF ProofActions
prGuiAcs
    (String -> G_theory -> KnownProversMap -> ProofState
initialState String
thName G_theory
th KnownProversMap
knownProvers)
    { comorphismsToProvers :: [(G_prover, AnyComorphism)]
comorphismsToProvers = [(G_prover, AnyComorphism)]
comorphList }
  MVar ProofState
state <- ProofState -> IO (MVar ProofState)
forall a. a -> IO (MVar a)
newMVar ProofState
initState
  MVar ()
wait <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
  IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Builder
builder <- (String, String) -> IO Builder
getGTKBuilder (String, String)
ProverGUI.get
    -- get objects
    Window
window <- Builder -> (GObject -> Window) -> String -> 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 "ProverGUI"
    -- buttons at buttom
    Button
btnShowTheory <- Builder -> (GObject -> Button) -> String -> 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 "btnShowTheory"
    Button
btnShowSelectedTheory <- Builder -> (GObject -> Button) -> String -> 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 "btnShowSelected"
    Button
btnClose <- Builder -> (GObject -> Button) -> String -> 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"
    -- goals view
    TreeView
trvGoals <- Builder -> (GObject -> TreeView) -> String -> 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 "trvGoals"
    Button
btnGoalsAll <- Builder -> (GObject -> Button) -> String -> 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 "btnGoalsAll"
    Button
btnGoalsNone <- Builder -> (GObject -> Button) -> String -> 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 "btnGoalsNone"
    Button
btnGoalsInvert <- Builder -> (GObject -> Button) -> String -> 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 "btnGoalsInvert"
    Button
btnGoalsSelectOpen <- Builder -> (GObject -> Button) -> String -> 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 "btnGoalsSelectOpen"
    -- axioms view
    TreeView
trvAxioms <- Builder -> (GObject -> TreeView) -> String -> 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 "trvAxioms"
    Button
btnAxiomsAll <- Builder -> (GObject -> Button) -> String -> 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 "btnAxiomsAll"
    Button
btnAxiomsNone <- Builder -> (GObject -> Button) -> String -> 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 "btnAxiomsNone"
    Button
btnAxiomsInvert <- Builder -> (GObject -> Button) -> String -> 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 "btnAxiomsInvert"
    Button
btnAxiomsFormer <- Builder -> (GObject -> Button) -> String -> 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 "btnAxiomsFormer"
    -- theorems view
    TreeView
trvTheorems <- Builder -> (GObject -> TreeView) -> String -> 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 "trvTheorems"
    Button
btnTheoremsAll <- Builder -> (GObject -> Button) -> String -> 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 "btnTheoremsAll"
    Button
btnTheoremsNone <- Builder -> (GObject -> Button) -> String -> 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 "btnTheoremsNone"
    Button
btnTheoremsInvert <- Builder -> (GObject -> Button) -> String -> 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 "btnTheoremsInvert"
    -- status
    Button
btnDisplay <- Builder -> (GObject -> Button) -> String -> 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 "btnDisplay"
    Button
btnProofDetails <- Builder -> (GObject -> Button) -> String -> 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 "btnProofDetails"
    Button
btnProve <- Builder -> (GObject -> Button) -> String -> 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 "btnProve"
    ComboBox
cbComorphism <- Builder -> (GObject -> ComboBox) -> String -> 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) -> String -> 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"
    -- prover
    TreeView
trvProvers <- Builder -> (GObject -> TreeView) -> String -> 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 "trvProvers"

    Window -> String -> IO ()
forall self string.
(WindowClass self, GlibString string) =>
self -> string -> IO ()
windowSetTitle Window
window (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Prove: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName

    -- set list data
    ListStore GProver
listProvers <- TreeView
-> (GProver -> String) -> [GProver] -> IO (ListStore GProver)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvProvers GProver -> String
pName []
    ListStore Goal
listGoals <- TreeView -> (Goal -> String) -> [Goal] -> IO (ListStore Goal)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvGoals Goal -> String
showGoal ([Goal] -> IO (ListStore Goal)) -> [Goal] -> IO (ListStore Goal)
forall a b. (a -> b) -> a -> b
$ ProofState -> [Goal]
toGoals ProofState
initState
    ListStore String
listAxioms <- TreeView -> (String -> String) -> [String] -> IO (ListStore String)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvAxioms String -> String
forall a. a -> a
id ([String] -> IO (ListStore String))
-> [String] -> IO (ListStore String)
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
toAxioms ProofState
initState
    ListStore String
listTheorems <- TreeView -> (String -> String) -> [String] -> IO (ListStore String)
forall a. TreeView -> (a -> String) -> [a] -> IO (ListStore a)
setListData TreeView
trvTheorems String -> String
forall a. a -> a
id ([String] -> IO (ListStore String))
-> [String] -> IO (ListStore String)
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
selectedGoals ProofState
initState

    -- 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
$ MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state
      ((ProofState -> IO ProofState) -> IO ())
-> (ProofState -> IO ProofState) -> IO ()
forall a b. (a -> b) -> a -> b
$ TreeView
-> ListStore GProver -> ComboBox -> ProofState -> IO ProofState
setSelectedComorphism TreeView
trvProvers ListStore GProver
listProvers ComboBox
cbComorphism

    -- setup provers list
    ConnectId TreeSelection
shP <- TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvProvers (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state
      ((ProofState -> IO ProofState) -> IO ())
-> (ProofState -> IO ProofState) -> IO ()
forall a b. (a -> b) -> a -> b
$ TreeView
-> ListStore GProver
-> ComboBox
-> ConnectId ComboBox
-> ProofState
-> IO ProofState
setSelectedProver TreeView
trvProvers ListStore GProver
listProvers ComboBox
cbComorphism ConnectId ComboBox
shC

    -- setup axioms list
    ConnectId TreeSelection
shA <- TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvAxioms Button
btnAxiomsAll Button
btnAxiomsNone
      Button
btnAxiomsInvert (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state
      ((ProofState -> IO ProofState) -> IO ())
-> (ProofState -> IO ProofState) -> IO ()
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore String -> ProofState -> IO ProofState
setSelectedAxioms TreeView
trvAxioms ListStore String
listAxioms

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnAxiomsFormer (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shA
      TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvAxioms
      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 :: Int
row : []) -> do
        String
i <- ListStore String -> Int -> IO String
forall a. ListStore a -> Int -> IO a
listStoreGetValue ListStore String
listAxioms Int
row
        (if ProofState -> String -> Bool
wasATheorem ProofState
initState (String -> String
stripPrefixAxiom String
i)
          then TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionUnselectPath else TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath) TreeSelection
sel TreePath
p) [TreePath]
rs
      ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shA
      MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state ((ProofState -> IO ProofState) -> IO ())
-> (ProofState -> IO ProofState) -> IO ()
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore String -> ProofState -> IO ProofState
setSelectedAxioms TreeView
trvAxioms ListStore String
listAxioms

   -- setup theorems list
    TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvTheorems Button
btnTheoremsAll Button
btnTheoremsNone
      Button
btnTheoremsInvert (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state
      ((ProofState -> IO ProofState) -> IO ())
-> (ProofState -> IO ProofState) -> IO ()
forall a b. (a -> b) -> a -> b
$ TreeView -> ListStore String -> ProofState -> IO ProofState
setSelectedTheorems TreeView
trvTheorems ListStore String
listTheorems

    let noProver :: [Widget]
noProver = [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnProve
                   , ComboBox -> Widget
forall o. WidgetClass o => o -> Widget
toWidget ComboBox
cbComorphism
                   , Label -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Label
lblSublogic ]
        noAxiom :: [Widget]
noAxiom = [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnAxiomsAll
                  , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnAxiomsNone
                  , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnAxiomsInvert
                  , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnAxiomsFormer ]
        noTheory :: [Widget]
noTheory = [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnTheoremsAll
                   , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnTheoremsNone
                   , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnTheoremsInvert ]
        noGoal :: [Widget]
noGoal = [ Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnGoalsAll
                 , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnGoalsNone
                 , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnGoalsInvert
                 , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnGoalsSelectOpen ]
        prove :: [Widget]
prove = [Window -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Window
window]
        update :: ProofState -> IO ProofState
update s' :: ProofState
s' = do
          ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shP
          ProofState
s <- TreeView
-> ListStore GProver
-> ComboBox
-> ConnectId ComboBox
-> ProofState
-> IO ProofState
setSelectedProver TreeView
trvProvers ListStore GProver
listProvers ComboBox
cbComorphism ConnectId ComboBox
shC
            (ProofState -> IO ProofState) -> IO ProofState -> IO ProofState
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TreeView -> ListStore GProver -> ProofState -> IO ProofState
updateProver TreeView
trvProvers ListStore GProver
listProvers
            (ProofState -> IO ProofState) -> IO ProofState -> IO ProofState
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Label
-> ProofActions -> KnownProversMap -> ProofState -> IO ProofState
updateSublogic Label
lblSublogic ProofActions
prGuiAcs KnownProversMap
knownProvers
            (ProofState -> IO ProofState) -> IO ProofState -> IO ProofState
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TreeView -> ListStore Goal -> ProofState -> IO ProofState
setSelectedGoals TreeView
trvGoals ListStore Goal
listGoals ProofState
s'
          ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shP
          [Widget] -> Bool -> IO ()
activate [Widget]
noProver
            (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (ProofState -> Maybe String
selectedProver ProofState
s) Bool -> Bool -> Bool
&& Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
selectedGoals ProofState
s))
          ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s
        hasGoals :: Bool
hasGoals = Bool -> Bool
not (Bool -> Bool) -> ([String] -> Bool) -> [String] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
selectedGoals ProofState
initState
    [Widget] -> Bool -> IO ()
activate [Widget]
noGoal Bool
hasGoals
    [Widget] -> Bool -> IO ()
activate [Widget]
noAxiom (Bool -> Bool
not (Bool -> Bool) -> ([String] -> Bool) -> [String] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ProofState -> [String]
includedAxioms ProofState
initState)
    [Widget] -> Bool -> IO ()
activate [Widget]
noTheory Bool
hasGoals

    -- setup goal list
    ConnectId TreeSelection
shG <- TreeView
-> Button
-> Button
-> Button
-> IO ()
-> IO (ConnectId TreeSelection)
setListSelectorMultiple TreeView
trvGoals Button
btnGoalsAll Button
btnGoalsNone
      Button
btnGoalsInvert (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state ProofState -> IO ProofState
update

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnGoalsSelectOpen (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shG
      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 :: Int
row : []) -> do
        Goal
g <- ListStore Goal -> Int -> IO Goal
forall a. ListStore a -> Int -> IO a
listStoreGetValue ListStore Goal
listGoals Int
row
        (if Goal -> GStatus
gStatus Goal
g GStatus -> [GStatus] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [GStatus
GOpen, GStatus
GTimeout]
          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
shG
      MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state ProofState -> IO ProofState
update

    -- button bindings
    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
btnShowTheory (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> G_theory -> IO ()
displayTheoryWithWarning "Theory" String
thName String
warn G_theory
th

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnShowSelectedTheory (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> IO ProofState
forall a. MVar a -> IO a
readMVar MVar ProofState
state IO ProofState -> (ProofState -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      String -> String -> String -> G_theory -> IO ()
displayTheoryWithWarning "Selected Theory" String
thName String
warn (G_theory -> IO ())
-> (ProofState -> G_theory) -> ProofState -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> G_theory
selectedTheory

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnDisplay (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> IO ProofState
forall a. MVar a -> IO a
readMVar MVar ProofState
state IO ProofState -> (ProofState -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProofState -> IO ()
displayGoals

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnProofDetails (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
forkIO_ (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ MVar ProofState -> IO ProofState
forall a. MVar a -> IO a
readMVar MVar ProofState
state IO ProofState -> (ProofState -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProofState -> IO ()
doShowProofDetails

    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnProve (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      MVar ProofState -> (ProofState -> IO ProofState) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar ProofState
state ProofState -> IO ProofState
update
      ProofState
s' <- MVar ProofState -> IO ProofState
forall a. MVar a -> IO a
takeMVar MVar ProofState
state
      [Widget] -> Bool -> IO ()
activate [Widget]
prove Bool
False
      IO (Result ProofState) -> (Result ProofState -> IO ()) -> IO ()
forall a. IO a -> (a -> IO ()) -> IO ()
forkIOWithPostProcessing (ProofActions -> ProofState -> IO (Result ProofState)
proveF ProofActions
prGuiAcs ProofState
s')
        ((Result ProofState -> IO ()) -> IO ())
-> (Result ProofState -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ (Result ds :: [Diagnosis]
ds ms :: Maybe ProofState
ms) -> do
            ProofState
s <- case Maybe ProofState
ms of
              Nothing -> String -> String -> IO ()
errorDialog "Error" (Int -> [Diagnosis] -> String
showRelDiags 2 [Diagnosis]
ds) IO () -> IO ProofState -> IO ProofState
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s'
              Just res :: ProofState
res -> ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
res
            [Widget] -> Bool -> IO ()
activate [Widget]
prove Bool
True
            ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId TreeSelection
shG
            TreeView -> ListStore Goal -> ProofState -> IO ()
updateGoals TreeView
trvGoals ListStore Goal
listGoals ProofState
s
            ConnectId TreeSelection -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId TreeSelection
shG
            MVar ProofState -> ProofState -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ProofState
state (ProofState -> IO ()) -> IO ProofState -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProofState -> IO ProofState
update ProofState
s { proverRunning :: Bool
proverRunning = Bool
False
                                       , accDiags :: [Diagnosis]
accDiags = ProofState -> [Diagnosis]
accDiags ProofState
s [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds }

    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
$ MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
wait ()

    TreeView -> IO ()
selectAllRows TreeView
trvTheorems
    TreeView -> IO ()
selectAllRows TreeView
trvAxioms
    TreeView -> IO ()
selectAllRows TreeView
trvGoals

    Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

  ()
_ <- MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
wait
  ProofState
s <- MVar ProofState -> IO ProofState
forall a. MVar a -> IO a
takeMVar MVar ProofState
state
  Result G_theory -> IO (Result G_theory)
forall (m :: * -> *) a. Monad m => a -> m a
return Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result
    { diags :: [Diagnosis]
diags = ProofState -> [Diagnosis]
accDiags ProofState
s
    , maybeResult :: Maybe G_theory
maybeResult = 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
$ ProofState -> G_theory
currentTheory ProofState
s }

-- | Called whenever the button "Display" is clicked.
displayGoals :: ProofState -> IO ()
displayGoals :: ProofState -> IO ()
displayGoals s :: ProofState
s = case ProofState -> G_theory
currentTheory ProofState
s of
  G_theory lid1 :: lid
lid1 _ (ExtSign sig1 :: sign
sig1 _) _ sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _ -> do
    let thName :: String
thName = ProofState -> String
theoryName ProofState
s
        goalsText :: String
goalsText = Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (ThSens sentence (AnyComorphism, BasicProof) -> Doc)
-> ThSens sentence (AnyComorphism, BasicProof)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
Pretty.vsep
          ([Doc] -> Doc)
-> (ThSens sentence (AnyComorphism, BasicProof) -> [Doc])
-> ThSens sentence (AnyComorphism, BasicProof)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SenAttr sentence String -> Doc)
-> [SenAttr sentence String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> SenAttr sentence String -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid
lid1 (SenAttr sentence String -> Doc)
-> (SenAttr sentence String -> SenAttr sentence String)
-> SenAttr sentence String
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (sentence -> sentence)
-> SenAttr sentence String -> SenAttr sentence String
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed (lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lid1 sign
sig1))
          ([SenAttr sentence String] -> [Doc])
-> (ThSens sentence (AnyComorphism, BasicProof)
    -> [SenAttr sentence String])
-> ThSens sentence (AnyComorphism, BasicProof)
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThSens sentence (AnyComorphism, BasicProof)
-> [SenAttr sentence String]
forall a b. ThSens a b -> [Named a]
toNamedList (ThSens sentence (AnyComorphism, BasicProof) -> String)
-> ThSens sentence (AnyComorphism, BasicProof) -> String
forall a b. (a -> b) -> a -> b
$ [String]
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k e. Ord k => [k] -> Map k e -> Map k e
filterMapWithList (ProofState -> [String]
selectedGoals ProofState
s) ThSens sentence (AnyComorphism, BasicProof)
sens1
    String -> String -> Maybe String -> IO ()
textView ("Selected Goals from Theory " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName) String
goalsText
             (Maybe String -> IO ()) -> Maybe String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-goals.txt")

updateComorphism :: TreeView -> ListStore GProver -> ComboBox
                 -> ConnectId ComboBox -> IO ()
updateComorphism :: TreeView
-> ListStore GProver -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism view :: TreeView
view list :: ListStore GProver
list cbComorphism :: ComboBox
cbComorphism sh :: ConnectId ComboBox
sh = do
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalBlock ConnectId ComboBox
sh
  ListStore ComboBoxText
model <- ComboBox -> IO (ListStore ComboBoxText)
forall self.
ComboBoxClass self =>
self -> IO (ListStore ComboBoxText)
comboBoxGetModelText ComboBox
cbComorphism
  ListStore ComboBoxText -> IO ()
forall a. ListStore a -> IO ()
listStoreClear ListStore ComboBoxText
model
  Maybe (Int, GProver)
mfinder <- TreeView -> ListStore GProver -> IO (Maybe (Int, GProver))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore GProver
list
  case Maybe (Int, GProver)
mfinder of
    Just (_, f :: GProver
f) -> do
      (ComboBoxText -> IO Int) -> [ComboBoxText] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ComboBox -> ComboBoxText -> IO Int
forall self. ComboBoxClass self => self -> ComboBoxText -> IO Int
comboBoxAppendText ComboBox
cbComorphism) ([ComboBoxText] -> IO ()) -> [ComboBoxText] -> IO ()
forall a b. (a -> b) -> a -> b
$ GProver -> [ComboBoxText]
expand GProver
f
      ComboBox -> Int -> IO ()
forall self. ComboBoxClass self => self -> Int -> IO ()
comboBoxSetActive ComboBox
cbComorphism (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$ GProver -> Int
selected GProver
f
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  ConnectId ComboBox -> IO ()
forall obj. GObjectClass obj => ConnectId obj -> IO ()
signalUnblock ConnectId ComboBox
sh

expand :: GProver -> [ComboBoxText]
expand :: GProver -> [ComboBoxText]
expand = [AnyComorphism] -> [ComboBoxText]
forall a. Show a => [a] -> [ComboBoxText]
toComboBoxText ([AnyComorphism] -> [ComboBoxText])
-> (GProver -> [AnyComorphism]) -> GProver -> [ComboBoxText]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GProver -> [AnyComorphism]
comorphism

setSelectedComorphism :: TreeView -> ListStore GProver -> ComboBox -> ProofState
  -> IO ProofState
setSelectedComorphism :: TreeView
-> ListStore GProver -> ComboBox -> ProofState -> IO ProofState
setSelectedComorphism view :: TreeView
view list :: ListStore GProver
list cbComorphism :: ComboBox
cbComorphism s :: ProofState
s = do
  Maybe (Int, GProver)
mfinder <- TreeView -> ListStore GProver -> IO (Maybe (Int, GProver))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
view ListStore GProver
list
  case Maybe (Int, GProver)
mfinder of
    Just (i :: Int
i, f :: GProver
f) -> do
      Int
sel <- ComboBox -> IO Int
forall self. ComboBoxClass self => self -> IO Int
comboBoxGetActive ComboBox
cbComorphism
      let nf :: GProver
nf = GProver
f { selected :: Int
selected = Int
sel }
      ListStore GProver -> Int -> GProver -> IO ()
forall a. ListStore a -> Int -> a -> IO ()
listStoreSetValue ListStore GProver
list Int
i GProver
nf
      ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> IO ProofState) -> ProofState -> IO ProofState
forall a b. (a -> b) -> a -> b
$ GProver -> ProofState -> ProofState
setGProver GProver
nf ProofState
s
    Nothing -> ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s

setGProver :: GProver -> ProofState -> ProofState
setGProver :: GProver -> ProofState -> ProofState
setGProver f :: GProver
f s :: ProofState
s =
  let pn :: String
pn = GProver -> String
pName GProver
f
      c :: AnyComorphism
c = GProver -> [AnyComorphism]
comorphism GProver
f [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! GProver -> Int
selected GProver
f
  in ProofState
s
  { selectedProver :: Maybe String
selectedProver = String -> Maybe String
forall a. a -> Maybe a
Just String
pn
  , proversMap :: KnownProversMap
proversMap = String -> [AnyComorphism] -> KnownProversMap -> KnownProversMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
pn [AnyComorphism
c] (KnownProversMap -> KnownProversMap)
-> KnownProversMap -> KnownProversMap
forall a b. (a -> b) -> a -> b
$ ProofState -> KnownProversMap
proversMap ProofState
s}

updateSublogic :: Label -> ProofActions
               -> KnownProvers.KnownProversMap -> ProofState
               -> IO ProofState
updateSublogic :: Label
-> ProofActions -> KnownProversMap -> ProofState -> IO ProofState
updateSublogic lbl :: Label
lbl prGuiAcs :: ProofActions
prGuiAcs knownProvers :: KnownProversMap
knownProvers s' :: ProofState
s' = do
  ProofState
s <- ProofActions -> ProofState -> IO ProofState
recalculateSublogicF ProofActions
prGuiAcs ProofState
s'
    { proversMap :: KnownProversMap
proversMap = ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> KnownProversMap -> KnownProversMap -> KnownProversMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++) (ProofState -> KnownProversMap
proversMap ProofState
s') KnownProversMap
knownProvers }
  Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lbl (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ G_sublogics -> String
forall a. Show a => a -> String
show (G_sublogics -> String) -> G_sublogics -> String
forall a b. (a -> b) -> a -> b
$ ProofState -> G_sublogics
sublogicOfTheory ProofState
s
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s

updateProver :: TreeView -> ListStore GProver -> ProofState
             -> IO ProofState
updateProver :: TreeView -> ListStore GProver -> ProofState -> IO ProofState
updateProver trvProvers :: TreeView
trvProvers listProvers :: ListStore GProver
listProvers s :: ProofState
s = do
  let new :: [GProver]
new = ProofState -> [GProver]
toProvers ProofState
s
  [GProver]
old <- ListStore GProver -> IO [GProver]
forall a. ListStore a -> IO [a]
listStoreToList ListStore GProver
listProvers
  let prvs :: [GProver]
prvs = (GProver -> GProver) -> [GProver] -> [GProver]
forall a b. (a -> b) -> [a] -> [b]
map (\ p :: GProver
p -> case (GProver -> Bool) -> [GProver] -> Maybe GProver
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((GProver -> String
pName GProver
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (GProver -> String) -> GProver -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GProver -> String
pName) [GProver]
old of
          Nothing -> GProver
p
          Just p' :: GProver
p' -> let oldC :: AnyComorphism
oldC = GProver -> [AnyComorphism]
comorphism GProver
p' [AnyComorphism] -> Int -> AnyComorphism
forall a. [a] -> Int -> a
!! GProver -> Int
selected GProver
p' in
            GProver
p { selected :: Int
selected = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> [AnyComorphism] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex AnyComorphism
oldC ([AnyComorphism] -> Maybe Int) -> [AnyComorphism] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ GProver -> [AnyComorphism]
comorphism GProver
p }
        ) [GProver]
new
  ListStore GProver -> [GProver] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore GProver
listProvers [GProver]
prvs
  case ProofState -> Maybe String
selectedProver ProofState
s of
    Just p :: String
p -> case (GProver -> Bool) -> [GProver] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((String
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (GProver -> String) -> GProver -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GProver -> String
pName) [GProver]
prvs of
      Just i :: Int
i -> do
        TreeSelection
sel <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvProvers
        TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
sel [Int
i]
      Nothing -> TreeView -> IO ()
selectFirst TreeView
trvProvers
    Nothing -> TreeView -> IO ()
selectFirst TreeView
trvProvers
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s

updateGoals :: TreeView -> ListStore Goal -> ProofState -> IO ()
updateGoals :: TreeView -> ListStore Goal -> ProofState -> IO ()
updateGoals trvGoals :: TreeView
trvGoals listGoals :: ListStore Goal
listGoals s :: ProofState
s = do
  let ng :: [Goal]
ng = ProofState -> [Goal]
toGoals ProofState
s
  [(Int, Goal)]
sel <- TreeView -> ListStore Goal -> IO [(Int, Goal)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvGoals ListStore Goal
listGoals
  ListStore Goal -> [Goal] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore Goal
listGoals [Goal]
ng
  TreeSelection
selector <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvGoals

  ((Int, Goal) -> IO ()) -> [(Int, Goal)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_, Goal { gName :: Goal -> String
gName = String
n }) -> TreeSelection -> TreePath -> IO ()
forall self. TreeSelectionClass self => self -> TreePath -> IO ()
treeSelectionSelectPath TreeSelection
selector
      [Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error "Goal not found!") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ (Goal -> Bool) -> [Goal] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (Goal -> String) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> String
gName) [Goal]
ng]
    ) [(Int, Goal)]
sel

setSelectedGoals :: TreeView -> ListStore Goal -> ProofState
                 -> IO ProofState
setSelectedGoals :: TreeView -> ListStore Goal -> ProofState -> IO ProofState
setSelectedGoals trvGoals :: TreeView
trvGoals listGoals :: ListStore Goal
listGoals s :: ProofState
s = do
  [(Int, Goal)]
goals <- TreeView -> ListStore Goal -> IO [(Int, Goal)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
trvGoals ListStore Goal
listGoals
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s { selectedGoals :: [String]
selectedGoals = ((Int, Goal) -> String) -> [(Int, Goal)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Goal -> String
gName (Goal -> String) -> ((Int, Goal) -> Goal) -> (Int, Goal) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Goal) -> Goal
forall a b. (a, b) -> b
snd) [(Int, Goal)]
goals }

setSelectedAxioms :: TreeView -> ListStore String -> ProofState
                  -> IO ProofState
setSelectedAxioms :: TreeView -> ListStore String -> ProofState -> IO ProofState
setSelectedAxioms axs :: TreeView
axs listAxs :: ListStore String
listAxs s :: ProofState
s = do
  [(Int, String)]
axioms <- TreeView -> ListStore String -> IO [(Int, String)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
axs ListStore String
listAxs
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s { includedAxioms :: [String]
includedAxioms = ((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
stripPrefixAxiom (String -> String)
-> ((Int, String) -> String) -> (Int, String) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, String) -> String
forall a b. (a, b) -> b
snd) [(Int, String)]
axioms }

setSelectedTheorems :: TreeView -> ListStore String -> ProofState
                    -> IO ProofState
setSelectedTheorems :: TreeView -> ListStore String -> ProofState -> IO ProofState
setSelectedTheorems ths :: TreeView
ths listThs :: ListStore String
listThs s :: ProofState
s = do
  [(Int, String)]
theorems <- TreeView -> ListStore String -> IO [(Int, String)]
forall a. TreeView -> ListStore a -> IO [(Int, a)]
getSelectedMultiple TreeView
ths ListStore String
listThs
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return ProofState
s { includedTheorems :: [String]
includedTheorems = ((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> String
forall a b. (a, b) -> b
snd [(Int, String)]
theorems }

stripPrefixAxiom :: String -> String
stripPrefixAxiom :: String -> String
stripPrefixAxiom a :: String
a = String -> String -> String
tryToStripPrefix "(Th) " String
a

-- | Called whenever a prover is selected from the "Pick Theorem Prover" list.
setSelectedProver :: TreeView -> ListStore GProver -> ComboBox
                  -> ConnectId ComboBox -> ProofState
                  -> IO ProofState
setSelectedProver :: TreeView
-> ListStore GProver
-> ComboBox
-> ConnectId ComboBox
-> ProofState
-> IO ProofState
setSelectedProver trvProvers :: TreeView
trvProvers listProvers :: ListStore GProver
listProvers cbComorphism :: ComboBox
cbComorphism shC :: ConnectId ComboBox
shC s :: ProofState
s = do
  Maybe (Int, GProver)
mprover <- TreeView -> ListStore GProver -> IO (Maybe (Int, GProver))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvProvers ListStore GProver
listProvers
  TreeView
-> ListStore GProver -> ComboBox -> ConnectId ComboBox -> IO ()
updateComorphism TreeView
trvProvers ListStore GProver
listProvers ComboBox
cbComorphism ConnectId ComboBox
shC
  ProofState -> IO ProofState
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> IO ProofState) -> ProofState -> IO ProofState
forall a b. (a -> b) -> a -> b
$ case Maybe (Int, GProver)
mprover of
    Nothing -> ProofState
s { selectedProver :: Maybe String
selectedProver = Maybe String
forall a. Maybe a
Nothing }
    Just (_, gp :: GProver
gp) -> GProver -> ProofState -> ProofState
setGProver GProver
gp ProofState
s

wasATheorem :: ProofState -> String -> Bool
wasATheorem :: ProofState -> String -> Bool
wasATheorem st :: ProofState
st i :: String
i = case ProofState -> G_theory
currentTheory ProofState
st of
   G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> Bool
-> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
    -> Bool)
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem (Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> Bool)
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> Bool
forall a b. (a -> b) -> a -> b
$ String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup String
i ThSens sentence (AnyComorphism, BasicProof)
sens

toGoals :: ProofState -> [Goal]
toGoals :: ProofState -> [Goal]
toGoals = [Goal] -> [Goal]
forall a. Ord a => [a] -> [a]
sort ([Goal] -> [Goal])
-> (ProofState -> [Goal]) -> ProofState -> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Maybe BasicProof) -> Goal)
-> [(String, Maybe BasicProof)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (String, Maybe BasicProof) -> Goal
toGtkGoal ([(String, Maybe BasicProof)] -> [Goal])
-> (ProofState -> [(String, Maybe BasicProof)])
-> ProofState
-> [Goal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> [(String, Maybe BasicProof)]
getGoals

toProvers :: ProofState -> [GProver]
toProvers :: ProofState -> [GProver]
toProvers = Map String GProver -> [GProver]
forall k a. Map k a -> [a]
Map.elems (Map String GProver -> [GProver])
-> (ProofState -> Map String GProver) -> ProofState -> [GProver]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((G_prover, AnyComorphism)
 -> Map String GProver -> Map String GProver)
-> Map String GProver
-> [(G_prover, AnyComorphism)]
-> Map String GProver
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (p' :: G_prover
p', c :: AnyComorphism
c) m :: Map String GProver
m ->
    let n :: String
n = G_prover -> String
getProverName G_prover
p'
        p :: GProver
p = GProver -> String -> Map String GProver -> GProver
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> [AnyComorphism] -> Int -> GProver
GProver String
n [] 0) String
n Map String GProver
m in
    String -> GProver -> Map String GProver -> Map String GProver
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
n (GProver
p { comorphism :: [AnyComorphism]
comorphism = AnyComorphism
c AnyComorphism -> [AnyComorphism] -> [AnyComorphism]
forall a. a -> [a] -> [a]
: GProver -> [AnyComorphism]
comorphism GProver
p}) Map String GProver
m
  ) Map String GProver
forall k a. Map k a
Map.empty ([(G_prover, AnyComorphism)] -> Map String GProver)
-> (ProofState -> [(G_prover, AnyComorphism)])
-> ProofState
-> Map String GProver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofState -> [(G_prover, AnyComorphism)]
comorphismsToProvers