1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederModule : $Header$

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederDescription : Goal management GUI.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCopyright : (c) Rene Wagner, Klaus L�ttich, Uni Bremen 2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederMaintainer : luecke@informatik.uni-bremen.de

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederStability : provisional

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederPortability : needs POSIX

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian MaederGoal management GUI for the structured level similar to how 'SPASS.Prove'

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederworks for SPASS.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule GUI.ProofManagement (proofManagementGUI,GUIMVar) where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Common.AS_Annotation as AS_Anno

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maederimport qualified Common.Doc as Pretty

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Common.Result as Result

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport qualified Data.Map as Map

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport qualified Common.OrderedMap as OMap

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.ExtSign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.List

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Control.Concurrent as Conc

67869d63d1725c79e4c07b51acd466a31932b275Christian Maederimport HTk

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzimport Separator

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Space

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport XSelection

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport GUI.HTkUtils

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport GUI.ProofDetails

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzimport Proofs.AbstractState

64e1905404e5135e98a26d2ab4150b6764956576Christian Maederimport Logic.Comorphism

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederimport Logic.Grothendieck

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederimport Logic.Logic

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederimport Logic.Prover

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Comorphisms.KnownProvers as KnownProvers

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Static.GTheory

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- debugging

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder-- import Debug.Trace

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- * Proof Management GUI

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- ** some types

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder-- | Type for storing the proof management window

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulztype GUIMVar = Conc.MVar (Maybe Toplevel)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder

65dce48b81f69e11a36bf1051314a845299446e1Christian Maeder-- ** Defining the view

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder{- |

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder Colors used by the GUI to indicate the status of a goal.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata ProverStatusColour

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- | Not running

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder = Black

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- | Running

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder | Blue

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder deriving (Bounded,Enum,Show)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maederdata SelButtonFrame = SBF { selAllEv :: Event ()

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder , deselAllEv :: Event ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , sbf_btns :: [Button]

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , sbf_btnFrame :: Frame}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata SelAllListbox = SAL SelButtonFrame (ListBox String)

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Generates a ('ProverStatusColour', 'String') tuple.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederstatusNotRunning :: (ProverStatusColour, String)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederstatusNotRunning = (Black, "No Prover Running")

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Generates a ('ProverStatusColour', 'String') tuple.

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder-}

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederstatusRunning :: (ProverStatusColour, String)

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederstatusRunning = (Blue, "Waiting for Prover")

62eaa2fb831613d8a6e59687f83a45be1041ab17Christian Maeder

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder{- | Converts a 'ProofState' into a ('ProverStatusColour',

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder 'String') tuple to be displayed by the GUI.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedertoGuiStatus :: ProofState lid sentence

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> (ProverStatusColour, String)

67869d63d1725c79e4c07b51acd466a31932b275Christian MaedertoGuiStatus st = if proverRunning st

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder then statusRunning

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else statusNotRunning

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- |

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Generates a list of 'GUI.HTkUtils.LBGoalView' representations of all goals

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder from a 'SPASS.Prove.State'.

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Uses a status indicator internally.

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-}

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergoalsView :: ProofState lid sentence -- ^ current global state

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -> [LBGoalView] -- ^ resulting ['LBGoalView'] list

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedergoalsView = map toStatus . OMap.toList . goalMap

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder where toStatus (l,st) =

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder let tStatus = thmStatus st

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder si = if null tStatus

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder then LBIndicatorOpen

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else indicatorFromBasicProof

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (maximum $ map snd $ tStatus)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in LBGoalView { statIndicator = si

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , goalDescription = l}

67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- ** GUI Implementation

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder

ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder-- *** Utility Functions

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder

935613eb8e67d724f1c4a4d4a37be3324ef6708dChristian Maeder{- |

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder Populates the "Pick Theorem Prover" 'ListBox' with prover names (or possibly

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder paths to provers).

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder-}

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederpopulatePathsListBox :: ListBox String

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -> KnownProvers.KnownProversMap

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -> IO ()

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaederpopulatePathsListBox lb prvs = do

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz lb # HTk.value (Map.keys prvs)

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder return ()

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder

083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederpopulateAxiomsList ::

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder ListBox String

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder -> ProofState lid1 sentence1

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -> IO ()

083a5256468076d5a9bfeb22a6e97076c224252eChristian MaederpopulateAxiomsList lbAxs s =

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder do aM' <- axiomMap s

392b67dbb9414475750ac2a977348de77354c600Christian Maeder lbAxs # HTk.value (map (\(k,sen) -> if (wasTheorem sen) then "(Th) "++k

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder else k) $

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder OMap.toList aM')

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder return ()

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian MaedersetSelectedProver :: ListBox String

de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder -> ProofState lid1 sentence1

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder -> IO ()

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian MaedersetSelectedProver lb st = do

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder let ind = case selectedProver st of

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder Just sp -> findIndex (==sp) $ Map.keys (proversMap st)

083a5256468076d5a9bfeb22a6e97076c224252eChristian Maeder Nothing -> Nothing

0d7d8e3dd817450cf792778d9d4e36420f5e8abfChristian Maeder maybe (return ()) (\i -> selection i lb >> return ()) ind

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-- *** Callbacks

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder{- |

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder Updates the display of the status of the selected goals.

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder-}

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederupdateDisplay :: ProofState lid sentence -- ^ current global state

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder -> Bool

6d4d212092e2edb139e0907a14e87c4df74ff06aChristian Maeder -- ^ 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 ()

updateStateGetSelectedGoals ::

(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

ProofState lid1 sentence1

-> ListBox String

-> IO (ProofState lid1 sentence1)

updateStateGetSelectedGoals s lb =

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

return (s {selectedGoals =

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

updateStateGetSelectedSens ::

(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>

ProofState lid1 sentence1

-> ListBox String -- ^ axioms listbox

-> ListBox String -- ^ theorems listbox

-> IO (ProofState lid1 sentence1)

updateStateGetSelectedSens s lbAxs lbThs =

do aM <- axiomMap s

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 str = map ((OMap.keys str)!!)

{- |

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 s' = show $ Pretty.vsep $

map (print_named lid1 .

AS_Anno.mapNamed (simplify_sen lid1 sig1)) $

toNamedList s'

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

, sbf_btns = [deselectAllButton,selectAllButton]

, sbf_btnFrame = 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 >>= (\ mmt ->

let err s = fail $ "ProofManagementGUI: ("++s++") MVar must be "++

"filled with Nothing when entering proofManagementGUI"

in do

maybe (err "not filled")

(maybe (Conc.putMVar guiMVar $ Just main)

(const $ err "filled with (Just x)"))

mmt)

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

, sbf_btns = goalBtns

, sbf_btnFrame = 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 [HTk.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:"] >>=

(\ lab -> pack lab [])

icomp <- newFrame compBox []

pack icomp [Expand On, Fill Both]

icBox <- newHBox icomp []

pack icBox [Expand On, Fill Both]

(SAL (SBF { selAllEv = selectAllAxs

, deselAllEv = deselectAllAxs

, sbf_btns = axsBtns

, sbf_btnFrame = 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

, sbf_btns = 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 # HTk.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

enableWidsUponSelection lb goalSpecificWids

pack main [Expand On, Fill Both]

putWinOnTop main

let updateStatusSublogic s = do

sWithSel <- (updateStateGetSelectedSens s lbAxs lbThs >>=

(\ si -> updateStateGetSelectedGoals si 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 isOpenGoal (_,st) =

let thst = thmStatus st

in if null thst

then True

else case maximum $ map snd $ thst of

BasicProof _ pst ->

case goalStatus pst of

Open -> True

_ -> False

_ -> False

mapM_ (\ i -> selection i lb)

(findIndices isOpenGoal $ 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_ (\ i -> selection i lbAxs) $

maybe [] (filter (isNotFormerTheorem . (!!) axiomList)) sel

s' <- updateStatusSublogic s

Conc.putMVar stateMVar s'

done)

+> (deselectAllGoals >>> do

doSelectAllEntries False lb

disableWids 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 (\ s ->

doSelectProverPath s 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

putStrLn "fineGrainedSelection returned Nothing"

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

putStrLn "proveF returned Nothing"

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 >>= (\ mmt ->

let err s = fail $ "ProofManagementGUI: ("++s++") MVar must be "++

"filled with Nothing when entering proofManagementGUI"

in do

maybe (err "not filled")

(maybe (err "filled with Nothing")

(const $ Conc.putMVar guiMVar Nothing))

mmt)

-- 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 {Result.diags = accDiags s,

Result.maybeResult =

Just (G_theory lidT sigT indT

(Map.union sensT gMap) startThId)

}

)