module Jukebox.TPTP.Parse where
import Jukebox.TPTP.FindFile
import qualified Jukebox.TPTP.Parse.Core as Parser
import Control.Monad.IO.Class
import Control.Monad.Trans.Except
import Jukebox.Form hiding (Pos, run)
import Control.Exception
import Data.List
parseString :: String -> IO (Problem Form)
parseString xs =
case Parser.parseProblem "<string>" xs of
Parser.ParseFailed loc msg ->
error ("Parse error at " ++ show loc ++ ":\n" ++ unlines msg)
Parser.ParseSucceeded prob ->
return prob
Parser.ParseStalled loc _ _ ->
error ("Include directive found at " ++ show loc)
parseProblem :: (FilePath -> IO ()) -> [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblem found dirs name = parseProblemWith found (findFileTPTP dirs) name
parseProblemWith :: (FilePath -> IO ()) -> (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))
parseProblemWith found findFile name =
runExceptT $ do
file <- readInFile (Parser.Location "<command line>" 0 0) name
process (Parser.parseProblem name file)
where
err loc msg = throwE msg'
where
msg' = "Error in " ++ show loc ++ ":\n" ++ msg
readInFile _ "-" =
ExceptT $ do
liftIO (found "standard input")
fmap Right getContents `catch`
\(e :: IOException) -> return (Left (show e))
readInFile pos name = do
mfile <- liftIO (findFile name)
case mfile of
Nothing ->
err pos ("File '" ++ name ++ "' not found")
Just file ->
ExceptT $ do
liftIO (found file)
fmap Right (readFile file) `catch`
\(e :: IOException) -> return (Left (show e))
process (Parser.ParseFailed loc msg) = err loc (intercalate "\n" msg)
process (Parser.ParseSucceeded prob) = return prob
process (Parser.ParseStalled loc name cont) = do
file <- readInFile loc name
process (cont file)