module GUI.GtkProverGUI ( showProverGUI ) where
import Graphics.UI.Gtk
import GUI.GtkUtils
import qualified GUI.Glade.ProverGUI as ProverGUI
import GUI.HTkProofDetails
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 }
showProverGUI :: ProofActions
-> String
-> String
-> G_theory
-> KnownProvers.KnownProversMap
-> [(G_prover, AnyComorphism)]
-> 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
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"
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"
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"
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"
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"
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"
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
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
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
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
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
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
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 -> 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 }
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
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