Copyright	(c) Evgenii Kotelnikov 2019-2021
License	GPL-3
Maintainer	evgeny.kotelnikov@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

ATP.Error

Description

Monads and monad transformers for computations with errors.

Synopsis

data Error
- = ExitCodeError Int Text
- | TimeLimitError
- | MemoryLimitError
- | ParsingError Text
- | ProofError Text
- | OtherError Text
type Partial = PartialT Identity
newtype PartialT m a = PartialT {
- runPartialT :: ExceptT Error m a
}
liftPartial :: Partial a -> Either Error a
isSuccess :: Partial a -> Bool
isFailure :: Partial a -> Bool
exitCodeError :: Monad m => Int -> Text -> PartialT m a
timeLimitError :: Monad m => PartialT m a
memoryLimitError :: Monad m => PartialT m a
parsingError :: Monad m => String -> PartialT m a
proofError :: Monad m => String -> PartialT m a
otherError :: Monad m => String -> PartialT m a

Documentation

data Error Source #

The error that might occur while reconstructing the proof.

Constructors

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.

Instances

Instances details

Eq Error Source #
Instance details Defined in ATP.Error Methods (==) :: Error -> Error -> Bool # (/=) :: Error -> Error -> Bool #
Ord Error Source #
Instance details Defined in ATP.Error Methods compare :: Error -> Error -> Ordering # (<) :: Error -> Error -> Bool # (<=) :: Error -> Error -> Bool # (>) :: Error -> Error -> Bool # (>=) :: Error -> Error -> Bool # max :: Error -> Error -> Error # min :: Error -> Error -> Error #
Show Error Source #
Instance details Defined in ATP.Error Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #
Pretty Error Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Error -> Doc # prettyList :: [Error] -> Doc #
Monad m => MonadError Error (PartialT m) Source #
Instance details Defined in ATP.Error Methods throwError :: Error -> PartialT m a # catchError :: PartialT m a -> (Error -> PartialT m a) -> PartialT m a #

type Partial = PartialT Identity Source #

The type of computations that might fail with an Error.

newtype PartialT m a Source #

A monad transformer that adds failing with an Error to other monads.

Constructors

PartialT
Fields runPartialT :: ExceptT Error m a

Instances

Instances details

MonadTrans PartialT Source #
Instance details Defined in ATP.Error Methods lift :: Monad m => m a -> PartialT m a #
Monad m => MonadError Error (PartialT m) Source #
Instance details Defined in ATP.Error Methods throwError :: Error -> PartialT m a # catchError :: PartialT m a -> (Error -> PartialT m a) -> PartialT m a #
Monad m => Monad (PartialT m) Source #
Instance details Defined in ATP.Error Methods (>>=) :: PartialT m a -> (a -> PartialT m b) -> PartialT m b # (>>) :: PartialT m a -> PartialT m b -> PartialT m b # return :: a -> PartialT m a #
Functor m => Functor (PartialT m) Source #
Instance details Defined in ATP.Error Methods fmap :: (a -> b) -> PartialT m a -> PartialT m b # (<$) :: a -> PartialT m b -> PartialT m a #
Monad m => Applicative (PartialT m) Source #
Instance details Defined in ATP.Error Methods pure :: a -> PartialT m a # (<>) :: PartialT m (a -> b) -> PartialT m a -> PartialT m b # liftA2 :: (a -> b -> c) -> PartialT m a -> PartialT m b -> PartialT m c # (>) :: PartialT m a -> PartialT m b -> PartialT m b # (<*) :: PartialT m a -> PartialT m b -> PartialT m a #
Pretty a => Pretty (Partial a) Source #
Instance details Defined in ATP.Pretty.FOL Methods pretty :: Partial a -> Doc # prettyList :: [Partial a] -> Doc #
(Eq1 m, Eq a) => Eq (PartialT m a) Source #
Instance details Defined in ATP.Error Methods (==) :: PartialT m a -> PartialT m a -> Bool # (/=) :: PartialT m a -> PartialT m a -> Bool #
(Ord1 m, Ord a) => Ord (PartialT m a) Source #
Instance details Defined in ATP.Error Methods compare :: 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 # max :: PartialT m a -> PartialT m a -> PartialT m a # min :: PartialT m a -> PartialT m a -> PartialT m a #
(Show1 m, Show a) => Show (PartialT m a) Source #
Instance details Defined in ATP.Error Methods showsPrec :: Int -> PartialT m a -> ShowS # show :: PartialT m a -> String # showList :: [PartialT m a] -> ShowS #

liftPartial :: Partial a -> Either Error a Source #

Extractor for computations in the Partial monad.

isSuccess :: Partial a -> Bool Source #

Check whether a partial computation resulted successfully.

isFailure :: Partial a -> Bool Source #

Check whether a partial computation resulted with an error.

exitCodeError :: Monad m => Int -> Text -> PartialT m a Source #

A smart constructor for a computation failed with an ExitCodeError.

timeLimitError :: Monad m => PartialT m a Source #

A smart constructor for a computation failed with a TimeLimitError.

memoryLimitError :: Monad m => PartialT m a Source #

A smart constructor for a computation failed with a MemoryLimitError.

parsingError :: Monad m => String -> PartialT m a Source #

A smart constructor for a computation failed with a ParsingError.

proofError :: Monad m => String -> PartialT m a Source #

A smart constructor for a computation failed with a ProofError.

otherError :: Monad m => String -> PartialT m a Source #

A smart constructor for a computation failed with a OtherError.