ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen{- |

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenModule : $Header$

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenDescription : Gtk GUI for the prover

723d1cf47a33d814dc2d980473060e8faf4036a2ndCopyright : (c) Thiemo Wiedemeyer, Uni Bremen 2008

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenMaintainer : raider@informatik.uni-bremen.de

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenStability : provisional

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenPortability : portable

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenThis module provides a GUI for the prover.

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen-}

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenmodule GUI.GtkProverGUI ( showProverGUI ) where

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Graphics.UI.Gtk

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Graphics.UI.Gtk.Glade

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport GUI.GtkUtils

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport GUI.GtkDisprove

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport qualified GUI.Glade.ProverGUI as ProverGUI

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport GUI.HTkProofDetails -- not implemented in Gtk

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Common.AS_Annotation as AS_Anno

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport qualified Common.Doc as Pretty

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Common.Result

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport qualified Common.OrderedMap as OMap

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Common.ExtSign

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Control.Concurrent.MVar

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Proofs.AbstractState

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Logic.Comorphism

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Logic.Logic

6bfe40590188aacf3e97bca51faa4dd027a10042rbowenimport Logic.Prover

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jimimport qualified Comorphisms.KnownProvers as KnownProvers

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Static.DevGraph (DGNodeLab)

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Static.GTheory

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport qualified Data.Map as Map

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Data.List

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Data.Maybe ( fromJust, fromMaybe, isJust )

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenimport Data.Graph.Inductive.Graph (LNode)

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowendata GProver = GProver { pName :: String

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , comorphism :: [AnyComorphism]

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen , selected :: Int }

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen{- ProverGUI -}

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen-- | Displays the consistency checker window

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowenshowProverGUI :: Logic lid sublogics basic_spec sentence symb_items

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen symb_map_items sign morphism symbol raw_symbol proof_tree

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen => lid

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> ProofActions lid sentence -- ^ record of possible GUI actions

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> String -- ^ theory name

c553c762594b98d5de7a53bf526801d0d6afacd9rbowen -> String -- ^ warning information

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim -> G_theory -- ^ theory

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> LNode DGNodeLab -- ^ node the proving is applied to

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> KnownProvers.KnownProversMap -- ^ map of known provers

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> [(G_prover,AnyComorphism)] -- ^ list of suitable comorphisms to provers

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -- for sublogic of G_theory

79ce57727aebbeb6cf8b2825f7c56a6282e688fbrbowen -> IO (Result G_theory)

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowenshowProverGUI lid prGuiAcs thName warn th node knownProvers comorphList = do

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen initState <- (initialState lid thName th knownProvers comorphList

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen >>= recalculateSublogicF prGuiAcs)

419d55842022e9e257941bfe226549661fb2c6c7humbedooh state <- newMVar initState

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh wait <- newEmptyMVar

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh postGUIAsync $ do

419d55842022e9e257941bfe226549661fb2c6c7humbedooh xml <- getGladeXML ProverGUI.get

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen -- get objects

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim window <- xmlGetWidget xml castToWindow "ProverGUI"

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim -- buttons at buttom

7408a7b242729f7e4546777b3beb2f76142b6843rbowen btnShowTheory <- xmlGetWidget xml castToButton "btnShowTheory"

7408a7b242729f7e4546777b3beb2f76142b6843rbowen btnShowSelectedTheory <- xmlGetWidget xml castToButton "btnShowSelected"

7408a7b242729f7e4546777b3beb2f76142b6843rbowen btnClose <- xmlGetWidget xml castToButton "btnClose"

7408a7b242729f7e4546777b3beb2f76142b6843rbowen -- goals view

7408a7b242729f7e4546777b3beb2f76142b6843rbowen trvGoals <- xmlGetWidget xml castToTreeView "trvGoals"

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen btnGoalsAll <- xmlGetWidget xml castToButton "btnGoalsAll"

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen btnGoalsNone <- xmlGetWidget xml castToButton "btnGoalsNone"

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen btnGoalsInvert <- xmlGetWidget xml castToButton "btnGoalsInvert"

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen btnGoalsSelectOpen <- xmlGetWidget xml castToButton "btnGoalsSelectOpen"

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen -- axioms view

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen trvAxioms <- xmlGetWidget xml castToTreeView "trvAxioms"

7a98571671f92e53441bf24a0222768072172f90coar btnAxiomsAll <- xmlGetWidget xml castToButton "btnAxiomsAll"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnAxiomsNone <- xmlGetWidget xml castToButton "btnAxiomsNone"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnAxiomsInvert <- xmlGetWidget xml castToButton "btnAxiomsInvert"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnAxiomsFormer <- xmlGetWidget xml castToButton "btnAxiomsFormer"

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen -- theorems view

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen trvTheorems <- xmlGetWidget xml castToTreeView "trvTheorems"

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen btnTheoremsAll <- xmlGetWidget xml castToButton "btnTheoremsAll"

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen btnTheoremsNone <- xmlGetWidget xml castToButton "btnTheoremsNone"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnTheoremsInvert <- xmlGetWidget xml castToButton "btnTheoremsInvert"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh -- status

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnDisplay <- xmlGetWidget xml castToButton "btnDisplay"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnProofDetails <- xmlGetWidget xml castToButton "btnProofDetails"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnProve <- xmlGetWidget xml castToButton "btnProve"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh btnDisprove <- xmlGetWidget xml castToButton "btnDisprove"

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

7a98571671f92e53441bf24a0222768072172f90coar -- prover

7a98571671f92e53441bf24a0222768072172f90coar trvProvers <- xmlGetWidget xml castToTreeView "trvProvers"

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen windowSetTitle window $ "Prove: " ++ thName

7a98571671f92e53441bf24a0222768072172f90coar

7a98571671f92e53441bf24a0222768072172f90coar axioms <- axiomMap initState

7a98571671f92e53441bf24a0222768072172f90coar

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen -- set list data

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen listProvers <- setListData trvProvers pName []

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen listGoals <- setListData trvGoals showGoal $ toGoals initState

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen listAxioms <- setListData trvAxioms id $ toAxioms axioms

419d55842022e9e257941bfe226549661fb2c6c7humbedooh listTheorems <- setListData trvTheorems id $ toTheorem initState

4e6e4fe9bb0d5a5416da0daf9784ee80dfbce58dhumbedooh

0a4691d5971ce68bc4778e4f45f1eb91118e2e5dhumbedooh -- setup comorphism combobox

fe071a5b5bed45ece47185da30a26817c42a3127humbedooh comboBoxSetModelText cbComorphism

419d55842022e9e257941bfe226549661fb2c6c7humbedooh shC <- after cbComorphism changed

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen $ setSelectedComorphism trvProvers listProvers cbComorphism

7408a7b242729f7e4546777b3beb2f76142b6843rbowen

7408a7b242729f7e4546777b3beb2f76142b6843rbowen -- setup provers list

7408a7b242729f7e4546777b3beb2f76142b6843rbowen shP <- setListSelectorSingle trvProvers $ modifyMVar_ state

7408a7b242729f7e4546777b3beb2f76142b6843rbowen $ setSelectedProver trvProvers listProvers cbComorphism shC

7408a7b242729f7e4546777b3beb2f76142b6843rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen -- setup axioms list

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen shA <- setListSelectorMultiple trvAxioms btnAxiomsAll btnAxiomsNone

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen btnAxiomsInvert $ modifyMVar_ state

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen $ setSelectedAxioms trvAxioms listAxioms

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

7408a7b242729f7e4546777b3beb2f76142b6843rbowen onClicked btnAxiomsFormer $ do

7408a7b242729f7e4546777b3beb2f76142b6843rbowen signalBlock shA

7408a7b242729f7e4546777b3beb2f76142b6843rbowen sel <- treeViewGetSelection trvAxioms

7408a7b242729f7e4546777b3beb2f76142b6843rbowen treeSelectionSelectAll sel

7408a7b242729f7e4546777b3beb2f76142b6843rbowen rs <- treeSelectionGetSelectedRows sel

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen mapM_ ( \ p@(row:[]) -> do

419d55842022e9e257941bfe226549661fb2c6c7humbedooh i <- listStoreGetValue listAxioms row

289b536921c2aae0f3eea868cdf44f25c451d5f7humbedooh (if wasTheorem $ fromJust $ OMap.lookup (stripPrefixAxiom i) axioms

524dbd8694f25703ec8eb70a57b12d701e5dbcebjailletc then treeSelectionUnselectPath else treeSelectionSelectPath) sel p) rs

15292da5451dea4ad10c12d35d9addc88be302c5humbedooh signalUnblock shA

419d55842022e9e257941bfe226549661fb2c6c7humbedooh modifyMVar_ state $ setSelectedAxioms trvAxioms listAxioms

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen -- setup theorems list

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen setListSelectorMultiple trvTheorems btnTheoremsAll btnTheoremsNone

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen btnTheoremsInvert $ modifyMVar_ state

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen $ setSelectedTheorems trvTheorems listTheorems

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen let noProver = [ toWidget btnProve

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen , toWidget cbComorphism

0321b828ccbef40f22ba06f3ae422cc19ee82b7crbowen , toWidget lblSublogic ]

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen noAxiom = [ toWidget btnAxiomsAll

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnAxiomsNone

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnAxiomsInvert

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnAxiomsFormer ]

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen noTheory = [ toWidget btnTheoremsAll

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnTheoremsNone

7408a7b242729f7e4546777b3beb2f76142b6843rbowen , toWidget btnTheoremsInvert ]

7408a7b242729f7e4546777b3beb2f76142b6843rbowen noGoal = [ toWidget btnGoalsAll

7408a7b242729f7e4546777b3beb2f76142b6843rbowen , toWidget btnGoalsNone

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnGoalsInvert

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnGoalsSelectOpen ]

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen prove = noProver ++ noAxiom ++ noTheory ++ noGoal ++

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen [ toWidget btnShowTheory

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen , toWidget btnShowSelectedTheory

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen , toWidget btnClose

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen , toWidget btnProofDetails

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen , toWidget btnDisplay ]

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen update s' = do

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen signalBlock shP

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen s <- setSelectedProver trvProvers listProvers cbComorphism shC

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen =<< updateProver trvProvers listProvers

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen =<< updateSublogic lblSublogic prGuiAcs knownProvers

419d55842022e9e257941bfe226549661fb2c6c7humbedooh =<< setSelectedGoals trvGoals listGoals s'

15292da5451dea4ad10c12d35d9addc88be302c5humbedooh signalUnblock shP

5d01f40ffd657dd2ac567aacd93cabd162ddfa79coar activate noProver

5d01f40ffd657dd2ac567aacd93cabd162ddfa79coar (isJust (selectedProver s) && not (null $ selectedGoals s))

5d01f40ffd657dd2ac567aacd93cabd162ddfa79coar return s

419d55842022e9e257941bfe226549661fb2c6c7humbedooh

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen activate noGoal (not $ Map.null $ goalMap initState)

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen activate noAxiom (not $ Map.null axioms)

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen activate noTheory (not $ Map.null $ goalMap initState)

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen -- setup goal list

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen shG <- setListSelectorMultiple trvGoals btnGoalsAll btnGoalsNone

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen btnGoalsInvert $ modifyMVar_ state update

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen onClicked btnGoalsSelectOpen $ do

6bfe40590188aacf3e97bca51faa4dd027a10042rbowen signalBlock shG

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen sel <- treeViewGetSelection trvGoals

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen treeSelectionSelectAll sel

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen rs <- treeSelectionGetSelectedRows sel

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen mapM_ ( \ p@(row:[]) -> do

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen g <- listStoreGetValue listGoals row

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen (if gStatus g == GOpen || gStatus g == GTimeout

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen then treeSelectionSelectPath else treeSelectionUnselectPath) sel p) rs

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen signalUnblock shG

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen modifyMVar_ state update

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen -- button bindings

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen onClicked btnClose $ widgetDestroy window

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen onClicked btnShowTheory $ displayTheoryWithWarning "Theory" thName warn th

d237ba65985614f0bbf2ec15098d40afa50b6e3frbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen onClicked btnShowSelectedTheory $ readMVar state >>=

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen displayTheoryWithWarning "Selected Theory" thName warn . selectedTheory

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen

ae99d131f770d4e1b6a712f947d5d0e928917a28rbowen onClicked btnDisplay $ readMVar state >>= displayGoals

onClicked btnProofDetails $ forkIO_ $ readMVar state >>= doShowProofDetails

onClicked btnDisprove $ do

selGoal <- getSelectedMultiple trvGoals listGoals

case selGoal of

[(i, g)] -> do

s' <- takeMVar state

s <- disproveThmSingle (gName g) node s' 1 $ map snd comorphList

putMVar state =<< update s

listStoreSetValue listGoals i $ fromJust $ find

(\g' -> gName g' == gName g) $ toGoals s

_ -> infoDialog "Disprove selected goal"

"please select one goal only!"

onClicked btnProve $ do

s' <- takeMVar state

activate prove False

forkIOWithPostProcessing (proveF prGuiAcs s')

$ \ (Result ds ms) -> do

s <- case ms of

Nothing -> errorDialog "Error" (showRelDiags 2 ds) >> return s'

Just res -> return res

activate prove True

signalBlock shG

updateGoals trvGoals listGoals s

signalUnblock shG

putMVar state =<< update s { proverRunning = False

, accDiags = accDiags s ++ ds }

onDestroy window $ putMVar wait ()

selectAllRows trvTheorems

selectAllRows trvAxioms

selectAllRows trvGoals

widgetShow window

_ <- takeMVar wait

s <- takeMVar state

case theory s of

G_theory lidT sigT indT sensT _ -> do

gMap <- coerceThSens (logicId s) lidT "ProverGUI last coerce" $ goalMap s

return Result { diags = accDiags s

, maybeResult = Just $ G_theory lidT sigT indT

(Map.union sensT gMap) startThId }

-- | Called whenever the button "Display" is clicked.

displayGoals :: Logic lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> ProofState lid sentence -> IO ()

displayGoals 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

textView ("Selected Goals from Theory " ++ thName) (goalsText sens')

$ Just (thName ++ "-goals.txt")

updateComorphism :: TreeView -> ListStore GProver -> ComboBox

-> ConnectId ComboBox -> IO ()

updateComorphism view list cbComorphism sh = do

signalBlock sh

model <- comboBoxGetModelText cbComorphism

listStoreClear model

mfinder <- getSelectedSingle view list

case mfinder of

Just (_, f) -> do

mapM_ (comboBoxAppendText cbComorphism) $ expand f

comboBoxSetActive cbComorphism $ selected f

Nothing -> return ()

signalUnblock sh

expand :: GProver -> [String]

expand = map show . comorphism

setSelectedComorphism :: TreeView -> ListStore GProver -> ComboBox -> IO ()

setSelectedComorphism view list cbComorphism = do

mfinder <- getSelectedSingle view list

case mfinder of

Just (i, f) -> do

sel <- comboBoxGetActive cbComorphism

listStoreSetValue list i f { selected = sel }

Nothing -> return ()

updateSublogic :: Label -> ProofActions lid sentence

-> KnownProvers.KnownProversMap -> ProofState lid sentence

-> IO (ProofState lid sentence)

updateSublogic lbl prGuiAcs knownProvers s' = do

s <- recalculateSublogicF prGuiAcs s' { proversMap = knownProvers }

labelSetLabel lbl $ show $ sublogicOfTheory s

return s

updateProver :: TreeView -> ListStore GProver -> ProofState lid sentence

-> IO (ProofState lid sentence)

updateProver trvProvers listProvers s = do

let new = toProvers s

old <- listStoreToList listProvers

let prvs = map (\ p -> case find ((pName p ==) . pName) old of

Nothing -> p

Just p' -> let oldC = comorphism p' !! selected p' in

p { selected = fromMaybe 0 $ findIndex (== oldC) $ comorphism p }

) new

updateListData listProvers prvs

case selectedProver s of

Just p -> case findIndex ((p ==) . pName) prvs of

Just i -> do

sel <- treeViewGetSelection trvProvers

treeSelectionSelectPath sel [i]

Nothing -> selectFirst trvProvers

Nothing -> selectFirst trvProvers

return s

updateGoals :: TreeView -> ListStore Goal -> ProofState lid sentence -> IO ()

updateGoals trvGoals listGoals s = do

let ng = toGoals s

sel <- getSelectedMultiple trvGoals listGoals

updateListData listGoals ng

selector <- treeViewGetSelection trvGoals

mapM_ (\ (_, Goal { gName = n }) -> treeSelectionSelectPath selector

[fromMaybe (error "Goal not found!") $ findIndex ((n ==) . gName) ng]

) sel

setSelectedGoals :: TreeView -> ListStore Goal -> ProofState lid sentence

-> IO (ProofState lid sentence)

setSelectedGoals trvGoals listGoals s = do

goals <- getSelectedMultiple trvGoals listGoals

return s { selectedGoals = map (gName . snd) goals }

setSelectedAxioms :: TreeView -> ListStore String -> ProofState lid sentence

-> IO (ProofState lid sentence)

setSelectedAxioms axs listAxs s = do

axioms <- getSelectedMultiple axs listAxs

return s { includedAxioms = map (stripPrefixAxiom . snd) axioms }

setSelectedTheorems :: TreeView -> ListStore String -> ProofState lid sentence

-> IO (ProofState lid sentence)

setSelectedTheorems ths listThs s = do

theorems <- getSelectedMultiple ths listThs

return s { includedTheorems = map snd theorems }

stripPrefixAxiom :: String -> String

stripPrefixAxiom a = case stripPrefix "(Th) " a of

Just a' -> a'

Nothing -> a

-- | Called whenever a prover is selected from the "Pick Theorem Prover" list.

setSelectedProver :: TreeView -> ListStore GProver -> ComboBox

-> ConnectId ComboBox -> ProofState lid sentence

-> IO (ProofState lid sentence)

setSelectedProver trvProvers listProvers cbComorphism shC s = do

mprover <- getSelectedSingle trvProvers listProvers

updateComorphism trvProvers listProvers cbComorphism shC

return s { selectedProver = maybe Nothing (Just . pName . snd) mprover }

toAxioms :: ThSens sentence (AnyComorphism, BasicProof) -> [String]

toAxioms =

map (\ (k,s) -> if wasTheorem s then "(Th) " ++ k else k) . OMap.toList

toGoals :: ProofState lid sentence -> [Goal]

toGoals = sort . map toGoal . OMap.toList . goalMap

where toGoal (n, st) = let ts = thmStatus st in

Goal { gName = n

, gStatus = if null ts then GOpen

else basicProofToGStatus $ maximum $ map snd ts }

toTheorem :: ProofState lid sentence -> [String]

toTheorem = OMap.keys . goalMap

toProvers :: ProofState lid sentence -> [GProver]

toProvers = Map.elems . foldr (\ (p', c) m ->

let n = getPName p'

p = Map.findWithDefault (GProver n [] 0) n m in

Map.insert n (p { comorphism = c : comorphism p}) m

) Map.empty . comorphismsToProvers