{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DeriveTraversable #-} {-| Module : ATP.Error Description : Monads and monad transformers for computations with errors. Copyright : (c) Evgenii Kotelnikov, 2019-2021 License : GPL-3 Maintainer : evgeny.kotelnikov@gmail.com Stability : experimental Monads and monad transformers for computations with errors. -} module ATP.Error ( Error(..), Partial, PartialT(..), liftPartial, isSuccess, isFailure, exitCodeError, timeLimitError, memoryLimitError, parsingError, proofError, otherError ) where import Control.Monad.Except (MonadTrans, ExceptT(..), MonadError(..), runExcept) import Data.Either (isLeft, isRight) import Data.Functor.Identity (Identity) import Data.Text (Text) import qualified Data.Text as T (pack) -- | The error that might occur while reconstructing the proof. data Error = ExitCodeError Int Text -- ^ The theorem prover terminated with a non-zero exit code. | TimeLimitError -- ^ The theorem prover reached the time limit without producing a solution. | MemoryLimitError -- ^ The theorem prover reached the memory limit without producing a solution. | ParsingError Text -- ^ The output of the theorem prover is not a well-formed TSTP. | ProofError Text -- ^ The proof returned by the theorem prover is not well-formed. | OtherError Text -- ^ An uncategorized error. deriving (Int -> Error -> ShowS [Error] -> ShowS Error -> String (Int -> Error -> ShowS) -> (Error -> String) -> ([Error] -> ShowS) -> Show Error forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Error] -> ShowS $cshowList :: [Error] -> ShowS show :: Error -> String $cshow :: Error -> String showsPrec :: Int -> Error -> ShowS $cshowsPrec :: Int -> Error -> ShowS Show, Error -> Error -> Bool (Error -> Error -> Bool) -> (Error -> Error -> Bool) -> Eq Error forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Error -> Error -> Bool $c/= :: Error -> Error -> Bool == :: Error -> Error -> Bool $c== :: Error -> Error -> Bool Eq, Eq Error Eq Error -> (Error -> Error -> Ordering) -> (Error -> Error -> Bool) -> (Error -> Error -> Bool) -> (Error -> Error -> Bool) -> (Error -> Error -> Bool) -> (Error -> Error -> Error) -> (Error -> Error -> Error) -> Ord Error Error -> Error -> Bool Error -> Error -> Ordering Error -> Error -> Error forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Error -> Error -> Error $cmin :: Error -> Error -> Error max :: Error -> Error -> Error $cmax :: Error -> Error -> Error >= :: Error -> Error -> Bool $c>= :: Error -> Error -> Bool > :: Error -> Error -> Bool $c> :: Error -> Error -> Bool <= :: Error -> Error -> Bool $c<= :: Error -> Error -> Bool < :: Error -> Error -> Bool $c< :: Error -> Error -> Bool compare :: Error -> Error -> Ordering $ccompare :: Error -> Error -> Ordering $cp1Ord :: Eq Error Ord) -- | The type of computations that might fail with an @'Error'@. type Partial = PartialT Identity -- | A monad transformer that adds failing with an @'Error'@ to other monads. newtype PartialT m a = PartialT { PartialT m a -> ExceptT Error m a runPartialT :: ExceptT Error m a } deriving (Int -> PartialT m a -> ShowS [PartialT m a] -> ShowS PartialT m a -> String (Int -> PartialT m a -> ShowS) -> (PartialT m a -> String) -> ([PartialT m a] -> ShowS) -> Show (PartialT m a) forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a forall (m :: * -> *) a. (Show1 m, Show a) => Int -> PartialT m a -> ShowS forall (m :: * -> *) a. (Show1 m, Show a) => [PartialT m a] -> ShowS forall (m :: * -> *) a. (Show1 m, Show a) => PartialT m a -> String showList :: [PartialT m a] -> ShowS $cshowList :: forall (m :: * -> *) a. (Show1 m, Show a) => [PartialT m a] -> ShowS show :: PartialT m a -> String $cshow :: forall (m :: * -> *) a. (Show1 m, Show a) => PartialT m a -> String showsPrec :: Int -> PartialT m a -> ShowS $cshowsPrec :: forall (m :: * -> *) a. (Show1 m, Show a) => Int -> PartialT m a -> ShowS Show, PartialT m a -> PartialT m a -> Bool (PartialT m a -> PartialT m a -> Bool) -> (PartialT m a -> PartialT m a -> Bool) -> Eq (PartialT m a) forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall (m :: * -> *) a. (Eq1 m, Eq a) => PartialT m a -> PartialT m a -> Bool /= :: PartialT m a -> PartialT m a -> Bool $c/= :: forall (m :: * -> *) a. (Eq1 m, Eq a) => PartialT m a -> PartialT m a -> Bool == :: PartialT m a -> PartialT m a -> Bool $c== :: forall (m :: * -> *) a. (Eq1 m, Eq a) => PartialT m a -> PartialT m a -> Bool Eq, Eq (PartialT m a) Eq (PartialT m a) -> (PartialT m a -> PartialT m a -> Ordering) -> (PartialT m a -> PartialT m a -> Bool) -> (PartialT m a -> PartialT m a -> Bool) -> (PartialT m a -> PartialT m a -> Bool) -> (PartialT m a -> PartialT m a -> Bool) -> (PartialT m a -> PartialT m a -> PartialT m a) -> (PartialT m a -> PartialT m a -> PartialT m a) -> Ord (PartialT m a) PartialT m a -> PartialT m a -> Bool PartialT m a -> PartialT m a -> Ordering PartialT m a -> PartialT m a -> PartialT m a forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall (m :: * -> *) a. (Ord1 m, Ord a) => Eq (PartialT m a) forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Bool forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Ordering forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> PartialT m a min :: PartialT m a -> PartialT m a -> PartialT m a $cmin :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> PartialT m a max :: PartialT m a -> PartialT m a -> PartialT m a $cmax :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> PartialT m a >= :: PartialT m a -> PartialT m a -> Bool $c>= :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Bool > :: PartialT m a -> PartialT m a -> Bool $c> :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Bool <= :: PartialT m a -> PartialT m a -> Bool $c<= :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Bool < :: PartialT m a -> PartialT m a -> Bool $c< :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Bool compare :: PartialT m a -> PartialT m a -> Ordering $ccompare :: forall (m :: * -> *) a. (Ord1 m, Ord a) => PartialT m a -> PartialT m a -> Ordering $cp1Ord :: forall (m :: * -> *) a. (Ord1 m, Ord a) => Eq (PartialT m a) Ord, a -> PartialT m b -> PartialT m a (a -> b) -> PartialT m a -> PartialT m b (forall a b. (a -> b) -> PartialT m a -> PartialT m b) -> (forall a b. a -> PartialT m b -> PartialT m a) -> Functor (PartialT m) forall a b. a -> PartialT m b -> PartialT m a forall a b. (a -> b) -> PartialT m a -> PartialT m b forall (m :: * -> *) a b. Functor m => a -> PartialT m b -> PartialT m a forall (m :: * -> *) a b. Functor m => (a -> b) -> PartialT m a -> PartialT m b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> PartialT m b -> PartialT m a $c<$ :: forall (m :: * -> *) a b. Functor m => a -> PartialT m b -> PartialT m a fmap :: (a -> b) -> PartialT m a -> PartialT m b $cfmap :: forall (m :: * -> *) a b. Functor m => (a -> b) -> PartialT m a -> PartialT m b Functor, Functor (PartialT m) a -> PartialT m a Functor (PartialT m) -> (forall a. a -> PartialT m a) -> (forall a b. PartialT m (a -> b) -> PartialT m a -> PartialT m b) -> (forall a b c. (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c) -> (forall a b. PartialT m a -> PartialT m b -> PartialT m b) -> (forall a b. PartialT m a -> PartialT m b -> PartialT m a) -> Applicative (PartialT m) PartialT m a -> PartialT m b -> PartialT m b PartialT m a -> PartialT m b -> PartialT m a PartialT m (a -> b) -> PartialT m a -> PartialT m b (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c forall a. a -> PartialT m a forall a b. PartialT m a -> PartialT m b -> PartialT m a forall a b. PartialT m a -> PartialT m b -> PartialT m b forall a b. PartialT m (a -> b) -> PartialT m a -> PartialT m b forall a b c. (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c forall (m :: * -> *). Monad m => Functor (PartialT m) forall (m :: * -> *) a. Monad m => a -> PartialT m a forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m a forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m b forall (m :: * -> *) a b. Monad m => PartialT m (a -> b) -> PartialT m a -> PartialT m b forall (m :: * -> *) a b c. Monad m => (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c forall (f :: * -> *). Functor f -> (forall a. a -> f a) -> (forall a b. f (a -> b) -> f a -> f b) -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c) -> (forall a b. f a -> f b -> f b) -> (forall a b. f a -> f b -> f a) -> Applicative f <* :: PartialT m a -> PartialT m b -> PartialT m a $c<* :: forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m a *> :: PartialT m a -> PartialT m b -> PartialT m b $c*> :: forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m b liftA2 :: (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c $cliftA2 :: forall (m :: * -> *) a b c. Monad m => (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c <*> :: PartialT m (a -> b) -> PartialT m a -> PartialT m b $c<*> :: forall (m :: * -> *) a b. Monad m => PartialT m (a -> b) -> PartialT m a -> PartialT m b pure :: a -> PartialT m a $cpure :: forall (m :: * -> *) a. Monad m => a -> PartialT m a $cp1Applicative :: forall (m :: * -> *). Monad m => Functor (PartialT m) Applicative, Applicative (PartialT m) a -> PartialT m a Applicative (PartialT m) -> (forall a b. PartialT m a -> (a -> PartialT m b) -> PartialT m b) -> (forall a b. PartialT m a -> PartialT m b -> PartialT m b) -> (forall a. a -> PartialT m a) -> Monad (PartialT m) PartialT m a -> (a -> PartialT m b) -> PartialT m b PartialT m a -> PartialT m b -> PartialT m b forall a. a -> PartialT m a forall a b. PartialT m a -> PartialT m b -> PartialT m b forall a b. PartialT m a -> (a -> PartialT m b) -> PartialT m b forall (m :: * -> *). Monad m => Applicative (PartialT m) forall (m :: * -> *) a. Monad m => a -> PartialT m a forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m b forall (m :: * -> *) a b. Monad m => PartialT m a -> (a -> PartialT m b) -> PartialT m b forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> (forall a. a -> m a) -> Monad m return :: a -> PartialT m a $creturn :: forall (m :: * -> *) a. Monad m => a -> PartialT m a >> :: PartialT m a -> PartialT m b -> PartialT m b $c>> :: forall (m :: * -> *) a b. Monad m => PartialT m a -> PartialT m b -> PartialT m b >>= :: PartialT m a -> (a -> PartialT m b) -> PartialT m b $c>>= :: forall (m :: * -> *) a b. Monad m => PartialT m a -> (a -> PartialT m b) -> PartialT m b $cp1Monad :: forall (m :: * -> *). Monad m => Applicative (PartialT m) Monad, m a -> PartialT m a (forall (m :: * -> *) a. Monad m => m a -> PartialT m a) -> MonadTrans PartialT forall (m :: * -> *) a. Monad m => m a -> PartialT m a forall (t :: (* -> *) -> * -> *). (forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t lift :: m a -> PartialT m a $clift :: forall (m :: * -> *) a. Monad m => m a -> PartialT m a MonadTrans, MonadError Error) -- | Extractor for computations in the @'Partial'@ monad. liftPartial :: Partial a -> Either Error a liftPartial :: Partial a -> Either Error a liftPartial = Except Error a -> Either Error a forall e a. Except e a -> Either e a runExcept (Except Error a -> Either Error a) -> (Partial a -> Except Error a) -> Partial a -> Either Error a forall b c a. (b -> c) -> (a -> b) -> a -> c . Partial a -> Except Error a forall (m :: * -> *) a. PartialT m a -> ExceptT Error m a runPartialT -- | Check whether a partial computation resulted successfully. isSuccess :: Partial a -> Bool isSuccess :: Partial a -> Bool isSuccess = Either Error a -> Bool forall a b. Either a b -> Bool isRight (Either Error a -> Bool) -> (Partial a -> Either Error a) -> Partial a -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Partial a -> Either Error a forall a. Partial a -> Either Error a liftPartial -- | Check whether a partial computation resulted with an error. isFailure :: Partial a -> Bool isFailure :: Partial a -> Bool isFailure = Either Error a -> Bool forall a b. Either a b -> Bool isLeft (Either Error a -> Bool) -> (Partial a -> Either Error a) -> Partial a -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Partial a -> Either Error a forall a. Partial a -> Either Error a liftPartial -- | A smart constructor for a computation failed with an @'ExitCodeError'@. exitCodeError :: Monad m => Int -> Text -> PartialT m a exitCodeError :: Int -> Text -> PartialT m a exitCodeError Int exitCode Text err = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (Error -> ExceptT Error m a) -> Error -> ExceptT Error m a forall a b. (a -> b) -> a -> b $ Int -> Text -> Error ExitCodeError Int exitCode Text err) -- | A smart constructor for a computation failed with a @'TimeLimitError'@. timeLimitError :: Monad m => PartialT m a timeLimitError :: PartialT m a timeLimitError = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError Error TimeLimitError) -- | A smart constructor for a computation failed with a @'MemoryLimitError'@. memoryLimitError :: Monad m => PartialT m a memoryLimitError :: PartialT m a memoryLimitError = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError Error MemoryLimitError) -- | A smart constructor for a computation failed with a @'ParsingError'@. parsingError :: Monad m => String -> PartialT m a parsingError :: String -> PartialT m a parsingError = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (ExceptT Error m a -> PartialT m a) -> (String -> ExceptT Error m a) -> String -> PartialT m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (Error -> ExceptT Error m a) -> (String -> Error) -> String -> ExceptT Error m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Text -> Error ParsingError (Text -> Error) -> (String -> Text) -> String -> Error forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> Text T.pack -- | A smart constructor for a computation failed with a @'ProofError'@. proofError :: Monad m => String -> PartialT m a proofError :: String -> PartialT m a proofError = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (ExceptT Error m a -> PartialT m a) -> (String -> ExceptT Error m a) -> String -> PartialT m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (Error -> ExceptT Error m a) -> (String -> Error) -> String -> ExceptT Error m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Text -> Error ProofError (Text -> Error) -> (String -> Text) -> String -> Error forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> Text T.pack -- | A smart constructor for a computation failed with a @'OtherError'@. otherError :: Monad m => String -> PartialT m a otherError :: String -> PartialT m a otherError = ExceptT Error m a -> PartialT m a forall (m :: * -> *) a. ExceptT Error m a -> PartialT m a PartialT (ExceptT Error m a -> PartialT m a) -> (String -> ExceptT Error m a) -> String -> PartialT m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Error -> ExceptT Error m a forall e (m :: * -> *) a. MonadError e m => e -> m a throwError (Error -> ExceptT Error m a) -> (String -> Error) -> String -> ExceptT Error m a forall b c a. (b -> c) -> (a -> b) -> a -> c . Text -> Error OtherError (Text -> Error) -> (String -> Text) -> String -> Error forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> Text T.pack