Documentation

vseProverName :: String

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

vse :: Prover VSESign Sentence VSEMor () ()

nameP :: String

linksP :: String

sigP :: String

lemsP :: String

prx :: String -> String

data MaybeChar

vseErrFile :: String

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

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

myGetChar :: ProcessHandle -> Handle -> IO MaybeChar

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

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

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

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

parseSymbol :: Parser SExpr

parseList :: Parser SExpr

parseSExpr :: Parser SExpr

skipWhite :: Parser a -> Parser a

skipJunk :: Parser ()

parseSExprs :: Parser [SExpr]

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

specDir :: String

allSpecFile :: String

allSpecInDir :: String

createVSETarFile :: FilePath -> IO ()

moveVSEFiles :: FilePath -> IO ()

vseBinary :: IO String

prepareAndCallVSE :: IO (Handle, Handle, ProcessHandle)

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

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

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