{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Unified.Internal.Class.UnifiedSymEq
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Unified.Internal.Class.UnifiedSymEq
  ( UnifiedSymEq (..),
    UnifiedSymEq1 (..),
    UnifiedSymEq2 (..),
    (.==),
    (./=),
    symDistinct,
    liftSymEq,
    symEq1,
    liftSymEq2,
    symEq2,
  )
where

import Control.Monad.Except (ExceptT)
import Control.Monad.Identity (Identity, IdentityT)
import Control.Monad.Trans.Maybe (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.Classes (Eq1 (liftEq), Eq2 (liftEq2), eq1, eq2)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import qualified Data.Text as T
import Data.Type.Bool (If)
import Data.Typeable (Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.SymEq (SymEq, SymEq1, SymEq2)
import qualified Grisette.Internal.Core.Data.Class.SymEq
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
import Grisette.Internal.TH.DeriveUnifiedInterface
  ( deriveFunctorArgUnifiedInterfaces,
    deriveUnifiedInterface1s,
  )
import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym), IsConMode)
import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool))
import Grisette.Unified.Internal.Util (withMode)

-- | Unified `(Grisette.Internal.Core.Data.Class.SymEq..==)`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > a .== b :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Unified.Internal.Class.UnifiedBranching.mrgIf`.
(.==) ::
  forall mode a. (Typeable mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
.== :: forall (mode :: EvalModeTag) a.
(Typeable mode, UnifiedSymEq mode a) =>
a -> a -> GetBool mode
(.==) a
a a
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
Grisette.Internal.Core.Data.Class.SymEq..== a
b)

-- | Unified `(Grisette.Internal.Core.Data.Class.SymEq../=)`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > a ./= b :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Unified.Internal.Class.UnifiedBranching.mrgIf`.
(./=) ::
  forall mode a. (Typeable mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
./= :: forall (mode :: EvalModeTag) a.
(Typeable mode, UnifiedSymEq mode a) =>
a -> a -> GetBool mode
(./=) a
a a
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
Grisette.Internal.Core.Data.Class.SymEq../= a
b)

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symDistinct`.
--
-- Note that you may sometimes need to write type annotations for the result
-- when the mode isn't clear:
--
-- > symDistinct l :: GetBool mode
--
-- One example when it isn't clear is when this is used in unified
-- `Grisette.Unified.Internal.Class.UnifiedBranching.mrgIf`.
symDistinct ::
  forall mode a. (Typeable mode, UnifiedSymEq mode a) => [a] -> GetBool mode
symDistinct :: forall (mode :: EvalModeTag) a.
(Typeable mode, UnifiedSymEq mode a) =>
[a] -> GetBool mode
symDistinct [a]
l =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        [a] -> Bool
forall a. Eq a => [a] -> Bool
Grisette.Internal.Core.Data.Class.SymEq.distinct [a]
l
    )
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        [a] -> SymBool
forall a. SymEq a => [a] -> SymBool
Grisette.Internal.Core.Data.Class.SymEq.symDistinct [a]
l
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.liftSymEq`.
liftSymEq ::
  forall mode f a b.
  (Typeable mode, UnifiedSymEq1 mode f) =>
  (a -> b -> GetBool mode) ->
  f a ->
  f b ->
  GetBool mode
liftSymEq :: forall (mode :: EvalModeTag) (f :: * -> *) a b.
(Typeable mode, UnifiedSymEq1 mode f) =>
(a -> b -> GetBool mode) -> f a -> f b -> GetBool mode
liftSymEq a -> b -> GetBool mode
f f a
a f b
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> f a -> f b -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
a -> b -> GetBool mode
f f a
a f b
b)
    ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> 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
Grisette.Internal.Core.Data.Class.SymEq.liftSymEq a -> b -> SymBool
a -> b -> GetBool mode
f f a
a f b
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symEq1`.
symEq1 ::
  forall mode f a.
  (Typeable mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) =>
  f a ->
  f a ->
  GetBool mode
symEq1 :: forall (mode :: EvalModeTag) (f :: * -> *) a.
(Typeable mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) =>
f a -> f a -> GetBool mode
symEq1 f a
a f a
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a f a -> f a -> Bool
f a -> f a -> GetBool mode
If (IsConMode mode) (Eq a) (SymEq a) => f a -> f a -> GetBool mode
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 f a
a f a
b)
    ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          f a -> f a -> SymBool
forall a (f :: * -> *).
(SymEq a, SymEq1 f) =>
f a -> f a -> SymBool
Grisette.Internal.Core.Data.Class.SymEq.symEq1 f a
a f a
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.liftSymEq2`.
liftSymEq2 ::
  forall mode f a b c d.
  (Typeable mode, UnifiedSymEq2 mode f) =>
  (a -> b -> GetBool mode) ->
  (c -> d -> GetBool mode) ->
  f a c ->
  f b d ->
  GetBool mode
liftSymEq2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b c d.
(Typeable mode, UnifiedSymEq2 mode f) =>
(a -> b -> GetBool mode)
-> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode
liftSymEq2 a -> b -> GetBool mode
f c -> d -> GetBool mode
a f a c
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => f b d -> GetBool mode)
 -> f b d -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) =>
    f b d -> GetBool mode)
-> f b d
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
forall a b c d.
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
forall (f :: * -> * -> *) a b c d.
Eq2 f =>
(a -> b -> Bool) -> (c -> d -> Bool) -> f a c -> f b d -> Bool
liftEq2 a -> b -> Bool
a -> b -> GetBool mode
f c -> d -> Bool
c -> d -> GetBool mode
a f a c
b)
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => f b d -> GetBool mode)
 -> f b d -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) =>
    f b d -> GetBool mode)
-> f b d
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        (a -> b -> SymBool)
-> (c -> d -> SymBool) -> f a c -> f b d -> 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
Grisette.Internal.Core.Data.Class.SymEq.liftSymEq2 a -> b -> SymBool
a -> b -> GetBool mode
f c -> d -> SymBool
c -> d -> GetBool mode
a f a c
b
    )

-- | Unified `Grisette.Internal.Core.Data.Class.SymEq.symEq2`.
symEq2 ::
  forall mode f a b.
  ( Typeable mode,
    UnifiedSymEq mode a,
    UnifiedSymEq mode b,
    UnifiedSymEq2 mode f
  ) =>
  f a b ->
  f a b ->
  GetBool mode
symEq2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b.
(Typeable mode, UnifiedSymEq mode a, UnifiedSymEq mode b,
 UnifiedSymEq2 mode f) =>
f a b -> f a b -> GetBool mode
symEq2 f a b
a f a b
b =
  forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b f a b -> f a b -> Bool
f a b -> f a b -> GetBool mode
If (IsConMode mode) (Eq b) (SymEq b) =>
f a b -> f a b -> GetBool mode
forall (f :: * -> * -> *) a b.
(Eq2 f, Eq a, Eq b) =>
f a b -> f a b -> Bool
eq2 f a b
a f a b
b
    )
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymEq2 mode f =>
(If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 @mode @f ((If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq2 f) (SymEq2 f) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq a) (SymEq a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b ((If (IsConMode mode) (Eq b) (SymEq b) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Eq b) (SymEq b) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$
            f a b -> f a b -> SymBool
forall a b (f :: * -> * -> *).
(SymEq a, SymEq b, SymEq2 f) =>
f a b -> f a b -> SymBool
Grisette.Internal.Core.Data.Class.SymEq.symEq2 f a b
a f a b
b
    )

-- | A class that provides unified equality comparison.
--
-- We use this type class to help resolve the constraints for `Eq` and `SymEq`.
class UnifiedSymEq mode a where
  withBaseSymEq :: ((If (IsConMode mode) (Eq a) (SymEq a)) => r) -> r

-- | A class that provides unified lifting of equality comparison.
--
-- We use this type class to help resolve the constraints for `Eq1` and
-- `SymEq1`.
class
  (forall a. (UnifiedSymEq mode a) => UnifiedSymEq mode (f a)) =>
  UnifiedSymEq1 mode f
  where
  withBaseSymEq1 :: ((If (IsConMode mode) (Eq1 f) (SymEq1 f)) => r) -> r

-- | A class that provides unified lifting of equality comparison.
--
-- We use this type class to help resolve the constraints for `Eq2` and
-- `SymEq2`.
class
  (forall a. (UnifiedSymEq mode a) => UnifiedSymEq1 mode (f a)) =>
  UnifiedSymEq2 mode f
  where
  withBaseSymEq2 :: ((If (IsConMode mode) (Eq2 f) (SymEq2 f)) => r) -> r

instance
  {-# INCOHERENT #-}
  (Typeable mode, If (IsConMode mode) (Eq a) (SymEq a)) =>
  UnifiedSymEq mode a
  where
  withBaseSymEq :: forall r. (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq If (IsConMode mode) (Eq a) (SymEq a) => r
r = r
If (IsConMode mode) (Eq a) (SymEq a) => r
r
  {-# INLINE withBaseSymEq #-}

instance
  {-# INCOHERENT #-}
  ( Typeable mode,
    If (IsConMode mode) (Eq1 f) (SymEq1 f),
    forall a. (UnifiedSymEq mode a) => UnifiedSymEq mode (f a)
  ) =>
  UnifiedSymEq1 mode f
  where
  withBaseSymEq1 :: forall r. (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 If (IsConMode mode) (Eq1 f) (SymEq1 f) => r
r = r
If (IsConMode mode) (Eq1 f) (SymEq1 f) => r
r
  {-# INLINE withBaseSymEq1 #-}

instance
  {-# INCOHERENT #-}
  ( Typeable mode,
    If (IsConMode mode) (Eq2 f) (SymEq2 f),
    forall a. (UnifiedSymEq mode a) => UnifiedSymEq1 mode (f a)
  ) =>
  UnifiedSymEq2 mode f
  where
  withBaseSymEq2 :: forall r. (If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
withBaseSymEq2 If (IsConMode mode) (Eq2 f) (SymEq2 f) => r
r = r
If (IsConMode mode) (Eq2 f) (SymEq2 f) => r
r
  {-# INLINE withBaseSymEq2 #-}

instance (UnifiedSymEq 'Sym v) => UnifiedSymEq 'Sym (Union v) where
  withBaseSymEq :: forall r.
(If (IsConMode 'Sym) (Eq (Union v)) (SymEq (Union v)) => r) -> r
withBaseSymEq If (IsConMode 'Sym) (Eq (Union v)) (SymEq (Union v)) => r
r = forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @'Sym @v r
If (IsConMode 'Sym) (Eq v) (SymEq v) => r
If (IsConMode 'Sym) (Eq (Union v)) (SymEq (Union v)) => r
r
  {-# INLINE withBaseSymEq #-}

deriveFunctorArgUnifiedInterfaces
  ''UnifiedSymEq
  'withBaseSymEq
  ''UnifiedSymEq1
  'withBaseSymEq1
  [ ''Bool,
    ''Integer,
    ''Char,
    ''Int,
    ''Int8,
    ''Int16,
    ''Int32,
    ''Int64,
    ''Word,
    ''Word8,
    ''Word16,
    ''Word32,
    ''Word64,
    ''Float,
    ''Double,
    ''B.ByteString,
    ''T.Text,
    ''FPRoundingMode,
    ''WordN,
    ''IntN,
    ''[],
    ''Maybe,
    ''Either,
    ''(),
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''ExceptT,
    ''MaybeT,
    ''WriterLazy.WriterT,
    ''WriterStrict.WriterT,
    ''Identity
  ]

deriveUnifiedInterface1s
  ''UnifiedSymEq
  'withBaseSymEq
  ''UnifiedSymEq1
  'withBaseSymEq1
  [ ''[],
    ''Maybe,
    ''Either,
    ''(,),
    ''ExceptT,
    ''MaybeT,
    ''WriterLazy.WriterT,
    ''WriterStrict.WriterT,
    ''Identity
  ]

-- Sum
instance
  ( Typeable mode,
    UnifiedSymEq1 mode f,
    UnifiedSymEq1 mode g,
    UnifiedSymEq mode a
  ) =>
  UnifiedSymEq mode (Sum f g a)
  where
  withBaseSymEq :: forall r.
(If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r)
-> r
withBaseSymEq If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g ((If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r)
-> (If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r
      )
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g ((If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r)
-> (If (IsConMode mode) (Eq1 g) (SymEq1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (Sum f g a)) (SymEq (Sum f g a)) => r
r
      )
  {-# INLINE withBaseSymEq #-}

instance
  (Typeable mode, UnifiedSymEq1 mode f, UnifiedSymEq1 mode g) =>
  UnifiedSymEq1 mode (Sum f g)
  where
  withBaseSymEq1 :: forall r.
(If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r) -> r
withBaseSymEq1 If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g r
If (IsConMode mode) (Eq1 g) (SymEq1 g) => r
If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @f ((If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r)
-> (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @g r
If (IsConMode mode) (Eq1 g) (SymEq1 g) => r
If (IsConMode mode) (Eq1 (Sum f g)) (SymEq1 (Sum f g)) => r
r)
  {-# INLINE withBaseSymEq1 #-}

-- IdentityT
instance
  (Typeable mode, UnifiedSymEq1 mode m, UnifiedSymEq mode a) =>
  UnifiedSymEq mode (IdentityT m a)
  where
  withBaseSymEq :: forall r.
(If
   (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
 r)
-> r
withBaseSymEq If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m ((If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r)
-> (If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m ((If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r)
-> (If (IsConMode mode) (Eq1 m) (SymEq1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq (IdentityT m a)) (SymEq (IdentityT m a)) =>
r
r)
  {-# INLINE withBaseSymEq #-}

instance
  (Typeable mode, UnifiedSymEq1 mode m) =>
  UnifiedSymEq1 mode (IdentityT m)
  where
  withBaseSymEq1 :: forall r.
(If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) =>
 r)
-> r
withBaseSymEq1 If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m r
If (IsConMode mode) (Eq1 m) (SymEq1 m) => r
If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r) (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymEq1 mode f =>
(If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
withBaseSymEq1 @mode @m r
If (IsConMode mode) (Eq1 m) (SymEq1 m) => r
If (IsConMode mode) (Eq1 (IdentityT m)) (SymEq1 (IdentityT m)) => r
r)
  {-# INLINE withBaseSymEq1 #-}

instance (Typeable mode, ValidFP eb sb) => UnifiedSymEq mode (FP eb sb) where
  withBaseSymEq :: forall r.
(If (IsConMode mode) (Eq (FP eb sb)) (SymEq (FP eb sb)) => r) -> r
withBaseSymEq If (IsConMode mode) (Eq (FP eb sb)) (SymEq (FP eb sb)) => r
r = forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode r
(mode ~ 'Con) => r
If (IsConMode mode) (Eq (FP eb sb)) (SymEq (FP eb sb)) => r
r r
(mode ~ 'Sym) => r
If (IsConMode mode) (Eq (FP eb sb)) (SymEq (FP eb sb)) => r
r
  {-# INLINE withBaseSymEq #-}

instance (Typeable mode) => UnifiedSymEq2 mode Either where
  withBaseSymEq2 :: forall r.
(If (IsConMode mode) (Eq2 Either) (SymEq2 Either) => r) -> r
withBaseSymEq2 If (IsConMode mode) (Eq2 Either) (SymEq2 Either) => r
r = forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode r
(mode ~ 'Con) => r
If (IsConMode mode) (Eq2 Either) (SymEq2 Either) => r
r r
(mode ~ 'Sym) => r
If (IsConMode mode) (Eq2 Either) (SymEq2 Either) => r
r
  {-# INLINE withBaseSymEq2 #-}

instance (Typeable mode) => UnifiedSymEq2 mode (,) where
  withBaseSymEq2 :: forall r. (If (IsConMode mode) (Eq2 (,)) (SymEq2 (,)) => r) -> r
withBaseSymEq2 If (IsConMode mode) (Eq2 (,)) (SymEq2 (,)) => r
r = forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode r
(mode ~ 'Con) => r
If (IsConMode mode) (Eq2 (,)) (SymEq2 (,)) => r
r r
(mode ~ 'Sym) => r
If (IsConMode mode) (Eq2 (,)) (SymEq2 (,)) => r
r
  {-# INLINE withBaseSymEq2 #-}

#if MIN_VERSION_base(4,16,0)
deriveUnifiedInterface1s
  ''UnifiedSymEq
  'withBaseSymEq
  ''UnifiedSymEq1
  'withBaseSymEq1
  [ ''(,,),
    ''(,,,)
  ]

instance (Typeable mode, UnifiedSymEq mode a) =>
  UnifiedSymEq2 mode ((,,) a) where
  withBaseSymEq2 :: forall r.
(If (IsConMode mode) (Eq2 ((,,) a)) (SymEq2 ((,,) a)) => r) -> r
withBaseSymEq2 If (IsConMode mode) (Eq2 ((,,) a)) (SymEq2 ((,,) a)) => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq2 ((,,) a)) (SymEq2 ((,,) a)) => r
r) (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a r
If (IsConMode mode) (Eq a) (SymEq a) => r
If (IsConMode mode) (Eq2 ((,,) a)) (SymEq2 ((,,) a)) => r
r)
  {-# INLINE withBaseSymEq2 #-}

instance
  (Typeable mode, UnifiedSymEq mode a, UnifiedSymEq mode b) =>
  UnifiedSymEq2 mode ((,,,) a b)
  where
  withBaseSymEq2 :: forall r.
(If (IsConMode mode) (Eq2 ((,,,) a b)) (SymEq2 ((,,,) a b)) => r)
-> r
withBaseSymEq2 If (IsConMode mode) (Eq2 ((,,,) a b)) (SymEq2 ((,,,) a b)) => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => r) -> r)
-> (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b r
If (IsConMode mode) (Eq b) (SymEq b) => r
If (IsConMode mode) (Eq2 ((,,,) a b)) (SymEq2 ((,,,) a b)) => r
r)
      (forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @a ((If (IsConMode mode) (Eq a) (SymEq a) => r) -> r)
-> (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymEq mode a =>
(If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
withBaseSymEq @mode @b r
If (IsConMode mode) (Eq b) (SymEq b) => r
If (IsConMode mode) (Eq2 ((,,,) a b)) (SymEq2 ((,,,) a b)) => r
r)
  {-# INLINE withBaseSymEq2 #-}
#endif