{- |
Module      :  ./GUI/GtkGenericATP.hs
Description :  Gtk Generic Prover GUI.
Copyright   :  (c) Thiemo Wiedemeyer, Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  raider@informatik.uni-bremen.de
Stability   :  provisional
Portability :  needs POSIX

Generic Gtk GUI for automatic theorem provers.
-}

module GUI.GtkGenericATP ( genericATPgui ) where

import Graphics.UI.Gtk
import Graphics.UI.Gtk.Glade

import GUI.GtkUtils
import qualified GUI.Glade.GenericATP as GenericATP

import Interfaces.GenericATPState

import Control.Concurrent (forkIO, killThread, yield)
import Control.Concurrent.MVar
import Control.Monad (unless, when)

import Common.AS_Annotation as AS_Anno
import Common.GtkGoal
import Common.Result
import Common.Utils (getEnvSave, readMaybe)

import Proofs.BatchProcessing

import Data.List
import Data.Maybe (fromMaybe, fromJust)
import qualified Data.Map as Map

import Logic.Prover

genericATPgui :: (Ord proof_tree, Ord sentence)
              => ATPFunctions sign sentence mor proof_tree pst
              -- ^ prover specific functions
              -> Bool -- ^ prover supports extra options
              -> String -- ^ prover name
              -> String -- ^ theory name
              -> Theory sign sentence proof_tree {- ^ theory consisting of a
                 signature and a list of Named sentence -}
              -> [FreeDefMorphism sentence mor] -- ^ freeness constraints
              -> proof_tree -- ^ initial empty proof_tree
              -> IO [ProofStatus proof_tree] -- ^ proof status for each goal
genericATPgui atpFun hasEOptions prName thName th freedefs pt = do
  result <- newEmptyMVar
  postGUIAsync $ do
    xml <- getGladeXML GenericATP.get
    -- get objects
    window <- xmlGetWidget xml castToWindow "GenericATP"
    -- buttons at buttom
    btnClose <- xmlGetWidget xml castToButton "btnClose"
    btnHelp <- xmlGetWidget xml castToButton "btnHelp"
    btnSaveConfig <- xmlGetWidget xml castToButton "btnSaveConfig"
    -- goal list
    trvGoals <- xmlGetWidget xml castToTreeView "trvGoals"
    -- options area
    sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"
    entryOptions <- xmlGetWidget xml castToEntry "entryOptions"
    cbIncludeProven <- xmlGetWidget xml castToCheckButton "cbIncludeProven"
    cbSaveBatch <- xmlGetWidget xml castToCheckButton "cbSaveBatch"
    -- prove buttons
    btnStop <- xmlGetWidget xml castToButton "btnStop"
    btnProveSelected <- xmlGetWidget xml castToButton "btnProveSelected"
    btnProveAll <- xmlGetWidget xml castToButton "btnProveAll"
    -- status and axioms
    lblStatus <- xmlGetWidget xml castToLabel "lblStatus"
    trvAxioms <- xmlGetWidget xml castToTreeView "trvAxioms"
    -- info and save buttons
    btnSaveProblem <- xmlGetWidget xml castToButton "btnSaveProblem"
    btnShowDetails <- xmlGetWidget xml castToButton "btnShowDetails"

    windowSetTitle window $ prName ++ ": " ++ thName

    let widgets = [toWidget entryOptions | hasEOptions] ++
                  [ toWidget btnClose , toWidget btnShowDetails
                  , toWidget btnHelp , toWidget btnSaveConfig
                  , toWidget sbTimeout
                  , toWidget cbIncludeProven , toWidget btnProveSelected
                  , toWidget btnProveSelected, toWidget btnProveAll
                  , toWidget lblStatus , toWidget btnSaveProblem ]
        switch = activate widgets
        switchAll b = do
          activate widgets b
          widgetSetSensitive btnStop $ not b

        -- setting up state
        initState = initialGenericState prName (initialProverState atpFun)
                      (atpTransSenName atpFun) th freedefs pt
        initGoals = goalsList initState

    stateMVar <- newMVar initState
    threadId <- newEmptyMVar
    finished <- newEmptyMVar

    -- setting up lists
    listGoals <- setListData trvGoals showGoal $ toGoals initState
    listAxioms <- setListData trvAxioms id []

    -- short update function
    let update' s = update s trvGoals listGoals listAxioms lblStatus sbTimeout
                           entryOptions
        save s = saveConfigCurrent s pt prName sbTimeout entryOptions

    -- set list selector and action
    setListSelectorSingle trvAxioms $ return ()
    setListSelectorSingle trvGoals $ do
      s'' <- takeMVar stateMVar
      -- saving options for previous selected goal
      s' <- save s''
      -- setting new selected goal
      mSelected <- getSelectedSingle trvGoals listGoals
      let s = maybe s' (\ (_, Goal { gName = n }) -> s' { currentGoal = Just n})
                    mSelected
      putMVar stateMVar s
      update' s

    -- setting options
    spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit
    widgetSetSensitive entryOptions hasEOptions
    widgetSetSensitive btnStop False
    enableSaveBatch <- getEnvSave False "HETS_ENABLE_BATCH_SAVE" readMaybe
    widgetSetSensitive cbSaveBatch enableSaveBatch

    -- setting save button name
    let ext = case problemOutput $ fileExtensions atpFun of
                e@('.' : _) -> e
                e -> '.' : e
    buttonSetLabel btnSaveProblem $ "Save " ++ tail ext ++ " File"

    -- bindings
    onClicked btnHelp $
      textView (prName ++ " Help") (proverHelpText atpFun) Nothing

    -- save config
    onClicked btnSaveConfig $ do
      state <- readMVar stateMVar
      -- save actual config
      s <- save state
      let cfgText = show $ printCfgText $ configsMap s
      textView (prName ++ " Configuration for Theory " ++ thName) cfgText
               $ Just $ thName ++ theoryConfiguration (fileExtensions atpFun)

    -- save problem output
    onClicked btnSaveProblem $ do
      state <- readMVar stateMVar
      -- save actual config
      s <- save state
      maybe (return ()) (\ g -> do
          inclProven <- toggleButtonGetActive cbIncludeProven
          let (nGoal, lp') = prepareLP (proverState s) s g inclProven
          prob <- goalOutput atpFun lp' nGoal $ createProverOptions atpFun
                    $ getConfig prName g pt $ configsMap s
          textView (prName ++ " Problem for Goal " ++ g) prob
            $ Just (thName ++ '_' : g ++ ext)
        ) $ currentGoal s

    -- show details of selected goal
    onClicked btnShowDetails $ do
      s <- readMVar stateMVar
      case currentGoal s of
        Nothing -> errorDialog "Error" "Please select a goal first."
        Just g -> do
          let res = Map.lookup g $ configsMap s
              output = maybe ["This goal hasn't been run through the prover."]
                             resultOutput res
              detailsText = concatMap ('\n' :) output
          textView (prName ++ " Output for Goal " ++ g)
            (seq (length detailsText) detailsText) $ Just $ g ++ ext

    -- show details of selected goal
    onClicked btnStop $ do
      tryTakeMVar threadId >>= maybe (error "MVar 'tId' not set") killThread
      putMVar finished ()

    -- show details of selected goal
    onClicked btnProveSelected $ do
      state <- takeMVar stateMVar
      -- save actual config
      s <- save state
      case currentGoal s of
        Nothing -> error "No goal selected."
        Just g -> do
          (_, exit) <- pulseBar "Proving" g
          inclProven <- toggleButtonGetActive cbIncludeProven
          let (nGoal, lp') = prepareLP (proverState s) s g inclProven
              cfg = configsMap s
          switch False
          forkIOWithPostProcessing
            (runProver atpFun lp' (getConfig prName g pt cfg) False thName nGoal)
            $ \ (retval, cfg') -> do
              case retval of
                ATPError m -> errorDialog "Error" m
                _ -> return ()
              let s' = s { configsMap = adjustOrSetConfig (\ c -> c
                           { timeLimitExceeded = isTimeLimitExceeded retval
                           , proofStatus = (proofStatus cfg')
                             { usedTime = timeUsed cfg' }
                           , resultOutput = resultOutput cfg'
                           , timeUsed = timeUsed cfg' }) prName g pt cfg }
              putMVar stateMVar s'
              updateGoals s' trvGoals listGoals
              exit
              switch True

    -- show details of selected goal
    onClicked btnProveAll $ do
      state <- readMVar stateMVar
      -- save actual config
      s <- save state
      let openGoalsMap = filterOpenGoals $ configsMap s
          numGoals = Map.size openGoalsMap
      if Map.null openGoalsMap then
        infoDialog "No open goals" "No open goals, nothing to do."
        else do
        timeout <- spinButtonGetValueAsInt sbTimeout
        opts' <- entryGetText entryOptions
        saveBatch <- toggleButtonGetActive cbSaveBatch
        inclProven <- toggleButtonGetActive cbIncludeProven
        (updat, exit) <- progressBar "Proving" "please wait..."
        let firstGoalName = head $ filter (`Map.member` openGoalsMap)
                              $ map AS_Anno.senAttr $ goalsList s
            opts = words opts'
            afterEachProofAttempt gPSF nSen nextSen cfg@(retval, _) = do
              cont <- goalProcessed stateMVar timeout opts numGoals prName
                                    gPSF nSen False cfg
              postGUISync $ do
                case retval of
                  ATPError m -> errorDialog "Error" m
                  _ -> return ()
                s' <- readMVar stateMVar
                updateGoals s' trvGoals listGoals
                let progress = fromIntegral gPSF / fromIntegral numGoals
                when cont $ updat progress $ AS_Anno.senAttr $ fromJust nextSen
                return cont
        updat 0 firstGoalName
        tid <- forkIO $ do
          yield
          genericProveBatch False timeout opts inclProven saveBatch
            afterEachProofAttempt (atpInsertSentence atpFun) (runProver atpFun)
            prName thName s Nothing
          b <- isEmptyMVar threadId
          unless b $ putMVar finished ()
        b <- tryPutMVar threadId tid
        unless b $ error "MVar 'threadId' already set"
        switchAll False
        forkIO_ $ do
          takeMVar finished
          tryTakeMVar threadId
          postGUIAsync $ do
            switchAll True
            exit

    onClicked btnClose $ widgetDestroy window

    -- read proofstate and store it in mvar
    onDestroy window $ do
      s <- takeMVar stateMVar
      let Result _ prst = revertRenamingOfLabels s $
            map ((\ g -> let res = Map.lookup g $ configsMap s
                             g' = Map.findWithDefault
                                    (error $ "Lookup of name failed: (1) " ++
                                           "should not happen \"" ++ g ++ "\"")
                                    g $ namesMap s
                  in maybe (openProofStatus g' prName $ currentProofTree s)
                           proofStatus res) . AS_Anno.senAttr) (goalsList s)
      putMVar result prst

    if null initGoals then do
        errorDialog "No goals available!" "No need to start prove window!"
        widgetDestroy window
      else do
        selectFirst trvGoals
        widgetShow window

  -- waiting for results
  res <- takeMVar result
  maybe (fail "reverse translation of names failed") return res

  where
    prepareLP prS s g' inclProven =
      let goals = goalsList s
          cfg = configsMap s
          idx = fromMaybe (error "Goal not found!")
                  $ findIndex ((== g') . AS_Anno.senAttr) goals
          (beforeThis, afterThis) = splitAt idx goals
          g = head afterThis -- Why use head and not goal?
          proved = filter (checkGoal cfg . AS_Anno.senAttr) beforeThis
      in if inclProven
        then (g, foldl (\ lp provedGoal -> atpInsertSentence atpFun lp
                            (provedGoal { AS_Anno.isAxiom = True }))
                          prS $ reverse proved)
        else (g, prS)

saveConfigCurrent :: (Ord proof_tree)
                  => GenericState sentence proof_tree pst -> proof_tree
                  -> String -> SpinButton -> Entry
                  -> IO (GenericState sentence proof_tree pst)
saveConfigCurrent s pt prName sbTimeout entryOptions = do
  -- saving options for previous selected goal
  timeout <- spinButtonGetValueAsInt sbTimeout
  opts <- entryGetText entryOptions
  let mn = currentGoal s
      cfg = maybe (configsMap s) (\ g ->
              adjustOrSetConfig (setExtraOpts $ words opts) prName g pt
                $ adjustOrSetConfig (setTimeLimit timeout) prName g pt
                $ configsMap s) mn
  return $ s { configsMap = cfg }

updateGoals :: GenericState sentence proof_tree pst -> TreeView
            -> ListStore Goal -> IO ()
updateGoals s trvGoals listGoals = do
  let ng = toGoals s
  selected <- getSelectedSingle trvGoals listGoals
  updateListData listGoals ng
  case selected of
    Just (_, Goal { gName = n }) -> do
      selector <- treeViewGetSelection trvGoals
      treeSelectionSelectPath selector
        [fromMaybe (error "Goal not found!") $ findIndex ((n ==) . gName) ng]
    Nothing -> return ()

-- | Updates the display of the status of the current goal.
update :: GenericState sentence proof_tree pst -> TreeView
       -> ListStore Goal -> ListStore String -> Label -> SpinButton -> Entry
       -> IO ()
update s trvGoals listGoals listAxioms lblStatus sbTimeout entryOptions = do
  -- update status and axioms
  selected <- getSelectedSingle trvGoals listGoals
  case selected of
    Just (_, Goal { gName = n, gStatus = stat }) -> do
      let cfg = Map.findWithDefault (error "GUI.GenericATP.updateDisplay") n
                  $ configsMap s
      spinButtonSetValue sbTimeout $ fromIntegral
        $ fromMaybe guiDefaultTimeLimit $ timeLimit cfg
      entrySetText entryOptions $ unwords $ extraOpts cfg
      labelSetLabel lblStatus $ show stat
      updateListData listAxioms $ usedAxioms $ proofStatus cfg
    Nothing -> return ()

-- | Utility function to set the time limit of a Config.
setTimeLimit :: Int -> GenericConfig proof_tree -> GenericConfig proof_tree
setTimeLimit n c = c { timeLimit = if n > 0 then Just n else Nothing }

-- | Utility function to set the extra options of a Config.
setExtraOpts :: [String] -> GenericConfig proof_tree -> GenericConfig proof_tree
setExtraOpts opts c = c { extraOpts = opts }

toGoals :: GenericState sentence proof_tree pst -> [Goal]
toGoals s = sort $ map (\ g ->
  let n = AS_Anno.senAttr g
      c = Map.findWithDefault (error "Config not found!") n $ configsMap s
  in Goal { gName = n, gStatus = genericConfigToGStatus c }) $ goalsList s
