4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeModule : $Header$

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeDescription : Goal management GUI.

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeCopyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeMaintainer : luecke@informatik.uni-bremen.de

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeStability : provisional

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckePortability : needs POSIX

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeGoal management GUI for the structured level similar to how 'SPASS.Prove'

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeworks for SPASS.

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-}

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckemodule GUI.HTkProverGUI (proofManagementGUI,GUIMVar) where

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Common.AS_Annotation as AS_Anno

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.Doc as Pretty

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Common.Result as Result

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Data.Map as Map

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.OrderedMap as OMap

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Common.ExtSign

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Data.List

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Control.Concurrent as Conc

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport HTk.Toolkit.Separator

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport HTk.Widgets.Space

548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckeimport HTk.Devices.XSelection

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport GUI.Utils

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport GUI.HTkUtils hiding

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke (createTextSaveDisplay, displayTheoryWithWarning)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport GUI.HTkProofDetails

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Proofs.AbstractState

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Logic.Comorphism

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Logic.Logic

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Logic.Prover

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Comorphisms.KnownProvers as KnownProvers

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport Static.GTheory

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- * Proof Management GUI

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- ** Defining the view

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke Colors used by the GUI to indicate the status of a goal.

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-}

548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckedata ProverStatusColour

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- | Not running

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke = Black

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- | Running

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke | Blue

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke deriving (Bounded,Enum,Show)

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckedata SelButtonFrame = SBF { selAllEv :: Event ()

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke , deselAllEv :: Event ()

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke , sbfBtns :: [Button]

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke , sbfBtnFrame :: Frame}

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckedata SelAllListbox = SAL SelButtonFrame (ListBox String)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke{- |

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke Generates a ('ProverStatusColour', 'String') tuple.

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-}

548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckestatusNotRunning :: (ProverStatusColour, String)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckestatusNotRunning = (Black, "No Prover Running")

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke{- |

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke Generates a ('ProverStatusColour', 'String') tuple.

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-}

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckestatusRunning :: (ProverStatusColour, String)

548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckestatusRunning = (Blue, "Waiting for Prover")

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke{- | Converts a 'ProofState' into a ('ProverStatusColour',

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke 'String') tuple to be displayed by the GUI.

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-}

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LuecketoGuiStatus :: ProofState lid sentence

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> (ProverStatusColour, String)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LuecketoGuiStatus st = if proverRunning st

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke then statusRunning

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke else statusNotRunning

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke Generates a list of 'GUI.HTkUtils.LBGoalView' representations of all goals

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke from a 'SPASS.Prove.State'.

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke Uses a status indicator internally.

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-}

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckegoalsView :: ProofState lid sentence -- ^ current global state

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> [LBGoalView] -- ^ resulting ['LBGoalView'] list

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckegoalsView = map toStatus . OMap.toList . goalMap

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke where toStatus (l,st) =

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke let tStatus = thmStatus st

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke si = if null tStatus

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke then LBIndicatorOpen

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke else indicatorFromBasicProof

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke (maximum $ map snd tStatus)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke in LBGoalView { statIndicator = si

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke , goalDescription = l}

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- ** GUI Implementation

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- *** Utility Functions

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke{- |

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke Populates the "Pick Theorem Prover" 'ListBox' with prover names (or possibly

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke paths to provers).

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-}

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckepopulatePathsListBox :: ListBox String

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> KnownProvers.KnownProversMap

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> IO ()

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckepopulatePathsListBox lb prvs = do

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke lb # value (Map.keys prvs)

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke return ()

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepopulateAxiomsList ::

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke ListBox String

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> ProofState lid1 sentence1

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> IO ()

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckepopulateAxiomsList lbAxs s =

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke do aM' <- axiomMap s

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke lbAxs # value (map (\ (k, sen) -> if wasTheorem sen then "(Th) " ++ k

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke else k) $

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke OMap.toList aM')

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke return ()

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckesetSelectedProver :: ListBox String

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> ProofState lid1 sentence1

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> IO ()

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckesetSelectedProver lb st = do

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke let ind = case selectedProver st of

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke Just sp -> findIndex (==sp) $ Map.keys (proversMap st)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke Nothing -> Nothing

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke maybe (return ()) (\i -> selection i lb >> return ()) ind

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- *** Callbacks

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke{- |

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke Updates the display of the status of the selected goals.

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-}

548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeupdateDisplay :: ProofState lid sentence -- ^ current global state

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Bool

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- ^ set to 'True' if you want the 'ListBox' to be updated

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> ListBox String

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- ^ 'ListBox' displaying the status of all goals (see 'goalsView')

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> ListBox String

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- ^ 'ListBox' displaying possible morphism paths to prover logics

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Label

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- ^ 'Label' displaying the status of the currently selected goal(s)

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> IO ()

548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeupdateDisplay st updateLb goalsLb pathsLb statusLabel = do

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -- update goals listbox

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke when updateLb

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke (do

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke (offScreen,_) <- view Vertical goalsLb

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke populateGoalsListBox goalsLb (goalsView st)

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke moveto Vertical goalsLb offScreen)

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke setSelectedProver pathsLb st

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke -- update status label

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke let (color, label) = toGuiStatus st

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke statusLabel # text label

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke statusLabel # foreground (show color)

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke return ()

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckeupdateStateGetSelectedGoals ::

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke ProofState lid1 sentence1

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> ListBox String

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> IO (ProofState lid1 sentence1)

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckeupdateStateGetSelectedGoals s lb =

648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke do sel <- getSelection lb :: IO (Maybe [Int])

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke return s {selectedGoals =

548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke maybe [] (map (OMap.keys (goalMap s) !!)) sel}

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeupdateStateGetSelectedSens ::

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke ProofState lid1 sentence1

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke -> ListBox String -- ^ axioms listbox

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke -> ListBox String -- ^ theorems listbox

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke -> IO (ProofState lid1 sentence1)

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeupdateStateGetSelectedSens s lbAxs lbThs =

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke do aM <- axiomMap s

4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke selA <- getSelection lbAxs :: IO (Maybe [Int])

selT <- getSelection lbThs :: IO (Maybe [Int])

return (s { includedAxioms = maybe [] (fil aM) selA

, includedTheorems = maybe [] (fil (goalMap s)) selT })

where fil = map . (!!) . OMap.keys

{- |

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 ::

(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

ProofState lid1 sentence1

-> IO ()

doDisplayGoals s =

case theory s of

G_theory lid1 (ExtSign sig1 _) _ _ _ -> do

let thName = theoryName s

goalsText = show . Pretty.vsep .

map (print_named lid1 .

AS_Anno.mapNamed (simplify_sen lid1 sig1))

. toNamedList

sens = selectedGoalMap s

sens' <- coerceThSens (logicId s) lid1 "" sens

createTextSaveDisplay ("Selected Goals from Theory " ++ thName)

(thName ++ "-goals.txt") (goalsText sens')

{- |

Called whenever a prover is selected from the "Pick Theorem Prover" ListBox.

-}

doSelectProverPath :: ProofState lid sentence

-> ListBox String

-> IO (ProofState lid sentence)

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 ::

(Logic lid sublogics1

basic_spec1

sentence

symb_items1

symb_map_items1

sign1

morphism1

symbol1

raw_symbol1

proof_tree1) =>

lid

-> ProofActions lid sentence -- ^ 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 lid prGuiAcs thName warningTxt th

knownProvers comorphList guiMVar = do

-- KnownProvers.showKnownProvers knownProvers

-- initial backing data structure

initState <- initialState lid thName th knownProvers comorphList

>>= recalculateSublogicF prGuiAcs

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 (OMap.keys (goalMap 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 ())

when (Map.keys (proversMap s) /= Map.keys (proversMap s'))

(do 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 (_, st) =

let thst = thmStatus st

in null thst

|| case maximum $ map snd thst of

BasicProof _ pst ->

isOpenGoal $ goalStatus pst

_ -> False

mapM_ (flip selection lb)

(findIndices isOpen $ OMap.toList $ goalMap s)

enableWidsUponSelection lb goalSpecificWids

s' <- updateStatusSublogic s

Conc.putMVar stateMVar s'

done

+> deselectFormerTheorems >>> do

s <- Conc.takeMVar stateMVar

aM <- axiomMap s

let axiomList = OMap.toList aM

isNotFormerTheorem (_,st) = not $ wasTheorem st

sel <- getSelection lbAxs :: IO (Maybe [Int])

clearSelection lbAxs

mapM_ (flip selection lbAxs) $

maybe [] (filter (isNotFormerTheorem . (!!) 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 (flip 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

case theory s of

G_theory lidT sigT indT sensT _ ->

do gMap <- coerceThSens (logicId s) lidT

"ProofManagement last coerce" (goalMap s)

return $ Result.Result (accDiags s)

$ Just $ G_theory lidT sigT indT (Map.union sensT gMap) startThId