hets/VSE/Prove.hs

	Prove.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{-# 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