{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# 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.Internal.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.Internal.Core.Control.Monad.CBMCExcept
  ( -- * CBMC-like error handling
    CBMCEither (..),
    CBMCExceptT (..),
    cbmcExcept,
    mapCBMCExceptT,
    withCBMCExceptT,
    OrigExcept.MonadError (..),
  )
where

#if MIN_VERSION_base(4,18,0)
import Control.Applicative
  ( Alternative (empty, (<|>)),
  )
#else
import Control.Applicative
  ( Alternative (empty, (<|>)),
    Applicative (liftA2),
  )
#endif
import Control.DeepSeq (NFData)
import Control.Monad (MonadPlus (mplus, mzero))
import qualified Control.Monad.Except as OrigExcept
import qualified Control.Monad.Fail as Fail
import Control.Monad.Fix (MonadFix (mfix))
import Control.Monad.Trans (MonadIO (liftIO), MonadTrans (lift))
import Control.Monad.Zip (MonadZip (mzipWith))
import Data.Functor.Classes
  ( Eq1 (liftEq),
    Ord1 (liftCompare),
    Read1 (liftReadList, liftReadsPrec),
    Show1 (liftShowList, liftShowsPrec),
    compare1,
    eq1,
    readsData,
    readsPrec1,
    readsUnaryWith,
    showsPrec1,
    showsUnaryWith,
  )
import Data.Functor.Contravariant (Contravariant (contramap))
import Data.Hashable (Hashable)
import GHC.Generics (Generic, Generic1)
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym (evalSym))
import Grisette.Internal.Core.Data.Class.ExtractSym
  ( ExtractSym (extractSymMaybe),
  )
import Grisette.Internal.Core.Data.Class.GenSym
  ( GenSym (fresh),
    GenSymSimple (simpleFresh),
    derivedNoSpecFresh,
    derivedSameShapeSimpleFresh,
  )
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    Mergeable1 (liftRootStrategy),
    MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
    rootStrategy1,
    wrapStrategy,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SimpleMergeable (mrgIte),
    SimpleMergeable1 (liftMrgIte),
    SymBranching (mrgIfPropagatedStrategy, mrgIfWithStrategy),
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))
import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd (symCompare, (.<), (.<=), (.>), (.>=)))
import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon), ToCon1)
import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym), ToSym1)
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge (tryMergeWithStrategy),
    tryMerge,
  )
import Language.Haskell.TH.Syntax (Lift)
import Unsafe.Coerce (unsafeCoerce)

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

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

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

deriving newtype instance
  (ExtractSym a, ExtractSym b) =>
  ExtractSym (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 = CBMCEither a b -> m (CBMCEither a b)
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 (Union (CBMCEither a b))
fresh = () -> m (Union (CBMCEither a b))
forall a (m :: * -> *).
(Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) =>
() -> m (Union a)
derivedNoSpecFresh

deriving newtype instance (SymOrd a, SymOrd b) => SymOrd (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) = Either e2 a2 -> CBMCEither e2 a2
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e2 a2 -> CBMCEither e2 a2)
-> Maybe (Either e2 a2) -> Maybe (CBMCEither e2 a2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either e1 a1 -> Maybe (Either e2 a2)
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) = Either e1 a1 -> Maybe (Either e2 a2)
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) = Either e2 a2 -> CBMCEither e2 a2
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e2 a2 -> CBMCEither e2 a2)
-> Either e2 a2 -> CBMCEither e2 a2
forall a b. (a -> b) -> a -> b
$ Either e1 a1 -> Either e2 a2
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) = Either e1 a1 -> Either e2 a2
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
(EitherIdx idx -> EitherIdx idx -> Bool)
-> (EitherIdx idx -> EitherIdx idx -> Bool) -> Eq (EitherIdx idx)
forall idx. Eq idx => EitherIdx idx -> EitherIdx idx -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: EitherIdx idx -> EitherIdx idx -> Bool
Eq, Eq (EitherIdx idx)
Eq (EitherIdx idx) =>
(EitherIdx idx -> EitherIdx idx -> Ordering)
-> (EitherIdx idx -> EitherIdx idx -> Bool)
-> (EitherIdx idx -> EitherIdx idx -> Bool)
-> (EitherIdx idx -> EitherIdx idx -> Bool)
-> (EitherIdx idx -> EitherIdx idx -> Bool)
-> (EitherIdx idx -> EitherIdx idx -> EitherIdx idx)
-> (EitherIdx idx -> EitherIdx idx -> EitherIdx idx)
-> Ord (EitherIdx idx)
EitherIdx idx -> EitherIdx idx -> Bool
EitherIdx idx -> EitherIdx idx -> Ordering
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
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
$ccompare :: forall idx. Ord idx => EitherIdx idx -> EitherIdx idx -> Ordering
compare :: EitherIdx idx -> EitherIdx idx -> Ordering
$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
>= :: EitherIdx idx -> EitherIdx idx -> Bool
$cmax :: forall idx.
Ord idx =>
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
max :: EitherIdx idx -> EitherIdx idx -> EitherIdx idx
$cmin :: forall idx.
Ord idx =>
EitherIdx idx -> EitherIdx idx -> EitherIdx idx
min :: EitherIdx idx -> EitherIdx idx -> EitherIdx idx
Ord, Int -> EitherIdx idx -> ShowS
[EitherIdx idx] -> ShowS
EitherIdx idx -> String
(Int -> EitherIdx idx -> ShowS)
-> (EitherIdx idx -> String)
-> ([EitherIdx idx] -> ShowS)
-> Show (EitherIdx idx)
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
$cshowsPrec :: forall idx. Show idx => Int -> EitherIdx idx -> ShowS
showsPrec :: Int -> EitherIdx idx -> ShowS
$cshow :: forall idx. Show idx => EitherIdx idx -> String
show :: EitherIdx idx -> String
$cshowList :: forall idx. Show idx => [EitherIdx idx] -> ShowS
showList :: [EitherIdx idx] -> ShowS
Show)

instance (Mergeable e, Mergeable a) => Mergeable (CBMCEither e a) where
  rootStrategy :: MergingStrategy (CBMCEither e a)
rootStrategy = MergingStrategy (CBMCEither e a)
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 MergingStrategy e
forall a. Mergeable a => MergingStrategy a
rootStrategy of
    SimpleStrategy SymBool -> e -> e -> e
m ->
      (CBMCEither e a -> Bool)
-> (Bool -> MergingStrategy (CBMCEither e a))
-> MergingStrategy (CBMCEither e a)
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 -> (SymBool -> CBMCEither e a -> CBMCEither e a -> CBMCEither e a)
-> MergingStrategy (CBMCEither e a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> CBMCEither e a -> CBMCEither e a -> CBMCEither e a)
 -> MergingStrategy (CBMCEither e a))
-> (SymBool -> CBMCEither e a -> CBMCEither e a -> CBMCEither e a)
-> MergingStrategy (CBMCEither e a)
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) -> Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a) -> Either e a -> CBMCEither e a
forall a b. (a -> b) -> a -> b
$ e -> Either e a
forall a b. a -> Either a b
Left (e -> Either e a) -> e -> Either e a
forall a b. (a -> b) -> a -> b
$ SymBool -> e -> e -> e
m SymBool
cond e
l e
r
                (Either e a, Either e a)
_ -> String -> CBMCEither e a
forall a. HasCallStack => String -> a
error String
"impossible"
            Bool
True -> MergingStrategy a
-> (a -> CBMCEither e a)
-> (CBMCEither e a -> a)
-> MergingStrategy (CBMCEither e a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> String -> a
forall a. HasCallStack => String -> a
error String
"impossible")
        )
    MergingStrategy e
NoStrategy ->
      (CBMCEither e a -> Bool)
-> (Bool -> MergingStrategy (CBMCEither e a))
-> MergingStrategy (CBMCEither e a)
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 -> MergingStrategy (CBMCEither e a)
forall a. MergingStrategy a
NoStrategy
            Bool
True -> MergingStrategy a
-> (a -> CBMCEither e a)
-> (CBMCEither e a -> a)
-> MergingStrategy (CBMCEither e a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> String -> a
forall a. HasCallStack => String -> a
error String
"impossible")
        )
    SortedStrategy e -> idx
idx idx -> MergingStrategy e
sub ->
      (CBMCEither e a -> EitherIdx idx)
-> (EitherIdx idx -> MergingStrategy (CBMCEither e a))
-> MergingStrategy (CBMCEither e a)
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 -> idx -> EitherIdx idx
forall idx. idx -> EitherIdx idx
L (idx -> EitherIdx idx) -> idx -> EitherIdx idx
forall a b. (a -> b) -> a -> b
$ e -> idx
idx e
v
            Right a
_ -> EitherIdx idx
forall idx. EitherIdx idx
R
        )
        ( \case
            L idx
i -> MergingStrategy e
-> (e -> CBMCEither e a)
-> (CBMCEither e a -> e)
-> MergingStrategy (CBMCEither e a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (idx -> MergingStrategy e
sub idx
i) (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (e -> Either e a) -> e -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left) (\case (CBMCEither (Left e
x)) -> e
x; CBMCEither e a
_ -> String -> e
forall a. HasCallStack => String -> a
error String
"impossible")
            EitherIdx idx
R -> MergingStrategy a
-> (a -> CBMCEither e a)
-> (CBMCEither e a -> a)
-> MergingStrategy (CBMCEither e a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
ms (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right) (\case (CBMCEither (Right a
x)) -> a
x; CBMCEither e a
_ -> String -> 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 = (a -> c) -> (b -> c) -> Either a b -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> c
l b -> c
r (CBMCEither a b -> Either a b
forall a b. a -> b
unsafeCoerce CBMCEither a b
v)

-- | Wrap an 'Either' value in t'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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CBMCEither e a -> m (CBMCEither e a))
-> CBMCEither e a -> m (CBMCEither e a)
forall a b. (a -> b) -> a -> b
$ Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither Either e a
m)

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

-- | Map the error in a t'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 = (m (Either e a) -> m (Either e' a))
-> CBMCExceptT e m a -> CBMCExceptT e' m a
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) -> m (Either e' a))
 -> CBMCExceptT e m a -> CBMCExceptT e' m a)
-> (m (Either e a) -> m (Either e' a))
-> CBMCExceptT e m a
-> CBMCExceptT e' m a
forall a b. (a -> b) -> a -> b
$ (Either e a -> Either e' a) -> m (Either e a) -> m (Either e' a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Either e a -> Either e' a) -> m (Either e a) -> m (Either e' a))
-> (Either e a -> Either e' a) -> m (Either e a) -> m (Either e' a)
forall a b. (a -> b) -> a -> b
$ (e -> Either e' a)
-> (a -> Either e' a) -> Either e a -> Either e' a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (e' -> Either e' a
forall a b. a -> Either a b
Left (e' -> Either e' a) -> (e -> e') -> e -> Either e' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e'
f) a -> Either e' a
forall a b. b -> Either a b
Right

-- | Similar to 'Control.Monad.Except.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 x. CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x)
-> (forall x. Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a)
-> Generic (CBMCExceptT e m a)
forall x. Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a
forall x. CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x
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
$cfrom :: forall e (m :: * -> *) a x.
CBMCExceptT e m a -> Rep (CBMCExceptT e m a) x
from :: forall 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
to :: forall x. Rep (CBMCExceptT e m a) x -> CBMCExceptT e m a
Generic, (forall a. CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a)
-> (forall a. Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a)
-> Generic1 (CBMCExceptT e m)
forall a. Rep1 (CBMCExceptT e m) a -> CBMCExceptT e m a
forall a. CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a
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
$cfrom1 :: forall e (m :: * -> *) a.
Functor m =>
CBMCExceptT e m a -> Rep1 (CBMCExceptT e m) a
from1 :: forall a. 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
to1 :: forall a. Rep1 (CBMCExceptT e m) a -> 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) = (CBMCEither e a -> CBMCEither e b -> Bool)
-> m (CBMCEither e a) -> m (CBMCEither e b) -> Bool
forall a b. (a -> b -> Bool) -> m a -> m b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> CBMCEither e a -> CBMCEither e b -> Bool
forall a b.
(a -> b -> Bool) -> CBMCEither e a -> CBMCEither e b -> Bool
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) =
    (CBMCEither e a -> CBMCEither e b -> Ordering)
-> m (CBMCEither e a) -> m (CBMCEither e b) -> Ordering
forall a b. (a -> b -> Ordering) -> m a -> m b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare ((a -> b -> Ordering)
-> CBMCEither e a -> CBMCEither e b -> Ordering
forall a b.
(a -> b -> Ordering)
-> CBMCEither e a -> CBMCEither e b -> Ordering
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 =
    (String -> ReadS (CBMCExceptT e m a))
-> Int -> ReadS (CBMCExceptT e m a)
forall a. (String -> ReadS a) -> Int -> ReadS a
readsData ((String -> ReadS (CBMCExceptT e m a))
 -> Int -> ReadS (CBMCExceptT e m a))
-> (String -> ReadS (CBMCExceptT e m a))
-> Int
-> ReadS (CBMCExceptT e m a)
forall a b. (a -> b) -> a -> b
$
      (Int -> ReadS (m (CBMCEither e a)))
-> String
-> (m (CBMCEither e a) -> CBMCExceptT e m a)
-> String
-> ReadS (CBMCExceptT e m a)
forall a t.
(Int -> ReadS a) -> String -> (a -> t) -> String -> ReadS t
readsUnaryWith ((Int -> ReadS (CBMCEither e a))
-> ReadS [CBMCEither e a] -> Int -> ReadS (m (CBMCEither e a))
forall a. (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (m a)
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" m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT
    where
      rp' :: Int -> ReadS (CBMCEither e a)
rp' = (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither e a)
forall a.
(Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (CBMCEither e a)
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' = (Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither e a]
forall a. (Int -> ReadS a) -> ReadS [a] -> ReadS [CBMCEither e a]
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) =
    (Int -> m (CBMCEither e a) -> ShowS)
-> String -> Int -> m (CBMCEither e a) -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith ((Int -> CBMCEither e a -> ShowS)
-> ([CBMCEither e a] -> ShowS)
-> Int
-> m (CBMCEither e a)
-> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> m a -> ShowS
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' = (Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither e a -> ShowS
forall a.
(Int -> a -> ShowS)
-> ([a] -> ShowS) -> Int -> CBMCEither e a -> ShowS
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' = (Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither e a] -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> [CBMCEither e a] -> ShowS
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
(==) = 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 = CBMCExceptT e m a -> CBMCExceptT e m a -> Ordering
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 = Int -> ReadS (CBMCExceptT e m a)
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 = Int -> CBMCExceptT e m a -> ShowS
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 = m (CBMCEither e b) -> CBMCExceptT e m b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e b) -> CBMCExceptT e m b)
-> (CBMCExceptT e m a -> m (CBMCEither e b))
-> CBMCExceptT e m a
-> CBMCExceptT e m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CBMCEither e a -> CBMCEither e b)
-> m (CBMCEither e a) -> m (CBMCEither e b)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> CBMCEither e a -> CBMCEither e b
forall a b. (a -> b) -> CBMCEither e a -> CBMCEither e b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (m (CBMCEither e a) -> m (CBMCEither e b))
-> (CBMCExceptT e m a -> m (CBMCEither e a))
-> CBMCExceptT e m a
-> m (CBMCEither e b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CBMCExceptT e m a -> m (CBMCEither e a)
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) = (CBMCEither e a -> m) -> f (CBMCEither e a) -> m
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((e -> m) -> (a -> m) -> CBMCEither e a -> m
forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (m -> e -> m
forall a b. a -> b -> a
const m
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) =
    f (CBMCEither e b) -> CBMCExceptT e f b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (f (CBMCEither e b) -> CBMCExceptT e f b)
-> f (f (CBMCEither e b)) -> f (CBMCExceptT e f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CBMCEither e a -> f (CBMCEither e b))
-> f (CBMCEither e a) -> f (f (CBMCEither e b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((e -> f (CBMCEither e b))
-> (a -> f (CBMCEither e b))
-> CBMCEither e a
-> f (CBMCEither e b)
forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (CBMCEither e b -> f (CBMCEither e b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CBMCEither e b -> f (CBMCEither e b))
-> (e -> CBMCEither e b) -> e -> f (CBMCEither e b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b)
-> (e -> Either e b) -> e -> CBMCEither e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e b
forall a b. a -> Either a b
Left) ((b -> CBMCEither e b) -> f b -> f (CBMCEither e b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b)
-> (b -> Either e b) -> b -> CBMCEither e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either e b
forall a b. b -> Either a b
Right) (f b -> f (CBMCEither e b))
-> (a -> f b) -> a -> f (CBMCEither e b)
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right (a -> CBMCEither e a) -> a -> CBMCEither e a
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 = m (CBMCEither e b) -> CBMCExceptT e m b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e b) -> CBMCExceptT e m b)
-> m (CBMCEither e b) -> CBMCExceptT e m b
forall a b. (a -> b) -> a -> b
$ do
    mf <- m (CBMCEither e (a -> b))
f
    case mf of
      CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b)
-> (e -> Either e b) -> e -> CBMCEither e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e b
forall a b. a -> Either a b
Left (e -> CBMCEither e b) -> e -> CBMCEither e b
forall a b. (a -> b) -> a -> b
$ e
e)
      CBMCEither (Right a -> b
k) -> do
        mv <- m (CBMCEither e a)
v
        case mv of
          CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b)
-> (e -> Either e b) -> e -> CBMCEither e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e b
forall a b. a -> Either a b
Left (e -> CBMCEither e b) -> e -> CBMCEither e b
forall a b. (a -> b) -> a -> b
$ e
e)
          CBMCEither (Right a
x) -> CBMCEither e b -> m (CBMCEither e b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b)
-> (b -> Either e b) -> b -> CBMCEither e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either e b
forall a b. b -> Either a b
Right (b -> CBMCEither e b) -> b -> CBMCEither e b
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 CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m b
forall a b.
CBMCExceptT e m a -> CBMCExceptT e m b -> CBMCExceptT e m b
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (e -> Either e a) -> e -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left (e -> CBMCEither e a) -> e -> CBMCEither e a
forall a b. (a -> b) -> a -> b
$ e
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ do
    ex <- m (CBMCEither e a)
mx
    case ex of
      CBMCEither (Left e
e) -> (CBMCEither e a -> CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((e -> CBMCEither e a)
-> (a -> CBMCEither e a) -> CBMCEither e a -> CBMCEither e a
forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (e -> Either e a) -> e -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left (e -> Either e a) -> (e -> e) -> e -> Either e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e -> e
forall a. Monoid a => a -> a -> a
mappend e
e) (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right)) m (CBMCEither e a)
my
      CBMCEither (Right a
x) -> CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right (a -> CBMCEither e a) -> a -> CBMCEither e a
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 = m (CBMCEither e b) -> CBMCExceptT e m b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e b) -> CBMCExceptT e m b)
-> m (CBMCEither e b) -> CBMCExceptT e m b
forall a b. (a -> b) -> a -> b
$ do
    a <- CBMCExceptT e m a -> m (CBMCEither e a)
forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT CBMCExceptT e m a
m
    case a of
      CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e b -> CBMCEither e b
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e b -> CBMCEither e b) -> Either e b -> CBMCEither e b
forall a b. (a -> b) -> a -> b
$ e -> Either e b
forall a b. a -> Either a b
Left e
e)
      CBMCEither (Right a
x) -> CBMCExceptT e m b -> m (CBMCEither e b)
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> (String -> m (CBMCEither e a)) -> String -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m (CBMCEither e a)
forall a. String -> m a
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a) -> Either e a -> CBMCEither e a
forall a b. (a -> b) -> a -> b
$ e -> Either e a
forall a b. a -> Either a b
Left e
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ do
    ex <- m (CBMCEither e a)
mx
    case ex of
      CBMCEither (Left e
e) -> (CBMCEither e a -> CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((e -> CBMCEither e a)
-> (a -> CBMCEither e a) -> CBMCEither e a -> CBMCEither e a
forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (e -> Either e a) -> e -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left (e -> Either e a) -> (e -> e) -> e -> Either e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e -> e
forall a. Monoid a => a -> a -> a
mappend e
e) (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
forall a b. b -> Either a b
Right)) m (CBMCEither e a)
my
      CBMCEither (Right a
x) -> CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a) -> Either e a -> CBMCEither e a
forall a b. (a -> b) -> a -> b
$ a -> Either e a
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT ((CBMCEither e a -> m (CBMCEither e a)) -> m (CBMCEither e a)
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (CBMCExceptT e m a -> m (CBMCEither e a)
forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT (CBMCExceptT e m a -> m (CBMCEither e a))
-> (CBMCEither e a -> CBMCExceptT e m a)
-> CBMCEither e a
-> m (CBMCEither e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CBMCExceptT e m a
f (a -> CBMCExceptT e m a)
-> (CBMCEither e a -> a) -> CBMCEither e a -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> a) -> (a -> a) -> CBMCEither e a -> a
forall a c b. (a -> c) -> (b -> c) -> CBMCEither a b -> c
cbmcEither (a -> e -> a
forall a b. a -> b -> a
const a
forall {a}. a
bomb) a -> a
forall a. a -> a
id))
    where
      bomb :: a
bomb = String -> a
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> (m a -> m (CBMCEither e a)) -> m a -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> CBMCEither e a) -> m a -> m (CBMCEither e a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (a -> Either e a) -> a -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e a
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 = m a -> CBMCExceptT e m a
forall (m :: * -> *) a. Monad m => m a -> CBMCExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> CBMCExceptT e m a)
-> (IO a -> m a) -> IO a -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall a. IO a -> m a
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) = m (CBMCEither e c) -> CBMCExceptT e m c
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e c) -> CBMCExceptT e m c)
-> m (CBMCEither e c) -> CBMCExceptT e m c
forall a b. (a -> b) -> a -> b
$ (CBMCEither e a -> CBMCEither e b -> CBMCEither e c)
-> m (CBMCEither e a) -> m (CBMCEither e b) -> m (CBMCEither e c)
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> m a -> m b -> m c
mzipWith ((a -> b -> c) -> CBMCEither e a -> CBMCEither e b -> CBMCEither e c
forall a b c.
(a -> b -> c) -> CBMCEither e a -> CBMCEither e b -> CBMCEither e c
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 = m (CBMCEither e a') -> CBMCExceptT e m a'
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a') -> CBMCExceptT e m a')
-> (CBMCExceptT e m a -> m (CBMCEither e a'))
-> CBMCExceptT e m a
-> CBMCExceptT e m a'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CBMCEither e a' -> CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a')
forall a' a. (a' -> a) -> m a -> m a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((a' -> a) -> CBMCEither e a' -> CBMCEither e a
forall a b. (a -> b) -> CBMCEither e a -> CBMCEither e b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a' -> a
f) (m (CBMCEither e a) -> m (CBMCEither e a'))
-> (CBMCExceptT e m a -> m (CBMCEither e a))
-> CBMCExceptT e m a
-> m (CBMCEither e a')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CBMCExceptT e m a -> m (CBMCEither e a)
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 = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> (e -> m (CBMCEither e a)) -> e -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CBMCEither e a -> m (CBMCEither e a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CBMCEither e a -> m (CBMCEither e a))
-> (e -> CBMCEither e a) -> e -> m (CBMCEither e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either e a -> CBMCEither e a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e a -> CBMCEither e a)
-> (e -> Either e a) -> e -> CBMCEither e a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
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 = m (CBMCEither e' a) -> CBMCExceptT e' m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e' a) -> CBMCExceptT e' m a)
-> m (CBMCEither e' a) -> CBMCExceptT e' m a
forall a b. (a -> b) -> a -> b
$ do
  a <- CBMCExceptT e m a -> m (CBMCEither e a)
forall e (m :: * -> *) a. CBMCExceptT e m a -> m (CBMCEither e a)
runCBMCExceptT CBMCExceptT e m a
m
  case a of
    CBMCEither (Left e
l) -> CBMCExceptT e' m a -> m (CBMCEither e' a)
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) -> CBMCEither e' a -> m (CBMCEither e' a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either e' a -> CBMCEither e' a
forall a b. Either a b -> CBMCEither a b
CBMCEither (Either e' a -> CBMCEither e' a)
-> (a -> Either e' a) -> a -> CBMCEither e' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either e' a
forall a b. b -> Either a b
Right (a -> CBMCEither e' a) -> a -> CBMCEither e' a
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 = e -> CBMCExceptT e m a
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 = CBMCExceptT e m a -> (e -> CBMCExceptT e m a) -> CBMCExceptT e m a
forall (m :: * -> *) e a e'.
Monad m =>
CBMCExceptT e m a
-> (e -> CBMCExceptT e' m a) -> CBMCExceptT e' m a
catchE
  {-# INLINE catchError #-}

instance (SymEq (m (CBMCEither e a))) => SymEq (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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== m (CBMCEither e a)
b
  {-# INLINE (.==) #-}

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

instance
  (ExtractSym (m (CBMCEither e a))) =>
  ExtractSym (CBMCExceptT e m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
CBMCExceptT e m a -> Maybe (SymbolSet knd)
extractSymMaybe (CBMCExceptT m (CBMCEither e a)
v) = m (CBMCEither e a) -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
m (CBMCEither e a) -> Maybe (SymbolSet knd)
extractSymMaybe 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 = MergingStrategy (m (CBMCEither e a))
-> (m (CBMCEither e a) -> CBMCExceptT e m a)
-> (CBMCExceptT e m a -> m (CBMCEither e a))
-> MergingStrategy (CBMCExceptT e m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy (m (CBMCEither e a))
forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1 m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT CBMCExceptT e m a -> m (CBMCEither e a)
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 = MergingStrategy (m (CBMCEither e a))
-> (m (CBMCEither e a) -> CBMCExceptT e m a)
-> (CBMCExceptT e m a -> m (CBMCEither e a))
-> MergingStrategy (CBMCExceptT e m a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergingStrategy (CBMCEither e a)
-> MergingStrategy (m (CBMCEither e a))
forall a. MergingStrategy a -> MergingStrategy (m a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergingStrategy a -> MergingStrategy (CBMCEither e a)
forall a. MergingStrategy a -> MergingStrategy (CBMCEither e a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
m)) m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT CBMCExceptT e m a -> m (CBMCEither e a)
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 (Union (CBMCExceptT a m b))
fresh spec
v = do
    x <- spec -> m (Union (m (CBMCEither a b)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *).
MonadFresh m =>
spec -> m (Union (m (CBMCEither a b)))
fresh spec
v
    return $ tryMerge . fmap CBMCExceptT $ 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 = m (CBMCEither a b) -> CBMCExceptT a m b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither a b) -> CBMCExceptT a m b)
-> m (m (CBMCEither a b)) -> m (CBMCExceptT a m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> spec -> m (m (CBMCEither a b))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
spec -> m (m (CBMCEither a b))
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) = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (m (CBMCEither e a)) -> m (CBMCExceptT e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (CBMCEither e a) -> m (m (CBMCEither e a))
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *).
MonadFresh m =>
m (CBMCEither e a) -> m (m (CBMCEither e 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
  (SymBranching 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 = SymBool
-> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
  {-# INLINE mrgIte #-}

instance
  (SymBranching 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 = MergingStrategy a
-> SymBool
-> CBMCExceptT e m a
-> CBMCExceptT e m a
-> CBMCExceptT e m a
forall a.
MergingStrategy a
-> SymBool
-> CBMCExceptT e m a
-> CBMCExceptT e m a
-> CBMCExceptT e m a
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> a -> a -> a
m)
  {-# INLINE liftMrgIte #-}

instance
  (TryMerge m, Mergeable e) =>
  TryMerge (CBMCExceptT e m)
  where
  tryMergeWithStrategy :: forall a.
MergingStrategy a -> CBMCExceptT e m a -> CBMCExceptT e m a
tryMergeWithStrategy MergingStrategy a
s (CBMCExceptT m (CBMCEither e a)
v) = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ MergingStrategy (CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a)
forall a. MergingStrategy a -> m a -> m a
forall (m :: * -> *) a.
TryMerge m =>
MergingStrategy a -> m a -> m a
tryMergeWithStrategy (MergingStrategy a -> MergingStrategy (CBMCEither e a)
forall a. MergingStrategy a -> MergingStrategy (CBMCEither e a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
s) m (CBMCEither e a)
v
  {-# INLINE tryMergeWithStrategy #-}

instance
  (SymBranching m, Mergeable e) =>
  SymBranching (CBMCExceptT e m)
  where
  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) = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ MergingStrategy (CBMCEither e a)
-> SymBool
-> m (CBMCEither e a)
-> m (CBMCEither e a)
-> m (CBMCEither e a)
forall a. MergingStrategy a -> SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
SymBranching u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (MergingStrategy a -> MergingStrategy (CBMCEither e a)
forall a. MergingStrategy a -> MergingStrategy (CBMCEither e a)
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 #-}
  mrgIfPropagatedStrategy :: forall a.
SymBool
-> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
mrgIfPropagatedStrategy SymBool
cond (CBMCExceptT m (CBMCEither e a)
t) (CBMCExceptT m (CBMCEither e a)
f) = m (CBMCEither e a) -> CBMCExceptT e m a
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m (CBMCEither e a) -> CBMCExceptT e m a)
-> m (CBMCEither e a) -> CBMCExceptT e m a
forall a b. (a -> b) -> a -> b
$ SymBool
-> m (CBMCEither e a) -> m (CBMCEither e a) -> m (CBMCEither e a)
forall a. SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
SymBranching u =>
SymBool -> u a -> u a -> u a
mrgIfPropagatedStrategy SymBool
cond m (CBMCEither e a)
t m (CBMCEither e a)
f
  {-# INLINE mrgIfPropagatedStrategy #-}

instance (SymOrd (m (CBMCEither e a))) => SymOrd (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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
forall a. SymOrd 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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
forall a. SymOrd 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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
forall a. SymOrd 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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> m (CBMCEither e a)
r
  symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> Union Ordering
symCompare (CBMCExceptT m (CBMCEither e a)
l) (CBMCExceptT m (CBMCEither e a)
r) = m (CBMCEither e a) -> m (CBMCEither e a) -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare m (CBMCEither e a)
l m (CBMCEither e a)
r

instance
  (ToCon1 m1 m2, ToCon e1 e2, ToCon a 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) = m2 (CBMCEither e2 b) -> CBMCExceptT e2 m2 b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m2 (CBMCEither e2 b) -> CBMCExceptT e2 m2 b)
-> Maybe (m2 (CBMCEither e2 b)) -> Maybe (CBMCExceptT e2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (CBMCEither e1 a) -> Maybe (m2 (CBMCEither e2 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) = m1 (CBMCEither e1 a) -> Maybe (Either e2 b)
forall a b. ToCon a b => a -> Maybe b
toCon m1 (CBMCEither e1 a)
v

instance
  (ToSym e1 e2, ToSym a b, ToSym1 m1 m2) =>
  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) = m2 (CBMCEither e2 b) -> CBMCExceptT e2 m2 b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (m2 (CBMCEither e2 b) -> CBMCExceptT e2 m2 b)
-> m2 (CBMCEither e2 b) -> CBMCExceptT e2 m2 b
forall a b. (a -> b) -> a -> b
$ m1 (CBMCEither e1 a) -> m2 (CBMCEither e2 b)
forall a b. ToSym a b => a -> b
toSym m1 (CBMCEither e1 a)
v

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

instance UnionWithExcept (Union (CBMCEither e v)) Union e v where
  extractUnionExcept :: Union (CBMCEither e v) -> Union (Either e v)
extractUnionExcept = (CBMCEither e v -> Either e v)
-> Union (CBMCEither e v) -> Union (Either e v)
forall a b. (a -> b) -> Union a -> Union b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CBMCEither e v -> Either e v
forall a b. CBMCEither a b -> Either a b
runCBMCEither