content: {- |
  Module      :  ./GUI/GtkProverGUI.hs
  Description :  Gtk GUI for the prover
  Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  raider@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  This module provides a GUI for the prover.
  -}
  
  module GUI.GtkProverGUI ( showProverGUI ) where
  
  import Graphics.UI.Gtk
  
  import GUI.GtkUtils
  import qualified GUI.Glade.ProverGUI as ProverGUI
  import GUI.HTkProofDetails -- not implemented in Gtk
  
  import Common.AS_Annotation as AS_Anno
  import qualified Common.Doc as Pretty
  import Common.Result
  import qualified Common.OrderedMap as OMap
  import Common.ExtSign
  import Common.GtkGoal
  import Common.Utils
  
  import Control.Concurrent.MVar
  
  import Proofs.AbstractState
  
  import Logic.Comorphism
  import Logic.Logic
  import Logic.Prover
  
  import qualified Comorphisms.KnownProvers as KnownProvers
  
  import Static.GTheory
  
  import qualified Data.Map as Map
  import Data.List
  import Data.Maybe (fromMaybe, isJust )
  
  data GProver = GProver
    { pName :: String
    , comorphism :: [AnyComorphism]
    , selected :: Int }
  
  -- ProverGUI
  
  -- | Displays the consistency checker window
  showProverGUI :: ProofActions -- ^ record of possible GUI actions
    -> String -- ^ theory name
    -> String -- ^ warning information
    -> G_theory -- ^ theory
    -> KnownProvers.KnownProversMap -- ^ map of known provers
    -> [(G_prover, AnyComorphism)]
       -- ^ list of suitable comorphisms to provers for sublogic of G_theory
    -> IO (Result G_theory)
  showProverGUI prGuiAcs thName warn th knownProvers comorphList = do
    initState <- recalculateSublogicF prGuiAcs
      (initialState thName th knownProvers)
      { comorphismsToProvers = comorphList }
    state <- newMVar initState
    wait <- newEmptyMVar
    postGUIAsync $ do
      builder <- getGTKBuilder ProverGUI.get
      -- get objects
      window <- builderGetObject builder castToWindow "ProverGUI"
      -- buttons at buttom
      btnShowTheory <- builderGetObject builder castToButton "btnShowTheory"
      btnShowSelectedTheory <- builderGetObject builder castToButton "btnShowSelected"
      btnClose <- builderGetObject builder castToButton "btnClose"
      -- goals view
      trvGoals <- builderGetObject builder castToTreeView "trvGoals"
      btnGoalsAll <- builderGetObject builder castToButton "btnGoalsAll"
      btnGoalsNone <- builderGetObject builder castToButton "btnGoalsNone"
      btnGoalsInvert <- builderGetObject builder castToButton "btnGoalsInvert"
      btnGoalsSelectOpen <- builderGetObject builder castToButton "btnGoalsSelectOpen"
      -- axioms view
      trvAxioms <- builderGetObject builder castToTreeView "trvAxioms"
      btnAxiomsAll <- builderGetObject builder castToButton "btnAxiomsAll"
      btnAxiomsNone <- builderGetObject builder castToButton "btnAxiomsNone"
      btnAxiomsInvert <- builderGetObject builder castToButton "btnAxiomsInvert"
      btnAxiomsFormer <- builderGetObject builder castToButton "btnAxiomsFormer"
      -- theorems view
      trvTheorems <- builderGetObject builder castToTreeView "trvTheorems"
      btnTheoremsAll <- builderGetObject builder castToButton "btnTheoremsAll"
      btnTheoremsNone <- builderGetObject builder castToButton "btnTheoremsNone"
      btnTheoremsInvert <- builderGetObject builder castToButton "btnTheoremsInvert"
      -- status
      btnDisplay <- builderGetObject builder castToButton "btnDisplay"
      btnProofDetails <- builderGetObject builder castToButton "btnProofDetails"
      btnProve <- builderGetObject builder castToButton "btnProve"
      cbComorphism <- builderGetObject builder castToComboBox "cbComorphism"
      lblSublogic <- builderGetObject builder castToLabel "lblSublogic"
      -- prover
      trvProvers <- builderGetObject builder castToTreeView "trvProvers"
  
      windowSetTitle window $ "Prove: " ++ thName
  
      -- set list data
      listProvers <- setListData trvProvers pName []
      listGoals <- setListData trvGoals showGoal $ toGoals initState
      listAxioms <- setListData trvAxioms id $ toAxioms initState
      listTheorems <- setListData trvTheorems id $ selectedGoals initState
  
      -- setup comorphism combobox
      comboBoxSetModelText cbComorphism
      shC <- after cbComorphism changed $ modifyMVar_ state
        $ setSelectedComorphism trvProvers listProvers cbComorphism
  
      -- setup provers list
      shP <- setListSelectorSingle trvProvers $ modifyMVar_ state
        $ setSelectedProver trvProvers listProvers cbComorphism shC
  
      -- setup axioms list
      shA <- setListSelectorMultiple trvAxioms btnAxiomsAll btnAxiomsNone
        btnAxiomsInvert $ modifyMVar_ state
        $ setSelectedAxioms trvAxioms listAxioms
  
      onClicked btnAxiomsFormer $ do
        signalBlock shA
        sel <- treeViewGetSelection trvAxioms
        treeSelectionSelectAll sel
        rs <- treeSelectionGetSelectedRows sel
        mapM_ ( \ ~p@(row : []) -> do
          i <- listStoreGetValue listAxioms row
          (if wasATheorem initState (stripPrefixAxiom i)
            then treeSelectionUnselectPath else treeSelectionSelectPath) sel p) rs
        signalUnblock shA
        modifyMVar_ state $ setSelectedAxioms trvAxioms listAxioms
  
     -- setup theorems list
      setListSelectorMultiple trvTheorems btnTheoremsAll btnTheoremsNone
        btnTheoremsInvert $ modifyMVar_ state
        $ setSelectedTheorems trvTheorems listTheorems
  
      let noProver = [ toWidget btnProve
                     , toWidget cbComorphism
                     , toWidget lblSublogic ]
          noAxiom = [ toWidget btnAxiomsAll
                    , toWidget btnAxiomsNone
                    , toWidget btnAxiomsInvert
                    , toWidget btnAxiomsFormer ]
          noTheory = [ toWidget btnTheoremsAll
                     , toWidget btnTheoremsNone
                     , toWidget btnTheoremsInvert ]
          noGoal = [ toWidget btnGoalsAll
                   , toWidget btnGoalsNone
                   , toWidget btnGoalsInvert
                   , toWidget btnGoalsSelectOpen ]
          prove = [toWidget window]
          update s' = do
            signalBlock shP
            s <- setSelectedProver trvProvers listProvers cbComorphism shC
              =<< updateProver trvProvers listProvers
              =<< updateSublogic lblSublogic prGuiAcs knownProvers
              =<< setSelectedGoals trvGoals listGoals s'
            signalUnblock shP
            activate noProver
              (isJust (selectedProver s) && not (null $ selectedGoals s))
            return s
          hasGoals = not . null $ selectedGoals initState
      activate noGoal hasGoals
      activate noAxiom (not . null $ includedAxioms initState)
      activate noTheory hasGoals
  
      -- setup goal list
      shG <- setListSelectorMultiple trvGoals btnGoalsAll btnGoalsNone
        btnGoalsInvert $ modifyMVar_ state update
  
      onClicked btnGoalsSelectOpen $ do
        signalBlock shG
        sel <- treeViewGetSelection trvGoals
        treeSelectionSelectAll sel
        rs <- treeSelectionGetSelectedRows sel
        mapM_ ( \ ~p@(row : []) -> do
          g <- listStoreGetValue listGoals row
          (if gStatus g `elem` [GOpen, GTimeout]
            then treeSelectionSelectPath else treeSelectionUnselectPath) sel p) rs
        signalUnblock shG
        modifyMVar_ state update
  
      -- button bindings
      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
  
      onClicked btnProve $ do
        modifyMVar_ state update
        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
    return Result
      { diags = accDiags s
      , maybeResult = Just $ currentTheory s }
  
  -- | Called whenever the button "Display" is clicked.
  displayGoals :: ProofState -> IO ()
  displayGoals s = case currentTheory s of
    G_theory lid1 _ (ExtSign sig1 _) _ sens1 _ -> do
      let thName = theoryName s
          goalsText = show . Pretty.vsep
            . map (print_named lid1 . AS_Anno.mapNamed (simplify_sen lid1 sig1))
            . toNamedList $ filterMapWithList (selectedGoals s) sens1
      textView ("Selected Goals from Theory " ++ thName) goalsText
               $ 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 -> [ComboBoxText]
  expand = toComboBoxText . comorphism
  
  setSelectedComorphism :: TreeView -> ListStore GProver -> ComboBox -> ProofState
    -> IO ProofState
  setSelectedComorphism view list cbComorphism s = do
    mfinder <- getSelectedSingle view list
    case mfinder of
      Just (i, f) -> do
        sel <- comboBoxGetActive cbComorphism
        let nf = f { selected = sel }
        listStoreSetValue list i nf
        return $ setGProver nf s
      Nothing -> return s
  
  setGProver :: GProver -> ProofState -> ProofState
  setGProver f s =
    let pn = pName f
        c = comorphism f !! selected f
    in s
    { selectedProver = Just pn
    , proversMap = Map.insert pn [c] $ proversMap s}
  
  updateSublogic :: Label -> ProofActions
                 -> KnownProvers.KnownProversMap -> ProofState
                 -> IO ProofState
  updateSublogic lbl prGuiAcs knownProvers s' = do
    s <- recalculateSublogicF prGuiAcs s'
      { proversMap = Map.unionWith (++) (proversMap s') knownProvers }
    labelSetLabel lbl $ show $ sublogicOfTheory s
    return s
  
  updateProver :: TreeView -> ListStore GProver -> ProofState
               -> IO ProofState
  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 $ elemIndex 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 -> 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
                   -> IO ProofState
  setSelectedGoals trvGoals listGoals s = do
    goals <- getSelectedMultiple trvGoals listGoals
    return s { selectedGoals = map (gName . snd) goals }
  
  setSelectedAxioms :: TreeView -> ListStore String -> ProofState
                    -> IO ProofState
  setSelectedAxioms axs listAxs s = do
    axioms <- getSelectedMultiple axs listAxs
    return s { includedAxioms = map (stripPrefixAxiom . snd) axioms }
  
  setSelectedTheorems :: TreeView -> ListStore String -> ProofState
                      -> IO ProofState
  setSelectedTheorems ths listThs s = do
    theorems <- getSelectedMultiple ths listThs
    return s { includedTheorems = map snd theorems }
  
  stripPrefixAxiom :: String -> String
  stripPrefixAxiom a = tryToStripPrefix "(Th) " a
  
  -- | Called whenever a prover is selected from the "Pick Theorem Prover" list.
  setSelectedProver :: TreeView -> ListStore GProver -> ComboBox
                    -> ConnectId ComboBox -> ProofState
                    -> IO ProofState
  setSelectedProver trvProvers listProvers cbComorphism shC s = do
    mprover <- getSelectedSingle trvProvers listProvers
    updateComorphism trvProvers listProvers cbComorphism shC
    return $ case mprover of
      Nothing -> s { selectedProver = Nothing }
      Just (_, gp) -> setGProver gp s
  
  wasATheorem :: ProofState -> String -> Bool
  wasATheorem st i = case currentTheory st of
     G_theory _ _ _ _ sens _ -> maybe False wasTheorem $ OMap.lookup i sens
  
  toGoals :: ProofState -> [Goal]
  toGoals = sort . map toGtkGoal . getGoals
  
  toProvers :: ProofState -> [GProver]
  toProvers = Map.elems . foldr (\ (p', c) m ->
      let n = getProverName p'
          p = Map.findWithDefault (GProver n [] 0) n m in
      Map.insert n (p { comorphism = c : comorphism p}) m
    ) Map.empty . comorphismsToProvers
  