content: {-# LANGUAGE CPP #-}
  {- |
  Module      :  ./VSE/Prove.hs
  Description :  Interface to the VSE prover
  Copyright   :  (c) C. Maeder, DFKI 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  call an adaption of VSE II to hets
  -}
  
  module VSE.Prove where
  
  import Logic.Prover
  import VSE.As
  import VSE.Ana
  import VSE.ToSExpr
  import Common.AS_Annotation
  import Common.IO
  import Common.ProverTools
  import Common.SExpr
  import Common.Utils
  
  import Data.Char
  import Data.Maybe
  import Data.List
  import qualified Data.Map as Map
  import System.Process
  import System.IO
  import Text.ParserCombinators.Parsec
  #ifdef TAR_PACKAGE
  import Control.Monad
  import System.Directory
  import qualified Codec.Archive.Tar as Tar
  #endif
  
  vseProverName :: String
  vseProverName = "VSE"
  
  mkVseProofStatus :: String -> [String] -> ProofStatus ()
  mkVseProofStatus n axs = (openProofStatus n vseProverName ())
     { goalStatus = Proved True
     , usedAxioms = axs }
  
  vse :: Prover VSESign Sentence VSEMor () ()
  vse = (mkProverTemplate vseProverName () prove)
    { proverUsable = vseBinary >>= checkBinary }
  
  nameP :: String
  nameP = "SPECIFICATION-NAMES"
  
  linksP :: String
  linksP = "IN-LINKS"
  
  sigP :: String
  sigP = "SIG"
  
  lemsP :: String
  lemsP = "LEMMABASE"
  
  prx :: String -> String
  prx = ("(API::GET-" ++)
  
  data MaybeChar = Wait | Stop | JustChar Char
  
  vseErrFile :: String
  vseErrFile = "hetsvse.out"
  
  readUntilMatchParen :: ProcessHandle -> Handle -> String -> IO String
  readUntilMatchParen = readUntilMatchParenAux 10000
  
  readUntilMatchParenAux :: Int -> ProcessHandle -> Handle -> String -> IO String
  readUntilMatchParenAux n cp h str =
    let os = length $ filter (== '(') str
        cs = length $ filter (== ')') str
    in if n < 1 then do
      appendFile vseErrFile $ "readUntilMatchParen failed after\n" ++ str ++ "\n"
      return ""
    else if os == cs && os > 0 then return str
    else do
    mc <- myGetChar cp h
    case mc of
      Wait -> do
        appendFile vseErrFile "waiting for character ...\n"
        readUntilMatchParenAux (n - 1) cp h str
      Stop -> return str
      JustChar c -> readUntilMatchParen cp h $ c : str
  
  myGetChar :: ProcessHandle -> Handle -> IO MaybeChar
  myGetChar cp h = do
    mc <- catchIOException Wait (fmap JustChar $ hGetChar h)
    case mc of
      Wait -> do
        ms <- getProcessExitCode cp
        return $ case ms of
          Nothing -> mc
          Just _ -> Stop
      _ -> return mc
  
  readMyMsg :: ProcessHandle -> Handle -> String -> IO String
  readMyMsg = readMyMsgAux 1000
  
  readMyMsgAux :: Int -> ProcessHandle -> Handle -> String -> IO String
  readMyMsgAux n cp h expect = if n < 1 then do
      appendFile vseErrFile $ "gave up waiting for: " ++ expect ++ "\n"
      return ""
    else do
    mc <- myGetChar cp h
    case mc of
      Wait -> do
        appendFile vseErrFile "waiting for first character ...\n"
        readMyMsgAux (n - 1) cp h expect
      Stop -> return ""
      JustChar c -> do
        r <- readUntilMatchParen cp h [c]
        let rr = reverse r
        if isPrefixOf (prx expect) $ dropWhile (/= '(') rr
          then return rr else do
          appendFile vseErrFile $ "waiting for '" ++ expect ++ "' got:\n" ++ rr
            ++ "\ntrying again\n"
          readMyMsgAux (n - 1) cp h expect -- try again
  
  sendMyMsg :: Handle -> String -> IO ()
  sendMyMsg cp str = catchIOException () $ hPutStrLn cp str >> hFlush cp
  
  readRest :: ProcessHandle -> Handle -> String -> IO String
  readRest cp out str = do
    mc <- myGetChar cp out
    case mc of
      Wait -> readRest cp out str
      Stop -> return str
      JustChar c -> readRest cp out $ c : str
  
  parseSymbol :: Parser SExpr
  parseSymbol = skipWhite
    $ fmap SSymbol $ many1 $ satisfy $ \ c -> not (isSpace c || elem c "()")
  
  parseList :: Parser SExpr
  parseList = do
    skipWhite $ char '('
    l <- many parseSExpr
    skipWhite $ char ')'
    return $ SList l
  
  parseSExpr :: Parser SExpr
  parseSExpr = parseList <|> parseSymbol
  
  skipWhite :: Parser a -> Parser a
  skipWhite p = do
    a <- p
    spaces
    return a
  
  skipJunk :: Parser ()
  skipJunk = skipMany $ satisfy (/= '(')
  
  parseSExprs :: Parser [SExpr]
  parseSExprs = do
    skipJunk
    sepEndBy parseSExpr skipJunk
  
  findState :: SExpr -> Maybe (String, String)
  findState sexpr = case sexpr of
    SList (SSymbol "API::SET-SENTENCE" : SSymbol nodeStr :
           SList (SSymbol "API::ASENTENCE" : SSymbol senStr :
                  SSymbol "API::OBLIGATION" : SSymbol "API::PROVED" : _) : _)
      | isPrefixOf "API::" nodeStr && isPrefixOf "API::" senStr
      -> Just (drop 5 nodeStr, drop 5 senStr)
    _ -> Nothing
  
  specDir :: String
  specDir = "specifications"
  
  allSpecFile :: String
  allSpecFile = "all-specifications"
  
  allSpecInDir :: String
  allSpecInDir = specDir ++ "/" ++ allSpecFile
  
  #ifdef TAR_PACKAGE
  createVSETarFile :: FilePath -> IO ()
  createVSETarFile tar = do
    hasSpecDir <- doesDirectoryExist specDir
    hasAllSpecFile <- doesFileExist allSpecFile
    if (hasSpecDir && hasAllSpecFile) then do
      renameFile allSpecFile allSpecInDir
      Tar.create (tar ++ ".tar") "" [specDir]
      else putStrLn $ "hetsvse did not create: "
        ++ if hasSpecDir then allSpecFile else specDir
  
  moveVSEFiles :: FilePath -> IO ()
  moveVSEFiles str = do
    let tarFile = str ++ ".tar"
    hasTarFile <- doesFileExist tarFile
    hasSpecDir <- doesDirectoryExist specDir
    hasAllSpecFile <- doesFileExist allSpecFile
    when (hasSpecDir && hasAllSpecFile) $ do
       createVSETarFile (specDir ++ ".bak")
       removeDirectoryRecursive specDir
    when hasTarFile $ do
      Tar.extract "" tarFile
      renameFile allSpecInDir allSpecFile
  #endif
  
  vseBinary :: IO String
  vseBinary = getEnvDef "HETS_VSE" "hetsvse"
  
  prepareAndCallVSE :: IO (Handle, Handle, ProcessHandle)
  prepareAndCallVSE = do
    vseBin <- vseBinary
    (inp, out, _, cp) <-
        runInteractiveProcess vseBin ["-std"] Nothing Nothing
    readMyMsg cp out nameP
    return (inp, out, cp)
  
  readFinalVSEOutput :: ProcessHandle -> Handle
                     -> IO (Maybe (Map.Map String [String]))
  readFinalVSEOutput cp out = do
    ms <- getProcessExitCode cp
    case ms of
      Just _ -> do
        appendFile vseErrFile "hetsvse unavailable\n"
        return Nothing
      Nothing -> do
        revres <- readRest cp out ""
        let res = reverse revres
        writeFile "hetsvse-debug.txt" res
        case parse parseSExprs vseErrFile res of
          Right l -> return $ Just $ readLemmas l
          Left e -> do
            print e
            appendFile vseErrFile $ res ++ "\n"
            return Nothing
  
  readLemmas :: [SExpr] -> Map.Map String [String]
  readLemmas =
    foldr (\ (node, sen) -> Map.insertWith (++) node [sen]) Map.empty
    . mapMaybe findState
  
  prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
  prove ostr (Theory sig thsens) _freedefs = do
    let str = map (\ c -> if c == '/' then '-' else c) ostr
        oSens = toNamedList thsens
        (fsig, sens) = addUniformRestr sig oSens
        (disAxs, disGoals) = partition isAxiom oSens
        rMap = Map.fromList $ map (\ SenAttr { senAttr = n } ->
                  (map toUpper $ transString n, n)) disGoals
  #ifdef TAR_PACKAGE
    moveVSEFiles str
  #endif
    (inp, out, cp) <- prepareAndCallVSE
    sendMyMsg inp $ "(" ++ str ++ ")"
    readMyMsg cp out linksP
    sendMyMsg inp "nil"
    readMyMsg cp out sigP
    sendMyMsg inp $ show $ prettySExpr $ vseSignToSExpr fsig
    readMyMsg cp out lemsP
    sendMyMsg inp $ show $ prettySExpr $ SList $ map (namedSenToSExpr fsig) sens
    ms <- readFinalVSEOutput cp out
  #ifdef TAR_PACKAGE
    createVSETarFile str
  #endif
    case ms of
      Nothing -> return []
      Just lemMap -> return
            $ foldr (\ s r -> case Map.lookup s rMap of
                   Nothing -> r
                   Just n -> mkVseProofStatus n (map senAttr disAxs) : r) []
            $ Map.findWithDefault [] (map toUpper str) lemMap
  