Hets - the Heterogeneous Tool Set
Copyright(c) C. Maeder DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

VSE.Prove

Description

call an adaption of VSE II to hets

Documentation

vseProverName :: String Source #

mkVseProofStatus :: String -> [String] -> ProofStatus () Source #

vse :: Prover VSESign Sentence VSEMor () () Source #

nameP :: String Source #

linksP :: String Source #

sigP :: String Source #

lemsP :: String Source #

prx :: String -> String Source #

data MaybeChar Source #

Constructors

Wait 
Stop 
JustChar Char 

vseErrFile :: String Source #

readUntilMatchParen :: ProcessHandle -> Handle -> String -> IO String Source #

readUntilMatchParenAux :: Int -> ProcessHandle -> Handle -> String -> IO String Source #

myGetChar :: ProcessHandle -> Handle -> IO MaybeChar Source #

readMyMsg :: ProcessHandle -> Handle -> String -> IO String Source #

readMyMsgAux :: Int -> ProcessHandle -> Handle -> String -> IO String Source #

sendMyMsg :: Handle -> String -> IO () Source #

readRest :: ProcessHandle -> Handle -> String -> IO String Source #

parseSymbol :: Parser SExpr Source #

parseList :: Parser SExpr Source #

parseSExpr :: Parser SExpr Source #

skipWhite :: Parser a -> Parser a Source #

skipJunk :: Parser () Source #

parseSExprs :: Parser [SExpr] Source #

findState :: SExpr -> Maybe (String, String) Source #

specDir :: String Source #

allSpecFile :: String Source #

allSpecInDir :: String Source #

createVSETarFile :: FilePath -> IO () Source #

moveVSEFiles :: FilePath -> IO () Source #

vseBinary :: IO String Source #

prepareAndCallVSE :: IO (Handle, Handle, ProcessHandle) Source #

readFinalVSEOutput :: ProcessHandle -> Handle -> IO (Maybe (Map String [String])) Source #

readLemmas :: [SExpr] -> Map String [String] Source #

prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()] Source #