{-# 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)