root/trunk/GUI/History.hs @ 11229

{- |
Module      :  $Header$
Description :  Manages the history of proof commands
Copyright   :  (c) Markus Gross 2008
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  Markus.Gross@dfki.de
Stability   :  provisional
Portability :  portable

Manages the history of proof commands.
-}
module GUI.History (CommandHistory,
                    emptyCommandHistory,
                    initCommandHistory,
                    addMenuItemToHist,
                    addProveToHist,
                    askSaveProofScript) where

import Common.OrderedMap (keys)
import Common.Utils (joinWith, splitOn)
import Driver.Options (rmSuffix)
import GUI.GraphAbstraction (GraphInfo, showTemporaryMessage)
import GUI.Utils (infoDialog, fileSaveDialog)
import Logic.Comorphism (AnyComorphism(..))
import Logic.Grothendieck (SigId(..))
import Logic.Logic (language_name)
import Logic.Prover
import Proofs.AbstractState
import Static.GTheory (G_theory(..))

import Control.Monad (when)
import Data.IORef
import Data.List (isPrefixOf, stripPrefix)
import Data.Maybe (fromMaybe)
import System.Directory (getCurrentDirectory)

-- This datastructure holds all information for the history.
data CommandHistory = CommandHistory {file :: String,
                                      hist :: IORef [Command]}

-- Represents a command in the history.
data Command = DGComm DGCommand | NodeChange Node | ProveCommand Prove
               deriving Eq

instance Show Command where
    show (DGComm c)       = show c
    show (NodeChange n)   = show n
    show (ProveCommand p) = show p

-- This is used to recognize a change of node between the proofs.
data Node = Node Int String deriving Eq

instance Show Node where
    show (Node _ nName) =
        "\n# " ++ (replicate 78 '-') ++ "\n\ndg basic " ++ nName ++ "\n"

-- This represents a dg menu-item.
data DGCommand = AllAuto      | AllGlobSubsume | AllGlobDecomp | AllLocInfer |
                 AllLocDecomp | AllComp        | AllCompNew    | AllHideThm  |
                 AllThmHide   deriving Eq

instance Show DGCommand where
    show AllAuto        = "dg-all auto"
    show AllGlobSubsume = "dg-all glob-subsume"
    show AllGlobDecomp  = "dg-all glob-decomp"
    show AllLocInfer    = "dg-all loc-infer"
    show AllLocDecomp   = "dg-all loc-decomp"
    show AllComp        = "dg-all comp"
    show AllCompNew     = "dg-all comp-new"
    show AllHideThm     = "dg-all hide-thm"
    show AllThmHide     = "dg-all thm-hide"

-- This represents a prove with all properties needed to add it to the history.
data Prove = Prove {prover      :: Maybe String,        -- name of the prover
                    translation :: Maybe AnyComorphism, -- used translation
                    provenGoals :: [ProvenGoal],        -- proven goals
                    allAxioms   :: [String]             -- all available axioms
                   } deriving Eq

instance Show Prove where
    show p =
        "drop-translations\n"
        ++
        -- selected translation
        (maybe "" (unlines . splitComorphism) $ translation p)
        ++
        -- selected prover
        (maybe "# no prover chosen" ("prover " ++) $ prover p) ++ "\n\n"
        ++
        -- proven goals
        (joinWith '\n' $ map (goalToString p) $ provenGoals p)

-- This represents the information about a proved goal
data ProvenGoal = ProvenGoal {name      :: String,   -- name of the goal
                              axioms    :: [String], -- used axioms in the prove
                              timeLimit :: Int       -- chosen time-limit
                             } deriving Eq

-- Converts a proven goal to a string.
goalToString :: Prove -> ProvenGoal -> String
goalToString p g =
    "set goals " ++ (name g)
    ++
    -- axioms to include in prove
    '\n':(if (allAxioms p == axioms g) || (null $ axioms g)
              then "set-all axioms"
              else "set axioms " ++ (joinWith ' ' $ axioms g))
    ++
    -- selected time-limit
    "\nset time-limit " ++ (show $ timeLimit g) ++ "\nprove\n"

-- Creates an empty command history.
emptyCommandHistory :: IO CommandHistory
emptyCommandHistory = initCommandHistory ""

-- Initializes the command history with a filename.
initCommandHistory :: String -> IO CommandHistory
initCommandHistory f =
    do
    ff <- tryRemoveAbsolutePathComponent f
    ch <- newIORef []
    return $ CommandHistory {file = rmSuffix ff, hist = ch}

-- Adds a single command to the history.
addToHist :: CommandHistory -> Command -> IO ()
addToHist (CommandHistory {hist = c}) cm =
    readIORef c >>= (\h -> writeIORef c $ h ++ [cm])

-- Adds a menu item to the history.
addMenuItemToHist :: CommandHistory -> String -> IO ()
addMenuItemToHist ch item =
    maybe (return ()) (addToHist ch . DGComm) (lookup item menuItems)

-- A List of menu items and their corresponding proof-script command.
menuItems :: [(String, DGCommand)]
menuItems = [
    ("Automatic",                            AllAuto),
    ("Global Subsumption",                   AllGlobSubsume),
    ("Global Decomposition",                 AllGlobDecomp),
    ("Local Inference",                      AllLocInfer),
    ("Local Decomposition (merge of rules)", AllLocDecomp),
    ("Composition (merge of rules)",         AllComp),
    ("Composition - creating new links",     AllCompNew),
    ("Hide Theorem Shift",                   AllHideThm),
    ("Theorem Hide Shift",                   AllThmHide)
    ]

-- If at least one goal was proved and the prove is not the same as last time
-- the prove gets added, otherwise not.
addProveToHist :: CommandHistory 
        -> ProofState lid sentence         -- current proofstate
        -> Maybe (G_prover, AnyComorphism) -- possible used translation
        -> [Proof_status proof_tree]       -- goals included in prove
        -> IO ()
addProveToHist ch st pcm pt
    | null $ filter (wasProved) pt = return ()
    | otherwise = do
                  p' <- proofTreeToProve st pcm pt
                  mp <- getLastProve ch
                  case mp of
                      Just p  -> when (p /= p') (addProve p')
                      Nothing -> addProve p'
    where
        -- Drops the filename as prefix from a node-name.
        dropName :: String -> String
        dropName s = maybe s (tail) (stripPrefix (file ch) s)
        -- Adds a prove to the history.
        addProve :: Prove -> IO ()
        addProve p =
            do
            -- Create new NodeChange and compare it with last found NodeChange.
            let (SigId nId) = gTheorySignIdx $ theory st
            let nc' = NodeChange $ Node nId (dropName $ theoryName st)
            mn <- getLastNode ch
            -- Add new NodeChange if it doesn't match.
            case mn of
                Just n  -> when (NodeChange n /= nc') (addToHist ch nc')
                Nothing -> addToHist ch nc'
            -- Finally add the prove.
            addToHist ch $ ProveCommand p

-- Converts a list of proof-trees to a prove.
proofTreeToProve :: ProofState lid sentence -- current proofstate
    -> Maybe (G_prover, AnyComorphism)      -- possible used translation
    -> [Proof_status proof_tree]            -- goals included in prove
    -> IO Prove
proofTreeToProve st pcm pt =
    do
    -- selected prover
    let prvr = maybe (selectedProver st) (Just . getProverName . fst) pcm
    -- selected translation
    let trans = maybe Nothing (Just . snd) pcm
    -- 1. filter out the not proven goals
    -- 2. reverse the list, because the last proven goals are on top
    -- 3. convert all proof-trees to goals
    -- 4. merge goals with same used axioms
    let goals = mergeGoals $ reverse $ map (convertGoal) $ filter (wasProved) pt
    -- axioms to include in prove
    let allax = case theory st of
                    G_theory _ _ _ axs _ -> keys axs
    return $ Prove {prover = prvr,
                    translation = trans,
                    provenGoals = goals,
                    allAxioms = allax}

-- This checks wether a goal was proved or not.
wasProved :: Proof_status proof_tree -> Bool
wasProved g = case goalStatus g of
    Proved _ -> True
    _        -> False

-- Converts a proof-tree into a goal.
convertGoal :: Proof_status proof_tree -> ProvenGoal
convertGoal pt =
    ProvenGoal {name = goalName pt, axioms = usedAxioms pt, timeLimit = tlimit}
    where
        (Tactic_script script) = tacticScript pt
        tlimit = maybe 20 (read) (parseTimeLimit $ splitOn '\n' script)

-- Parses time-limit from the tactic-script of a goal.
parseTimeLimit :: [String] -> Maybe String
parseTimeLimit l =
    if null l' then Nothing else Just $ drop (length tlStr) $ last l'
    where
        l' = filter (isPrefixOf tlStr) l
        tlStr = "Time limit: "

-- Merges goals with the same used axioms into one goal.
mergeGoals :: [ProvenGoal] -> [ProvenGoal]
mergeGoals []     = []
mergeGoals (h:[]) = [h]
mergeGoals (h:t)  | mergeAble h h' = mergeGoals $ (merge h h'):(tail t)
                  | otherwise      = h:(mergeGoals t)
                  where
                      h' = head t
                      mergeAble :: ProvenGoal -> ProvenGoal -> Bool
                      mergeAble a b = axioms a == axioms b &&
                                      timeLimit a == timeLimit b
                      merge :: ProvenGoal -> ProvenGoal -> ProvenGoal
                      merge a b = a{name = name a ++ ' ':(name b)}

-- Returns the last nodechange in the history.
getLastNode :: CommandHistory -> IO (Maybe Node)
getLastNode (CommandHistory{hist = c}) =
    do
    h <- readIORef c
    let h' = [n | NodeChange n <- h]
    return $ if null h' then Nothing else Just $ last h'

-- If the last command in history is a prove it gets returned.
getLastProve :: CommandHistory -> IO (Maybe Prove)
getLastProve (CommandHistory{hist = c}) =
    do
    h <- readIORef c
    return $ if null h
               then Nothing
               else case last h of
                        ProveCommand p -> Just p
                        _              -> Nothing

-- | Displays a Save-As dialog and writes the proof-script.
askSaveProofScript :: GraphInfo -> CommandHistory -> IO ()
askSaveProofScript graphInfo ch =
    do
    h <- readIORef $ hist ch
    if null h
        then infoDialog "Information" "The history is empty. No file written."
        else do
             f <- getProofScriptFileName ch
             maybeFilePath <- fileSaveDialog f [ ("Proof-Script",["*.hpf"])
                                               , ("All Files", ["*"])] Nothing
             case maybeFilePath of
                 Just filePath -> do
                    showTemporaryMessage graphInfo "Saving proof-script..."
                    saveCommandHistory ch filePath
                    showTemporaryMessage graphInfo $ "Proof-script saved to " ++
                                                     filePath ++ "!"
                 Nothing -> showTemporaryMessage graphInfo $ "Aborted!"

-- Saves the history of commands in a file.
saveCommandHistory :: CommandHistory -> String -> IO ()
saveCommandHistory (CommandHistory {file = ff, hist = c}) f =
    do
    h <- readIORef c
    let history = ["# automatically generated hets proof-script", "",
                   "use " ++ ff, ""] ++ map (show) h
    writeFile f $ joinWith '\n' history

-- Suggests a proof-script filename.
getProofScriptFileName :: CommandHistory -> IO FilePath
getProofScriptFileName (CommandHistory {file = f})
    | "/" `isPrefixOf` f = return $ f ++ ".hpf"
    | otherwise          = do
                           dir <- getCurrentDirectory
                           return $ dir ++ '/':f ++ ".hpf"

-- Splits the comorphism string into its translations.
splitComorphism :: AnyComorphism -> [String]
splitComorphism (Comorphism cid) =
    map ("translate " ++) $ tail $ splitOn ';' $ language_name cid

-- If an absolute path is given,
-- it tries to remove the current working directory as prefix of it.
tryRemoveAbsolutePathComponent :: String -> IO String
tryRemoveAbsolutePathComponent f
    | "/" `isPrefixOf` f = do
                           dir <- getCurrentDirectory
                           return $ fromMaybe f (stripPrefix (dir ++ "/") f)
    | otherwise          = return f