Grisette.Core.Data.Class.Error

Error transformation

class TransformError from to where

This class indicates that the error type to can always represent the error type from.

This is useful in implementing generic procedures that may throw errors. For example, we support symbolic division and modulo operations. These operations should throw an error when the divisor is zero, and we use the standard error type ArithException for this purpose. However, the user may use other type to represent errors, so we need this type class to transform the ArithException to the user-defined types.

Another example of these generic procedures is the symAssert and symAssume functions. They can be used with any error types that are compatible with the AssertionError and VerificationConditions types, respectively.

Methods

transformError :: from -> to

Transforms an error with type from to an error with type to.

Instances

TransformError ArithException AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: ArithException -> AssertionError

TransformError ArrayException AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: ArrayException -> AssertionError

TransformError AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

Methods

transformError :: AssertionError -> AssertionError

TransformError AssertionError VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

transformError :: AssertionError -> VerificationConditions

TransformError VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

transformError :: VerificationConditions -> VerificationConditions

TransformError () ()

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: () -> ()

TransformError a ()

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: a -> ()

TransformError a a

Defined in Grisette.Core.Data.Class.Error

Methods

transformError :: a -> a

Throwing error

symAssertTransformableError :: (Mergeable to, TransformError from to, MonadError to erm, MonadUnion erm) => from -> SymBool -> erm ()

Used within a monadic multi path computation for exception processing.

Terminate the current execution path with the specified error if the condition does not hold. Compatible error can be transformed.

>>> let assert = symAssertTransformableError AssertionError
>>> assert "a" :: ExceptT AssertionError UnionM ()
ExceptT {If (! a) (Left AssertionError) (Right ())}

symThrowTransformableError :: (Mergeable to, Mergeable a, TransformError from to, MonadError to erm, MonadUnion erm) => from -> erm a

Used within a monadic multi path computation to begin exception processing.

Terminate the current execution path with the specified error. Compatible errors can be transformed.

>>> symThrowTransformableError Overflow :: ExceptT AssertionError UnionM ()
ExceptT {Left AssertionError}