ATP.Error

Monads and monad transformers for computations with errors.

Documentation

data Error

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

Eq Error

Defined in ATP.Error

Methods

(==) :: Error -> Error -> Bool

(/=) :: Error -> Error -> Bool

Ord Error

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

Defined in ATP.Error

Methods

showsPrec :: Int -> Error -> ShowS

show :: Error -> String

showList :: [Error] -> ShowS

Pretty Error

Defined in ATP.Pretty.FOL

Methods

pretty :: Error -> Doc

prettyList :: [Error] -> Doc

Monad m => MonadError Error (PartialT m)

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

The type of computations that might fail with an Error.

newtype PartialT m a

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

Constructors

PartialT

Fields

• runPartialT :: ExceptT Error m a

Instances

MonadTrans PartialT

Defined in ATP.Error

Methods

lift :: Monad m => m a -> PartialT m a

Monad m => MonadError Error (PartialT m)

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)

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)

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)

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)

Defined in ATP.Pretty.FOL

Methods

pretty :: Partial a -> Doc

prettyList :: [Partial a] -> Doc

(Eq1 m, Eq a) => Eq (PartialT m a)

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)

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)

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

Extractor for computations in the Partial monad.

isSuccess :: Partial a -> Bool

Check whether a partial computation resulted successfully.

isFailure :: Partial a -> Bool

Check whether a partial computation resulted with an error.

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

A smart constructor for a computation failed with an ExitCodeError.

timeLimitError :: Monad m => PartialT m a

A smart constructor for a computation failed with a TimeLimitError.

memoryLimitError :: Monad m => PartialT m a

A smart constructor for a computation failed with a MemoryLimitError.

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

A smart constructor for a computation failed with a ParsingError.

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

A smart constructor for a computation failed with a ProofError.

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

A smart constructor for a computation failed with a OtherError.