{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Core.Control.Monad.CBMCExcept
-- 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.Core.Control.Monad.CBMCExcept
  ( -- * CBMC-like error handling
    CBMCEither (..),
    CBMCExceptT (..),
    cbmcExcept,
    mapCBMCExceptT,
    withCBMCExceptT,
    OrigExcept.MonadError (..),
  )
where

import Control.Applicative
import Control.DeepSeq
import Control.Monad
import qualified Control.Monad.Except as OrigExcept
import qualified Control.Monad.Fail as Fail
import Control.Monad.Fix
import Control.Monad.Trans
import Control.Monad.Zip
import Data.Functor.Classes
import Data.Functor.Contravariant
import Data.Hashable
import GHC.Generics
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.Evaluate
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.GenSym
import Grisette.Core.Data.Class.Mergeable
import Grisette.Core.Data.Class.SOrd
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solver
import Grisette.Core.Data.Class.ToCon
import Grisette.Core.Data.Class.ToSym
import Language.Haskell.TH.Syntax (Lift)
import Unsafe.Coerce

-- | A wrapper type for 'Either'. Uses different merging strategies.
newtype CBMCEither a b = CBMCEither {forall a b. CBMCEither a b -> Either a b
runCBMCEither :: Either a b}
  deriving newtype (CBMCEither a b -> CBMCEither a b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b.
(Eq a, Eq b) =>
CBMCEither a b -> CBMCEither a b -> Bool
/= :: CBMCEither a b -> CBMCEither a b -> Bool
$c/= :: forall a b.
(Eq a, Eq b) =>
CBMCEither a b -> CBMCEither a b -> Bool
== :: CBMCEither a b -> CBMCEither a b -> Bool
$c== :: forall a b.
(Eq a, Eq b) =>
CBMCEither a b -> CBMCEither a b -> Bool
Eq, forall a a b.
Eq a =>
(a -> b -> Bool) -> CBMCEither a a -> CBMCEither a b -> Bool
forall a b.
(a -> b -> Bool) -> CBMCEither a a -> CBMCEither a b -> Bool
forall (f :: * -> *).
(forall a b. (a -> b -> Bool) -> f a -> f b -> Bool) -> Eq1 f
liftEq :: forall a b.
(a -> b -> Bool) -> CBMCEither a a -> CBMCEither a b -> Bool
$cliftEq :: forall a a b.
Eq a =>
(a -> b -> Bool) -> CBMCEither a a -> CBMCEither a b -> Bool
Eq1, CBMCEither a b -> CBMCEither a b -> Bool
CBMCEither a b -> CBMCEither a b -> Ordering
CBMCEither a b -> CBMCEither a b -> CBMCEither a b
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
forall {a} {b}. (Ord a, Ord b) => Eq (CBMCEither a b)
forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Bool
forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Ordering
forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> CBMCEither a b
min :: CBMCEither a b -> CBMCEither a b -> CBMCEither a b
$cmin :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> CBMCEither a b
max :: CBMCEither a b -> CBMCEither a b -> CBMCEither a b
$cmax :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> CBMCEither a b
>= :: CBMCEither a b -> CBMCEither a b -> Bool
$c>= :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Bool
> :: CBMCEither a b -> CBMCEither a b -> Bool
$c> :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Bool
<= :: CBMCEither a b -> CBMCEither a b -> Bool
$c<= :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Bool
< :: CBMCEither a b -> CBMCEither a b -> Bool
$c< :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Bool
compare :: CBMCEither a b -> CBMCEither a b -> Ordering
$ccompare :: forall a b.
(Ord a, Ord b) =>
CBMCEither a b -> CBMCEither a b -> Ordering
Ord, forall {a}. Ord a => Eq1 (CBMCEither a)
forall a a b.
Ord a =>
(a -> b -> Ordering)
-> CBMCEither a a -> CBMCEither a b -> Ordering
forall a b.
(a -> b -> Ordering)
-> CBMCEither a a -> CBMCEither a b -> Ordering
forall (f :: * -> *).
Eq1 f
-> (forall a b. (a -> b -> Ordering) -> f a -> f b -> Ordering)
-> Ord1 f
liftCompare :: forall a b.
(a -> b -> Ordering)
-> CBMCEither a a -> CBMCEither a b -> Ordering
$cliftCompare :: forall a a b.
Ord a =>
(a -> b -> Ordering)
-> CBMCEither a a -> CBMCEither a b -> Ordering
Ord1, ReadPrec [CBMCEither a b]
ReadPrec (CBMCEither a b)
Int -> ReadS (CBMCEither a b)
ReadS [CBMCEither a b]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall a b. (Read a, Read b) => ReadPrec [CBMCEither a b]
forall a b. (Read a, Read b) => ReadPrec (CBMCEither a b)
forall a b. (Read a, Read b) => Int -> ReadS (CBMCEither a b)
forall a b. (Read a, Read b) => ReadS [CBMCEither a b]
readListPrec :: ReadPrec [CBMCEither a b]
$creadListPrec :: forall a b. (Read a, Read b) => ReadPrec [CBMCEither a b]
readPrec :: ReadPrec (CBMCEither a b)
$creadPrec :: forall a b. (Read a, Read b) => ReadPrec (CBMCEither a b)
readList :: ReadS [CBMCEither a b]
$creadList :: forall a b. (Read a, Read b) => ReadS [CBMCEither a b]
readsPrec :: Int -> ReadS (CBMCEither a b)
$creadsPrec :: forall a b. (Read a, Read b) => Int -> ReadS (CBMCEither a b)
Read, forall a a.
Read a =>
ReadPrec a -> ReadPrec [a] -> ReadPrec [CBMCEither a a]
forall a a.
Read a =>
ReadPrec a -> ReadPrec [a] -> ReadPrec (CBMCEither a a)
forall a a.
Read a =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither a a)
forall a a.
Read a =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither a a]
forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec [CBMCEither a a]
forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec (CBMCEither a a)
forall a.
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither a a)
forall a. (Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither a a]
forall (f :: * -> *).
(forall a. (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a))
-> (forall a. (Int -> ReadS a) -> ReadS [a] -> ReadS [f a])
-> (forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec (f a))
-> (forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec [f a])
-> Read1 f
liftReadListPrec :: forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec [CBMCEither a a]
$cliftReadListPrec :: forall a a.
Read a =>
ReadPrec a -> ReadPrec [a] -> ReadPrec [CBMCEither a a]
liftReadPrec :: forall a. ReadPrec a -> ReadPrec [a] -> ReadPrec (CBMCEither a a)
$cliftReadPrec :: forall a a.
Read a =>
ReadPrec a -> ReadPrec [a] -> ReadPrec (CBMCEither a a)
liftReadList :: forall a. (Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither a a]
$cliftReadList :: forall a a.
Read a =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither a a]
liftReadsPrec :: forall a.
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither a a)
$cliftReadsPrec :: forall a a.
Read a =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither a a)
Read1, Int -> CBMCEither a b -> ShowS
[CBMCEither a b] -> ShowS
CBMCEither a b -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> CBMCEither a b -> ShowS
forall a b. (Show a, Show b) => [CBMCEither a b] -> ShowS
forall a b. (Show a, Show b) => CBMCEither a b -> String
showList :: [CBMCEither a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [CBMCEither a b] -> ShowS
show :: CBMCEither a b -> String
$cshow :: forall a b. (Show a, Show b) => CBMCEither a b -> String
showsPrec :: Int -> CBMCEither a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> CBMCEither a b -> ShowS
Show, forall a a.
Show a =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither a a -> ShowS
forall a a.
Show a =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither a a] -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither a a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither a a] -> ShowS
forall (f :: * -> *).
(forall a.
 (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS)
-> (forall a.
    (Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS)
-> Show1 f
liftShowList :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither a a] -> ShowS
$cliftShowList :: forall a a.
Show a =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither a a] -> ShowS
liftShowsPrec :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither a a -> ShowS
$cliftShowsPrec :: forall a a.
Show a =>
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither a a -> ShowS
Show1, forall a b. a -> CBMCEither a b -> CBMCEither a a
forall a b. (a -> b) -> CBMCEither a a -> CBMCEither a b
forall a a b. a -> CBMCEither a b -> CBMCEither a a
forall a a b. (a -> b) -> CBMCEither a a -> CBMCEither a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> CBMCEither a b -> CBMCEither a a
$c<$ :: forall a a b. a -> CBMCEither a b -> CBMCEither a a
fmap :: forall a b. (a -> b) -> CBMCEither a a -> CBMCEither a b
$cfmap :: forall a a b. (a -> b) -> CBMCEither a a -> CBMCEither a b
Functor, forall a. Functor (CBMCEither a)
forall a. a -> CBMCEither a a
forall a a. a -> CBMCEither a a
forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a a
forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
forall a b.
CBMCEither a (a -> b) -> CBMCEither a a -> CBMCEither a b
forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a a
forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
forall a a b.
CBMCEither a (a -> b) -> CBMCEither a a -> CBMCEither a b
forall a b c.
(a -> b -> c) -> CBMCEither a a -> CBMCEither a b -> CBMCEither a c
forall a a b c.
(a -> b -> c) -> CBMCEither a a -> CBMCEither a b -> CBMCEither a c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a a
$c<* :: forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a a
*> :: forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
$c*> :: forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
liftA2 :: forall a b c.
(a -> b -> c) -> CBMCEither a a -> CBMCEither a b -> CBMCEither a c
$cliftA2 :: forall a a b c.
(a -> b -> c) -> CBMCEither a a -> CBMCEither a b -> CBMCEither a c
<*> :: forall a b.
CBMCEither a (a -> b) -> CBMCEither a a -> CBMCEither a b
$c<*> :: forall a a b.
CBMCEither a (a -> b) -> CBMCEither a a -> CBMCEither a b
pure :: forall a. a -> CBMCEither a a
$cpure :: forall a a. a -> CBMCEither a a
Applicative, forall a. Applicative (CBMCEither a)
forall a. a -> CBMCEither a a
forall a a. a -> CBMCEither a a
forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
forall a b.
CBMCEither a a -> (a -> CBMCEither a b) -> CBMCEither a b
forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
forall a a b.
CBMCEither a a -> (a -> CBMCEither a b) -> CBMCEither a b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> CBMCEither a a
$creturn :: forall a a. a -> CBMCEither a a
>> :: forall a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
$c>> :: forall a a b. CBMCEither a a -> CBMCEither a b -> CBMCEither a b
>>= :: forall a b.
CBMCEither a a -> (a -> CBMCEither a b) -> CBMCEither a b
$c>>= :: forall a a b.
CBMCEither a a -> (a -> CBMCEither a b) -> CBMCEither a b
Monad, Int -> CBMCEither a b -> Int
CBMCEither a b -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a} {b}. (Hashable a, Hashable b) => Eq (CBMCEither a b)
forall a b.
(Hashable a, Hashable b) =>
Int -> CBMCEither a b -> Int
forall a b. (Hashable a, Hashable b) => CBMCEither a b -> Int
hash :: CBMCEither a b -> Int
$chash :: forall a b. (Hashable a, Hashable b) => CBMCEither a b -> Int
hashWithSalt :: Int -> CBMCEither a b -> Int
$chashWithSalt :: forall a b.
(Hashable a, Hashable b) =>
Int -> CBMCEither a b -> Int
Hashable, CBMCEither a b -> ()
forall a. (a -> ()) -> NFData a
forall a b. (NFData a, NFData b) => CBMCEither a b -> ()
rnf :: CBMCEither a b -> ()
$crnf :: forall a b. (NFData a, NFData b) => CBMCEither a b -> ()
NFData)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (CBMCEither a b) x -> CBMCEither a b
forall a b x. CBMCEither a b -> Rep (CBMCEither a b) x
$cto :: forall a b x. Rep (CBMCEither a b) x -> CBMCEither a b
$cfrom :: forall a b x. CBMCEither a b -> Rep (CBMCEither a b) x
Generic, forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
CBMCEither a b -> m Exp
forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
CBMCEither a b -> Code m (CBMCEither a b)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => CBMCEither a b -> m Exp
forall (m :: * -> *).
Quote m =>
CBMCEither a b -> Code m (CBMCEither a b)
liftTyped :: forall (m :: * -> *).
Quote m =>
CBMCEither a b -> Code m (CBMCEither a b)
$cliftTyped :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
CBMCEither a b -> Code m (CBMCEither a b)
lift :: forall (m :: * -> *). Quote m => CBMCEither a b -> m Exp
$clift :: forall a b (m :: * -> *).
(Lift a, Lift b, Quote m) =>
CBMCEither a b -> m Exp
Lift)

deriving newtype instance (SEq e, SEq a) => SEq (CBMCEither e a)

deriving newtype instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (CBMCEither a b)

deriving newtype instance
  (ExtractSymbolics a, ExtractSymbolics b) =>
  ExtractSymbolics (CBMCEither a b)

instance
  ( GenSymSimple a a,
    Mergeable a,
    GenSymSimple b b,
    Mergeable b
  ) =>
  GenSym (CBMCEither a b) (CBMCEither a b)

instance
  ( GenSymSimple a a,
    GenSymSimple b b
  ) =>
  GenSymSimple (CBMCEither a b) (CBMCEither a b)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
CBMCEither a b -> m (CBMCEither a b)
simpleFresh = forall a (m :: * -> *).
(Generic a, GenSymSameShape (Rep a), MonadFresh m) =>
a -> m a
derivedSameShapeSimpleFresh

instance
  (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>
  GenSym () (CBMCEither a b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
() -> m (UnionM (CBMCEither a b))
fresh = forall bool a (m :: * -> *) u.
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (UnionM a)
derivedNoSpecFresh

deriving newtype instance (SOrd a, SOrd b) => SOrd (CBMCEither a b)

deriving newtype instance (ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (CBMCEither e2 a2)

instance (ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (CBMCEither e2 a2) where
  toCon :: CBMCEither e1 a1 -> Maybe (CBMCEither e2 a2)
toCon (CBMCEither Either e1 a1
a) = forall a b. Either a b -> CBMCEither a b
CBMCEither forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. ToCon a b => a -> Maybe b
toCon Either e1 a1
a

instance (ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (Either e2 a2) where
  toCon :: CBMCEither e1 a1 -> Maybe (Either e2 a2)
toCon (CBMCEither Either e1 a1
a) = forall a b. ToCon a b => a -> Maybe b
toCon Either e1 a1
a

deriving newtype instance (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2)

instance (ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (CBMCEither e2 a2) where
  toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2
toSym (CBMCEither Either e1 a1
a) = forall a b. Either a b -> CBMCEither a b
CBMCEither forall a b. (a -> b) -> a -> b
$ forall a b. ToSym a b => a -> b
toSym Either e1 a1
a

instance (ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2) where
  toSym :: CBMCEither e1 a1 -> Either e2 a2
toSym (CBMCEither Either e1 a1
a) = forall a b. ToSym a b => a -> b
toSym Either e1 a1
a

data EitherIdx idx = L idx | R deriving (EitherIdx idx -> EitherIdx idx -> Bool
forall idx. Eq idx => EitherIdx idx -> EitherIdx idx -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EitherIdx idx -> EitherIdx idx -> Bool
$c/= :: forall idx. Eq idx => EitherIdx idx -> EitherIdx idx -> Bool
== :: EitherIdx idx -> EitherIdx idx -> Bool
$c== :: forall idx. Eq idx => EitherIdx idx -> EitherIdx idx -> Bool
Eq, EitherIdx idx -> EitherIdx idx -> Bool
EitherIdx idx -> EitherIdx idx -> Ordering
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
forall {idx}. Ord idx => Eq (EitherIdx idx)
forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Bool
forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Ordering
forall idx.
Ord idx =>
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
min :: EitherIdx idx -> EitherIdx idx -> EitherIdx idx
$cmin :: forall idx.
Ord idx =>
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
max :: EitherIdx idx -> EitherIdx idx -> EitherIdx idx
$cmax :: forall idx.
Ord idx =>
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
>= :: EitherIdx idx -> EitherIdx idx -> Bool
$c>= :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Bool
> :: EitherIdx idx -> EitherIdx idx -> Bool
$c> :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Bool
<= :: EitherIdx idx -> EitherIdx idx -> Bool
$c<= :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Bool
< :: EitherIdx idx -> EitherIdx idx -> Bool
$c< :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Bool
compare :: EitherIdx idx -> EitherIdx idx -> Ordering
$ccompare :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Ordering
Ord, Int -> EitherIdx idx -> ShowS
forall idx. Show idx => Int -> EitherIdx idx -> ShowS
forall idx. Show idx => [EitherIdx idx] -> ShowS
forall idx. Show idx => EitherIdx idx -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EitherIdx idx] -> ShowS
$cshowList :: forall idx. Show idx => [EitherIdx idx] -> ShowS
show :: EitherIdx idx -> String
$cshow :: forall idx. Show idx => EitherIdx idx -> String
showsPrec :: Int -> EitherIdx idx -> ShowS
$cshowsPrec :: forall idx. Show idx => Int -> EitherIdx idx -> ShowS
Show)

instance (Mergeable e, Mergeable a) => Mergeable (CBMCEither e a) where
  rootStrategy :: MergingStrategy (CBMCEither e a)
rootStrategy = forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1

instance (Mergeable e) => Mergeable1 (CBMCEither e) where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (CBMCEither e a)
liftRootStrategy MergingStrategy a
ms = case forall a. Mergeable a => MergingStrategy a
rootStrategy of
    SimpleStrategy SymBool -> e -> e -> e
m ->
      forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
        ( \(CBMCEither Either e a
e) -> case Either e a
e of
            Left e
_ -> Bool
False
            Right a
_ -> Bool
True
        )
        ( \case
            Bool
False -> forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy forall a b. (a -> b) -> a -> b
$
              \SymBool
cond (CBMCEither Either e a
le) (CBMCEither Either e a
re) -> case (Either e a
le, Either e a
re) of
                (Left e
l, Left e
r) -> forall a b. Either a b -> CBMCEither a b
CBMCEither forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ SymBool -> e -> e -> e
m SymBool
cond e
l e
r
                (Either e a, Either e a)
_ -> forall a. HasCallStack => String -> a
error String
"impossible"
            Bool
True -> forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> forall a. HasCallStack => String -> a
error String
"impossible")
        )
    MergingStrategy e
NoStrategy ->
      forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
        ( \(CBMCEither Either e a
e) -> case Either e a
e of
            Left e
_ -> Bool
False
            Right a
_ -> Bool
True
        )
        ( \case
            Bool
False -> forall a. MergingStrategy a
NoStrategy
            Bool
True -> forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> forall a. HasCallStack => String -> a
error String
"impossible")
        )
    SortedStrategy e -> idx
idx idx -> MergingStrategy e
sub ->
      forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
        ( \(CBMCEither Either e a
e) -> case Either e a
e of
            Left e
v -> forall idx. idx -> EitherIdx idx
L forall a b. (a -> b) -> a -> b
$ e -> idx
idx e
v
            Right a
_ -> forall idx. EitherIdx idx
R
        )
        ( \case
            L idx
i -> forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (idx -> MergingStrategy e
sub idx
i) (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left) (\case (CBMCEither (Left e
x)) -> e
x; CBMCEither e a
_ -> forall a. HasCallStack => String -> a
error String
"impossible")
            EitherIdx idx
R -> forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> forall a. HasCallStack => String -> a
error String
"impossible")
        )

cbmcEither :: forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither :: forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither a -> c
l b -> c
r CBMCEither a b
v = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> c
l b -> c
r (forall a b. a -> b
unsafeCoerce CBMCEither a b
v)

-- | Wrap an 'Either' value in 'CBMCExceptT'
cbmcExcept :: (Monad m) => Either e a -> CBMCExceptT e m a
cbmcExcept :: forall (m :: * -> *) e a.
Monad m =>
Either e a -> CBMCExceptT e m a
cbmcExcept Either e a
m = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. Either a b -> CBMCEither a b
CBMCEither Either e a
m)

-- | Map the error and values in a 'CBMCExceptT'
mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b
mapCBMCExceptT :: forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> CBMCExceptT e m a -> CBMCExceptT e' n b
mapCBMCExceptT m (Either e a) -> n (Either e' b)
f CBMCExceptT e m a
m = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ (forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Either e a) -> n (Either e' b)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce) (forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT CBMCExceptT e m a
m)

-- | Map the error in a 'CBMCExceptT'
withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
withCBMCExceptT :: forall (m :: * -> *) e e' a.
Functor m =>
(e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
withCBMCExceptT e -> e'
f = forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> CBMCExceptT e m a -> CBMCExceptT e' n b
mapCBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e'
f) forall a b. b -> Either a b
Right

-- | Similar to 'ExceptT', but with different error handling mechanism.
newtype CBMCExceptT e m a = CBMCExceptT {forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT :: m (CBMCEither e a)} deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall e (m :: * -> *) a x.
Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a
forall e (m :: * -> *) a x.
CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x
$cto :: forall e (m :: * -> *) a x.
Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a
$cfrom :: forall e (m :: * -> *) a x.
CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x
Generic, forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall e (m :: * -> *) a.
Functor m =>
Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a
forall e (m :: * -> *) a.
Functor m =>
CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a
$cto1 :: forall e (m :: * -> *) a.
Functor m =>
Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a
$cfrom1 :: forall e (m :: * -> *) a.
Functor m =>
CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a
Generic1)

instance (Eq e, Eq1 m) => Eq1 (CBMCExceptT e m) where
  liftEq :: forall a b.
(a -> b -> Bool) -> CBMCExceptT e m a -> CBMCExceptT e m b -> Bool
liftEq a -> b -> Bool
eq (CBMCExceptT m (CBMCEither e a)
x) (CBMCExceptT m (CBMCEither e b)
y) = forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq (forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq) m (CBMCEither e a)
x m (CBMCEither e b)
y
  {-# INLINE liftEq #-}

instance (Ord e, Ord1 m) => Ord1 (CBMCExceptT e m) where
  liftCompare :: forall a b.
(a -> b -> Ordering)
-> CBMCExceptT e m a -> CBMCExceptT e m b -> Ordering
liftCompare a -> b -> Ordering
comp (CBMCExceptT m (CBMCEither e a)
x) (CBMCExceptT m (CBMCEither e b)
y) =
    forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
comp) m (CBMCEither e a)
x m (CBMCEither e b)
y
  {-# INLINE liftCompare #-}

instance (Read e, Read1 m) => Read1 (CBMCExceptT e m) where
  liftReadsPrec :: forall a.
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCExceptT e m a)
liftReadsPrec Int -> ReadS a
rp ReadS [a]
rl =
    forall a. (String -> ReadS a) -> Int -> ReadS a
readsData forall a b. (a -> b) -> a -> b
$
      forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith (forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS (CBMCEither e a)
rp' ReadS [CBMCEither e a]
rl') String
"CBMCExceptT" forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT
    where
      rp' :: Int -> ReadS (CBMCEither e a)
rp' = forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (f a)
liftReadsPrec Int -> ReadS a
rp ReadS [a]
rl
      rl' :: ReadS [CBMCEither e a]
rl' = forall (f :: * -> *) a.
Read1 f =>
(Int -> ReadS a) -> ReadS [a] -> ReadS [f a]
liftReadList Int -> ReadS a
rp ReadS [a]
rl

instance (Show e, Show1 m) => Show1 (CBMCExceptT e m) where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCExceptT e m a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (CBMCExceptT m (CBMCEither e a)
m) =
    forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith (forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> CBMCEither e a -> ShowS
sp' [CBMCEither e a] -> ShowS
sl') String
"CBMCExceptT" Int
d m (CBMCEither e a)
m
    where
      sp' :: Int -> CBMCEither e a -> ShowS
sp' = forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl
      sl' :: [CBMCEither e a] -> ShowS
sl' = forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [f a] -> ShowS
liftShowList Int -> a -> ShowS
sp [a] -> ShowS
sl

instance (Eq e, Eq1 m, Eq a) => Eq (CBMCExceptT e m a) where
  == :: CBMCExceptT e m a -> CBMCExceptT e m a -> Bool
(==) = forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1

instance (Ord e, Ord1 m, Ord a) => Ord (CBMCExceptT e m a) where
  compare :: CBMCExceptT e m a -> CBMCExceptT e m a -> Ordering
compare = forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1

instance (Read e, Read1 m, Read a) => Read (CBMCExceptT e m a) where
  readsPrec :: Int -> ReadS (CBMCExceptT e m a)
readsPrec = forall (f :: * -> *) a. (Read1 f, Read a) => Int -> ReadS (f a)
readsPrec1

instance (Show e, Show1 m, Show a) => Show (CBMCExceptT e m a) where
  showsPrec :: Int -> CBMCExceptT e m a -> ShowS
showsPrec = forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance (Functor m) => Functor (CBMCExceptT e m) where
  fmap :: forall a b. (a -> b) -> CBMCExceptT e m a -> CBMCExceptT e m b
fmap a -> b
f = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT
  {-# INLINE fmap #-}

instance (Foldable f) => Foldable (CBMCExceptT e f) where
  foldMap :: forall m a. Monoid m => (a -> m) -> CBMCExceptT e f a -> m
foldMap a -> m
f (CBMCExceptT f (CBMCEither e a)
a) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty) a -> m
f) f (CBMCEither e a)
a
  {-# INLINE foldMap #-}

instance (Traversable f) => Traversable (CBMCExceptT e f) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CBMCExceptT e f a -> f (CBMCExceptT e f b)
traverse a -> f b
f (CBMCExceptT f (CBMCEither e a)
a) =
    forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f)) f (CBMCEither e a)
a
  {-# INLINE traverse #-}

instance (Functor m, Monad m) => Applicative (CBMCExceptT e m) where
  pure :: forall a. a -> CBMCExceptT e m a
pure a
a = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ a
a)
  {-# INLINE pure #-}
  CBMCExceptT m (CBMCEither e (a -> b))
f <*> :: forall a b.
CBMCExceptT e m (a -> b) -> CBMCExceptT e m a -> CBMCExceptT e m b
<*> CBMCExceptT m (CBMCEither e a)
v = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ do
    CBMCEither e (a -> b)
mf <- m (CBMCEither e (a -> b))
f
    case CBMCEither e (a -> b)
mf of
      CBMCEither (Left e
e) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ e
e)
      CBMCEither (Right a -> b
k) -> do
        CBMCEither e a
mv <- m (CBMCEither e a)
v
        case CBMCEither e a
mv of
          CBMCEither (Left e
e) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ e
e)
          CBMCEither (Right a
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ a -> b
k a
x)
  {-# INLINEABLE (<*>) #-}
  CBMCExceptT e m a
m *> :: forall a b.
CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m b
*> CBMCExceptT e m b
k = CBMCExceptT e m a
m forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CBMCExceptT e m b
k
  {-# INLINE (*>) #-}

instance (Functor m, Monad m, Monoid e) => Alternative (CBMCExceptT e m) where
  empty :: forall a. CBMCExceptT e m a
empty = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
mempty)
  {-# INLINE empty #-}
  CBMCExceptT m (CBMCEither e a)
mx <|> :: forall a.
CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
<|> CBMCExceptT m (CBMCEither e a)
my = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ do
    CBMCEither e a
ex <- m (CBMCEither e a)
mx
    case CBMCEither e a
ex of
      CBMCEither (Left e
e) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend e
e) (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right)) m (CBMCEither e a)
my
      CBMCEither (Right a
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ a
x)
  {-# INLINEABLE (<|>) #-}

instance (Monad m) => Monad (CBMCExceptT e m) where
  CBMCExceptT e m a
m >>= :: forall a b.
CBMCExceptT e m a -> (a -> CBMCExceptT e m b) -> CBMCExceptT e m b
>>= a -> CBMCExceptT e m b
k = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ do
    CBMCEither e a
a <- forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT CBMCExceptT e m a
m
    case CBMCEither e a
a of
      CBMCEither (Left e
e) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left e
e)
      CBMCEither (Right a
x) -> forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT (a -> CBMCExceptT e m b
k a
x)
  {-# INLINE (>>=) #-}

instance (Fail.MonadFail m) => Fail.MonadFail (CBMCExceptT e m) where
  fail :: forall a. String -> CBMCExceptT e m a
fail = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail
  {-# INLINE fail #-}

instance (Monad m, Monoid e) => MonadPlus (CBMCExceptT e m) where
  mzero :: forall a. CBMCExceptT e m a
mzero = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a. Monoid a => a
mempty)
  {-# INLINE mzero #-}
  CBMCExceptT m (CBMCEither e a)
mx mplus :: forall a.
CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
`mplus` CBMCExceptT m (CBMCEither e a)
my = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ do
    CBMCEither e a
ex <- m (CBMCEither e a)
mx
    case CBMCEither e a
ex of
      CBMCEither (Left e
e) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend e
e) (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right)) m (CBMCEither e a)
my
      CBMCEither (Right a
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right a
x)
  {-# INLINEABLE mplus #-}

instance (MonadFix m) => MonadFix (CBMCExceptT e m) where
  mfix :: forall a. (a -> CBMCExceptT e m a) -> CBMCExceptT e m a
mfix a -> CBMCExceptT e m a
f = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CBMCExceptT e m a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (forall a b. a -> b -> a
const forall {a}. a
bomb) forall a. a -> a
id))
    where
      bomb :: a
bomb = forall a. HasCallStack => String -> a
error String
"mfix (CBMCExceptT): inner computation returned Left value"
  {-# INLINE mfix #-}

instance MonadTrans (CBMCExceptT e) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> CBMCExceptT e m a
lift = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right)
  {-# INLINE lift #-}

instance (MonadIO m) => MonadIO (CBMCExceptT e m) where
  liftIO :: forall a. IO a -> CBMCExceptT e m a
liftIO = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
  {-# INLINE liftIO #-}

instance (MonadZip m) => MonadZip (CBMCExceptT e m) where
  mzipWith :: forall a b c.
(a -> b -> c)
-> CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m c
mzipWith a -> b -> c
f (CBMCExceptT m (CBMCEither e a)
a) (CBMCExceptT m (CBMCEither e b)
b) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> m a -> m b -> m c
mzipWith (forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
f) m (CBMCEither e a)
a m (CBMCEither e b)
b
  {-# INLINE mzipWith #-}

instance Contravariant m => Contravariant (CBMCExceptT e m) where
  contramap :: forall a' a. (a' -> a) -> CBMCExceptT e m a -> CBMCExceptT e m a'
contramap a' -> a
f = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a' -> a
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT
  {-# INLINE contramap #-}

throwE :: (Monad m) => e -> CBMCExceptT e m a
throwE :: forall (m :: * -> *) e a. Monad m => e -> CBMCExceptT e m a
throwE = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
{-# INLINE throwE #-}

catchE ::
  (Monad m) =>
  CBMCExceptT e m a ->
  (e -> CBMCExceptT e' m a) ->
  CBMCExceptT e' m a
CBMCExceptT e m a
m catchE :: forall (m :: * -> *) e a e'.
Monad m =>
CBMCExceptT e m a
-> (e -> CBMCExceptT e' m a) -> CBMCExceptT e' m a
`catchE` e -> CBMCExceptT e' m a
h = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ do
  CBMCEither e a
a <- forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT CBMCExceptT e m a
m
  case CBMCEither e a
a of
    CBMCEither (Left e
l) -> forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT (e -> CBMCExceptT e' m a
h e
l)
    CBMCEither (Right a
r) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. Either a b -> CBMCEither a b
CBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ a
r)
{-# INLINE catchE #-}

instance Monad m => OrigExcept.MonadError e (CBMCExceptT e m) where
  throwError :: forall a. e -> CBMCExceptT e m a
throwError = forall (m :: * -> *) e a. Monad m => e -> CBMCExceptT e m a
throwE
  {-# INLINE throwError #-}
  catchError :: forall a.
CBMCExceptT e m a -> (e -> CBMCExceptT e m a) -> CBMCExceptT e m a
catchError = forall (m :: * -> *) e a e'.
Monad m =>
CBMCExceptT e m a
-> (e -> CBMCExceptT e' m a) -> CBMCExceptT e' m a
catchE
  {-# INLINE catchError #-}

instance (SEq (m (CBMCEither e a))) => SEq (CBMCExceptT e m a) where
  (CBMCExceptT m (CBMCEither e a)
a) ==~ :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool
==~ (CBMCExceptT m (CBMCEither e a)
b) = m (CBMCEither e a)
a forall a. SEq a => a -> a -> SymBool
==~ m (CBMCEither e a)
b
  {-# INLINE (==~) #-}

instance (EvaluateSym (m (CBMCEither e a))) => EvaluateSym (CBMCExceptT e m a) where
  evaluateSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a
evaluateSym Bool
fillDefault Model
model (CBMCExceptT m (CBMCEither e a)
v) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m (CBMCEither e a)
v
  {-# INLINE evaluateSym #-}

instance
  (ExtractSymbolics (m (CBMCEither e a))) =>
  ExtractSymbolics (CBMCExceptT e m a)
  where
  extractSymbolics :: CBMCExceptT e m a -> SymbolSet
extractSymbolics (CBMCExceptT m (CBMCEither e a)
v) = forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m (CBMCEither e a)
v

instance
  (Mergeable1 m, Mergeable e, Mergeable a) =>
  Mergeable (CBMCExceptT e m a)
  where
  rootStrategy :: MergingStrategy (CBMCExceptT e m a)
rootStrategy = forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1 forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT
  {-# INLINE rootStrategy #-}

instance (Mergeable1 m, Mergeable e) => Mergeable1 (CBMCExceptT e m) where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (CBMCExceptT e m a)
liftRootStrategy MergingStrategy a
m = forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
m)) forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT
  {-# INLINE liftRootStrategy #-}

instance
  {-# OVERLAPPABLE #-}
  ( GenSym spec (m (CBMCEither a b)),
    Mergeable1 m,
    Mergeable a,
    Mergeable b
  ) =>
  GenSym spec (CBMCExceptT a m b)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
spec -> m (UnionM (CBMCExceptT a m b))
fresh spec
v = do
    UnionM (m (CBMCEither a b))
x <- forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
v
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ UnionM (m (CBMCEither a b))
x

instance
  {-# OVERLAPPABLE #-}
  ( GenSymSimple spec (m (CBMCEither a b))
  ) =>
  GenSymSimple spec (CBMCExceptT a m b)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => spec -> m (CBMCExceptT a m b)
simpleFresh spec
v = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh spec
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a))
  ) =>
  GenSymSimple (CBMCExceptT e m a) (CBMCExceptT e m a)
  where
  simpleFresh :: forall (m :: * -> *).
MonadFresh m =>
CBMCExceptT e m a -> m (CBMCExceptT e m a)
simpleFresh (CBMCExceptT m (CBMCEither e a)
v) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
simpleFresh m (CBMCEither e a)
v

instance
  {-# OVERLAPPING #-}
  ( GenSymSimple (m (CBMCEither e a)) (m (CBMCEither e a)),
    Mergeable1 m,
    Mergeable e,
    Mergeable a
  ) =>
  GenSym (CBMCExceptT e m a) (CBMCExceptT e m a)

instance
  (UnionLike m, Mergeable e, Mergeable a) =>
  SimpleMergeable (CBMCExceptT e m a)
  where
  mrgIte :: SymBool
-> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
mrgIte = forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
  {-# INLINE mrgIte #-}

instance
  (UnionLike m, Mergeable e) =>
  SimpleMergeable1 (CBMCExceptT e m)
  where
  liftMrgIte :: forall a.
(SymBool -> a -> a -> a)
-> SymBool
-> CBMCExceptT e m a
-> CBMCExceptT e m a
-> CBMCExceptT e m a
liftMrgIte SymBool -> a -> a -> a
m = forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
  {-# INLINE liftMrgIte #-}

instance
  (UnionLike m, Mergeable e) =>
  UnionLike (CBMCExceptT e m)
  where
  mergeWithStrategy :: forall a.
MergingStrategy a -> CBMCExceptT e m a -> CBMCExceptT e m a
mergeWithStrategy MergingStrategy a
s (CBMCExceptT m (CBMCEither e a)
v) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
s) m (CBMCEither e a)
v
  {-# INLINE mergeWithStrategy #-}
  mrgIfWithStrategy :: forall a.
MergingStrategy a
-> SymBool
-> CBMCExceptT e m a
-> CBMCExceptT e m a
-> CBMCExceptT e m a
mrgIfWithStrategy MergingStrategy a
s SymBool
cond (CBMCExceptT m (CBMCEither e a)
t) (CBMCExceptT m (CBMCEither e a)
f) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
s) SymBool
cond m (CBMCEither e a)
t m (CBMCEither e a)
f
  {-# INLINE mrgIfWithStrategy #-}
  single :: forall a. a -> CBMCExceptT e m a
single = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: * -> *) a. UnionLike u => a -> u a
single forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return
  {-# INLINE single #-}
  unionIf :: forall a.
SymBool
-> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
unionIf SymBool
cond (CBMCExceptT m (CBMCEither e a)
l) (CBMCExceptT m (CBMCEither e a)
r) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall (u :: * -> *) a. UnionLike u => SymBool -> u a -> u a -> u a
unionIf SymBool
cond m (CBMCEither e a)
l m (CBMCEither e a)
r
  {-# INLINE unionIf #-}

instance (SOrd (m (CBMCEither e a))) => SOrd (CBMCExceptT e m a) where
  (CBMCExceptT m (CBMCEither e a)
l) <=~ :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool
<=~ (CBMCExceptT m (CBMCEither e a)
r) = m (CBMCEither e a)
l forall a. SOrd a => a -> a -> SymBool
<=~ m (CBMCEither e a)
r
  (CBMCExceptT m (CBMCEither e a)
l) <~ :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool
<~ (CBMCExceptT m (CBMCEither e a)
r) = m (CBMCEither e a)
l forall a. SOrd a => a -> a -> SymBool
<~ m (CBMCEither e a)
r
  (CBMCExceptT m (CBMCEither e a)
l) >=~ :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool
>=~ (CBMCExceptT m (CBMCEither e a)
r) = m (CBMCEither e a)
l forall a. SOrd a => a -> a -> SymBool
>=~ m (CBMCEither e a)
r
  (CBMCExceptT m (CBMCEither e a)
l) >~ :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool
>~ (CBMCExceptT m (CBMCEither e a)
r) = m (CBMCEither e a)
l forall a. SOrd a => a -> a -> SymBool
>~ m (CBMCEither e a)
r
  symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> UnionM Ordering
symCompare (CBMCExceptT m (CBMCEither e a)
l) (CBMCExceptT m (CBMCEither e a)
r) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare m (CBMCEither e a)
l m (CBMCEither e a)
r

instance
  ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) =>
  ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)
  where
  toCon :: CBMCExceptT e1 m1 a -> Maybe (CBMCExceptT e2 m2 b)
toCon (CBMCExceptT m1 (CBMCEither e1 a)
v) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. ToCon a b => a -> Maybe b
toCon m1 (CBMCEither e1 a)
v

instance
  ToCon (m1 (CBMCEither e1 a)) (Either e2 b) =>
  ToCon (CBMCExceptT e1 m1 a) (Either e2 b)
  where
  toCon :: CBMCExceptT e1 m1 a -> Maybe (Either e2 b)
toCon (CBMCExceptT m1 (CBMCEither e1 a)
v) = forall a b. ToCon a b => a -> Maybe b
toCon m1 (CBMCEither e1 a)
v

instance
  (ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b))) =>
  ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)
  where
  toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b
toSym (CBMCExceptT m1 (CBMCEither e1 a)
v) = forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT forall a b. (a -> b) -> a -> b
$ forall a b. ToSym a b => a -> b
toSym m1 (CBMCEither e1 a)
v

instance
  (Monad u, UnionLike u, Mergeable e, Mergeable v) =>
  UnionWithExcept (CBMCExceptT e u v) u e v
  where
  extractUnionExcept :: CBMCExceptT e u v -> u (Either e v)
extractUnionExcept = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. CBMCEither a b -> Either a b
runCBMCEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT