{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Trustworthy #-}

-- |
-- Module      :   Grisette.Internal.Core.Control.Exception
-- 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.Control.Exception
  ( -- * Predefined exceptions
    AssertionError (..),
    VerificationConditions (..),
  )
where

import Control.DeepSeq (NFData)
import GHC.Generics (Generic)

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

-- | Assertion error.
data AssertionError = AssertionError
  deriving (Int -> AssertionError -> ShowS
[AssertionError] -> ShowS
AssertionError -> String
(Int -> AssertionError -> ShowS)
-> (AssertionError -> String)
-> ([AssertionError] -> ShowS)
-> Show AssertionError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AssertionError -> ShowS
showsPrec :: Int -> AssertionError -> ShowS
$cshow :: AssertionError -> String
show :: AssertionError -> String
$cshowList :: [AssertionError] -> ShowS
showList :: [AssertionError] -> ShowS
Show, AssertionError -> AssertionError -> Bool
(AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool) -> Eq AssertionError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssertionError -> AssertionError -> Bool
== :: AssertionError -> AssertionError -> Bool
$c/= :: AssertionError -> AssertionError -> Bool
/= :: AssertionError -> AssertionError -> Bool
Eq, Eq AssertionError
Eq AssertionError =>
(AssertionError -> AssertionError -> Ordering)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> Bool)
-> (AssertionError -> AssertionError -> AssertionError)
-> (AssertionError -> AssertionError -> AssertionError)
-> Ord AssertionError
AssertionError -> AssertionError -> Bool
AssertionError -> AssertionError -> Ordering
AssertionError -> AssertionError -> AssertionError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AssertionError -> AssertionError -> Ordering
compare :: AssertionError -> AssertionError -> Ordering
$c< :: AssertionError -> AssertionError -> Bool
< :: AssertionError -> AssertionError -> Bool
$c<= :: AssertionError -> AssertionError -> Bool
<= :: AssertionError -> AssertionError -> Bool
$c> :: AssertionError -> AssertionError -> Bool
> :: AssertionError -> AssertionError -> Bool
$c>= :: AssertionError -> AssertionError -> Bool
>= :: AssertionError -> AssertionError -> Bool
$cmax :: AssertionError -> AssertionError -> AssertionError
max :: AssertionError -> AssertionError -> AssertionError
$cmin :: AssertionError -> AssertionError -> AssertionError
min :: AssertionError -> AssertionError -> AssertionError
Ord, (forall x. AssertionError -> Rep AssertionError x)
-> (forall x. Rep AssertionError x -> AssertionError)
-> Generic AssertionError
forall x. Rep AssertionError x -> AssertionError
forall x. AssertionError -> Rep AssertionError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AssertionError -> Rep AssertionError x
from :: forall x. AssertionError -> Rep AssertionError x
$cto :: forall x. Rep AssertionError x -> AssertionError
to :: forall x. Rep AssertionError x -> AssertionError
Generic, AssertionError -> ()
(AssertionError -> ()) -> NFData AssertionError
forall a. (a -> ()) -> NFData a
$crnf :: AssertionError -> ()
rnf :: AssertionError -> ()
NFData)

-- | Verification conditions.
-- A crashed program path can terminate with either assertion violation errors or assumption violation errors.
data VerificationConditions
  = AssertionViolation
  | AssumptionViolation
  deriving (Int -> VerificationConditions -> ShowS
[VerificationConditions] -> ShowS
VerificationConditions -> String
(Int -> VerificationConditions -> ShowS)
-> (VerificationConditions -> String)
-> ([VerificationConditions] -> ShowS)
-> Show VerificationConditions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VerificationConditions -> ShowS
showsPrec :: Int -> VerificationConditions -> ShowS
$cshow :: VerificationConditions -> String
show :: VerificationConditions -> String
$cshowList :: [VerificationConditions] -> ShowS
showList :: [VerificationConditions] -> ShowS
Show, VerificationConditions -> VerificationConditions -> Bool
(VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> Eq VerificationConditions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VerificationConditions -> VerificationConditions -> Bool
== :: VerificationConditions -> VerificationConditions -> Bool
$c/= :: VerificationConditions -> VerificationConditions -> Bool
/= :: VerificationConditions -> VerificationConditions -> Bool
Eq, Eq VerificationConditions
Eq VerificationConditions =>
(VerificationConditions -> VerificationConditions -> Ordering)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions -> VerificationConditions -> Bool)
-> (VerificationConditions
    -> VerificationConditions -> VerificationConditions)
-> (VerificationConditions
    -> VerificationConditions -> VerificationConditions)
-> Ord VerificationConditions
VerificationConditions -> VerificationConditions -> Bool
VerificationConditions -> VerificationConditions -> Ordering
VerificationConditions
-> VerificationConditions -> VerificationConditions
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: VerificationConditions -> VerificationConditions -> Ordering
compare :: VerificationConditions -> VerificationConditions -> Ordering
$c< :: VerificationConditions -> VerificationConditions -> Bool
< :: VerificationConditions -> VerificationConditions -> Bool
$c<= :: VerificationConditions -> VerificationConditions -> Bool
<= :: VerificationConditions -> VerificationConditions -> Bool
$c> :: VerificationConditions -> VerificationConditions -> Bool
> :: VerificationConditions -> VerificationConditions -> Bool
$c>= :: VerificationConditions -> VerificationConditions -> Bool
>= :: VerificationConditions -> VerificationConditions -> Bool
$cmax :: VerificationConditions
-> VerificationConditions -> VerificationConditions
max :: VerificationConditions
-> VerificationConditions -> VerificationConditions
$cmin :: VerificationConditions
-> VerificationConditions -> VerificationConditions
min :: VerificationConditions
-> VerificationConditions -> VerificationConditions
Ord, (forall x. VerificationConditions -> Rep VerificationConditions x)
-> (forall x.
    Rep VerificationConditions x -> VerificationConditions)
-> Generic VerificationConditions
forall x. Rep VerificationConditions x -> VerificationConditions
forall x. VerificationConditions -> Rep VerificationConditions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. VerificationConditions -> Rep VerificationConditions x
from :: forall x. VerificationConditions -> Rep VerificationConditions x
$cto :: forall x. Rep VerificationConditions x -> VerificationConditions
to :: forall x. Rep VerificationConditions x -> VerificationConditions
Generic, VerificationConditions -> ()
(VerificationConditions -> ()) -> NFData VerificationConditions
forall a. (a -> ()) -> NFData a
$crnf :: VerificationConditions -> ()
rnf :: VerificationConditions -> ()
NFData)