{-# 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
(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
/= :: 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 b.
 (a -> b -> Bool) -> CBMCEither a a -> CBMCEither a b -> Bool)
-> Eq1 (CBMCEither 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 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, 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
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, Eq1 (CBMCEither a)
Eq1 (CBMCEither a)
-> (forall a b.
    (a -> b -> Ordering)
    -> CBMCEither a a -> CBMCEither a b -> Ordering)
-> Ord1 (CBMCEither a)
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]
(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]
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.
 (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 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
(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
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.
 (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 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 -> 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
<$ :: 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, 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
<* :: 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, 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
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
(Int -> CBMCEither a b -> Int)
-> (CBMCEither a b -> Int) -> Hashable (CBMCEither a b)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
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 -> ()
(CBMCEither a b -> ()) -> NFData (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 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
$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 (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)
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 = 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 (UnionM (CBMCEither a b))
fresh = () -> m (UnionM (CBMCEither a b))
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) = 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
/= :: 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, 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
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
[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
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 = 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 '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 (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 '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 '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 (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 '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
$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 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
$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) = (CBMCEither e a -> CBMCEither e b -> Bool)
-> m (CBMCEither e a) -> m (CBMCEither e 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 (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)
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 (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 (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 (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
    CBMCEither e (a -> b)
mf <- m (CBMCEither e (a -> b))
f
    case CBMCEither e (a -> b)
mf of
      CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
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
        CBMCEither e a
mv <- m (CBMCEither e a)
v
        case CBMCEither e a
mv of
          CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
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 (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 (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 (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
    CBMCEither e a
ex <- m (CBMCEither e a)
mx
    case CBMCEither e a
ex of
      CBMCEither (Left e
e) -> (CBMCEither e a -> CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a)
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 (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
    CBMCEither e a
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 CBMCEither e a
a of
      CBMCEither (Left e
e) -> CBMCEither e b -> m (CBMCEither e b)
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 (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 (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
    CBMCEither e a
ex <- m (CBMCEither e a)
mx
    case CBMCEither e a
ex of
      CBMCEither (Left e
e) -> (CBMCEither e a -> CBMCEither e a)
-> m (CBMCEither e a) -> m (CBMCEither e a)
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 (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 (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 (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 (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 (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 (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 (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 (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((a' -> a) -> CBMCEither e a' -> CBMCEither e a
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 (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
  CBMCEither e a
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 CBMCEither e a
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 (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 (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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
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) = 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. 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) = m (CBMCEither e a) -> SymbolSet
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 = 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 (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (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 (UnionM (CBMCExceptT a m b))
fresh spec
v = do
    UnionM (m (CBMCEither a b))
x <- spec -> m (UnionM (m (CBMCEither a b)))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
fresh spec
v
    UnionM (CBMCExceptT a m b) -> m (UnionM (CBMCExceptT a m b))
forall (m :: * -> *) a. Monad m => a -> m a
return (UnionM (CBMCExceptT a m b) -> m (UnionM (CBMCExceptT a m b)))
-> UnionM (CBMCExceptT a m b) -> m (UnionM (CBMCExceptT a m b))
forall a b. (a -> b) -> a -> b
$ UnionM (CBMCExceptT a m b) -> UnionM (CBMCExceptT a m b)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (UnionM (CBMCExceptT a m b) -> UnionM (CBMCExceptT a m b))
-> (UnionM (m (CBMCEither a b)) -> UnionM (CBMCExceptT a m b))
-> UnionM (m (CBMCEither a b))
-> UnionM (CBMCExceptT a m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (CBMCEither a b) -> CBMCExceptT a m b)
-> UnionM (m (CBMCEither a b)) -> UnionM (CBMCExceptT a m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (CBMCEither a b) -> CBMCExceptT a m b
forall e (m :: * -> *) a. m (CBMCEither e a) -> CBMCExceptT e m a
CBMCExceptT (UnionM (m (CBMCEither a b)) -> UnionM (CBMCExceptT a m b))
-> UnionM (m (CBMCEither a b)) -> UnionM (CBMCExceptT a m b)
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 = 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
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
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 = SymBool
-> CBMCExceptT e m a -> CBMCExceptT e m a -> CBMCExceptT e m a
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 = MergingStrategy a
-> SymBool
-> CBMCExceptT e m a
-> CBMCExceptT e m a
-> CBMCExceptT e m a
forall (u :: * -> *) a.
UnionLike 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
  (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) = 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 (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> u a -> u a
mergeWithStrategy (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 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) = 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 (u :: * -> *) a.
UnionLike u =>
MergingStrategy a -> SymBool -> u a -> u a -> u a
mrgIfWithStrategy (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 #-}
  single :: forall a. a -> CBMCExceptT e m a
single = 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)
-> (a -> m (CBMCEither e a)) -> a -> CBMCExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CBMCEither e a -> m (CBMCEither e a)
forall (u :: * -> *) a. UnionLike u => a -> u a
single (CBMCEither e a -> m (CBMCEither e a))
-> (a -> CBMCEither e a) -> a -> m (CBMCEither e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CBMCEither e a
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) = 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 (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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
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 m (CBMCEither e a) -> m (CBMCEither e a) -> SymBool
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) = m (CBMCEither e a) -> m (CBMCEither e a) -> UnionM Ordering
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) = 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 (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) = 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, 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 = u (Either e v) -> u (Either e v)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => u a -> u a
merge (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 (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