{- |
Module : ./GUI/HTkProverGUI.hs
Description : Goal management GUI.
Copyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : provisional
Portability : needs POSIX
Goal management GUI for the structured level similar to how 'SPASS.Prove'
works for SPASS.
-}
module GUI.HTkProverGUI (proofManagementGUI, GUIMVar) where
import Common.AS_Annotation as AS_Anno
import qualified Common.Doc as Pretty
import Common.Result as Result
import qualified Data.Map as Map
import Common.ExtSign
import Common.Utils
import Data.List
import qualified Control.Concurrent as Conc
import HTk.Toolkit.Separator
import HTk.Widgets.Space
import HTk.Devices.XSelection
import GUI.Utils
import GUI.HTkUtils hiding
(createTextSaveDisplay, displayTheoryWithWarning)
import GUI.HTkProofDetails
import Proofs.AbstractState
import Logic.Comorphism
import Logic.Logic
import Logic.Prover
import qualified Comorphisms.KnownProvers as KnownProvers
import Static.GTheory
-- * Proof Management GUI
-- ** Defining the view
{- |
Colors used by the GUI to indicate the status of a goal.
-}
data ProverStatusColour
-- | Not running
= Black
-- | Running
| Blue
deriving (Bounded, Enum, Show)
data SelButtonFrame = SBF { selAllEv :: Event ()
, deselAllEv :: Event ()
, sbfBtns :: [Button]
, sbfBtnFrame :: Frame}
data SelAllListbox = SAL SelButtonFrame (ListBox String)
{- |
Generates a ('ProverStatusColour', 'String') tuple.
-}
statusNotRunning :: (ProverStatusColour, String)
statusNotRunning = (Black, "No Prover Running")
{- |
Generates a ('ProverStatusColour', 'String') tuple.
-}
statusRunning :: (ProverStatusColour, String)
statusRunning = (Blue, "Waiting for Prover")
{- | Converts a 'ProofState' into a ('ProverStatusColour',
'String') tuple to be displayed by the GUI.
-}
toGuiStatus :: ProofState
-> (ProverStatusColour, String)
toGuiStatus st = if proverRunning st
then statusRunning
else statusNotRunning
{- |
Generates a list of 'GUI.HTkUtils.LBGoalView' representations of all goals
from a 'SPASS.Prove.State'.
Uses a status indicator internally.
-}
goalsView :: ProofState -- ^ current global state
-> [LBGoalView] -- ^ resulting ['LBGoalView'] list
goalsView = map toStatus . getGoals
where toStatus (l, st) =
let si = maybe LBIndicatorOpen indicatorFromBasicProof st
in LBGoalView { statIndicator = si
, goalDescription = l}
-- ** GUI Implementation
-- *** Utility Functions
{- |
Populates the "Pick Theorem Prover" 'ListBox' with prover names (or possibly
paths to provers).
-}
populatePathsListBox :: ListBox String
-> IO ()
populatePathsListBox lb prvs = do
lb # value (Map.keys prvs)
return ()
populateAxiomsList :: ListBox String
-> ProofState
-> IO ()
populateAxiomsList lbAxs s = do
lbAxs # value (toAxioms s)
return ()
setSelectedProver :: ListBox String
-> ProofState
-> IO ()
setSelectedProver lb st = do
let ind = case selectedProver st of
Just sp -> elemIndex sp $ Map.keys (proversMap st)
Nothing -> Nothing
maybe (return ()) (\ i -> selection i lb >> return ()) ind
-- *** Callbacks
{- |
Updates the display of the status of the selected goals.
-}
updateDisplay :: ProofState -- ^ current global state
-> Bool
-- ^ set to 'True' if you want the 'ListBox' to be updated
-> ListBox String
-- ^ 'ListBox' displaying the status of all goals (see 'goalsView')
-> ListBox String
-- ^ 'ListBox' displaying possible morphism paths to prover logics
-> Label
-- ^ 'Label' displaying the status of the currently selected goal(s)
-> IO ()
updateDisplay st updateLb goalsLb pathsLb statusLabel = do
-- update goals listbox
when updateLb
(do
(offScreen, _) <- view Vertical goalsLb
populateGoalsListBox goalsLb (goalsView st)
moveto Vertical goalsLb offScreen)
setSelectedProver pathsLb st
-- update status label
let (color, label) = toGuiStatus st
statusLabel # text label
statusLabel # foreground (show color)
return ()
toGoals :: ProofState -> [String]
toGoals = map fst . getGoals
updateStateGetSelectedGoals :: ProofState
-> ListBox String
-> IO ProofState
updateStateGetSelectedGoals s lb =
do sel <- getSelection lb :: IO (Maybe [Int])
return s {selectedGoals =
maybe [] (map (toGoals s !!)) sel}
updateStateGetSelectedSens :: ProofState
-> ListBox String -- ^ axioms listbox
-> ListBox String -- ^ theorems listbox
-> IO ProofState
updateStateGetSelectedSens s lbAxs lbThs = do
selA <- getSelection lbAxs :: IO (Maybe [Int])
selT <- getSelection lbThs :: IO (Maybe [Int])
return (s { includedAxioms = maybe [] (fil $ toAxioms s) selA
, includedTheorems = maybe [] (fil $ toGoals s) selT })
where fil = map . (!!)
{- |
Depending on the first argument all entries in a ListBox are selected
or deselected
-}
doSelectAllEntries :: Bool {- ^ indicates wether all entries should be selected
or deselected -}
-> ListBox a
-> IO ()
doSelectAllEntries selectAll lb =
if selectAll
then selectionRange (0 :: Int) EndOfText lb >> return ()
else clearSelection lb
{- |
Called whenever the button "Display" is clicked.
-}
doDisplayGoals :: ProofState -> IO ()
doDisplayGoals s =
case currentTheory s of
G_theory lid1 _ (ExtSign sig1 _) _ sens1 _ -> do
let thName = theoryName s
goalsText = show . Pretty.vsep .
map (print_named lid1 .
AS_Anno.mapNamed (simplify_sen lid1 sig1))
. toNamedList
$ filterMapWithList (selectedGoals s) sens1
createTextSaveDisplay ("Selected Goals from Theory " ++ thName)
(thName ++ "-goals.txt") goalsText
{- |
Called whenever a prover is selected from the "Pick Theorem Prover" ListBox.
-}
doSelectProverPath :: ProofState -> ListBox String -> IO ProofState
doSelectProverPath s lb =
do selected <- getSelection lb :: IO (Maybe [Int])
return s {selectedProver =
maybe Nothing
(\ (index : _) ->
Just (Map.keys (proversMap s) !! index))
selected
}
newSelectButtonsFrame :: (Container par) => par -> IO SelButtonFrame
newSelectButtonsFrame b3 = do
selFrame <- newFrame b3 []
pack selFrame [Expand Off, Fill None, Side AtLeft, Anchor SouthWest]
selHBox <- newHBox selFrame []
pack selHBox [Expand Off, Fill None, Anchor West]
selectAllButton <- newButton selHBox [text "Select all"]
pack selectAllButton [Expand Off, Fill None]
deselectAllButton <- newButton selHBox [text "Deselect all"]
pack deselectAllButton [Expand Off, Fill None]
-- events
selectAll <- clicked selectAllButton
deselectAll <- clicked deselectAllButton
return SBF
{ selAllEv = selectAll
, deselAllEv = deselectAll
, sbfBtns = [deselectAllButton, selectAllButton]
, sbfBtnFrame = selFrame }
newExtSelListBoxFrame :: (Container par) => par -> String -> Distance
-> IO SelAllListbox
newExtSelListBoxFrame b2 title hValue = do
left <- newFrame b2 []
pack left [Expand On, Fill Both]
b3 <- newVBox left []
pack b3 [Expand On, Fill Both]
l0 <- newLabel b3 [text title]
pack l0 [Anchor NorthWest]
lbFrame <- newFrame b3 []
pack lbFrame [Expand On, Fill Both, Anchor NorthWest]
lb <- newListBox lbFrame [bg "white", exportSelection False,
selectMode Multiple,
height hValue] :: IO (ListBox String)
pack lb [Expand On, Side AtLeft, Fill Both]
sb <- newScrollBar lbFrame []
pack sb [Expand On, Side AtRight, Fill Y, Anchor West]
lb # scrollbar Vertical sb
-- buttons for goal selection
sbf <- newSelectButtonsFrame b3
return (SAL sbf lb)
-- *** Main GUI
-- | Invokes the GUI.
proofManagementGUI :: ProofActions -- ^ record of possible GUI actions
-> String -- ^ theory name
-> String -- ^ warning information
-> G_theory -- ^ theory
-> KnownProvers.KnownProversMap -- ^ map of known provers
-> [(G_prover, AnyComorphism)] {- ^ list of suitable comorphisms to provers
for sublogic of G_theory -}
-> GUIMVar {- ^ allows only one Proof window per graph;
must be filled with Nothing and is filled with Nothing after
closing the window; while the window is open it is filled with
the Toplevel -}
-> IO (Result.Result G_theory)
proofManagementGUI prGuiAcs thName warningTxt th
knownProvers comorphList guiMVar = do
{- KnownProvers.showKnownProvers knownProvers
initial backing data structure -}
initState <- recalculateSublogicF prGuiAcs
(initialState thName th knownProvers)
{ comorphismsToProvers = comorphList }
stateMVar <- Conc.newMVar initState
lockMVar <- Conc.newMVar ()
-- main window
main <- createToplevel [text $ thName ++ " - Select Goal(s) and Prove"]
Conc.tryTakeMVar guiMVar >>=
let err s = fail $ "ProofManagementGUI: (" ++ s ++ ") MVar must be "
++ "filled with Nothing when entering proofManagementGUI"
in maybe (err "not filled")
(maybe (Conc.putMVar guiMVar $ Just main)
(const $ err "filled with (Just x)"))
-- VBox for the whole window
b <- newVBox main []
pack b [Expand On, Fill Both]
-- HBox for the upper part (goals on the left, options/results on the right)
b2 <- newHBox b []
pack b2 [Expand On, Fill Both]
-- ListBox for goal selection
(SAL (SBF { selAllEv = selectAllGoals
, deselAllEv = deselectAllGoals
, sbfBtns = goalBtns
, sbfBtnFrame = goalsBtnFrame}) lb)
<- newExtSelListBoxFrame b2 "Goals:" 14
-- button to select only the open goals
selectOpenGoalsButton <- newButton goalsBtnFrame [text "Select open goals"]
pack selectOpenGoalsButton [Expand Off, Fill None, Side AtLeft]
-- right frame (options/results)
right <- newFrame b2 []
pack right [Expand On, Fill Both, Anchor NorthWest]
let hindent = " "
let vspacing = cm 0.2
rvb <- newVBox right []
pack rvb [Expand On, Fill Both]
l1 <- newLabel rvb [text "Selected Goal(s):"]
pack l1 [Anchor NorthWest]
rhb1 <- newHBox rvb []
pack rhb1 [Expand On, Fill Both]
hsp1 <- newLabel rhb1 [text hindent]
pack hsp1 []
displayGoalsButton <- newButton rhb1 [text "Display"]
pack displayGoalsButton []
proveButton <- newButton rhb1 [text "Prove"]
pack proveButton []
proofDetailsButton <- newButton rhb1 [text "Show proof details"]
pack proofDetailsButton []
vsp1 <- newSpace rvb vspacing []
pack vsp1 []
l2 <- newLabel rvb [text "Status:"]
pack l2 [Anchor NorthWest]
rhb2 <- newHBox rvb []
pack rhb2 [Expand On, Fill Both]
hsp2 <- newLabel rhb2 [text hindent]
pack hsp2 []
statusLabel <- newLabel rhb2 [text (snd statusNotRunning)]
pack statusLabel []
vsp2 <- newSpace rvb vspacing []
pack vsp2 []
l3 <- newLabel rvb [text "Sublogic of Currently Selected Theory:"]
pack l3 [Anchor NorthWest]
rhb3 <- newHBox rvb []
pack rhb3 [Expand On, Fill Both]
hsp3 <- newLabel rhb3 [text hindent]
pack hsp3 []
sublogicLabel <- newLabel rhb3 [text (show $ sublogicOfTheory initState)]
pack sublogicLabel []
vsp3 <- newSpace rvb vspacing []
pack vsp3 []
l4 <- newLabel rvb [text "Pick Theorem Prover:"]
pack l4 [Anchor NorthWest]
rhb4 <- newHBox rvb []
pack rhb4 [Expand On, Fill Both]
hsp4 <- newLabel rhb4 [text hindent]
pack hsp4 []
pathsFrame <- newFrame rhb4 []
pack pathsFrame []
pathsLb <- newListBox pathsFrame [value ([] :: [String]), bg "white",
selectMode Single, exportSelection False,
height 4, width 28] :: IO (ListBox String)
pack pathsLb [Expand On, Side AtLeft, Fill Both]
pathsSb <- newScrollBar pathsFrame []
pack pathsSb [Expand On, Side AtRight, Fill Y]
pathsLb # scrollbar Vertical pathsSb
moreButton <- newButton rvb [text "More fine grained selection..."]
pack moreButton [Anchor SouthEast]
-- separator
sp1 <- newSpace b (cm 0.15) []
pack sp1 [Expand Off, Fill X, Side AtBottom]
newHSeparator b
sp2 <- newSpace b (cm 0.15) []
pack sp2 [Expand Off, Fill X, Side AtBottom]
-- theory composer frame (toggled with button)
composer <- newFrame b []
pack composer [Expand On, Fill Both]
compBox <- newVBox composer []
pack compBox [Expand On, Fill Both]
newLabel compBox [text "Fine grained composition of theory:"]
>>= flip pack []
icomp <- newFrame compBox []
pack icomp [Expand On, Fill Both]
icBox <- newHBox icomp []
pack icBox [Expand On, Fill Both]
(SAL (SBF { selAllEv = selectAllAxs
, deselAllEv = deselectAllAxs
, sbfBtns = axsBtns
, sbfBtnFrame = axiomsBtnFrame}) lbAxs)
<- newExtSelListBoxFrame icBox "Axioms to include:" 10
-- button to deselect axioms that are former theorems
deselectFormerTheoremsButton <- newButton axiomsBtnFrame
[text "Deselect former theorems"]
pack deselectFormerTheoremsButton [Expand Off, Fill None, Side AtLeft]
(SAL (SBF { selAllEv = selectAllThs
, deselAllEv = deselectAllThs
, sbfBtns = thsBtns}) lbThs)
<- newExtSelListBoxFrame icBox "Theorems to include if proven:" 10
-- separator
spac1 <- newSpace b (cm 0.15) []
pack spac1 [Expand Off, Fill X, Side AtBottom]
newHSeparator b
spac2 <- newSpace b (cm 0.15) []
pack spac2 [Expand Off, Fill X, Side AtBottom]
-- bottom frame (close button)
bottom <- newFrame b []
pack bottom [Expand Off, Fill Both]
bottomThFrame <- newFrame bottom []
pack bottomThFrame [Expand Off, Fill Both, Side AtLeft]
showThButton <- newButton bottomThFrame [text "Show theory"]
pack showThButton [Expand Off, Fill None, Side AtLeft]
showSelThButton <- newButton bottomThFrame [text "Show selected theory"]
pack showSelThButton [Expand Off, Fill None, Side AtRight]
closeButton <- newButton bottom [text "Close"]
pack closeButton [Expand Off, Fill None, Side AtRight, PadX (pp 13)]
-- put the labels in the listboxes
populateGoalsListBox lb (goalsView initState)
populateAxiomsList lbAxs initState
populatePathsListBox pathsLb (proversMap initState)
lbThs # value (toGoals initState)
doSelectAllEntries True lb
doSelectAllEntries True lbAxs
doSelectAllEntries True lbThs
updateDisplay initState False lb pathsLb statusLabel
let goalSpecificWids = map EnW [displayGoalsButton, proveButton,
proofDetailsButton, moreButton]
wids = [EnW pathsLb, EnW lbThs, EnW lb, EnW lbAxs] ++
map EnW (selectOpenGoalsButton : closeButton : showThButton :
showSelThButton : deselectFormerTheoremsButton :
axsBtns ++ goalBtns ++ thsBtns) ++
goalSpecificWids
enableWids goalSpecificWids
pack main [Expand On, Fill Both]
putWinOnTop main
let updateStatusSublogic s = do
sWithSel <- updateStateGetSelectedSens s lbAxs lbThs
>>= flip updateStateGetSelectedGoals lb
s' <- recalculateSublogicF prGuiAcs
sWithSel {proversMap = knownProvers}
let newSublogicText = show $ sublogicOfTheory s'
sublogicText <- getText sublogicLabel
when (sublogicText /= newSublogicText)
(sublogicLabel # text newSublogicText >> return ())
populatePathsListBox pathsLb (proversMap s')
setSelectedProver pathsLb s'
return s' { selectedProver =
maybe Nothing
(\ sp -> find (== sp) $ Map.keys (proversMap s'))
(selectedProver s')}
-- events
(selectProverPath, _) <- bindSimple pathsLb (ButtonPress (Just 1))
(selectGoals, _) <- bindSimple lb (ButtonPress (Just 1))
(selectAxioms, _) <- bindSimple lbAxs (ButtonPress (Just 1))
(selectTheorems, _) <- bindSimple lbThs (ButtonPress (Just 1))
selectOpenGoals <- clicked selectOpenGoalsButton
deselectFormerTheorems <- clicked deselectFormerTheoremsButton
displayGoals <- clicked displayGoalsButton
moreProverPaths <- clicked moreButton
doProve <- clicked proveButton
showProofDetails <- clicked proofDetailsButton
close <- clicked closeButton
showTh <- clicked showThButton
showSelTh <- clicked showSelThButton
(closeWindow, _) <- bindSimple main Destroy
-- event handlers
_ <- spawnEvent $ forever
$ selectGoals >>> do
Conc.modifyMVar_ stateMVar updateStatusSublogic
enableWidsUponSelection lb goalSpecificWids
done
+> selectAxioms >>> do
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> selectTheorems >>> do
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> selectOpenGoals >>> do
s <- Conc.takeMVar stateMVar
clearSelection lb
let isOpen = maybe True (\ bp -> case bp of
BasicProof _ pst -> isOpenGoal $ goalStatus pst
_ -> False)
mapM_ (`selection` lb)
(findIndices (isOpen . snd) $ getGoals s)
enableWidsUponSelection lb goalSpecificWids
s' <- updateStatusSublogic s
Conc.putMVar stateMVar s'
done
+> deselectFormerTheorems >>> do
s <- Conc.takeMVar stateMVar
let axiomList = getAxioms s
sel <- getSelection lbAxs :: IO (Maybe [Int])
clearSelection lbAxs
mapM_ (`selection` lbAxs) $
maybe [] (filter (not . snd . (!!) axiomList)) sel
s' <- updateStatusSublogic s
Conc.putMVar stateMVar s'
done
+> deselectAllGoals >>> do
doSelectAllEntries False lb
enableWids goalSpecificWids
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> selectAllGoals >>> do
doSelectAllEntries True lb
enableWids goalSpecificWids
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> selectAllAxs >>> do
doSelectAllEntries True lbAxs
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> selectAllThs >>> do
doSelectAllEntries True lbThs
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> deselectAllAxs >>> do
doSelectAllEntries False lbAxs
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> deselectAllThs >>> do
doSelectAllEntries False lbThs
Conc.modifyMVar_ stateMVar updateStatusSublogic
done
+> displayGoals >>> do
s <- Conc.readMVar stateMVar
s' <- updateStateGetSelectedGoals s lb
doDisplayGoals s'
done
+> selectProverPath >>> do
Conc.modifyMVar_ stateMVar (`doSelectProverPath` pathsLb)
done
+> moreProverPaths >>> do
s <- Conc.readMVar stateMVar
let s' = s {proverRunning = True}
updateDisplay s' True lb pathsLb statusLabel
disableWids wids
prState <- updateStatusSublogic s'
Result.Result ds ms'' <- fineGrainedSelectionF prGuiAcs prState
s'' <- case ms'' of
Nothing -> do
when (null ds
|| diagString (head ds) /= "Proofs.Proofs: selection")
$ errorDialog "Error" (showRelDiags 2 ds)
return s'
Just res -> return res
let s''' = s'' { proverRunning = False
, accDiags = accDiags s'' ++ ds }
enableWids wids
updateDisplay s''' True lb pathsLb statusLabel
putWinOnTop main
Conc.tryTakeMVar stateMVar -- ensure that MVar is empty
Conc.putMVar stateMVar s'''
done
+> doProve >>> do
s <- Conc.takeMVar stateMVar
let s' = s {proverRunning = True}
updateDisplay s' True lb pathsLb statusLabel
disableWids wids
prState <- updateStatusSublogic s'
Result.Result ds ms'' <- proveF prGuiAcs prState
s'' <- case ms'' of
Nothing -> do
errorDialog "Error" (showRelDiags 2 ds)
return s'
Just res -> return res
let s''' = s'' {proverRunning = False,
accDiags = accDiags s'' ++ ds}
Conc.putMVar stateMVar s'''
mv <- Conc.tryTakeMVar lockMVar
case mv of
Nothing -> done
Just _ -> do
enable lb
updateDisplay s''' True lb pathsLb statusLabel
enableWids wids
putWinOnTop main
Conc.tryPutMVar lockMVar ()
done
+> showProofDetails >>> do
s <- Conc.readMVar stateMVar
s' <- updateStateGetSelectedGoals s lb
doShowProofDetails s'
done
+> showTh >>> do
displayTheoryWithWarning "Theory" thName warningTxt th
done
+> showSelTh >>> do
s <- Conc.readMVar stateMVar
displayTheoryWithWarning "Selected Theory" thName warningTxt
(selectedTheory s)
done
sync $ close >>> destroy main
+> closeWindow >>> Conc.takeMVar lockMVar
-- clean up locking of window
Conc.tryTakeMVar guiMVar >>=
let err s = fail $ "ProofManagementGUI: (" ++ s ++ ") MVar must be "
++ "filled with Nothing when entering proofManagementGUI"
in maybe (err "not filled")
(maybe (err "filled with Nothing")
(const $ Conc.putMVar guiMVar Nothing))
-- read the global state back in
s <- Conc.takeMVar stateMVar
return . Result.Result (accDiags s) . Just $ currentTheory s