grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Error

Description

 
Synopsis

Error transformation

class TransformError from to where Source #

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

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

Throwing error

symAssertWith :: (Mergeable e, MonadError e erm, MonadUnion erm) => e -> SymBool -> erm () Source #

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

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

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}