module Jukebox.TPTP.ParseProblem where
import Jukebox.ProgressBar
import Jukebox.TPTP.FindFile
import Jukebox.TPTP.ClauseParser
import Jukebox.TPTP.Lexer hiding (Include, Error)
import Jukebox.TPTP.Parsec
import Jukebox.TPTP.Print
import qualified Jukebox.TPTP.Lexer as L
import Control.Monad.Error
import Jukebox.Form hiding (Pos)
import qualified Data.ByteString.Lazy.Char8 as BSL
import qualified Data.ByteString.Char8 as BS
import Control.Monad.Identity
import Control.Exception
import Prelude hiding (catch)
import Data.List
import Jukebox.Name
parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblem dirs name = withProgressBar $ \pb -> parseProblemWith (findFileTPTP dirs) pb name
parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> ProgressBar -> FilePath -> IO (Either String (Problem Form))
parseProblemWith findFile progressBar name = runErrorT (fmap finalise (parseFile name Nothing "<command line>" (Pos 0 0) initialState))
where err file (Pos l c) msg = throwError msg'
where msg' = "Error at " ++ file ++ " (line " ++ show l ++ ", column " ++ show c ++ "):\n" ++ msg
liftMaybeIO :: IO (Maybe a) -> FilePath -> Pos -> String -> ErrorT String IO a
liftMaybeIO m file pos msg = do
x <- liftIO m
case x of
Nothing -> err file pos msg
Just x -> return x
liftEitherIO :: IO (Either a b) -> FilePath -> Pos -> (a -> String) -> ErrorT String IO b
liftEitherIO m file pos msg = do
x <- liftIO m
case x of
Left e -> err file pos (msg e)
Right x -> return x
parseFile :: FilePath -> Maybe [Tag] -> FilePath -> Pos ->
ParseState -> ErrorT FilePath IO ParseState
parseFile name clauses file0 pos st = do
file <- liftMaybeIO (findFile name) file0 pos ("File " ++ name ++ " not found")
liftIO $ enter progressBar $ "Reading " ++ file
contents <- liftEitherIO
(fmap Right (BSL.readFile file >>= tickOnRead progressBar)
`catch` (\(e :: IOException) -> return (Left e)))
file (Pos 0 0) show
let s = UserState st (scan contents)
fmap userState (parseSections clauses file s)
parseSections :: Maybe [Tag] -> FilePath -> ParsecState -> ErrorT String IO ParsecState
parseSections clauses file s =
let report UserState{userStream = At _ (Cons Eof _)} =
["Unexpected end of file"]
report UserState{userStream = At _ (Cons L.Error _)} =
["Lexical error"]
report UserState{userStream = At _ (Cons t _)} =
["Unexpected " ++ show t] in
case run report (section (included clauses)) s of
(UserState{userStream=At pos _}, Left e) ->
err file pos (concat (intersperse "\n" e))
(s'@UserState{userStream=At _ (Cons Eof _)}, Right Nothing) -> do
liftIO $ leave progressBar
return s'
(UserState{userStream=stream@(At pos _),userState=state},
Right (Just (Include name clauses'))) -> do
s' <- parseFile (BS.unpack name) (clauses `merge` clauses') file pos state
parseSections clauses file (UserState s' stream)
included :: Maybe [Tag] -> Tag -> Bool
included Nothing _ = True
included (Just xs) x = x `elem` xs
merge :: Maybe [Tag] -> Maybe [Tag] -> Maybe [Tag]
merge Nothing x = x
merge x Nothing = x
merge (Just xs) (Just ys) = Just (xs `intersect` ys)
finalise :: ParseState -> Problem Form
finalise (MkState p _ _ _ _ n) = close_ n (return (reverse p))