{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.Error
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.Error
  ( -- * Error transformation
    TransformError (..),

    -- * Throwing error
    symAssertWith,
    symAssertTransformableError,
    symThrowTransformableError,
    symAssert,
    symAssume,
  )
where

import Control.Exception (ArithException, ArrayException)
import Control.Monad.Except (MonadError (throwError))
import Grisette.Internal.Core.Control.Exception
  ( AssertionError (AssertionError),
    VerificationConditions (AssertionViolation, AssumptionViolation),
  )
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf)
import Grisette.Internal.Core.Data.Class.TryMerge (tryMerge)
import Grisette.Internal.SymPrim.SymBool (SymBool)

-- $setup
-- >>> import Control.Exception
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Lib.Control.Monad
-- >>> import Control.Monad.Except

-- | 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 'Control.Exception.ArithException' for this purpose.
-- However, the user may use other type to represent errors, so we need this
-- type class to transform the 'Control.Exception.ArithException' to the
-- user-defined types.
--
-- Another example of these generic procedures is the
-- 'Grisette.Core.symAssert' and 'Grisette.Core.symAssume' functions.
-- They can be used with any error types that are
-- compatible with the 'Grisette.Core.AssertionError' and
-- 'Grisette.Core.VerificationConditions' types, respectively.
class TransformError from to where
  -- | Transforms an error with type @from@ to an error with type @to@.
  transformError :: from -> to

instance {-# OVERLAPPABLE #-} TransformError a a where
  transformError :: a -> a
transformError = a -> a
forall a. a -> a
id
  {-# INLINE transformError #-}

instance {-# OVERLAPS #-} TransformError a () where
  transformError :: a -> ()
transformError a
_ = ()
  {-# INLINE transformError #-}

instance {-# OVERLAPPING #-} TransformError () () where
  transformError :: () -> ()
transformError ()
_ = ()
  {-# INLINE transformError #-}

-- | 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 Union ()
-- ExceptT {Left AssertionError}
symThrowTransformableError ::
  ( Mergeable to,
    Mergeable a,
    TransformError from to,
    MonadError to erm,
    MonadUnion erm
  ) =>
  from ->
  erm a
symThrowTransformableError :: forall to a from (erm :: * -> *).
(Mergeable to, Mergeable a, TransformError from to,
 MonadError to erm, MonadUnion erm) =>
from -> erm a
symThrowTransformableError = erm a -> erm a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (erm a -> erm a) -> (from -> erm a) -> from -> erm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. to -> erm a
forall a. to -> erm a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (to -> erm a) -> (from -> to) -> from -> erm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. from -> to
forall from to. TransformError from to => from -> to
transformError
{-# INLINE symThrowTransformableError #-}

-- | 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 :: SymBool -> ExceptT AssertionError Union ()
-- >>> assert "a"
-- ExceptT {If (! a) (Left AssertionError) (Right ())}
symAssertTransformableError ::
  ( Mergeable to,
    TransformError from to,
    MonadError to erm,
    MonadUnion erm
  ) =>
  from ->
  SymBool ->
  erm ()
symAssertTransformableError :: forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError from
err SymBool
cond = SymBool -> erm () -> erm () -> erm ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (() -> erm ()
forall a. a -> erm a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (from -> erm ()
forall to a from (erm :: * -> *).
(Mergeable to, Mergeable a, TransformError from to,
 MonadError to erm, MonadUnion erm) =>
from -> erm a
symThrowTransformableError from
err)
{-# INLINE symAssertTransformableError #-}

-- | Symbolic assertion with a custom error.
symAssertWith ::
  ( Mergeable e,
    MonadError e erm,
    MonadUnion erm
  ) =>
  e ->
  SymBool ->
  erm ()
symAssertWith :: forall e (erm :: * -> *).
(Mergeable e, MonadError e erm, MonadUnion erm) =>
e -> SymBool -> erm ()
symAssertWith e
err SymBool
cond = SymBool -> erm () -> erm () -> erm ()
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond (() -> erm ()
forall a. a -> erm a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (e -> erm ()
forall a. e -> erm a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
err)
{-# INLINE symAssertWith #-}

instance TransformError VerificationConditions VerificationConditions where
  transformError :: VerificationConditions -> VerificationConditions
transformError = VerificationConditions -> VerificationConditions
forall a. a -> a
id

instance TransformError AssertionError VerificationConditions where
  transformError :: AssertionError -> VerificationConditions
transformError AssertionError
_ = VerificationConditions
AssertionViolation

instance TransformError ArithException AssertionError where
  transformError :: ArithException -> AssertionError
transformError ArithException
_ = AssertionError
AssertionError

instance TransformError ArrayException AssertionError where
  transformError :: ArrayException -> AssertionError
transformError ArrayException
_ = AssertionError
AssertionError

instance TransformError AssertionError AssertionError where
  transformError :: AssertionError -> AssertionError
transformError = AssertionError -> AssertionError
forall a. a -> a
id

-- | Used within a monadic multi path computation to begin exception processing.
--
-- Checks the condition passed to the function.
-- The current execution path will be terminated with assertion error if the condition is false.
--
-- If the condition is symbolic, Grisette will split the execution into two paths based on the condition.
-- The symbolic execution will continue on the then-branch, where the condition is true.
-- For the else branch, where the condition is false, the execution will be terminated.
--
-- The resulting monadic environment should be compatible with the t'AssertionError'
-- error type. See 'TransformError' type class for details.
--
-- __/Examples/__:
--
-- Terminates the execution if the condition is false.
-- Note that we may lose the 'Mergeable' knowledge here if no possible execution
-- path is viable. This may affect the efficiency in theory, but in practice this
-- should not be a problem as all paths are terminated and no further evaluation
-- would be performed.
--
-- >>> symAssert (con False) :: ExceptT AssertionError Union ()
-- ExceptT {Left AssertionError}
-- >>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError Union Integer
-- ExceptT <Left AssertionError>
--
-- No effect if the condition is true:
--
-- >>> symAssert (con True) :: ExceptT AssertionError Union ()
-- ExceptT {Right ()}
-- >>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError Union Integer
-- ExceptT {Right 1}
--
-- Splitting the path and terminate one of them when the condition is symbolic.
--
-- >>> symAssert (ssym "a") :: ExceptT AssertionError Union ()
-- ExceptT {If (! a) (Left AssertionError) (Right ())}
-- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError Union Integer
-- ExceptT {If (! a) (Left AssertionError) (Right 1)}
--
-- t'AssertionError' is compatible with 'VerificationConditions':
--
-- >>> symAssert (ssym "a") :: ExceptT VerificationConditions Union ()
-- ExceptT {If (! a) (Left AssertionViolation) (Right ())}
symAssert ::
  (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) =>
  SymBool ->
  erm ()
symAssert :: forall to (erm :: * -> *).
(TransformError AssertionError to, Mergeable to, MonadError to erm,
 MonadUnion erm) =>
SymBool -> erm ()
symAssert = AssertionError -> SymBool -> erm ()
forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError AssertionError
AssertionError

-- | Used within a monadic multi path computation to begin exception processing.
--
-- Similar to 'symAssert', but terminates the execution path with 'AssumptionViolation' error.
--
-- /Examples/:
--
-- >>> symAssume (ssym "a") :: ExceptT VerificationConditions Union ()
-- ExceptT {If (! a) (Left AssumptionViolation) (Right ())}
symAssume ::
  (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) =>
  SymBool ->
  erm ()
symAssume :: forall to (erm :: * -> *).
(TransformError VerificationConditions to, Mergeable to,
 MonadError to erm, MonadUnion erm) =>
SymBool -> erm ()
symAssume = VerificationConditions -> SymBool -> erm ()
forall to from (erm :: * -> *).
(Mergeable to, TransformError from to, MonadError to erm,
 MonadUnion erm) =>
from -> SymBool -> erm ()
symAssertTransformableError VerificationConditions
AssumptionViolation