{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SymEq
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.SymEq
  ( -- * Symbolic equality
    SymEq (..),
    SymEq1 (..),
    symEq1,
    SymEq2 (..),
    symEq2,

    -- * Generic 'SymEq'
    SymEqArgs (..),
    GSymEq (..),
    genericSymEq,
    genericLiftSymEq,
  )
where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Compose (Compose (Compose))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Kind (Type)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default),
    Default1 (Default1),
    Generic (Rep, from),
    Generic1 (Rep1, from1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&)))
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
import Grisette.Internal.SymPrim.Prim.Term (pevalEqTerm)
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP
  ( SymFP (SymFP),
    SymFPRoundingMode (SymFPRoundingMode),
  )
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins)
import Grisette.Internal.TH.DeriveInstanceProvider
  ( Strategy (ViaDefault, ViaDefault1),
  )
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> :set -XDataKinds
-- >>> :set -XBinaryLiterals
-- >>> :set -XFlexibleContexts
-- >>> :set -XFlexibleInstances
-- >>> :set -XFunctionalDependencies

-- | Symbolic equality. Note that we can't use Haskell's 'Eq' class since
-- symbolic comparison won't necessarily return a concrete 'Bool' value.
--
-- >>> let a = 1 :: SymInteger
-- >>> let b = 2 :: SymInteger
-- >>> a .== b
-- false
-- >>> a ./= b
-- true
--
-- >>> let a = "a" :: SymInteger
-- >>> let b = "b" :: SymInteger
-- >>> a ./= b
-- (! (= a b))
-- >>> a ./= b
-- (! (= a b))
--
-- __Note:__ This type class can be derived for algebraic data types.
-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.
--
-- > data X = ... deriving Generic deriving SymEq via (Default X)
class SymEq a where
  (.==) :: a -> a -> SymBool
  a
a .== a
b = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (SymBool -> SymBool) -> SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
./= a
b
  {-# INLINE (.==) #-}
  infix 4 .==

  (./=) :: a -> a -> SymBool
  a
a ./= a
b = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (SymBool -> SymBool) -> SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
b
  {-# INLINE (./=) #-}
  infix 4 ./=
  {-# MINIMAL (.==) | (./=) #-}

-- | Lifting of the 'SymEq' class to unary type constructors.
--
-- Any instance should be subject to the following law that canonicity is
-- preserved:
--
-- @liftSymEq (.==)@ should be equivalent to @(.==)@, under the symbolic
-- semantics.
--
-- This class therefore represents the generalization of 'SymEq' by decomposing
-- its main method into a canonical lifting on a canonical inner method, so that
-- the lifting can be reused for other arguments than the canonical one.
class (forall a. (SymEq a) => SymEq (f a)) => SymEq1 f where
  -- | Lift a symbolic equality test through the type constructor.
  --
  -- The function will usually be applied to an symbolic equality function, but
  -- the more general type ensures that the implementation uses it to compare
  -- elements of the first container with elements of the second.
  liftSymEq :: (a -> b -> SymBool) -> f a -> f b -> SymBool

-- | Lift the standard @('.==')@ function through the type constructor.
symEq1 :: (SymEq a, SymEq1 f) => f a -> f a -> SymBool
symEq1 :: forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1 = (a -> a -> SymBool) -> f a -> f a -> SymBool
forall a b. (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Lifting of the 'SymEq' class to binary type constructors.
class (forall a. (SymEq a) => SymEq1 (f a)) => SymEq2 f where
  -- | Lift symbolic equality tests through the type constructor.
  --
  -- The function will usually be applied to an symbolic equality function, but
  -- the more general type ensures that the implementation uses it to compare
  -- elements of the first container with elements of the second.
  liftSymEq2 ::
    (a -> b -> SymBool) ->
    (c -> d -> SymBool) ->
    f a c ->
    f b d ->
    SymBool

-- | Lift the standard @('.==')@ function through the type constructor.
symEq2 :: (SymEq a, SymEq b, SymEq2 f) => f a b -> f a b -> SymBool
symEq2 :: forall a b (f :: * -> * -> *).
(SymEq a, SymEq b, SymEq2 f) =>
f a b -> f a b -> SymBool
symEq2 = (a -> a -> SymBool)
-> (b -> b -> SymBool) -> f a b -> f a b -> SymBool
forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
forall (f :: * -> * -> *) a b c d.
SymEq2 f =>
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
liftSymEq2 a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==) b -> b -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- Derivations

-- | The arguments to the generic equality function.
data family SymEqArgs arity a b :: Type

data instance SymEqArgs Arity0 _ _ = SymEqArgs0

newtype instance SymEqArgs Arity1 a b = SymEqArgs1 (a -> b -> SymBool)

-- | The class of types that can be generically compared for symbolic equality.
class GSymEq arity f where
  gsymEq :: SymEqArgs arity a b -> f a -> f b -> SymBool

instance GSymEq arity V1 where
  gsymEq :: forall a b. SymEqArgs arity a b -> V1 a -> V1 b -> SymBool
gsymEq SymEqArgs arity a b
_ V1 a
_ V1 b
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  {-# INLINE gsymEq #-}

instance GSymEq arity U1 where
  gsymEq :: forall a b. SymEqArgs arity a b -> U1 a -> U1 b -> SymBool
gsymEq SymEqArgs arity a b
_ U1 a
_ U1 b
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  {-# INLINE gsymEq #-}

instance (GSymEq arity a, GSymEq arity b) => GSymEq arity (a :*: b) where
  gsymEq :: forall a b.
SymEqArgs arity a b -> (:*:) a b a -> (:*:) a b b -> SymBool
gsymEq SymEqArgs arity a b
args (a a
a1 :*: b a
b1) (a b
a2 :*: b b
b2) = SymEqArgs arity a b -> a a -> a b -> SymBool
forall a b. SymEqArgs arity a b -> a a -> a b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs arity a b
args a a
a1 a b
a2 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymEqArgs arity a b -> b a -> b b -> SymBool
forall a b. SymEqArgs arity a b -> b a -> b b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs arity a b
args b a
b1 b b
b2
  {-# INLINE gsymEq #-}

instance (GSymEq arity a, GSymEq arity b) => GSymEq arity (a :+: b) where
  gsymEq :: forall a b.
SymEqArgs arity a b -> (:+:) a b a -> (:+:) a b b -> SymBool
gsymEq SymEqArgs arity a b
args (L1 a a
a1) (L1 a b
a2) = SymEqArgs arity a b -> a a -> a b -> SymBool
forall a b. SymEqArgs arity a b -> a a -> a b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs arity a b
args a a
a1 a b
a2
  gsymEq SymEqArgs arity a b
args (R1 b a
b1) (R1 b b
b2) = SymEqArgs arity a b -> b a -> b b -> SymBool
forall a b. SymEqArgs arity a b -> b a -> b b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs arity a b
args b a
b1 b b
b2
  gsymEq SymEqArgs arity a b
_ (:+:) a b a
_ (:+:) a b b
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  {-# INLINE gsymEq #-}

instance (GSymEq arity a) => GSymEq arity (M1 i c a) where
  gsymEq :: forall a b.
SymEqArgs arity a b -> M1 i c a a -> M1 i c a b -> SymBool
gsymEq SymEqArgs arity a b
args (M1 a a
a1) (M1 a b
a2) = SymEqArgs arity a b -> a a -> a b -> SymBool
forall a b. SymEqArgs arity a b -> a a -> a b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs arity a b
args a a
a1 a b
a2
  {-# INLINE gsymEq #-}

instance (SymEq a) => GSymEq arity (K1 i a) where
  gsymEq :: forall a b. SymEqArgs arity a b -> K1 i a a -> K1 i a b -> SymBool
gsymEq SymEqArgs arity a b
_ (K1 a
a) (K1 a
b) = a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
b
  {-# INLINE gsymEq #-}

instance GSymEq Arity1 Par1 where
  gsymEq :: forall a b. SymEqArgs Arity1 a b -> Par1 a -> Par1 b -> SymBool
gsymEq (SymEqArgs1 a -> b -> SymBool
e) (Par1 a
a) (Par1 b
b) = a -> b -> SymBool
e a
a b
b
  {-# INLINE gsymEq #-}

instance (SymEq1 f) => GSymEq Arity1 (Rec1 f) where
  gsymEq :: forall a b. SymEqArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> SymBool
gsymEq (SymEqArgs1 a -> b -> SymBool
e) (Rec1 f a
a) (Rec1 f b
b) = (a -> b -> SymBool) -> f a -> f b -> SymBool
forall a b. (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> b -> SymBool
e f a
a f b
b
  {-# INLINE gsymEq #-}

instance (SymEq1 f, GSymEq Arity1 g) => GSymEq Arity1 (f :.: g) where
  gsymEq :: forall a b.
SymEqArgs Arity1 a b -> (:.:) f g a -> (:.:) f g b -> SymBool
gsymEq SymEqArgs Arity1 a b
targs (Comp1 f (g a)
a) (Comp1 f (g b)
b) = (g a -> g b -> SymBool) -> f (g a) -> f (g b) -> SymBool
forall a b. (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq (SymEqArgs Arity1 a b -> g a -> g b -> SymBool
forall a b. SymEqArgs Arity1 a b -> g a -> g b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs Arity1 a b
targs) f (g a)
a f (g b)
b
  {-# INLINE gsymEq #-}

instance (Generic a, GSymEq Arity0 (Rep a)) => SymEq (Default a) where
  Default a
l .== :: Default a -> Default a -> SymBool
.== Default a
r = a -> a -> SymBool
forall a. (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool
genericSymEq a
l a
r
  {-# INLINE (.==) #-}

-- | Generic @('.==')@ function.
genericSymEq :: (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool
genericSymEq :: forall a. (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool
genericSymEq a
l a
r = SymEqArgs Arity0 Any Any -> Rep a Any -> Rep a Any -> SymBool
forall a b. SymEqArgs Arity0 a b -> Rep a a -> Rep a b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq SymEqArgs Arity0 Any Any
forall _ _. SymEqArgs Arity0 _ _
SymEqArgs0 (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
l) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
r)
{-# INLINE genericSymEq #-}

instance (Generic1 f, GSymEq Arity1 (Rep1 f), SymEq a) => SymEq (Default1 f a) where
  .== :: Default1 f a -> Default1 f a -> SymBool
(.==) = Default1 f a -> Default1 f a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (Generic1 f, GSymEq Arity1 (Rep1 f)) => SymEq1 (Default1 f) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> Default1 f a -> Default1 f b -> SymBool
liftSymEq a -> b -> SymBool
f (Default1 f a
l) (Default1 f b
r) = (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
(Generic1 f, GSymEq Arity1 (Rep1 f)) =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
genericLiftSymEq a -> b -> SymBool
f f a
l f b
r
  {-# INLINE liftSymEq #-}

-- | Generic 'liftSymEq' function.
genericLiftSymEq ::
  (Generic1 f, GSymEq Arity1 (Rep1 f)) =>
  (a -> b -> SymBool) ->
  f a ->
  f b ->
  SymBool
genericLiftSymEq :: forall (f :: * -> *) a b.
(Generic1 f, GSymEq Arity1 (Rep1 f)) =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
genericLiftSymEq a -> b -> SymBool
f f a
l f b
r = SymEqArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> SymBool
forall a b. SymEqArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> SymBool
forall arity (f :: * -> *) a b.
GSymEq arity f =>
SymEqArgs arity a b -> f a -> f b -> SymBool
gsymEq ((a -> b -> SymBool) -> SymEqArgs Arity1 a b
forall a b. (a -> b -> SymBool) -> SymEqArgs Arity1 a b
SymEqArgs1 a -> b -> SymBool
f) (f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a
l) (f b -> Rep1 f b
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f b
r)
{-# INLINE genericLiftSymEq #-}

#define CONCRETE_SEQ(type) \
instance SymEq type where \
  l .== r = con $ l == r; \
  {-# INLINE (.==) #-}

#define CONCRETE_SEQ_BV(type) \
instance (KnownNat n, 1 <= n) => SymEq (type n) where \
  l .== r = con $ l == r; \
  {-# INLINE (.==) #-}

#if 1
CONCRETE_SEQ(Bool)
CONCRETE_SEQ(Integer)
CONCRETE_SEQ(Char)
CONCRETE_SEQ(Int)
CONCRETE_SEQ(Int8)
CONCRETE_SEQ(Int16)
CONCRETE_SEQ(Int32)
CONCRETE_SEQ(Int64)
CONCRETE_SEQ(Word)
CONCRETE_SEQ(Word8)
CONCRETE_SEQ(Word16)
CONCRETE_SEQ(Word32)
CONCRETE_SEQ(Word64)
CONCRETE_SEQ(Float)
CONCRETE_SEQ(Double)
CONCRETE_SEQ(B.ByteString)
CONCRETE_SEQ(T.Text)
CONCRETE_SEQ(FPRoundingMode)
CONCRETE_SEQ(Monoid.All)
CONCRETE_SEQ(Monoid.Any)
CONCRETE_SEQ(Ordering)
CONCRETE_SEQ_BV(WordN)
CONCRETE_SEQ_BV(IntN)
#endif

instance (ValidFP eb sb) => SymEq (FP eb sb) where
  FP eb sb
l .== :: FP eb sb -> FP eb sb -> SymBool
.== FP eb sb
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
r
  {-# INLINE (.==) #-}

-- Symbolic types
#define SEQ_SIMPLE(symtype) \
instance SymEq symtype where \
  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r; \
  {-# INLINE (.==) #-}

#define SEQ_BV(symtype) \
instance (KnownNat n, 1 <= n) => SymEq (symtype n) where \
  (symtype l) .== (symtype r) = SymBool $ pevalEqTerm l r; \
  {-# INLINE (.==) #-}

#if 1
SEQ_SIMPLE(SymBool)
SEQ_SIMPLE(SymInteger)
SEQ_SIMPLE(SymFPRoundingMode)
SEQ_BV(SymIntN)
SEQ_BV(SymWordN)
#endif

instance (ValidFP eb sb) => SymEq (SymFP eb sb) where
  (SymFP Term (FP eb sb)
l) .== :: SymFP eb sb -> SymFP eb sb -> SymBool
.== (SymFP Term (FP eb sb)
r) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (FP eb sb)
l Term (FP eb sb)
r
  {-# INLINE (.==) #-}

-- Instances
deriveBuiltins
  (ViaDefault ''SymEq)
  [''SymEq]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(),
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]
deriveBuiltins
  (ViaDefault1 ''SymEq1)
  [''SymEq, ''SymEq1]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

-- ExceptT
instance (SymEq1 m, SymEq e, SymEq a) => SymEq (ExceptT e m a) where
  .== :: ExceptT e m a -> ExceptT e m a -> SymBool
(.==) = ExceptT e m a -> ExceptT e m a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (SymEq1 m, SymEq e) => SymEq1 (ExceptT e m) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> ExceptT e m a -> ExceptT e m b -> SymBool
liftSymEq a -> b -> SymBool
f (ExceptT m (Either e a)
l) (ExceptT m (Either e b)
r) = (Either e a -> Either e b -> SymBool)
-> m (Either e a) -> m (Either e b) -> SymBool
forall a b. (a -> b -> SymBool) -> m a -> m b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq ((a -> b -> SymBool) -> Either e a -> Either e b -> SymBool
forall a b.
(a -> b -> SymBool) -> Either e a -> Either e b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> b -> SymBool
f) m (Either e a)
l m (Either e b)
r
  {-# INLINE liftSymEq #-}

-- MaybeT
instance (SymEq1 m, SymEq a) => SymEq (MaybeT m a) where
  .== :: MaybeT m a -> MaybeT m a -> SymBool
(.==) = MaybeT m a -> MaybeT m a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (SymEq1 m) => SymEq1 (MaybeT m) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> MaybeT m a -> MaybeT m b -> SymBool
liftSymEq a -> b -> SymBool
f (MaybeT m (Maybe a)
l) (MaybeT m (Maybe b)
r) = (Maybe a -> Maybe b -> SymBool)
-> m (Maybe a) -> m (Maybe b) -> SymBool
forall a b. (a -> b -> SymBool) -> m a -> m b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq ((a -> b -> SymBool) -> Maybe a -> Maybe b -> SymBool
forall a b. (a -> b -> SymBool) -> Maybe a -> Maybe b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> b -> SymBool
f) m (Maybe a)
l m (Maybe b)
r
  {-# INLINE liftSymEq #-}

-- Writer
instance (SymEq1 m, SymEq w, SymEq a) => SymEq (WriterLazy.WriterT w m a) where
  .== :: WriterT w m a -> WriterT w m a -> SymBool
(.==) = WriterT w m a -> WriterT w m a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (SymEq1 m, SymEq w) => SymEq1 (WriterLazy.WriterT w m) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> WriterT w m a -> WriterT w m b -> SymBool
liftSymEq a -> b -> SymBool
f (WriterLazy.WriterT m (a, w)
l) (WriterLazy.WriterT m (b, w)
r) =
    ((a, w) -> (b, w) -> SymBool) -> m (a, w) -> m (b, w) -> SymBool
forall a b. (a -> b -> SymBool) -> m a -> m b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq ((a -> b -> SymBool)
-> (w -> w -> SymBool) -> (a, w) -> (b, w) -> SymBool
forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> (a, c) -> (b, d) -> SymBool
forall (f :: * -> * -> *) a b c d.
SymEq2 f =>
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
liftSymEq2 a -> b -> SymBool
f w -> w -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)) m (a, w)
l m (b, w)
r
  {-# INLINE liftSymEq #-}

instance (SymEq1 m, SymEq w, SymEq a) => SymEq (WriterStrict.WriterT w m a) where
  .== :: WriterT w m a -> WriterT w m a -> SymBool
(.==) = WriterT w m a -> WriterT w m a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (SymEq1 m, SymEq w) => SymEq1 (WriterStrict.WriterT w m) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> WriterT w m a -> WriterT w m b -> SymBool
liftSymEq a -> b -> SymBool
f (WriterStrict.WriterT m (a, w)
l) (WriterStrict.WriterT m (b, w)
r) =
    ((a, w) -> (b, w) -> SymBool) -> m (a, w) -> m (b, w) -> SymBool
forall a b. (a -> b -> SymBool) -> m a -> m b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq ((a -> b -> SymBool)
-> (w -> w -> SymBool) -> (a, w) -> (b, w) -> SymBool
forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> (a, c) -> (b, d) -> SymBool
forall (f :: * -> * -> *) a b c d.
SymEq2 f =>
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
liftSymEq2 a -> b -> SymBool
f w -> w -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)) m (a, w)
l m (b, w)
r
  {-# INLINE liftSymEq #-}

-- IdentityT
instance (SymEq1 m, SymEq a) => SymEq (IdentityT m a) where
  .== :: IdentityT m a -> IdentityT m a -> SymBool
(.==) = IdentityT m a -> IdentityT m a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
symEq1
  {-# INLINE (.==) #-}

instance (SymEq1 m) => SymEq1 (IdentityT m) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> IdentityT m a -> IdentityT m b -> SymBool
liftSymEq a -> b -> SymBool
f (IdentityT m a
l) (IdentityT m b
r) = (a -> b -> SymBool) -> m a -> m b -> SymBool
forall a b. (a -> b -> SymBool) -> m a -> m b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> b -> SymBool
f m a
l m b
r
  {-# INLINE liftSymEq #-}

-- Product
deriving via
  (Default (Product l r a))
  instance
    (SymEq (l a), SymEq (r a)) => SymEq (Product l r a)

deriving via
  (Default1 (Product l r))
  instance
    (SymEq1 l, SymEq1 r) => SymEq1 (Product l r)

-- Sum
deriving via
  (Default (Sum l r a))
  instance
    (SymEq (l a), SymEq (r a)) => SymEq (Sum l r a)

deriving via
  (Default1 (Sum l r))
  instance
    (SymEq1 l, SymEq1 r) => SymEq1 (Sum l r)

-- Compose
deriving via
  (Default (Compose f g a))
  instance
    (SymEq (f (g a))) => SymEq (Compose f g a)

instance (SymEq1 f, SymEq1 g) => SymEq1 (Compose f g) where
  liftSymEq :: forall a b.
(a -> b -> SymBool) -> Compose f g a -> Compose f g b -> SymBool
liftSymEq a -> b -> SymBool
f (Compose f (g a)
l) (Compose f (g b)
r) = (g a -> g b -> SymBool) -> f (g a) -> f (g b) -> SymBool
forall a b. (a -> b -> SymBool) -> f a -> f b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq ((a -> b -> SymBool) -> g a -> g b -> SymBool
forall a b. (a -> b -> SymBool) -> g a -> g b -> SymBool
forall (f :: * -> *) a b.
SymEq1 f =>
(a -> b -> SymBool) -> f a -> f b -> SymBool
liftSymEq a -> b -> SymBool
f) f (g a)
l f (g b)
r

-- Const
deriving via (Default (Const a b)) instance (SymEq a) => SymEq (Const a b)

deriving via (Default1 (Const a)) instance (SymEq a) => SymEq1 (Const a)

-- Alt
deriving via (Default (Alt f a)) instance (SymEq (f a)) => SymEq (Alt f a)

deriving via (Default1 (Alt f)) instance (SymEq1 f) => SymEq1 (Alt f)

-- Ap
deriving via (Default (Ap f a)) instance (SymEq (f a)) => SymEq (Ap f a)

deriving via (Default1 (Ap f)) instance (SymEq1 f) => SymEq1 (Ap f)

-- Generic
deriving via (Default (U1 p)) instance SymEq (U1 p)

deriving via (Default (V1 p)) instance SymEq (V1 p)

deriving via
  (Default (K1 i c p))
  instance
    (SymEq c) => SymEq (K1 i c p)

deriving via
  (Default (M1 i c f p))
  instance
    (SymEq (f p)) => SymEq (M1 i c f p)

deriving via
  (Default ((f :+: g) p))
  instance
    (SymEq (f p), SymEq (g p)) => SymEq ((f :+: g) p)

deriving via
  (Default ((f :*: g) p))
  instance
    (SymEq (f p), SymEq (g p)) => SymEq ((f :*: g) p)

deriving via
  (Default (Par1 p))
  instance
    (SymEq p) => SymEq (Par1 p)

deriving via
  (Default (Rec1 f p))
  instance
    (SymEq (f p)) => SymEq (Rec1 f p)

deriving via
  (Default ((f :.: g) p))
  instance
    (SymEq (f (g p))) => SymEq ((f :.: g) p)

instance SymEq2 Either where
  liftSymEq2 :: forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> Either a c -> Either b d -> SymBool
liftSymEq2 a -> b -> SymBool
f c -> d -> SymBool
_ (Left a
l) (Left b
r) = a -> b -> SymBool
f a
l b
r
  liftSymEq2 a -> b -> SymBool
_ c -> d -> SymBool
g (Right c
l) (Right d
r) = c -> d -> SymBool
g c
l d
r
  liftSymEq2 a -> b -> SymBool
_ c -> d -> SymBool
_ Either a c
_ Either b d
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  {-# INLINE liftSymEq2 #-}

instance SymEq2 (,) where
  liftSymEq2 :: forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> (a, c) -> (b, d) -> SymBool
liftSymEq2 a -> b -> SymBool
f c -> d -> SymBool
g (a
l1, c
l2) (b
r1, d
r2) = a -> b -> SymBool
f a
l1 b
r1 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& c -> d -> SymBool
g c
l2 d
r2
  {-# INLINE liftSymEq2 #-}

instance (SymEq a) => SymEq2 ((,,) a) where
  liftSymEq2 :: forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> (a, a, c) -> (a, b, d) -> SymBool
liftSymEq2 a -> b -> SymBool
f c -> d -> SymBool
g (a
l1, a
l2, c
l3) (a
r1, b
r2, d
r3) = a
l1 a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
r1 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a -> b -> SymBool
f a
l2 b
r2 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& c -> d -> SymBool
g c
l3 d
r3
  {-# INLINE liftSymEq2 #-}

instance (SymEq a, SymEq b) => SymEq2 ((,,,) a b) where
  liftSymEq2 :: forall a b c d.
(a -> b -> SymBool)
-> (c -> d -> SymBool) -> (a, b, a, c) -> (a, b, b, d) -> SymBool
liftSymEq2 a -> b -> SymBool
f c -> d -> SymBool
g (a
l1, b
l2, a
l3, c
l4) (a
r1, b
r2, b
r3, d
r4) =
    a
l1 a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
r1 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& b
l2 b -> b -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== b
r2 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a -> b -> SymBool
f a
l3 b
r3 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& c -> d -> SymBool
g c
l4 d
r4
  {-# INLINE liftSymEq2 #-}