{-# 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 :: String
vseProverName = "VSE"

mkVseProofStatus :: String -> [String] -> ProofStatus ()
mkVseProofStatus :: String -> [String] -> ProofStatus ()
mkVseProofStatus n :: String
n axs :: [String]
axs = (String -> String -> () -> ProofStatus ()
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
n String
vseProverName ())
   { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
   , usedAxioms :: [String]
usedAxioms = [String]
axs }

vse :: Prover VSESign Sentence VSEMor () ()
vse :: Prover VSESign Sentence VSEMor () ()
vse = (String
-> ()
-> (String
    -> Theory VSESign Sentence ()
    -> [FreeDefMorphism Sentence VSEMor]
    -> IO [ProofStatus ()])
-> Prover VSESign Sentence VSEMor () ()
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate String
vseProverName () String
-> Theory VSESign Sentence ()
-> [FreeDefMorphism Sentence VSEMor]
-> IO [ProofStatus ()]
forall a.
String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
prove)
  { proverUsable :: IO (Maybe String)
proverUsable = IO String
vseBinary IO String -> (String -> IO (Maybe String)) -> IO (Maybe String)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> IO (Maybe String)
checkBinary }

nameP :: String
nameP :: String
nameP = "SPECIFICATION-NAMES"

linksP :: String
linksP :: String
linksP = "IN-LINKS"

sigP :: String
sigP :: String
sigP = "SIG"

lemsP :: String
lemsP :: String
lemsP = "LEMMABASE"

prx :: String -> String
prx :: String -> String
prx = ("(API::GET-" String -> String -> String
forall a. [a] -> [a] -> [a]
++)

data MaybeChar = Wait | Stop | JustChar Char

vseErrFile :: String
vseErrFile :: String
vseErrFile = "hetsvse.out"

readUntilMatchParen :: ProcessHandle -> Handle -> String -> IO String
readUntilMatchParen :: ProcessHandle -> Handle -> String -> IO String
readUntilMatchParen = Int -> ProcessHandle -> Handle -> String -> IO String
readUntilMatchParenAux 10000

readUntilMatchParenAux :: Int -> ProcessHandle -> Handle -> String -> IO String
readUntilMatchParenAux :: Int -> ProcessHandle -> Handle -> String -> IO String
readUntilMatchParenAux n :: Int
n cp :: ProcessHandle
cp h :: Handle
h str :: String
str =
  let os :: Int
os = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '(') String
str
      cs :: Int
cs = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')') String
str
  in if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then do
    String -> String -> IO ()
appendFile String
vseErrFile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "readUntilMatchParen failed after\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
  else if Int
os Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
cs Bool -> Bool -> Bool
&& Int
os Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
str
  else do
  MaybeChar
mc <- ProcessHandle -> Handle -> IO MaybeChar
myGetChar ProcessHandle
cp Handle
h
  case MaybeChar
mc of
    Wait -> do
      String -> String -> IO ()
appendFile String
vseErrFile "waiting for character ...\n"
      Int -> ProcessHandle -> Handle -> String -> IO String
readUntilMatchParenAux (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ProcessHandle
cp Handle
h String
str
    Stop -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
str
    JustChar c :: Char
c -> ProcessHandle -> Handle -> String -> IO String
readUntilMatchParen ProcessHandle
cp Handle
h (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
str

myGetChar :: ProcessHandle -> Handle -> IO MaybeChar
myGetChar :: ProcessHandle -> Handle -> IO MaybeChar
myGetChar cp :: ProcessHandle
cp h :: Handle
h = do
  MaybeChar
mc <- MaybeChar -> IO MaybeChar -> IO MaybeChar
forall a. a -> IO a -> IO a
catchIOException MaybeChar
Wait ((Char -> MaybeChar) -> IO Char -> IO MaybeChar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> MaybeChar
JustChar (IO Char -> IO MaybeChar) -> IO Char -> IO MaybeChar
forall a b. (a -> b) -> a -> b
$ Handle -> IO Char
hGetChar Handle
h)
  case MaybeChar
mc of
    Wait -> do
      Maybe ExitCode
ms <- ProcessHandle -> IO (Maybe ExitCode)
getProcessExitCode ProcessHandle
cp
      MaybeChar -> IO MaybeChar
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeChar -> IO MaybeChar) -> MaybeChar -> IO MaybeChar
forall a b. (a -> b) -> a -> b
$ case Maybe ExitCode
ms of
        Nothing -> MaybeChar
mc
        Just _ -> MaybeChar
Stop
    _ -> MaybeChar -> IO MaybeChar
forall (m :: * -> *) a. Monad m => a -> m a
return MaybeChar
mc

readMyMsg :: ProcessHandle -> Handle -> String -> IO String
readMyMsg :: ProcessHandle -> Handle -> String -> IO String
readMyMsg = Int -> ProcessHandle -> Handle -> String -> IO String
readMyMsgAux 1000

readMyMsgAux :: Int -> ProcessHandle -> Handle -> String -> IO String
readMyMsgAux :: Int -> ProcessHandle -> Handle -> String -> IO String
readMyMsgAux n :: Int
n cp :: ProcessHandle
cp h :: Handle
h expect :: String
expect = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1 then do
    String -> String -> IO ()
appendFile String
vseErrFile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "gave up waiting for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
expect String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
  else do
  MaybeChar
mc <- ProcessHandle -> Handle -> IO MaybeChar
myGetChar ProcessHandle
cp Handle
h
  case MaybeChar
mc of
    Wait -> do
      String -> String -> IO ()
appendFile String
vseErrFile "waiting for first character ...\n"
      Int -> ProcessHandle -> Handle -> String -> IO String
readMyMsgAux (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ProcessHandle
cp Handle
h String
expect
    Stop -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
    JustChar c :: Char
c -> do
      String
r <- ProcessHandle -> Handle -> String -> IO String
readUntilMatchParen ProcessHandle
cp Handle
h [Char
c]
      let rr :: String
rr = String -> String
forall a. [a] -> [a]
reverse String
r
      if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf (String -> String
prx String
expect) (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '(') String
rr
        then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
rr else do
        String -> String -> IO ()
appendFile String
vseErrFile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "waiting for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
expect String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' got:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rr
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\ntrying again\n"
        Int -> ProcessHandle -> Handle -> String -> IO String
readMyMsgAux (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) ProcessHandle
cp Handle
h String
expect -- try again

sendMyMsg :: Handle -> String -> IO ()
sendMyMsg :: Handle -> String -> IO ()
sendMyMsg cp :: Handle
cp str :: String
str = () -> IO () -> IO ()
forall a. a -> IO a -> IO a
catchIOException () (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
cp String
str IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
cp

readRest :: ProcessHandle -> Handle -> String -> IO String
readRest :: ProcessHandle -> Handle -> String -> IO String
readRest cp :: ProcessHandle
cp out :: Handle
out str :: String
str = do
  MaybeChar
mc <- ProcessHandle -> Handle -> IO MaybeChar
myGetChar ProcessHandle
cp Handle
out
  case MaybeChar
mc of
    Wait -> ProcessHandle -> Handle -> String -> IO String
readRest ProcessHandle
cp Handle
out String
str
    Stop -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
str
    JustChar c :: Char
c -> ProcessHandle -> Handle -> String -> IO String
readRest ProcessHandle
cp Handle
out (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
str

parseSymbol :: Parser SExpr
parseSymbol :: Parser SExpr
parseSymbol = Parser SExpr -> Parser SExpr
forall a. Parser a -> Parser a
skipWhite
  (Parser SExpr -> Parser SExpr) -> Parser SExpr -> Parser SExpr
forall a b. (a -> b) -> a -> b
$ (String -> SExpr)
-> ParsecT String () Identity String -> Parser SExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> SExpr
SSymbol (ParsecT String () Identity String -> Parser SExpr)
-> ParsecT String () Identity String -> Parser SExpr
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String () Identity Char
 -> ParsecT String () Identity String)
-> ParsecT String () Identity Char
-> ParsecT String () Identity String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String () Identity Char)
-> (Char -> Bool) -> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ \ c :: Char
c -> Bool -> Bool
not (Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "()")

parseList :: Parser SExpr
parseList :: Parser SExpr
parseList = do
  ParsecT String () Identity Char -> ParsecT String () Identity Char
forall a. Parser a -> Parser a
skipWhite (ParsecT String () Identity Char
 -> ParsecT String () Identity Char)
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '('
  [SExpr]
l <- Parser SExpr -> ParsecT String () Identity [SExpr]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser SExpr
parseSExpr
  ParsecT String () Identity Char -> ParsecT String () Identity Char
forall a. Parser a -> Parser a
skipWhite (ParsecT String () Identity Char
 -> ParsecT String () Identity Char)
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ')'
  SExpr -> Parser SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr -> Parser SExpr) -> SExpr -> Parser SExpr
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
SList [SExpr]
l

parseSExpr :: Parser SExpr
parseSExpr :: Parser SExpr
parseSExpr = Parser SExpr
parseList Parser SExpr -> Parser SExpr -> Parser SExpr
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser SExpr
parseSymbol

skipWhite :: Parser a -> Parser a
skipWhite :: Parser a -> Parser a
skipWhite p :: Parser a
p = do
  a
a <- Parser a
p
  ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

skipJunk :: Parser ()
skipJunk :: ParsecT String () Identity ()
skipJunk = ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (ParsecT String () Identity Char -> ParsecT String () Identity ())
-> ParsecT String () Identity Char -> ParsecT String () Identity ()
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '(')

parseSExprs :: Parser [SExpr]
parseSExprs :: ParsecT String () Identity [SExpr]
parseSExprs = do
  ParsecT String () Identity ()
skipJunk
  Parser SExpr
-> ParsecT String () Identity ()
-> ParsecT String () Identity [SExpr]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepEndBy Parser SExpr
parseSExpr ParsecT String () Identity ()
skipJunk

findState :: SExpr -> Maybe (String, String)
findState :: SExpr -> Maybe (String, String)
findState sexpr :: SExpr
sexpr = case SExpr
sexpr of
  SList (SSymbol "API::SET-SENTENCE" : SSymbol nodeStr :: String
nodeStr :
         SList (SSymbol "API::ASENTENCE" : SSymbol senStr :: String
senStr :
                SSymbol "API::OBLIGATION" : SSymbol "API::PROVED" : _) : _)
    | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "API::" String
nodeStr Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "API::" String
senStr
    -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just (Int -> String -> String
forall a. Int -> [a] -> [a]
drop 5 String
nodeStr, Int -> String -> String
forall a. Int -> [a] -> [a]
drop 5 String
senStr)
  _ -> Maybe (String, String)
forall a. Maybe a
Nothing

specDir :: String
specDir :: String
specDir = "specifications"

allSpecFile :: String
allSpecFile :: String
allSpecFile = "all-specifications"

allSpecInDir :: String
allSpecInDir :: String
allSpecInDir = String
specDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
allSpecFile

#ifdef TAR_PACKAGE
createVSETarFile :: FilePath -> IO ()
createVSETarFile :: String -> IO ()
createVSETarFile tar :: String
tar = do
  Bool
hasSpecDir <- String -> IO Bool
doesDirectoryExist String
specDir
  Bool
hasAllSpecFile <- String -> IO Bool
doesFileExist String
allSpecFile
  if (Bool
hasSpecDir Bool -> Bool -> Bool
&& Bool
hasAllSpecFile) then do
    String -> String -> IO ()
renameFile String
allSpecFile String
allSpecInDir
    String -> String -> [String] -> IO ()
Tar.create (String
tar String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".tar") "" [String
specDir]
    else String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "hetsvse did not create: "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool
hasSpecDir then String
allSpecFile else String
specDir

moveVSEFiles :: FilePath -> IO ()
moveVSEFiles :: String -> IO ()
moveVSEFiles str :: String
str = do
  let tarFile :: String
tarFile = String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".tar"
  Bool
hasTarFile <- String -> IO Bool
doesFileExist String
tarFile
  Bool
hasSpecDir <- String -> IO Bool
doesDirectoryExist String
specDir
  Bool
hasAllSpecFile <- String -> IO Bool
doesFileExist String
allSpecFile
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
hasSpecDir Bool -> Bool -> Bool
&& Bool
hasAllSpecFile) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
     String -> IO ()
createVSETarFile (String
specDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".bak")
     String -> IO ()
removeDirectoryRecursive String
specDir
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hasTarFile (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> String -> IO ()
Tar.extract "" String
tarFile
    String -> String -> IO ()
renameFile String
allSpecInDir String
allSpecFile
#endif

vseBinary :: IO String
vseBinary :: IO String
vseBinary = String -> String -> IO String
getEnvDef "HETS_VSE" "hetsvse"

prepareAndCallVSE :: IO (Handle, Handle, ProcessHandle)
prepareAndCallVSE :: IO (Handle, Handle, ProcessHandle)
prepareAndCallVSE = do
  String
vseBin <- IO String
vseBinary
  (inp :: Handle
inp, out :: Handle
out, _, cp :: ProcessHandle
cp) <-
      String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess String
vseBin ["-std"] Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing
  ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
nameP
  (Handle, Handle, ProcessHandle)
-> IO (Handle, Handle, ProcessHandle)
forall (m :: * -> *) a. Monad m => a -> m a
return (Handle
inp, Handle
out, ProcessHandle
cp)

readFinalVSEOutput :: ProcessHandle -> Handle
                   -> IO (Maybe (Map.Map String [String]))
readFinalVSEOutput :: ProcessHandle -> Handle -> IO (Maybe (Map String [String]))
readFinalVSEOutput cp :: ProcessHandle
cp out :: Handle
out = do
  Maybe ExitCode
ms <- ProcessHandle -> IO (Maybe ExitCode)
getProcessExitCode ProcessHandle
cp
  case Maybe ExitCode
ms of
    Just _ -> do
      String -> String -> IO ()
appendFile String
vseErrFile "hetsvse unavailable\n"
      Maybe (Map String [String]) -> IO (Maybe (Map String [String]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map String [String])
forall a. Maybe a
Nothing
    Nothing -> do
      String
revres <- ProcessHandle -> Handle -> String -> IO String
readRest ProcessHandle
cp Handle
out ""
      let res :: String
res = String -> String
forall a. [a] -> [a]
reverse String
revres
      String -> String -> IO ()
writeFile "hetsvse-debug.txt" String
res
      case ParsecT String () Identity [SExpr]
-> String -> String -> Either ParseError [SExpr]
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse ParsecT String () Identity [SExpr]
parseSExprs String
vseErrFile String
res of
        Right l :: [SExpr]
l -> Maybe (Map String [String]) -> IO (Maybe (Map String [String]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Map String [String]) -> IO (Maybe (Map String [String])))
-> Maybe (Map String [String]) -> IO (Maybe (Map String [String]))
forall a b. (a -> b) -> a -> b
$ Map String [String] -> Maybe (Map String [String])
forall a. a -> Maybe a
Just (Map String [String] -> Maybe (Map String [String]))
-> Map String [String] -> Maybe (Map String [String])
forall a b. (a -> b) -> a -> b
$ [SExpr] -> Map String [String]
readLemmas [SExpr]
l
        Left e :: ParseError
e -> do
          ParseError -> IO ()
forall a. Show a => a -> IO ()
print ParseError
e
          String -> String -> IO ()
appendFile String
vseErrFile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
          Maybe (Map String [String]) -> IO (Maybe (Map String [String]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Map String [String])
forall a. Maybe a
Nothing

readLemmas :: [SExpr] -> Map.Map String [String]
readLemmas :: [SExpr] -> Map String [String]
readLemmas =
  ((String, String) -> Map String [String] -> Map String [String])
-> Map String [String] -> [(String, String)] -> Map String [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (node :: String
node, sen :: String
sen) -> ([String] -> [String] -> [String])
-> String -> [String] -> Map String [String] -> Map String [String]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
(++) String
node [String
sen]) Map String [String]
forall k a. Map k a
Map.empty
  ([(String, String)] -> Map String [String])
-> ([SExpr] -> [(String, String)])
-> [SExpr]
-> Map String [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SExpr -> Maybe (String, String)) -> [SExpr] -> [(String, String)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SExpr -> Maybe (String, String)
findState

prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
prove ostr :: String
ostr (Theory sig :: VSESign
sig thsens :: ThSens Sentence (ProofStatus ())
thsens) _freedefs :: a
_freedefs = do
  let str :: String
str = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '/' then '-' else Char
c) String
ostr
      oSens :: [Named Sentence]
oSens = ThSens Sentence (ProofStatus ()) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ())
thsens
      (fsig :: VSESign
fsig, sens :: [Named Sentence]
sens) = VSESign -> [Named Sentence] -> (VSESign, [Named Sentence])
forall f.
Sign f Procs
-> [Named Sentence] -> (Sign f Procs, [Named Sentence])
addUniformRestr VSESign
sig [Named Sentence]
oSens
      (disAxs :: [Named Sentence]
disAxs, disGoals :: [Named Sentence]
disGoals) = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named Sentence]
oSens
      rMap :: Map String String
rMap = [(String, String)] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, String)] -> Map String String)
-> [(String, String)] -> Map String String
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> (String, String))
-> [Named Sentence] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ SenAttr { senAttr :: forall s a. SenAttr s a -> a
senAttr = String
n } ->
                ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
transString String
n, String
n)) [Named Sentence]
disGoals
#ifdef TAR_PACKAGE
  String -> IO ()
moveVSEFiles String
str
#endif
  (inp :: Handle
inp, out :: Handle
out, cp :: ProcessHandle
cp) <- IO (Handle, Handle, ProcessHandle)
prepareAndCallVSE
  Handle -> String -> IO ()
sendMyMsg Handle
inp (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
  ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
linksP
  Handle -> String -> IO ()
sendMyMsg Handle
inp "nil"
  ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
sigP
  Handle -> String -> IO ()
sendMyMsg Handle
inp (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SExpr -> Doc
prettySExpr (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ VSESign -> SExpr
forall f. Sign f Procs -> SExpr
vseSignToSExpr VSESign
fsig
  ProcessHandle -> Handle -> String -> IO String
readMyMsg ProcessHandle
cp Handle
out String
lemsP
  Handle -> String -> IO ()
sendMyMsg Handle
inp (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SExpr -> Doc
prettySExpr (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
SList ([SExpr] -> SExpr) -> [SExpr] -> SExpr
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> SExpr) -> [Named Sentence] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (VSESign -> Named Sentence -> SExpr
forall f. Sign f Procs -> Named Sentence -> SExpr
namedSenToSExpr VSESign
fsig) [Named Sentence]
sens
  Maybe (Map String [String])
ms <- ProcessHandle -> Handle -> IO (Maybe (Map String [String]))
readFinalVSEOutput ProcessHandle
cp Handle
out
#ifdef TAR_PACKAGE
  String -> IO ()
createVSETarFile String
str
#endif
  case Maybe (Map String [String])
ms of
    Nothing -> [ProofStatus ()] -> IO [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just lemMap :: Map String [String]
lemMap -> [ProofStatus ()] -> IO [ProofStatus ()]
forall (m :: * -> *) a. Monad m => a -> m a
return
          ([ProofStatus ()] -> IO [ProofStatus ()])
-> [ProofStatus ()] -> IO [ProofStatus ()]
forall a b. (a -> b) -> a -> b
$ (String -> [ProofStatus ()] -> [ProofStatus ()])
-> [ProofStatus ()] -> [String] -> [ProofStatus ()]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ s :: String
s r :: [ProofStatus ()]
r -> case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String String
rMap of
                 Nothing -> [ProofStatus ()]
r
                 Just n :: String
n -> String -> [String] -> ProofStatus ()
mkVseProofStatus String
n ((Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr [Named Sentence]
disAxs) ProofStatus () -> [ProofStatus ()] -> [ProofStatus ()]
forall a. a -> [a] -> [a]
: [ProofStatus ()]
r) []
          ([String] -> [ProofStatus ()]) -> [String] -> [ProofStatus ()]
forall a b. (a -> b) -> a -> b
$ [String] -> String -> Map String [String] -> [String]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [] ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
str) Map String [String]
lemMap