{- |
Module      :  ./GUI/GtkGenericATP.hs
Description :  Gtk Generic Prover GUI.
Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

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

Generic Gtk GUI for automatic theorem provers.
-}

module GUI.GtkGenericATP ( genericATPgui ) where

import Graphics.UI.Gtk

import GUI.GtkUtils
import qualified GUI.Glade.GenericATP as GenericATP

import Interfaces.GenericATPState

import Control.Concurrent (forkIO, killThread, yield)
import Control.Concurrent.MVar
import Control.Monad (unless, when)
import qualified Control.Monad.Fail as Fail

import Common.AS_Annotation as AS_Anno
import Common.GtkGoal
import Common.Result
import Common.Utils (getEnvSave, readMaybe)

import Proofs.BatchProcessing

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

import Logic.Prover

genericATPgui :: (Show sentence, Ord proof_tree, Ord sentence)
              => ATPFunctions sign sentence mor proof_tree pst
              -- ^ prover specific functions
              -> Bool -- ^ prover supports extra options
              -> String -- ^ prover name
              -> String -- ^ theory name
              -> Theory sign sentence proof_tree {- ^ theory consisting of a
                 signature and a list of Named sentence -}
              -> [FreeDefMorphism sentence mor] -- ^ freeness constraints
              -> proof_tree -- ^ initial empty proof_tree
              -> IO [ProofStatus proof_tree] -- ^ proof status for each goal
genericATPgui :: ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui atpFun :: ATPFunctions sign sentence mor proof_tree pst
atpFun hasEOptions :: Bool
hasEOptions prName :: String
prName thName :: String
thName th :: Theory sign sentence proof_tree
th freedefs :: [FreeDefMorphism sentence mor]
freedefs pt :: proof_tree
pt = do
  MVar (Maybe [ProofStatus proof_tree])
result <- IO (MVar (Maybe [ProofStatus proof_tree]))
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)
GenericATP.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 "GenericATP"
    -- buttons at buttom
    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"
    Button
btnHelp <- 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 "btnHelp"
    Button
btnSaveConfig <- 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 "btnSaveConfig"
    -- goal list
    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"
    -- options area
    SpinButton
sbTimeout <- Builder -> (GObject -> SpinButton) -> String -> 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"
    Entry
entryOptions <- Builder -> (GObject -> Entry) -> String -> IO Entry
forall cls string.
(GObjectClass cls, GlibString string) =>
Builder -> (GObject -> cls) -> string -> IO cls
builderGetObject Builder
builder GObject -> Entry
forall obj. GObjectClass obj => obj -> Entry
castToEntry "entryOptions"
    CheckButton
cbIncludeProven <- Builder -> (GObject -> CheckButton) -> String -> 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 "cbIncludeProven"
    CheckButton
cbSaveBatch <- Builder -> (GObject -> CheckButton) -> String -> 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 "cbSaveBatch"
    -- prove buttons
    Button
btnStop <- 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 "btnStop"
    Button
btnProveSelected <- 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 "btnProveSelected"
    Button
btnProveAll <- 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 "btnProveAll"
    -- status and axioms
    Label
lblStatus <- 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 "lblStatus"
    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"
    -- info and save buttons
    Button
btnSaveProblem <- 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 "btnSaveProblem"
    Button
btnShowDetails <- 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 "btnShowDetails"

    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
$ String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName

    let widgets :: [Widget]
widgets = [Entry -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Entry
entryOptions | Bool
hasEOptions] [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
btnShowDetails
                  , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnHelp , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnSaveConfig
                  , SpinButton -> Widget
forall o. WidgetClass o => o -> Widget
toWidget SpinButton
sbTimeout
                  , CheckButton -> Widget
forall o. WidgetClass o => o -> Widget
toWidget CheckButton
cbIncludeProven , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnProveSelected
                  , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnProveSelected, Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnProveAll
                  , Label -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Label
lblStatus , Button -> Widget
forall o. WidgetClass o => o -> Widget
toWidget Button
btnSaveProblem ]
        switch :: Bool -> IO ()
switch = [Widget] -> Bool -> IO ()
activate [Widget]
widgets
        switchAll :: Bool -> IO ()
switchAll b :: Bool
b = do
          [Widget] -> Bool -> IO ()
activate [Widget]
widgets Bool
b
          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

        -- setting up state
        initState :: GenericState sentence proof_tree pst
initState = String
-> InitialProverState sign sentence mor pst
-> (String -> String)
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> GenericState sentence proof_tree pst
forall sentence proof_tree sign morphism pst.
(Ord sentence, Ord proof_tree) =>
String
-> InitialProverState sign sentence morphism pst
-> (String -> String)
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence morphism]
-> proof_tree
-> GenericState sentence proof_tree pst
initialGenericState String
prName (ATPFunctions sign sentence mor proof_tree pst
-> InitialProverState sign sentence mor pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> InitialProverState sign sentence morphism pst
initialProverState ATPFunctions sign sentence mor proof_tree pst
atpFun)
                      (ATPFunctions sign sentence mor proof_tree pst -> String -> String
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> String -> String
atpTransSenName ATPFunctions sign sentence mor proof_tree pst
atpFun) Theory sign sentence proof_tree
th [FreeDefMorphism sentence mor]
freedefs proof_tree
pt
        initGoals :: [Named sentence]
initGoals = GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
initState

    MVar (GenericState sentence proof_tree pst)
stateMVar <- GenericState sentence proof_tree pst
-> IO (MVar (GenericState sentence proof_tree pst))
forall a. a -> IO (MVar a)
newMVar GenericState sentence proof_tree pst
initState
    MVar ThreadId
threadId <- IO (MVar ThreadId)
forall a. IO (MVar a)
newEmptyMVar
    MVar ()
finished <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar

    -- setting up lists
    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
$ GenericState sentence proof_tree pst -> [Goal]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Goal]
toGoals GenericState sentence proof_tree pst
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 []

    -- short update function
    let update' :: GenericState sentence proof_tree pst -> IO ()
update' s :: GenericState sentence proof_tree pst
s = GenericState sentence proof_tree pst
-> TreeView
-> ListStore Goal
-> ListStore String
-> Label
-> SpinButton
-> Entry
-> IO ()
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> TreeView
-> ListStore Goal
-> ListStore String
-> Label
-> SpinButton
-> Entry
-> IO ()
update GenericState sentence proof_tree pst
s TreeView
trvGoals ListStore Goal
listGoals ListStore String
listAxioms Label
lblStatus SpinButton
sbTimeout
                           Entry
entryOptions
        save :: GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save s :: GenericState sentence proof_tree pst
s = GenericState sentence proof_tree pst
-> proof_tree
-> String
-> SpinButton
-> Entry
-> IO (GenericState sentence proof_tree pst)
forall proof_tree sentence pst.
Ord proof_tree =>
GenericState sentence proof_tree pst
-> proof_tree
-> String
-> SpinButton
-> Entry
-> IO (GenericState sentence proof_tree pst)
saveConfigCurrent GenericState sentence proof_tree pst
s proof_tree
pt String
prName SpinButton
sbTimeout Entry
entryOptions

    -- set list selector and action
    TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvAxioms (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    TreeView -> IO () -> IO (ConnectId TreeSelection)
setListSelectorSingle TreeView
trvGoals (IO () -> IO (ConnectId TreeSelection))
-> IO () -> IO (ConnectId TreeSelection)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
s'' <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
takeMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      -- saving options for previous selected goal
      GenericState sentence proof_tree pst
s' <- GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall sentence pst.
GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save GenericState sentence proof_tree pst
s''
      -- setting new selected goal
      Maybe (Int, Goal)
mSelected <- TreeView -> ListStore Goal -> IO (Maybe (Int, Goal))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvGoals ListStore Goal
listGoals
      let s :: GenericState sentence proof_tree pst
s = GenericState sentence proof_tree pst
-> ((Int, Goal) -> GenericState sentence proof_tree pst)
-> Maybe (Int, Goal)
-> GenericState sentence proof_tree pst
forall b a. b -> (a -> b) -> Maybe a -> b
maybe GenericState sentence proof_tree pst
s' (\ (_, Goal { gName :: Goal -> String
gName = String
n }) -> GenericState sentence proof_tree pst
s' { currentGoal :: Maybe String
currentGoal = String -> Maybe String
forall a. a -> Maybe a
Just String
n})
                    Maybe (Int, Goal)
mSelected
      MVar (GenericState sentence proof_tree pst)
-> GenericState sentence proof_tree pst -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (GenericState sentence proof_tree pst)
stateMVar GenericState sentence proof_tree pst
s
      GenericState sentence proof_tree pst -> IO ()
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> IO ()
update' GenericState sentence proof_tree pst
s

    -- setting options
    SpinButton -> Double -> IO ()
forall self. SpinButtonClass self => self -> Double -> IO ()
spinButtonSetValue SpinButton
sbTimeout (Double -> IO ()) -> Double -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
guiDefaultTimeLimit
    Entry -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Entry
entryOptions Bool
hasEOptions
    Button -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive Button
btnStop Bool
False
    Bool
enableSaveBatch <- Bool -> String -> (String -> Maybe Bool) -> IO Bool
forall a. a -> String -> (String -> Maybe a) -> IO a
getEnvSave Bool
False "HETS_ENABLE_BATCH_SAVE" String -> Maybe Bool
forall a. Read a => String -> Maybe a
readMaybe
    CheckButton -> Bool -> IO ()
forall self. WidgetClass self => self -> Bool -> IO ()
widgetSetSensitive CheckButton
cbSaveBatch Bool
enableSaveBatch

    -- setting save button name
    let ext :: String
ext = case FileExtensions -> String
problemOutput (FileExtensions -> String) -> FileExtensions -> String
forall a b. (a -> b) -> a -> b
$ ATPFunctions sign sentence mor proof_tree pst -> FileExtensions
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> FileExtensions
fileExtensions ATPFunctions sign sentence mor proof_tree pst
atpFun of
                e :: String
e@('.' : _) -> String
e
                e :: String
e -> '.' Char -> String -> String
forall a. a -> [a] -> [a]
: String
e
    Button -> String -> IO ()
forall self string.
(ButtonClass self, GlibString string) =>
self -> string -> IO ()
buttonSetLabel Button
btnSaveProblem (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Save " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. [a] -> [a]
tail String
ext String -> String -> String
forall a. [a] -> [a] -> [a]
++ " File"

    -- bindings
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnHelp (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$
      String -> String -> Maybe String -> IO ()
textView (String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Help") (ATPFunctions sign sentence mor proof_tree pst -> String
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst -> String
proverHelpText ATPFunctions sign sentence mor proof_tree pst
atpFun) Maybe String
forall a. Maybe a
Nothing

    -- save config
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnSaveConfig (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
state <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
readMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      -- save actual config
      GenericState sentence proof_tree pst
s <- GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall sentence pst.
GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save GenericState sentence proof_tree pst
state
      let cfgText :: String
cfgText = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Map String (GenericConfig proof_tree) -> Doc
forall proof_tree. Map String (GenericConfig proof_tree) -> Doc
printCfgText (Map String (GenericConfig proof_tree) -> Doc)
-> Map String (GenericConfig proof_tree) -> Doc
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
      String -> String -> Maybe String -> IO ()
textView (String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Configuration for Theory " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName) String
cfgText
               (Maybe String -> IO ()) -> Maybe String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ FileExtensions -> String
theoryConfiguration (ATPFunctions sign sentence mor proof_tree pst -> FileExtensions
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> FileExtensions
fileExtensions ATPFunctions sign sentence mor proof_tree pst
atpFun)

    -- save problem output
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnSaveProblem (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
state <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
readMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      -- save actual config
      GenericState sentence proof_tree pst
s <- GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall sentence pst.
GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save GenericState sentence proof_tree pst
state
      IO () -> (String -> IO ()) -> Maybe String -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (\ g :: String
g -> do
          Bool
inclProven <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbIncludeProven
          let (nGoal :: Named sentence
nGoal, lp' :: pst
lp') = pst
-> GenericState sentence proof_tree pst
-> String
-> Bool
-> (Named sentence, pst)
forall proof_tree pst.
pst
-> GenericState sentence proof_tree pst
-> String
-> Bool
-> (Named sentence, pst)
prepareLP (GenericState sentence proof_tree pst -> pst
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> pst
proverState GenericState sentence proof_tree pst
s) GenericState sentence proof_tree pst
s String
g Bool
inclProven
          String
prob <- ATPFunctions sign sentence mor proof_tree pst
-> pst -> Named sentence -> [String] -> IO String
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> [String] -> IO String
goalOutput ATPFunctions sign sentence mor proof_tree pst
atpFun pst
lp' Named sentence
nGoal ([String] -> IO String) -> [String] -> IO String
forall a b. (a -> b) -> a -> b
$ ATPFunctions sign sentence mor proof_tree pst
-> GenericConfig proof_tree -> [String]
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> GenericConfig proof_tree -> [String]
createProverOptions ATPFunctions sign sentence mor proof_tree pst
atpFun
                    (GenericConfig proof_tree -> [String])
-> GenericConfig proof_tree -> [String]
forall a b. (a -> b) -> a -> b
$ String
-> String
-> proof_tree
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree
getConfig String
prName String
g proof_tree
pt (Map String (GenericConfig proof_tree) -> GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
          String -> String -> Maybe String -> IO ()
textView (String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Problem for Goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g) String
prob
            (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]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: String
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ext)
        ) (Maybe String -> IO ()) -> Maybe String -> IO ()
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst -> Maybe String
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> Maybe String
currentGoal GenericState sentence proof_tree pst
s

    -- show details of selected goal
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnShowDetails (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
s <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
readMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      case GenericState sentence proof_tree pst -> Maybe String
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> Maybe String
currentGoal GenericState sentence proof_tree pst
s of
        Nothing -> String -> String -> IO ()
errorDialog "Error" "Please select a goal first."
        Just g :: String
g -> do
          let res :: Maybe (GenericConfig proof_tree)
res = String
-> Map String (GenericConfig proof_tree)
-> Maybe (GenericConfig proof_tree)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
g (Map String (GenericConfig proof_tree)
 -> Maybe (GenericConfig proof_tree))
-> Map String (GenericConfig proof_tree)
-> Maybe (GenericConfig proof_tree)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
              output :: [String]
output = [String]
-> (GenericConfig proof_tree -> [String])
-> Maybe (GenericConfig proof_tree)
-> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ["This goal hasn't been run through the prover."]
                             GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
resultOutput Maybe (GenericConfig proof_tree)
res
              detailsText :: String
detailsText = (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ('\n' Char -> String -> String
forall a. a -> [a] -> [a]
:) [String]
output
          String -> String -> Maybe String -> IO ()
textView (String
prName String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Output for Goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g)
            (Int -> String -> String
forall a b. a -> b -> b
seq (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
detailsText) String
detailsText) (Maybe String -> IO ()) -> Maybe String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ext

    -- show details of selected goal
    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
$ do
      MVar ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ThreadId
threadId IO (Maybe ThreadId) -> (Maybe ThreadId -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO () -> (ThreadId -> IO ()) -> Maybe ThreadId -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> IO ()
forall a. HasCallStack => String -> a
error "MVar 'tId' not set") ThreadId -> IO ()
killThread
      MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
finished ()

    -- show details of selected goal
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnProveSelected (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
state <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
takeMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      -- save actual config
      GenericState sentence proof_tree pst
s <- GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall sentence pst.
GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save GenericState sentence proof_tree pst
state
      case GenericState sentence proof_tree pst -> Maybe String
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> Maybe String
currentGoal GenericState sentence proof_tree pst
s of
        Nothing -> String -> IO ()
forall a. HasCallStack => String -> a
error "No goal selected."
        Just g :: String
g -> do
          (_, exit :: IO ()
exit) <- String -> String -> IO (String -> IO (), IO ())
pulseBar "Proving" String
g
          Bool
inclProven <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbIncludeProven
          let (nGoal :: Named sentence
nGoal, lp' :: pst
lp') = pst
-> GenericState sentence proof_tree pst
-> String
-> Bool
-> (Named sentence, pst)
forall proof_tree pst.
pst
-> GenericState sentence proof_tree pst
-> String
-> Bool
-> (Named sentence, pst)
prepareLP (GenericState sentence proof_tree pst -> pst
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> pst
proverState GenericState sentence proof_tree pst
s) GenericState sentence proof_tree pst
s String
g Bool
inclProven
              cfg :: Map String (GenericConfig proof_tree)
cfg = GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
          Bool -> IO ()
switch Bool
False
          IO (ATPRetval, GenericConfig proof_tree)
-> ((ATPRetval, GenericConfig proof_tree) -> IO ()) -> IO ()
forall a. IO a -> (a -> IO ()) -> IO ()
forkIOWithPostProcessing
            (ATPFunctions sign sentence mor proof_tree pst
-> RunProver sentence proof_tree pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> RunProver sentence proof_tree pst
runProver ATPFunctions sign sentence mor proof_tree pst
atpFun pst
lp' (String
-> String
-> proof_tree
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall proof_tree.
Ord proof_tree =>
String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfig proof_tree
getConfig String
prName String
g proof_tree
pt Map String (GenericConfig proof_tree)
cfg) Bool
False String
thName Named sentence
nGoal)
            (((ATPRetval, GenericConfig proof_tree) -> IO ()) -> IO ())
-> ((ATPRetval, GenericConfig proof_tree) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ (retval :: ATPRetval
retval, cfg' :: GenericConfig proof_tree
cfg') -> do
              case ATPRetval
retval of
                ATPError m :: String
m -> String -> String -> IO ()
errorDialog "Error" String
m
                _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              let s' :: GenericState sentence proof_tree pst
s' = GenericState sentence proof_tree pst
s { configsMap :: Map String (GenericConfig proof_tree)
configsMap = (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> Map String (GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
forall proof_tree.
Ord proof_tree =>
(GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
adjustOrSetConfig (\ c :: GenericConfig proof_tree
c -> GenericConfig proof_tree
c
                           { timeLimitExceeded :: Bool
timeLimitExceeded = ATPRetval -> Bool
isTimeLimitExceeded ATPRetval
retval
                           , proofStatus :: ProofStatus proof_tree
proofStatus = (GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
cfg')
                             { usedTime :: TimeOfDay
usedTime = GenericConfig proof_tree -> TimeOfDay
forall proof_tree. GenericConfig proof_tree -> TimeOfDay
timeUsed GenericConfig proof_tree
cfg' }
                           , resultOutput :: [String]
resultOutput = GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
resultOutput GenericConfig proof_tree
cfg'
                           , timeUsed :: TimeOfDay
timeUsed = GenericConfig proof_tree -> TimeOfDay
forall proof_tree. GenericConfig proof_tree -> TimeOfDay
timeUsed GenericConfig proof_tree
cfg' }) String
prName String
g proof_tree
pt Map String (GenericConfig proof_tree)
cfg }
              MVar (GenericState sentence proof_tree pst)
-> GenericState sentence proof_tree pst -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (GenericState sentence proof_tree pst)
stateMVar GenericState sentence proof_tree pst
s'
              GenericState sentence proof_tree pst
-> TreeView -> ListStore Goal -> IO ()
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> TreeView -> ListStore Goal -> IO ()
updateGoals GenericState sentence proof_tree pst
s' TreeView
trvGoals ListStore Goal
listGoals
              IO ()
exit
              Bool -> IO ()
switch Bool
True

    -- show details of selected goal
    Button -> IO () -> IO (ConnectId Button)
forall b. ButtonClass b => b -> IO () -> IO (ConnectId b)
onClicked Button
btnProveAll (IO () -> IO (ConnectId Button)) -> IO () -> IO (ConnectId Button)
forall a b. (a -> b) -> a -> b
$ do
      GenericState sentence proof_tree pst
state <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
readMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      -- save actual config
      GenericState sentence proof_tree pst
s <- GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall sentence pst.
GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
save GenericState sentence proof_tree pst
state
      let openGoalsMap :: Map String (GenericConfig proof_tree)
openGoalsMap = Map String (GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
forall proof_tree.
GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
filterOpenGoals (Map String (GenericConfig proof_tree)
 -> Map String (GenericConfig proof_tree))
-> Map String (GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
          numGoals :: Int
numGoals = Map String (GenericConfig proof_tree) -> Int
forall k a. Map k a -> Int
Map.size Map String (GenericConfig proof_tree)
openGoalsMap
      if Map String (GenericConfig proof_tree) -> Bool
forall k a. Map k a -> Bool
Map.null Map String (GenericConfig proof_tree)
openGoalsMap then
        String -> String -> IO ()
infoDialog "No open goals" "No open goals, nothing to do."
        else do
        Int
timeout <- SpinButton -> IO Int
forall self. SpinButtonClass self => self -> IO Int
spinButtonGetValueAsInt SpinButton
sbTimeout
        String
opts' <- Entry -> IO String
forall self string.
(EntryClass self, GlibString string) =>
self -> IO string
entryGetText Entry
entryOptions
        Bool
saveBatch <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbSaveBatch
        Bool
inclProven <- CheckButton -> IO Bool
forall self. ToggleButtonClass self => self -> IO Bool
toggleButtonGetActive CheckButton
cbIncludeProven
        (updat :: Double -> String -> IO ()
updat, exit :: IO ()
exit) <- String -> String -> IO (Double -> String -> IO (), IO ())
progressBar "Proving" "please wait..."
        let firstGoalName :: String
firstGoalName = [String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> Map String (GenericConfig proof_tree) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map String (GenericConfig proof_tree)
openGoalsMap)
                              ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (Named sentence -> String) -> [Named sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr ([Named sentence] -> [String]) -> [Named sentence] -> [String]
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
s
            opts :: [String]
opts = String -> [String]
words String
opts'
            afterEachProofAttempt :: Int
-> Named sentence
-> Maybe (SenAttr s String)
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
afterEachProofAttempt gPSF :: Int
gPSF nSen :: Named sentence
nSen nextSen :: Maybe (SenAttr s String)
nextSen cfg :: (ATPRetval, GenericConfig proof_tree)
cfg@(retval :: ATPRetval
retval, _) = do
              Bool
cont <- MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
forall proof_tree sentence pst.
Ord proof_tree =>
MVar (GenericState sentence proof_tree pst)
-> Int
-> [String]
-> Int
-> String
-> Int
-> Named sentence
-> Bool
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
goalProcessed MVar (GenericState sentence proof_tree pst)
stateMVar Int
timeout [String]
opts Int
numGoals String
prName
                                    Int
gPSF Named sentence
nSen Bool
False (ATPRetval, GenericConfig proof_tree)
cfg
              IO Bool -> IO Bool
forall a. IO a -> IO a
postGUISync (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
                case ATPRetval
retval of
                  ATPError m :: String
m -> String -> String -> IO ()
errorDialog "Error" String
m
                  _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                GenericState sentence proof_tree pst
s' <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
readMVar MVar (GenericState sentence proof_tree pst)
stateMVar
                GenericState sentence proof_tree pst
-> TreeView -> ListStore Goal -> IO ()
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> TreeView -> ListStore Goal -> IO ()
updateGoals GenericState sentence proof_tree pst
s' TreeView
trvGoals ListStore Goal
listGoals
                let progress :: Double
progress = Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
gPSF Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numGoals
                Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cont (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Double -> String -> IO ()
updat Double
progress (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SenAttr s String -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr (SenAttr s String -> String) -> SenAttr s String -> String
forall a b. (a -> b) -> a -> b
$ Maybe (SenAttr s String) -> SenAttr s String
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (SenAttr s String)
nextSen
                Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
cont
        Double -> String -> IO ()
updat 0 String
firstGoalName
        ThreadId
tid <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ do
          IO ()
yield
          Bool
-> Int
-> [String]
-> Bool
-> Bool
-> (Int
    -> Named sentence
    -> Maybe (Named sentence)
    -> (ATPRetval, GenericConfig proof_tree)
    -> IO Bool)
-> (pst -> Named sentence -> pst)
-> RunProver sentence proof_tree pst
-> String
-> String
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO [ProofStatus proof_tree]
forall sentence proof_tree pst.
(Show sentence, Ord sentence, Ord proof_tree) =>
Bool
-> Int
-> [String]
-> Bool
-> Bool
-> (Int
    -> Named sentence
    -> Maybe (Named sentence)
    -> (ATPRetval, GenericConfig proof_tree)
    -> IO Bool)
-> (pst -> Named sentence -> pst)
-> RunProver sentence proof_tree pst
-> String
-> String
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))
-> IO [ProofStatus proof_tree]
genericProveBatch Bool
False Int
timeout [String]
opts Bool
inclProven Bool
saveBatch
            Int
-> Named sentence
-> Maybe (Named sentence)
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
forall s.
Int
-> Named sentence
-> Maybe (SenAttr s String)
-> (ATPRetval, GenericConfig proof_tree)
-> IO Bool
afterEachProofAttempt (ATPFunctions sign sentence mor proof_tree pst
-> pst -> Named sentence -> pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> pst
atpInsertSentence ATPFunctions sign sentence mor proof_tree pst
atpFun) (ATPFunctions sign sentence mor proof_tree pst
-> RunProver sentence proof_tree pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> RunProver sentence proof_tree pst
runProver ATPFunctions sign sentence mor proof_tree pst
atpFun)
            String
prName String
thName GenericState sentence proof_tree pst
s Maybe (MVar (Result [ProofStatus proof_tree]))
forall a. Maybe a
Nothing
          Bool
b <- MVar ThreadId -> IO Bool
forall a. MVar a -> IO Bool
isEmptyMVar MVar ThreadId
threadId
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
finished ()
        Bool
b <- MVar ThreadId -> ThreadId -> IO Bool
forall a. MVar a -> a -> IO Bool
tryPutMVar MVar ThreadId
threadId ThreadId
tid
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error "MVar 'threadId' already set"
        Bool -> IO ()
switchAll Bool
False
        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 ()
finished
          MVar ThreadId -> IO (Maybe ThreadId)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar ThreadId
threadId
          IO () -> IO ()
postGUIAsync (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            Bool -> IO ()
switchAll Bool
True
            IO ()
exit

    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

    -- read proofstate and store it in mvar
    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
      GenericState sentence proof_tree pst
s <- MVar (GenericState sentence proof_tree pst)
-> IO (GenericState sentence proof_tree pst)
forall a. MVar a -> IO a
takeMVar MVar (GenericState sentence proof_tree pst)
stateMVar
      let Result _ prst :: Maybe [ProofStatus proof_tree]
prst = GenericState sentence proof_tree pst
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall sentence proof_tree pst.
(Ord sentence, Ord proof_tree) =>
GenericState sentence proof_tree pst
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
revertRenamingOfLabels GenericState sentence proof_tree pst
s ([ProofStatus proof_tree] -> Result [ProofStatus proof_tree])
-> [ProofStatus proof_tree] -> Result [ProofStatus proof_tree]
forall a b. (a -> b) -> a -> b
$
            (Named sentence -> ProofStatus proof_tree)
-> [Named sentence] -> [ProofStatus proof_tree]
forall a b. (a -> b) -> [a] -> [b]
map ((\ g :: String
g -> let res :: Maybe (GenericConfig proof_tree)
res = String
-> Map String (GenericConfig proof_tree)
-> Maybe (GenericConfig proof_tree)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
g (Map String (GenericConfig proof_tree)
 -> Maybe (GenericConfig proof_tree))
-> Map String (GenericConfig proof_tree)
-> Maybe (GenericConfig proof_tree)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
                             g' :: String
g' = String -> String -> Map String String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                                    (String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "Lookup of name failed: (1) " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                           "should not happen \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"")
                                    String
g (Map String String -> String) -> Map String String -> String
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst -> Map String String
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> Map String String
namesMap GenericState sentence proof_tree pst
s
                  in ProofStatus proof_tree
-> (GenericConfig proof_tree -> ProofStatus proof_tree)
-> Maybe (GenericConfig proof_tree)
-> ProofStatus proof_tree
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> String -> proof_tree -> ProofStatus proof_tree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
g' String
prName (proof_tree -> ProofStatus proof_tree)
-> proof_tree -> ProofStatus proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst -> proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> proof_tree
currentProofTree GenericState sentence proof_tree pst
s)
                           GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus Maybe (GenericConfig proof_tree)
res) (String -> ProofStatus proof_tree)
-> (Named sentence -> String)
-> Named sentence
-> ProofStatus proof_tree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr) (GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
s)
      MVar (Maybe [ProofStatus proof_tree])
-> Maybe [ProofStatus proof_tree] -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar (Maybe [ProofStatus proof_tree])
result Maybe [ProofStatus proof_tree]
prst

    if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
initGoals then do
        String -> String -> IO ()
errorDialog "No goals available!" "No need to start prove window!"
        Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetDestroy Window
window
      else do
        TreeView -> IO ()
selectFirst TreeView
trvGoals
        Window -> IO ()
forall self. WidgetClass self => self -> IO ()
widgetShow Window
window

  -- waiting for results
  Maybe [ProofStatus proof_tree]
res <- MVar (Maybe [ProofStatus proof_tree])
-> IO (Maybe [ProofStatus proof_tree])
forall a. MVar a -> IO a
takeMVar MVar (Maybe [ProofStatus proof_tree])
result
  IO [ProofStatus proof_tree]
-> ([ProofStatus proof_tree] -> IO [ProofStatus proof_tree])
-> Maybe [ProofStatus proof_tree]
-> IO [ProofStatus proof_tree]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> IO [ProofStatus proof_tree]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "reverse translation of names failed") [ProofStatus proof_tree] -> IO [ProofStatus proof_tree]
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [ProofStatus proof_tree]
res

  where
    prepareLP :: pst
-> GenericState sentence proof_tree pst
-> String
-> Bool
-> (Named sentence, pst)
prepareLP prS :: pst
prS s :: GenericState sentence proof_tree pst
s g' :: String
g' inclProven :: Bool
inclProven =
      let goals :: [Named sentence]
goals = GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
s
          cfg :: GenericConfigsMap proof_tree
cfg = GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
          idx :: Int
idx = 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
$ (Named sentence -> Bool) -> [Named sentence] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
g') (String -> Bool)
-> (Named sentence -> String) -> Named sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr) [Named sentence]
goals
          (beforeThis :: [Named sentence]
beforeThis, afterThis :: [Named sentence]
afterThis) = Int -> [Named sentence] -> ([Named sentence], [Named sentence])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
idx [Named sentence]
goals
          g :: Named sentence
g = [Named sentence] -> Named sentence
forall a. [a] -> a
head [Named sentence]
afterThis -- Why use head and not goal?
          proved :: [Named sentence]
proved = (Named sentence -> Bool) -> [Named sentence] -> [Named sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (GenericConfigsMap proof_tree -> String -> Bool
forall proof_tree. GenericConfigsMap proof_tree -> String -> Bool
checkGoal GenericConfigsMap proof_tree
cfg (String -> Bool)
-> (Named sentence -> String) -> Named sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr) [Named sentence]
beforeThis
      in if Bool
inclProven
        then (Named sentence
g, (pst -> Named sentence -> pst) -> pst -> [Named sentence] -> pst
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ lp :: pst
lp provedGoal :: Named sentence
provedGoal -> ATPFunctions sign sentence mor proof_tree pst
-> pst -> Named sentence -> pst
forall sign sentence morphism proof_tree pst.
ATPFunctions sign sentence morphism proof_tree pst
-> pst -> Named sentence -> pst
atpInsertSentence ATPFunctions sign sentence mor proof_tree pst
atpFun pst
lp
                            (Named sentence
provedGoal { isAxiom :: Bool
AS_Anno.isAxiom = Bool
True }))
                          pst
prS ([Named sentence] -> pst) -> [Named sentence] -> pst
forall a b. (a -> b) -> a -> b
$ [Named sentence] -> [Named sentence]
forall a. [a] -> [a]
reverse [Named sentence]
proved)
        else (Named sentence
g, pst
prS)

saveConfigCurrent :: (Ord proof_tree)
                  => GenericState sentence proof_tree pst -> proof_tree
                  -> String -> SpinButton -> Entry
                  -> IO (GenericState sentence proof_tree pst)
saveConfigCurrent :: GenericState sentence proof_tree pst
-> proof_tree
-> String
-> SpinButton
-> Entry
-> IO (GenericState sentence proof_tree pst)
saveConfigCurrent s :: GenericState sentence proof_tree pst
s pt :: proof_tree
pt prName :: String
prName sbTimeout :: SpinButton
sbTimeout entryOptions :: Entry
entryOptions = do
  -- saving options for previous selected goal
  Int
timeout <- SpinButton -> IO Int
forall self. SpinButtonClass self => self -> IO Int
spinButtonGetValueAsInt SpinButton
sbTimeout
  String
opts <- Entry -> IO String
forall self string.
(EntryClass self, GlibString string) =>
self -> IO string
entryGetText Entry
entryOptions
  let mn :: Maybe String
mn = GenericState sentence proof_tree pst -> Maybe String
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> Maybe String
currentGoal GenericState sentence proof_tree pst
s
      cfg :: GenericConfigsMap proof_tree
cfg = GenericConfigsMap proof_tree
-> (String -> GenericConfigsMap proof_tree)
-> Maybe String
-> GenericConfigsMap proof_tree
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s) (\ g :: String
g ->
              (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall proof_tree.
Ord proof_tree =>
(GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
adjustOrSetConfig ([String] -> GenericConfig proof_tree -> GenericConfig proof_tree
forall proof_tree.
[String] -> GenericConfig proof_tree -> GenericConfig proof_tree
setExtraOpts ([String] -> GenericConfig proof_tree -> GenericConfig proof_tree)
-> [String] -> GenericConfig proof_tree -> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
opts) String
prName String
g proof_tree
pt
                (GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree)
-> GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
forall a b. (a -> b) -> a -> b
$ (GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
forall proof_tree.
Ord proof_tree =>
(GenericConfig proof_tree -> GenericConfig proof_tree)
-> String
-> String
-> proof_tree
-> GenericConfigsMap proof_tree
-> GenericConfigsMap proof_tree
adjustOrSetConfig (Int -> GenericConfig proof_tree -> GenericConfig proof_tree
forall proof_tree.
Int -> GenericConfig proof_tree -> GenericConfig proof_tree
setTimeLimit Int
timeout) String
prName String
g proof_tree
pt
                (GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree)
-> GenericConfigsMap proof_tree -> GenericConfigsMap proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s) Maybe String
mn
  GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall (m :: * -> *) a. Monad m => a -> m a
return (GenericState sentence proof_tree pst
 -> IO (GenericState sentence proof_tree pst))
-> GenericState sentence proof_tree pst
-> IO (GenericState sentence proof_tree pst)
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
s { configsMap :: GenericConfigsMap proof_tree
configsMap = GenericConfigsMap proof_tree
cfg }

updateGoals :: GenericState sentence proof_tree pst -> TreeView
            -> ListStore Goal -> IO ()
updateGoals :: GenericState sentence proof_tree pst
-> TreeView -> ListStore Goal -> IO ()
updateGoals s :: GenericState sentence proof_tree pst
s trvGoals :: TreeView
trvGoals listGoals :: ListStore Goal
listGoals = do
  let ng :: [Goal]
ng = GenericState sentence proof_tree pst -> [Goal]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Goal]
toGoals GenericState sentence proof_tree pst
s
  Maybe (Int, Goal)
selected <- TreeView -> ListStore Goal -> IO (Maybe (Int, Goal))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvGoals ListStore Goal
listGoals
  ListStore Goal -> [Goal] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore Goal
listGoals [Goal]
ng
  case Maybe (Int, Goal)
selected of
    Just (_, Goal { gName :: Goal -> String
gName = String
n }) -> do
      TreeSelection
selector <- TreeView -> IO TreeSelection
forall self. TreeViewClass self => self -> IO TreeSelection
treeViewGetSelection TreeView
trvGoals
      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]
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Updates the display of the status of the current goal.
update :: GenericState sentence proof_tree pst -> TreeView
       -> ListStore Goal -> ListStore String -> Label -> SpinButton -> Entry
       -> IO ()
update :: GenericState sentence proof_tree pst
-> TreeView
-> ListStore Goal
-> ListStore String
-> Label
-> SpinButton
-> Entry
-> IO ()
update s :: GenericState sentence proof_tree pst
s trvGoals :: TreeView
trvGoals listGoals :: ListStore Goal
listGoals listAxioms :: ListStore String
listAxioms lblStatus :: Label
lblStatus sbTimeout :: SpinButton
sbTimeout entryOptions :: Entry
entryOptions = do
  -- update status and axioms
  Maybe (Int, Goal)
selected <- TreeView -> ListStore Goal -> IO (Maybe (Int, Goal))
forall a. TreeView -> ListStore a -> IO (Maybe (Int, a))
getSelectedSingle TreeView
trvGoals ListStore Goal
listGoals
  case Maybe (Int, Goal)
selected of
    Just (_, Goal { gName :: Goal -> String
gName = String
n, gStatus :: Goal -> GStatus
gStatus = GStatus
stat }) -> do
      let cfg :: GenericConfig proof_tree
cfg = GenericConfig proof_tree
-> String
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> GenericConfig proof_tree
forall a. HasCallStack => String -> a
error "GUI.GenericATP.updateDisplay") String
n
                  (Map String (GenericConfig proof_tree) -> GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
      SpinButton -> Double -> IO ()
forall self. SpinButtonClass self => self -> Double -> IO ()
spinButtonSetValue SpinButton
sbTimeout (Double -> IO ()) -> Double -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral
        (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
guiDefaultTimeLimit (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ GenericConfig proof_tree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig proof_tree
cfg
      Entry -> String -> IO ()
forall self string.
(EntryClass self, GlibString string) =>
self -> string -> IO ()
entrySetText Entry
entryOptions (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig proof_tree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig proof_tree
cfg
      Label -> String -> IO ()
forall self string.
(LabelClass self, GlibString string) =>
self -> string -> IO ()
labelSetLabel Label
lblStatus (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ GStatus -> String
forall a. Show a => a -> String
show GStatus
stat
      ListStore String -> [String] -> IO ()
forall a. ListStore a -> [a] -> IO ()
updateListData ListStore String
listAxioms ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
usedAxioms (ProofStatus proof_tree -> [String])
-> ProofStatus proof_tree -> [String]
forall a b. (a -> b) -> a -> b
$ GenericConfig proof_tree -> ProofStatus proof_tree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig proof_tree
cfg
    Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Utility function to set the time limit of a Config.
setTimeLimit :: Int -> GenericConfig proof_tree -> GenericConfig proof_tree
setTimeLimit :: Int -> GenericConfig proof_tree -> GenericConfig proof_tree
setTimeLimit n :: Int
n c :: GenericConfig proof_tree
c = GenericConfig proof_tree
c { timeLimit :: Maybe Int
timeLimit = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n else Maybe Int
forall a. Maybe a
Nothing }

-- | Utility function to set the extra options of a Config.
setExtraOpts :: [String] -> GenericConfig proof_tree -> GenericConfig proof_tree
setExtraOpts :: [String] -> GenericConfig proof_tree -> GenericConfig proof_tree
setExtraOpts opts :: [String]
opts c :: GenericConfig proof_tree
c = GenericConfig proof_tree
c { extraOpts :: [String]
extraOpts = [String]
opts }

toGoals :: GenericState sentence proof_tree pst -> [Goal]
toGoals :: GenericState sentence proof_tree pst -> [Goal]
toGoals s :: GenericState sentence proof_tree pst
s = [Goal] -> [Goal]
forall a. Ord a => [a] -> [a]
sort ([Goal] -> [Goal]) -> [Goal] -> [Goal]
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Goal) -> [Named sentence] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (\ g :: Named sentence
g ->
  let n :: String
n = Named sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named sentence
g
      c :: GenericConfig proof_tree
c = GenericConfig proof_tree
-> String
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> GenericConfig proof_tree
forall a. HasCallStack => String -> a
error "Config not found!") String
n (Map String (GenericConfig proof_tree) -> GenericConfig proof_tree)
-> Map String (GenericConfig proof_tree)
-> GenericConfig proof_tree
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst
-> Map String (GenericConfig proof_tree)
forall sentence proof_tree pst.
GenericState sentence proof_tree pst
-> GenericConfigsMap proof_tree
configsMap GenericState sentence proof_tree pst
s
  in Goal :: GStatus -> String -> Goal
Goal { gName :: String
gName = String
n, gStatus :: GStatus
gStatus = GenericConfig proof_tree -> GStatus
forall a. GenericConfig a -> GStatus
genericConfigToGStatus GenericConfig proof_tree
c }) ([Named sentence] -> [Goal]) -> [Named sentence] -> [Goal]
forall a b. (a -> b) -> a -> b
$ GenericState sentence proof_tree pst -> [Named sentence]
forall sentence proof_tree pst.
GenericState sentence proof_tree pst -> [Named sentence]
goalsList GenericState sentence proof_tree pst
s