{- |
Module      :  $Header$
Description :  interface to the Isabelle theorem prover
Copyright   :  (c) University of Cambridge, Cambridge, England
               adaption (c) Till Mossakowski, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Interface for Isabelle theorem prover.
-}
{-
  Interface between Isabelle and Hets:
   Hets writes Isabelle .thy file and starts Isabelle
   User extends .thy file with proofs
   User finishes Isabelle
   Hets reads in created *.deps files
-}

module Isabelle.IsaProve where

import Logic.Prover
import Isabelle.IsaSign
import Isabelle.IsaConsts
import Isabelle.IsaPrint
import Isabelle.IsaParse
import Isabelle.Translate
import Isabelle.MarkSimp

import Common.AS_Annotation
import Common.DocUtils
import Common.DefaultMorphism
import Common.ProofUtils
import Common.Utils (getEnvDef)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Text.ParserCombinators.Parsec
import Data.Char
import Data.List (isSuffixOf)
import Control.Monad
import Data.Time (midnight)

import System.Directory
import System.Exit
import System.Cmd

isabelleS :: String
isabelleS = "Isabelle"

openIsaProofStatus :: String -> ProofStatus ()
openIsaProofStatus n = openProofStatus n isabelleS ()

isabelleProver :: Prover Sign Sentence (DefaultMorphism Sign) () ()
isabelleProver = mkProverTemplate isabelleS () isaProve

isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
isabelleConsChecker = (mkConsChecker "Isabelle-refute" () consCheck)
  { ccBatch = False
  , ccNeedsTimer = False }

-- | the name of the inconsistent lemma for consistency checks
inconsistentS :: String
inconsistentS = "inconsistent"

metaToTerm :: MetaTerm -> Term
metaToTerm mt = case mt of
  Term t -> t
  Conditional ts t -> case ts of
    [] -> t
    _ -> binImpl (foldr1 binConj ts) t

consCheck :: String -> b
  -> TheoryMorphism Sign Sentence (DefaultMorphism Sign) () -> a
  -> IO (CCStatus ())
consCheck thName _tac tm freedefs = case tTarget tm of
    Theory sig nSens -> do
      let (axs, _) = getAxioms $ toNamedList nSens
      l <- isaProve (thName ++ "_c")
           (Theory sig
               $ markAsGoal $ toThSens $ if null axs then [] else
                   [ makeNamed inconsistentS $ mkRefuteSen $ termAppl notOp
                     $ foldr1 binConj
                     $ map (metaToTerm . metaTerm . sentence) axs ])
           freedefs
      return $ CCStatus () midnight $ case filter isProvedStat l of
        [_] -> Just False -- inconsistency was proven
        _ -> Nothing -- consistency cannot be recorded automatically

prepareTheory :: Theory Sign Sentence ()
    -> (Sign, [Named Sentence], [Named Sentence], Map.Map String String)
prepareTheory (Theory sig nSens) = let
    oSens = toNamedList nSens
    nSens' = prepareSenNames transString oSens
    (disAxs, disGoals) = getAxioms nSens'
    in (sig, map markSimp disAxs, map markThSimp disGoals,
       Map.fromList $ zip (map senAttr nSens') $ map senAttr oSens)
-- return a reverse mapping for renamed sentences

removeDepFiles :: String -> [String] -> IO ()
removeDepFiles thName = mapM_ $ \ thm -> do
  let depFile = getDepsFileName thName thm
  ex <- doesFileExist depFile
  when ex $ removeFile depFile

getDepsFileName :: String -> String -> String
getDepsFileName thName thm = thName ++ "_" ++ thm ++ ".deps"

getProofDeps :: Map.Map String String -> String -> String
             -> IO (ProofStatus ())
getProofDeps m thName thm = do
    let file = getDepsFileName thName thm
        mapN n = Map.findWithDefault n n m
        strip = takeWhile (not . isSpace) . dropWhile isSpace
    b <- doesFileExist file
    if b then do
        s <- readFile file
        return $ mkProved (mapN thm) $ map mapN $
               Set.toList $ Set.filter (not . null) $
               Set.fromList $ map strip $ lines s
      else return $ openIsaProofStatus $ mapN thm

getAllProofDeps :: Map.Map String String -> String -> [String]
                -> IO([ProofStatus ()])
getAllProofDeps m = mapM . getProofDeps m

checkFinalThyFile :: (TheoryHead, Body) -> String -> IO Bool
checkFinalThyFile (ho, bo) thyFile = do
  s <- readFile thyFile
  case parse parseTheory thyFile s of
    Right (hb, b) -> do
            let ds = compatibleBodies bo b
            mapM_ (\ d -> putStrLn $ showDoc d "") $ ds ++ warnSimpAttr b
            if hb /= ho then do
                  putStrLn "illegal change of theory header"
                  return False
              else return $ null ds
    Left err -> print err >> return False

mkProved :: String -> [String] -> ProofStatus ()
mkProved thm used = (openIsaProofStatus thm)
    { goalStatus = Proved True
    , usedAxioms = used
    , tacticScript = TacticScript "unknown isabelle user input" }

prepareThyFiles :: (TheoryHead, Body) -> String -> String -> IO ()
prepareThyFiles ast thyFile thy = do
    let origFile = thyFile ++ ".orig"
    exOrig <- doesFileExist origFile
    exThyFile <- doesFileExist thyFile
    unless exOrig $ writeFile origFile thy
    unless exThyFile $ writeFile thyFile thy
    thy_time <- getModificationTime thyFile
    orig_time <- getModificationTime origFile
    s <- readFile origFile
    unless (thy_time >= orig_time && s == thy)
      $ patchThyFile ast origFile thyFile thy

patchThyFile :: (TheoryHead, Body) -> FilePath -> FilePath -> String -> IO ()
patchThyFile (ho, bo) origFile thyFile thy = do
  let patchFile = thyFile ++ ".patch"
      oldFile = thyFile ++ ".old"
      diffCall = "diff -u " ++ origFile ++ " " ++ thyFile
                 ++ " > " ++ patchFile
      patchCall = "patch -bfu " ++ thyFile ++ " " ++ patchFile
  callSystem diffCall
  renameFile thyFile oldFile
  removeFile origFile
  writeFile origFile thy
  writeFile thyFile thy
  callSystem patchCall
  s <- readFile thyFile
  case parse parseTheory thyFile s of
    Right (hb, b) -> do
            let ds = compatibleBodies bo b
                h = hb == ho
            mapM_ (\ d -> putStrLn $ showDoc d "") ds
            unless h $ putStrLn "theory header is corrupt"
            unless (h && null ds) $ revertThyFile thyFile thy
    Left err -> do
      print err
      revertThyFile thyFile thy

revertThyFile :: String -> String -> IO ()
revertThyFile thyFile thy = do
    putStrLn $ "replacing corrupt file " ++ show thyFile
    removeFile thyFile
    writeFile thyFile thy

callSystem :: String -> IO ExitCode
callSystem s = putStrLn s >> system s

isaProve :: String -> Theory Sign Sentence () -> a -> IO([ProofStatus ()])
isaProve thName th _freedefs = do
  let (sig, axs, ths, m) = prepareTheory th
      thms = map senAttr ths
      thBaseName = reverse . takeWhile (/= '/') $ reverse thName
      useaxs = filter (\ s ->
            sentence s /= mkSen true && (isDef s ||
               isSuffixOf "def" (senAttr s))) axs
      defaultProof = Just $ IsaProof
        (if null useaxs then [] else [Using $ map senAttr useaxs])
        $ By Auto
      thy = shows (printIsaTheory thBaseName sig
        $ axs ++ map (mapNamed $ \ t -> case t of
           Sentence { thmProof = Nothing } -> t { thmProof = defaultProof }
           _ -> t) ths)
        "\n"
      thyFile = thBaseName ++ ".thy"
  case parse parseTheory thyFile thy of
    Right (ho, bo) -> do
      prepareThyFiles (ho, bo) thyFile thy
      removeDepFiles thBaseName thms
      isabelle <- getEnvDef "HETS_ISABELLE" "isabelle emacs"
      callSystem $ isabelle ++ " " ++ thyFile
      ok <- checkFinalThyFile (ho, bo) thyFile
      if ok then getAllProofDeps m thBaseName thms
          else return []
    Left err -> do
      print err
      putStrLn $ "Sorry, generated theory cannot be parsed, see: " ++ thyFile
      writeFile thyFile thy
      putStrLn "aborting Isabelle proof attempt"
      return []
