{-# LANGUAGE ScopedTypeVariables #-}
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 :: String -> IO (Problem Form)
parseString String
xs =
  case String -> String -> ParseResult (Problem Form)
Parser.parseProblem String
"<string>" String
xs of
    Parser.ParseFailed Location
loc [String]
msg ->
      String -> IO (Problem Form)
forall a. HasCallStack => String -> a
error (String
"Parse error at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Location -> String
forall a. Show a => a -> String
show Location
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
msg)
    Parser.ParseSucceeded Problem Form
prob ->
      Problem Form -> IO (Problem Form)
forall (m :: * -> *) a. Monad m => a -> m a
return Problem Form
prob
    Parser.ParseStalled Location
loc String
_ String -> ParseResult (Problem Form)
_ ->
      String -> IO (Problem Form)
forall a. HasCallStack => String -> a
error (String
"Include directive found at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Location -> String
forall a. Show a => a -> String
show Location
loc)

parseProblem :: [FilePath] -> FilePath -> IO (Either String (Problem Form))
parseProblem :: [String] -> String -> IO (Either String (Problem Form))
parseProblem [String]
dirs String
name = (String -> IO (Maybe String))
-> String -> IO (Either String (Problem Form))
parseProblemWith ([String] -> String -> IO (Maybe String)
findFileTPTP [String]
dirs) String
name

parseProblemWith :: (FilePath -> IO (Maybe FilePath)) -> FilePath -> IO (Either String (Problem Form))
parseProblemWith :: (String -> IO (Maybe String))
-> String -> IO (Either String (Problem Form))
parseProblemWith String -> IO (Maybe String)
findFile String
name =
  ExceptT String IO (Problem Form)
-> IO (Either String (Problem Form))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String IO (Problem Form)
 -> IO (Either String (Problem Form)))
-> ExceptT String IO (Problem Form)
-> IO (Either String (Problem Form))
forall a b. (a -> b) -> a -> b
$ do
    String
file <- Location -> String -> ExceptT String IO String
forall a. Show a => a -> String -> ExceptT String IO String
readInFile (String -> Integer -> Integer -> Location
Parser.Location String
"<command line>" Integer
0 Integer
0) String
name
    ParseResult (Problem Form) -> ExceptT String IO (Problem Form)
forall a. ParseResult a -> ExceptT String IO a
process (String -> String -> ParseResult (Problem Form)
Parser.parseProblem String
name String
file)

  where
    err :: a -> String -> ExceptT String m a
err a
loc String
msg = String -> ExceptT String m a
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE String
msg'
      where
        msg' :: String
msg' = String
"Error in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
loc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg

    readInFile :: a -> String -> ExceptT String IO String
readInFile a
_ String
"-" =
      IO (Either String String) -> ExceptT String IO String
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either String String) -> ExceptT String IO String)
-> IO (Either String String) -> ExceptT String IO String
forall a b. (a -> b) -> a -> b
$ do
        (String -> Either String String)
-> IO String -> IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Either String String
forall a b. b -> Either a b
Right IO String
getContents IO (Either String String)
-> (IOException -> IO (Either String String))
-> IO (Either String String)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch`
          \(IOException
e :: IOException) -> Either String String -> IO (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String String
forall a b. a -> Either a b
Left (IOException -> String
forall a. Show a => a -> String
show IOException
e))
    readInFile a
pos String
name = do
      Maybe String
mfile <- IO (Maybe String) -> ExceptT String IO (Maybe String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO (Maybe String)
findFile String
name)
      case Maybe String
mfile of
        Maybe String
Nothing ->
          a -> String -> ExceptT String IO String
forall (m :: * -> *) a a.
(Monad m, Show a) =>
a -> String -> ExceptT String m a
err a
pos (String
"File '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' not found")
        Just String
file ->
          IO (Either String String) -> ExceptT String IO String
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (Either String String) -> ExceptT String IO String)
-> IO (Either String String) -> ExceptT String IO String
forall a b. (a -> b) -> a -> b
$ do
            (String -> Either String String)
-> IO String -> IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Either String String
forall a b. b -> Either a b
Right (String -> IO String
readFile String
file) IO (Either String String)
-> (IOException -> IO (Either String String))
-> IO (Either String String)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch`
              \(IOException
e :: IOException) -> Either String String -> IO (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String String
forall a b. a -> Either a b
Left (IOException -> String
forall a. Show a => a -> String
show IOException
e))

    process :: ParseResult a -> ExceptT String IO a
process (Parser.ParseFailed Location
loc [String]
msg) = Location -> String -> ExceptT String IO a
forall (m :: * -> *) a a.
(Monad m, Show a) =>
a -> String -> ExceptT String m a
err Location
loc (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
msg)
    process (Parser.ParseSucceeded a
prob) = a -> ExceptT String IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
prob
    process (Parser.ParseStalled Location
loc String
name String -> ParseResult a
cont) = do
      String
file <- Location -> String -> ExceptT String IO String
forall a. Show a => a -> String -> ExceptT String IO String
readInFile Location
loc String
name
      ParseResult a -> ExceptT String IO a
process (String -> ParseResult a
cont String
file)