{- |
Module      :  $Header$
Description :  GUI for showing and saving proof details.
Copyright   :  (c) Rainer Grabbe 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Additional window used by 'GUI.ProofManagement' for displaying proof details.
-}

module GUI.HTkProofDetails (doShowProofDetails) where

import qualified Common.Doc as Pretty
import qualified Common.OrderedMap as OMap
import Common.AS_Annotation

import qualified Data.Map as Map
import Data.Maybe
import Data.List
import Data.IORef

import GUI.Utils (fileSaveDialog)

import System.Directory

import GUI.HTkUtils

import Proofs.AbstractState
import Logic.Comorphism
import Logic.Prover
import Static.GTheory

-- * record structures and basic functions for handling

{- |
  Record structure containing proof details for a single proof.
-}
data GoalDescription = GoalDescription {
    proverInfo :: String, -- ^ standard proof details
    tacticScriptText :: OpenText, -- ^ more details for tactic script
    proofTreeText :: OpenText -- ^ more details for proof tree
    }

{- |
  Current state of a text tag providing additional information. The text can be
  folded or unfolded.
-}
data OpenText = OpenText {
    additionalText :: String, -- ^ additional information
    textShown :: Bool, -- ^ if true, text is unfolded (default: false)
    textStartPosition :: Position -- ^ start position in editor widget
    }

{- |
  Creates an initial 'GoalDescription' filled with just the standard prover
  info.
-}
emptyGoalDescription :: String -- ^ information about the used prover
                     -> GoalDescription -- ^ initiated GoalDescription
emptyGoalDescription st =
    GoalDescription {
      proverInfo = st,
      tacticScriptText = emptyOpenText,
      proofTreeText = emptyOpenText }

{- |
  Creates an empty 'OpenText' with start position (0,0).
-}
emptyOpenText :: OpenText
emptyOpenText = OpenText {
      additionalText = "",
      textShown = False,
      textStartPosition = (Distance 0, Distance 0) }

-- | Determines the kind of content of a 'HTk.TextTag'.
data Content = TacticScriptText | ProofTreeText deriving Eq


-- * GUI for show proof details

-- ** help functions

-- | Return number of new lines in a string.
numberOfLines :: String
              -> Int
numberOfLines =
    foldr (\ ch -> if ch == '\n' then (+ 1) else id) 0

{- |
  Change the x-value of a 'Position' by a given arithmetical function and value.
-}
changePosition :: (Int -> Int -> Int)  -- ^ mostly add or subtract values
               -> Int -- ^ (difference) value
               -> Position -- ^ old position
               -> Position -- ^ changed position with new x-value
changePosition f diff (Distance posX, Distance posY) =
    (Distance $ f posX diff, Distance posY)

{- |
  Indentation of a 'String' (also multiple lines) by a number of spaces.
-}
indent :: Int -- ^ number of spaces
       -> String -- ^ input String
       -> Pretty.Doc -- ^ output document
indent numSp st =
  Pretty.text (replicate numSp ' ') Pretty.<>
    (Pretty.vcat . map Pretty.text . lines) st

{- |
  Standard indent width.
-}
stdIndent :: Int
stdIndent = 4

{- |
  An item of thmStatus will be put into 'GoalDescription' structure.
  Pretty printing of proof details, adding additional information
  for text tags.
-}
fillGoalDescription :: (AnyComorphism, BasicProof)
                    -> GoalDescription -- ^ contents in pretty format
fillGoalDescription (cmo, basicProof) =
    let gd = indent stdIndent $ show $ printCmWStat (cmo, basicProof)
        stat str = Pretty.text "Status:" Pretty.<+> Pretty.text str
        printCmWStat (c, bp) =
            Pretty.text "Com:" Pretty.<+> Pretty.text (show c)
            Pretty.$+$ indent stdIndent (show $ printBP bp)
        printBP bp = case bp of
                     BasicProof _ ps ->
                      stat (show $ goalStatus ps) Pretty.$+$
                      (case goalStatus ps of
                       Proved _ -> Pretty.text "Used axioms:" Pretty.<+>
                           Pretty.fsep (Pretty.punctuate Pretty.comma
                             $ map (Pretty.text . show) $ usedAxioms ps)
                           Pretty.$+$ Pretty.text "Used time:" Pretty.<+>
                                 Pretty.text (show $ usedTime ps)
                       _ -> Pretty.empty)
                      Pretty.$+$ Pretty.text "Prover:" Pretty.<+>
                            Pretty.text (usedProver ps)
                     otherProof -> stat (show otherProof)
        printTS bp = case bp of
                     BasicProof _ ps ->
                       indent (2 * stdIndent) $ (\ (TacticScript xs) -> xs) $
                                                tacticScript ps
                     _ -> Pretty.empty
        printPT bp = case bp of
                     BasicProof _ ps ->
                       indent (2 * stdIndent) $ show $ proofTree ps
                     _ -> Pretty.empty
    in  (emptyGoalDescription $ show gd) {
           tacticScriptText = emptyOpenText {
             additionalText = show $ printTS basicProof },
           proofTreeText = emptyOpenText {
             additionalText = show $ printPT basicProof } }

{- |
  Gets real 'EndOfText' index at the char position after (in x-direction)
  the last written text. This is because 'EndOfText' only gives a value where a
  text would be after an imaginary newline.
-}
getRealEndOfTextIndex :: Editor -- ^ the editor whose end index is determined
                      -> IO Position -- ^ position behind last char in widget
getRealEndOfTextIndex ed = do
    (Distance eotX, _) <- getIndexPosition ed EndOfText
    lineBefore <- getTextLine ed $ IndexPos (Distance (eotX - 1), 0)
    return (Distance eotX - 1, Distance $ length lineBefore)

{- |
  For a given Ordered Map containing all proof values, this function adapts the
  text positions lying behind after a given reference position. This is called
  when a position in the text is moved after clicking a text tag button.
-}
adaptTextPositions :: (Int -> Int -> Int)  -- ^ mostly add or subtract values
                   -> Int -- ^ (difference) value
                   -> Position -- ^ reference Position
                   -> OMap.OMap (String, Int) GoalDescription
                      -- ^ Map for all proofs
                   -> OMap.OMap (String, Int) GoalDescription -- ^ adapted Map
adaptTextPositions f diff pos =
    OMap.map $ \ gDesc ->
      let tst = tacticScriptText gDesc
          ptt = proofTreeText gDesc
      in gDesc {
           tacticScriptText = if textStartPosition tst > pos
               then tst { textStartPosition = changePosition f diff $
                                textStartPosition tst }
               else tst,
           proofTreeText = if textStartPosition ptt > pos
               then ptt { textStartPosition = changePosition f diff $
                                textStartPosition ptt }
               else ptt }

-- ** main GUI

{- |
  Called whenever the button /Show proof details/ is clicked.
-}
doShowProofDetails :: ProofState -> IO ()
doShowProofDetails prGUISt =
   do
    let thName = theoryName prGUISt
        winTitleStr = "Proof Details of Selected Goals from Theory " ++ thName
    win       <- createToplevel [text winTitleStr]
    bFrame    <- newFrame win [relief Groove, borderwidth (cm 0.05)]
    winTitle  <- newLabel bFrame [text winTitleStr,
                                  font (Helvetica, Roman, 18 :: Int)]
    btnBox    <- newHBox bFrame []
    tsBut     <- newButton btnBox [text expand_tacticScripts, width 18]
    ptBut     <- newButton btnBox [text expand_proofTrees, width 18]
    sBut      <- newButton btnBox [text "Save", width 12]
    qBut      <- newButton btnBox [text "Close", width 12]
    pack winTitle [Side AtTop, Expand Off, PadY 10]

    (sb, ed) <- newScrollBox bFrame
        (`newEditor` [state Normal, size (80, 40)]) []
    ed # state Disabled
    pack bFrame [Side AtTop, Expand On, Fill Both]
    pack sb     [Side AtTop, Expand On, Fill Both]
    pack ed     [Side AtTop, Expand On, Fill Both]

    pack btnBox [Side AtTop, Expand On, Fill X]
    pack tsBut [PadX 5, PadY 5]
    pack ptBut [PadX 5, PadY 5]
    pack sBut  [PadX 5, PadY 5]
    pack qBut  [PadX 8, PadY 5]
    G_theory _ _ _ sSens _ <- return $ selectedTheory prGUISt
    let sttDesc = "Tactic script"
        sptDesc = "Proof tree"
        sens = OMap.filter (not . isAxiom) sSens
        elementMap = foldr insertSenSt Map.empty (reverse $ OMap.toList sens)
        insertSenSt (gN, st) resOMap =
            foldl (flip $ \ (s2, ind) -> OMap.insert (gN, ind) $
                                                     fillGoalDescription s2)
              resOMap $
               zip (sortBy (\ (_, a) (_, b) -> compare a b) $ thmStatus st)
                   [(0 :: Int) ..]

    stateRef <- newIORef elementMap
    ed # state Normal
    mapM_ (\ ((gName, ind), goalDesc) -> do
        when (ind == 0) $
          appendText ed $ replicate 75 '-' ++ "\n" ++ gName ++ "\n"
        appendText ed $ proverInfo goalDesc ++ "\n"
        opTextTS <- addTextTagButton sttDesc (tacticScriptText goalDesc)
                       TacticScriptText ed (gName, ind) stateRef
        opTextPT <- addTextTagButton sptDesc (proofTreeText goalDesc)
                       ProofTreeText ed (gName, ind) stateRef
        appendText ed "\n"
        let goalDesc' = goalDesc { tacticScriptText = opTextTS,
                                  proofTreeText    = opTextPT }
        modifyIORef stateRef (OMap.update (\ _ -> Just goalDesc') (gName, ind))
      ) $ OMap.toList elementMap

    ed # state Disabled

    (editClicked, _) <- bindSimple ed (ButtonPress (Just 1))
    quit <- clicked qBut
    save <- clicked sBut
    toggleTacticScript <- clicked tsBut
    toggleProofTree <- clicked ptBut
    btnState <- newIORef (False, False)
    _ <- spawnEvent $ forever
        $ quit >>> destroy win
        +> save >>> do
          disable qBut
          disable sBut
          curDir <- getCurrentDirectory
          let f = curDir ++ '/' : thName ++ "-proof-details.txt"
          mfile <- fileSaveDialog f [ ("Text", ["*.txt"])
                                    , ("All Files", ["*"])] Nothing
          maybe done (writeTextToFile ed) mfile
          enable qBut
          enable sBut
          done
        +> toggleTacticScript >>> do
             (expTS, expPT) <- readIORef btnState
             tsBut # text (if expTS then expand_tacticScripts
                                    else hide_tacticScripts)
             toggleMultipleTags TacticScriptText expTS ed stateRef
             writeIORef btnState (not expTS, expPT)
        +> toggleProofTree >>> do
             (expTS, expPT) <- readIORef btnState
             ptBut # text (if expPT then expand_proofTrees
                                    else hide_proofTrees)
             toggleMultipleTags ProofTreeText expPT ed stateRef
             writeIORef btnState (expTS, not expPT)
        +> editClicked >>> forceFocus ed
    return ()
  where
    expand_tacticScripts = "Expand tactic scripts"
    expand_proofTrees = "Expand proof trees"
    hide_tacticScripts = "Hide tactic scripts"
    hide_proofTrees = "Hide proof trees"

{- |
  Toggle all 'TextTag's of one kind to the same state (visible or invisible),
  either tactic script or proof tree.
-}
toggleMultipleTags :: Content -- ^ kind of text tag to toggle
                   -> Bool -- ^ current visibility state
                   -> Editor
                      -- ^ editor window to which button will be attached
                   -> IORef (OMap.OMap (String, Int) GoalDescription)
                      -- ^ current state of all proof descriptions
                   -> IO ()
toggleMultipleTags content expanded ed stateRef = do
    s <- readIORef stateRef
    mapM_ (\ (dKey, goalDesc) -> do
        let openText = if content == TacticScriptText
                         then tacticScriptText goalDesc
                         else proofTreeText goalDesc
        when (textShown openText == expanded)
             (toggleTextTag content ed dKey stateRef)
      ) $ OMap.toList s
    done

{- |
  This functions toggles the state from a given TextTag from visible to
  invisible or vice versa. This depends on the current state in the ordered map
  of goal descriptions. First parameter indicates whether the tactic script
  or the proof tree text from a goal description will be toggled.
-}
toggleTextTag :: Content -- ^ kind of text tag to toggle
              -> Editor -- ^ editor window to which button will be attached
              -> (String, Int) {- ^ key in single proof descriptions
                               (goal name and index) -}
              -> IORef (OMap.OMap (String, Int) GoalDescription)
                 -- ^ current state of all proof descriptions
              -> IO ()
toggleTextTag content ed (gName, ind) stateRef = do
    s <- readIORef stateRef
    let gd = fromMaybe (emptyGoalDescription gName)
             $ OMap.lookup (gName, ind) s
        openText = if content == TacticScriptText then tacticScriptText gd
                                                    else proofTreeText gd
        tsp = textStartPosition openText
        nol = (numberOfLines $ additionalText openText)
    if not $ textShown openText then do
        ed # state Normal
        insertText ed tsp $ additionalText openText
        ed # state Disabled
        done
      else do
        ed # state Normal
        deleteTextRange ed tsp $ changePosition (+) nol tsp
        ed # state Disabled
        done
    let openText' = openText { textShown = not $ textShown openText }
        s' = OMap.update
                 (\ _ -> Just $ if content == TacticScriptText
                          then gd { tacticScriptText = openText' }
                          else gd { proofTreeText = openText' } )
                 (gName, ind) s
    writeIORef stateRef $ adaptTextPositions
         (if textShown openText then (-) else (+))
         nol tsp s'

{- |
  A button in form of a text tag will be added to the specified editor window.
  The events for clicking on a button are set up: adding or removing
  additional text lines by alternately clicking. All positions of text lying
  behind have to be adapted.
  The current state of text tags is stored and modified in 'IORef'.
  Initial call of this function returns an 'OpenText' containing the status of
  the added text tag button.
-}
addTextTagButton :: String -- ^ caption for button
                 -> OpenText -- ^ conatins text to be outfolded if clicked
                 -> Content -- ^ either text from tacticScript or proofTree
                 -> Editor -- ^ editor window to which button will be attached
                 -> (String, Int) {- ^ key in single proof descriptions
                                  (goal name and index) -}
                 -> IORef (OMap.OMap (String, Int) GoalDescription)
                    -- ^ current state of all proof descriptions
                 -> IO OpenText -- ^ information about OpenText status
addTextTagButton cap addText content ed dKey stateRef = do
    appendText ed $ replicate (2 * stdIndent) ' '
    curPosStart <- getRealEndOfTextIndex ed
    appendText ed cap
    curPosEnd <- getRealEndOfTextIndex ed
    insertNewline ed
    ttag <- createTextTag ed curPosStart curPosEnd [underlined On]

    (selectTextTag, _) <- bindSimple ttag (ButtonPress (Just 1))
    (enterTT, _) <- bindSimple ttag Enter
    (leaveTT, _) <- bindSimple ttag Leave
    _ <- spawnEvent $ forever
                   $ selectTextTag >>> toggleTextTag content ed dKey stateRef
                   +> enterTT >>> do
                     ed # cursor hand2
                     done
                   +> leaveTT >>> do
                     ed # cursor xterm
                     done
    return OpenText {additionalText = "\n" ++ additionalText addText ++ "\n",
                     textShown = False,
                     textStartPosition = curPosEnd}
