>>= recalculateSublogicF prGuiAcs)
state <- newMVar initState
window <- xmlGetWidget xml castToWindow "ProverGUI"
btnShowTheory <- xmlGetWidget xml castToButton "btnShowTheory"
btnShowSelectedTheory <- xmlGetWidget xml castToButton "btnShowSelected"
btnClose <- xmlGetWidget xml castToButton "btnClose"
trvGoals <- xmlGetWidget xml castToTreeView "trvGoals"
btnGoalsAll <- xmlGetWidget xml castToButton "btnGoalsAll"
btnGoalsNone <- xmlGetWidget xml castToButton "btnGoalsNone"
btnGoalsInvert <- xmlGetWidget xml castToButton "btnGoalsInvert"
btnGoalsSelectOpen <- xmlGetWidget xml castToButton "btnGoalsSelectOpen"
trvAxioms <- xmlGetWidget xml castToTreeView "trvAxioms"
btnAxiomsAll <- xmlGetWidget xml castToButton "btnAxiomsAll"
btnAxiomsNone <- xmlGetWidget xml castToButton "btnAxiomsNone"
btnAxiomsInvert <- xmlGetWidget xml castToButton "btnAxiomsInvert"
btnAxiomsFormer <- xmlGetWidget xml castToButton "btnAxiomsFormer"
trvTheorems <- xmlGetWidget xml castToTreeView "trvTheorems"
btnTheoremsAll <- xmlGetWidget xml castToButton "btnTheoremsAll"
btnTheoremsNone <- xmlGetWidget xml castToButton "btnTheoremsNone"
btnTheoremsInvert <- xmlGetWidget xml castToButton "btnTheoremsInvert"
btnDisplay <- xmlGetWidget xml castToButton "btnDisplay"
btnProofDetails <- xmlGetWidget xml castToButton "btnProofDetails"
btnProve <- xmlGetWidget xml castToButton "btnProve"
btnDisprove <- xmlGetWidget xml castToButton "btnDisprove"
cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"
lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"
trvProvers <- xmlGetWidget xml castToTreeView "trvProvers"
windowSetTitle window $ "Prove: " ++ thName
axioms <- axiomMap initState
listProvers <- setListData trvProvers pName []
listGoals <- setListData trvGoals showGoal $ toGoals initState
listAxioms <- setListData trvAxioms id $ toAxioms axioms
listTheorems <- setListData trvTheorems id $ toTheorem initState
-- setup comorphism combobox
comboBoxSetModelText cbComorphism
shC <- after cbComorphism changed
$ setSelectedComorphism trvProvers listProvers cbComorphism
shP <- setListSelectorSingle trvProvers $ modifyMVar_ state
$ setSelectedProver trvProvers listProvers cbComorphism shC
shA <- setListSelectorMultiple trvAxioms btnAxiomsAll btnAxiomsNone
btnAxiomsInvert $ modifyMVar_ state
$ setSelectedAxioms trvAxioms listAxioms
onClicked btnAxiomsFormer $ do
sel <- treeViewGetSelection trvAxioms
treeSelectionSelectAll sel
rs <- treeSelectionGetSelectedRows sel
mapM_ ( \ p@(row:[]) -> do
i <- listStoreGetValue listAxioms row
(if wasTheorem $ fromJust $
OMap.lookup (stripPrefixAxiom i) axioms
then treeSelectionUnselectPath else treeSelectionSelectPath) sel p) rs
modifyMVar_ state $ setSelectedAxioms trvAxioms listAxioms
setListSelectorMultiple trvTheorems btnTheoremsAll btnTheoremsNone
btnTheoremsInvert $ modifyMVar_ state
$ setSelectedTheorems trvTheorems listTheorems
let noProver = [ toWidget btnProve
noAxiom = [ toWidget btnAxiomsAll
, toWidget btnAxiomsInvert
, toWidget btnAxiomsFormer ]
noTheory = [ toWidget btnTheoremsAll
, toWidget btnTheoremsNone
, toWidget btnTheoremsInvert ]
noGoal = [ toWidget btnGoalsAll
, toWidget btnGoalsInvert
, toWidget btnGoalsSelectOpen ]
prove = noProver ++ noAxiom ++ noTheory ++ noGoal ++
, toWidget btnShowSelectedTheory
, toWidget btnProofDetails
s <- setSelectedProver trvProvers listProvers cbComorphism shC
=<< updateProver trvProvers listProvers
=<< updateSublogic lblSublogic prGuiAcs knownProvers
=<< setSelectedGoals trvGoals listGoals s'
(isJust (selectedProver s) && not (null $ selectedGoals s))
activate noGoal (not $
Map.null $ goalMap initState)
activate noAxiom (not $
Map.null axioms)
activate noTheory (not $
Map.null $ goalMap initState)
shG <- setListSelectorMultiple trvGoals btnGoalsAll btnGoalsNone
btnGoalsInvert $ modifyMVar_ state update
onClicked btnGoalsSelectOpen $ do
sel <- treeViewGetSelection trvGoals
treeSelectionSelectAll sel
rs <- treeSelectionGetSelectedRows sel
mapM_ ( \ p@(row:[]) -> do
g <- listStoreGetValue listGoals row
(if gStatus g == GOpen || gStatus g == GTimeout
then treeSelectionSelectPath else treeSelectionUnselectPath) sel p) rs
onClicked btnClose $ widgetDestroy window
onClicked btnShowTheory $ displayTheoryWithWarning "Theory" thName warn th
onClicked btnShowSelectedTheory $ readMVar state >>=
displayTheoryWithWarning "Selected Theory" thName warn . selectedTheory
onClicked btnDisplay $ readMVar state >>= displayGoals
onClicked btnProofDetails $ forkIO_ $ readMVar state >>= doShowProofDetails
-- TODO implement disprove function on ONE GOAL only
-- call consistencyCheck on negated selected sentence
-- if consistent, mark node DISPROVED and write back into dgraph
-- maybe disable button if more than one goal selected
onClicked btnDisprove $ do
selGoal <- getSelectedMultiple trvGoals listGoals
[(_, g)] -> infoDialog "Disprove selected goal"
"currently being implemented. please wait."
-- selectedCM <- comboBoxGetActive cbComorphism
-- disproveNode cbComorphism (gName g) node 10
_ -> infoDialog "Disprove selected goal"
"please select one goal only!"
forkIOWithPostProcessing (proveF prGuiAcs s')
Nothing -> errorDialog "Error" (showRelDiags 2 ds) >> return s'
updateGoals trvGoals listGoals s
putMVar state =<< update s { proverRunning = False
, accDiags = accDiags s ++ ds }
onDestroy window $ putMVar wait ()
selectAllRows trvTheorems
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
-- | 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
sens' <- coerceThSens (logicId s) lid1 "" sens
textView ("Selected Goals from Theory " ++ thName) (goalsText sens')
updateComorphism :: TreeView -> ListStore GProver -> ComboBox
-> ConnectId ComboBox -> IO ()
updateComorphism view list cbComorphism sh = do
model <- comboBoxGetModelText cbComorphism
mfinder <- getSelectedSingle view list
mapM_ (comboBoxAppendText cbComorphism) $ expand f
comboBoxSetActive cbComorphism $ selected f
expand :: GProver -> [String]
expand = map show . comorphism
setSelectedComorphism :: TreeView -> ListStore GProver -> ComboBox -> IO ()
setSelectedComorphism view list cbComorphism = do
mfinder <- getSelectedSingle view list
sel <- comboBoxGetActive cbComorphism
listStoreSetValue list i f { selected = sel }
updateSublogic :: Label -> ProofActions lid sentence
-> IO (ProofState lid sentence)
updateSublogic lbl prGuiAcs knownProvers s' = do
s <- recalculateSublogicF prGuiAcs s' { proversMap = knownProvers }
labelSetLabel lbl $ show $ sublogicOfTheory s
updateProver :: TreeView -> ListStore GProver -> ProofState lid sentence
-> IO (ProofState lid sentence)
updateProver trvProvers listProvers s = do
old <- listStoreToList listProvers
let prvs = map (\ p -> case find ((pName p ==) . pName) old of
Just p' -> let oldC = comorphism p' !! selected p' in
p { selected = fromMaybe 0 $ findIndex (== oldC) $ comorphism p }
updateListData listProvers prvs
Just p -> case findIndex ((p ==) . pName) prvs of
sel <- treeViewGetSelection trvProvers
treeSelectionSelectPath sel [i]
Nothing -> selectFirst trvProvers
Nothing -> selectFirst trvProvers
updateGoals :: TreeView -> ListStore Goal -> ProofState lid sentence -> IO ()
updateGoals trvGoals listGoals s = do
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]
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
-- | 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]
map (\ (k,s) -> if wasTheorem s then "(Th) " ++ k else k) .
OMap.toListtoGoals :: ProofState lid sentence -> [Goal]
where toGoal (n, st) = let ts = thmStatus st in
, gStatus = if null ts then GOpen
else basicProofToGStatus $ maximum $ map snd ts }
toTheorem :: ProofState lid sentence -> [String]
toProvers :: ProofState lid sentence -> [GProver]
toProvers =
Map.elems . foldr (\ (p', c) m ->
Map.insert n (p { comorphism = c : comorphism p}) m