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