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

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

-- |
-- Module      :   Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd
-- 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.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd
  ( (.<=),
    (.<),
    (.>=),
    (.>),
    symMax,
    symMin,
    mrgMax,
    mrgMin,
  )
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 (Ord1, Ord2)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Ratio (Ratio)
import qualified Data.Text as T
import Data.Type.Bool (If)
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.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.TryMerge (tryMerge)
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd
  ( SymOrd,
    SymOrd1,
    SymOrd2,
  )
import qualified Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd as SymOrd
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedITEOp
  ( UnifiedITEOp (withBaseITEOp),
  )
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSimpleMergeable
  ( UnifiedBranching (withBaseBranching),
  )
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymOrd
  ( UnifiedSymOrd (withBaseSymOrd),
    UnifiedSymOrd1 (withBaseSymOrd1),
    UnifiedSymOrd2 (withBaseSymOrd2),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode)
import Grisette.Internal.TH.Derivation.Common
  ( DeriveConfig (bitSizePositions, fpBitSizePositions),
  )
import Grisette.Internal.TH.Derivation.Derive (derive, deriveWith)
import Grisette.Internal.Unified.EvalModeTag
  ( EvalModeTag (S),
    IsConMode,
  )
import Grisette.Internal.Unified.UnifiedBool (GetBool)
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- | Unified `(Grisette.Internal.Core.Data.Class.SymOrd..<=)`.
--
-- 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.Internal.Unified.Class.UnifiedBranching.mrgIf`.
(.<=) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
.<= :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
(.<=) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
SymOrd..<= a
b)
{-# INLINE (.<=) #-}

infix 4 .<=

-- | Unified `(Grisette.Internal.Core.Data.Class.SymOrd..<)`.
(.<) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
.< :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
(.<) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
SymOrd..< a
b)
{-# INLINE (.<) #-}

infix 4 .<

-- | Unified `(Grisette.Internal.Core.Data.Class.SymOrd..>=)`.
(.>=) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
.>= :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
(.>=) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
SymOrd..>= a
b)
{-# INLINE (.>=) #-}

infix 4 .>=

-- | Unified `(Grisette.Internal.Core.Data.Class.SymOrd..>)`.
(.>) ::
  forall mode a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
.> :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetBool mode
(.>) a
a a
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b)
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
 -> GetBool mode)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => GetBool mode)
-> GetBool mode
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
SymOrd..> a
b)
{-# INLINE (.>) #-}

infix 4 .>

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symMax`.
symMax ::
  forall mode a.
  (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) =>
  a ->
  a ->
  a
symMax :: forall (mode :: EvalModeTag) a.
(UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) =>
a -> a -> a
symMax a
x a
y =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Ord a => a -> a -> a
max a
x a
y)
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @a
          a -> a -> a
If (IsConMode mode) (() :: Constraint) (ITEOp a) => a -> a -> a
forall a. (SymOrd a, ITEOp a) => a -> a -> a
SymOrd.symMax
          a
x
          a
y
    )
{-# INLINE symMax #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symMin`.
symMin ::
  forall mode a.
  (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) =>
  a ->
  a ->
  a
symMin :: forall (mode :: EvalModeTag) a.
(UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) =>
a -> a -> a
symMin a
x a
y =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Ord a => a -> a -> a
min a
x a
y)
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => a) -> a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @a
          a -> a -> a
If (IsConMode mode) (() :: Constraint) (ITEOp a) => a -> a -> a
forall a. (SymOrd a, ITEOp a) => a -> a -> a
SymOrd.symMin
          a
x
          a
y
    )
{-# INLINE symMin #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.mrgMax`.
mrgMax ::
  forall mode a m.
  ( UnifiedSymOrd mode a,
    UnifiedBranching mode m,
    DecideEvalMode mode,
    Applicative m,
    Mergeable a
  ) =>
  a ->
  a ->
  m a
mrgMax :: forall (mode :: EvalModeTag) a (m :: * -> *).
(UnifiedSymOrd mode a, UnifiedBranching mode m,
 DecideEvalMode mode, Applicative m, Mergeable a) =>
a -> a -> m a
mrgMax a
x a
y =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m ((If (IsConMode mode) (TryMerge m) (SymBranching m) => m a) -> m a)
-> (If (IsConMode mode) (TryMerge m) (SymBranching m) => m a)
-> m a
forall a b. (a -> b) -> a -> b
$
          m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
            a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$
              a -> a -> a
forall a. Ord a => a -> a -> a
max a
x a
y
    )
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m ((If (IsConMode mode) (TryMerge m) (SymBranching m) => m a) -> m a)
-> (If (IsConMode mode) (TryMerge m) (SymBranching m) => m a)
-> m a
forall a b. (a -> b) -> a -> b
$
          a -> a -> m a
forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
SymOrd.mrgMax a
x a
y
    )
{-# INLINE mrgMax #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.mrgMin`.
mrgMin ::
  forall mode a m.
  ( UnifiedSymOrd mode a,
    UnifiedBranching mode m,
    DecideEvalMode mode,
    Applicative m,
    Mergeable a
  ) =>
  a ->
  a ->
  m a
mrgMin :: forall (mode :: EvalModeTag) a (m :: * -> *).
(UnifiedSymOrd mode a, UnifiedBranching mode m,
 DecideEvalMode mode, Applicative m, Mergeable a) =>
a -> a -> m a
mrgMin a
x a
y =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m ((If (IsConMode mode) (TryMerge m) (SymBranching m) => m a) -> m a)
-> (If (IsConMode mode) (TryMerge m) (SymBranching m) => m a)
-> m a
forall a b. (a -> b) -> a -> b
$
          m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
            a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$
              a -> a -> a
forall a. Ord a => a -> a -> a
min a
x a
y
    )
    ( forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a ((If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a)
-> (If (IsConMode mode) (Ord a) (SymOrd a) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m ((If (IsConMode mode) (TryMerge m) (SymBranching m) => m a) -> m a)
-> (If (IsConMode mode) (TryMerge m) (SymBranching m) => m a)
-> m a
forall a b. (a -> b) -> a -> b
$
          a -> a -> m a
forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
SymOrd.mrgMin a
x a
y
    )
{-# INLINE mrgMin #-}

instance
  {-# INCOHERENT #-}
  (DecideEvalMode mode, If (IsConMode mode) (Ord a) (SymOrd a)) =>
  UnifiedSymOrd mode a
  where
  withBaseSymOrd :: forall r. (If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd If (IsConMode mode) (Ord a) (SymOrd a) => r
r = r
If (IsConMode mode) (Ord a) (SymOrd a) => r
r
  {-# INLINE withBaseSymOrd #-}

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    If (IsConMode mode) (Ord1 f) (SymOrd1 f),
    forall a. (UnifiedSymOrd mode a) => UnifiedSymOrd mode (f a)
  ) =>
  UnifiedSymOrd1 mode f
  where
  withBaseSymOrd1 :: forall r. (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r
r = r
If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r
r
  {-# INLINE withBaseSymOrd1 #-}

instance
  {-# INCOHERENT #-}
  ( DecideEvalMode mode,
    If (IsConMode mode) (Ord2 f) (SymOrd2 f),
    forall a. (UnifiedSymOrd mode a) => UnifiedSymOrd1 mode (f a)
  ) =>
  UnifiedSymOrd2 mode f
  where
  withBaseSymOrd2 :: forall r. (If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
withBaseSymOrd2 If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r
r = r
If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r
r
  {-# INLINE withBaseSymOrd2 #-}

instance (UnifiedSymOrd 'S v) => UnifiedSymOrd 'S (Union v) where
  withBaseSymOrd :: forall r.
(If (IsConMode 'S) (Ord (Union v)) (SymOrd (Union v)) => r) -> r
withBaseSymOrd If (IsConMode 'S) (Ord (Union v)) (SymOrd (Union v)) => r
r = forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @'S @v r
If (IsConMode 'S) (Ord v) (SymOrd v) => r
If (IsConMode 'S) (Ord (Union v)) (SymOrd (Union v)) => r
r
  {-# INLINE withBaseSymOrd #-}

derive
  [ ''Either,
    ''(,)
  ]
  [''UnifiedSymOrd, ''UnifiedSymOrd1, ''UnifiedSymOrd2]

derive
  [ ''[],
    ''Maybe,
    ''Identity,
    ''ExceptT,
    ''MaybeT,
    ''WriterLazy.WriterT,
    ''WriterStrict.WriterT
  ]
  [''UnifiedSymOrd, ''UnifiedSymOrd1]

derive
  [ ''Bool,
    ''Integer,
    ''Char,
    ''Int,
    ''Int8,
    ''Int16,
    ''Int32,
    ''Int64,
    ''Word,
    ''Word8,
    ''Word16,
    ''Word32,
    ''Word64,
    ''Float,
    ''Double,
    ''B.ByteString,
    ''T.Text,
    ''FPRoundingMode,
    ''(),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions
  ]
  [''UnifiedSymOrd]

#if MIN_VERSION_base(4,16,0)
derive
  [ ''(,,),
    ''(,,,)
  ]
  [''UnifiedSymOrd, ''UnifiedSymOrd1, ''UnifiedSymOrd2]
#else
derive
  [ ''(,,),
    ''(,,,)
  ]
  [''UnifiedSymOrd]
#endif

deriveWith
  (mempty {bitSizePositions = [0]})
  [''WordN, ''IntN]
  [''UnifiedSymOrd]

deriveWith
  (mempty {fpBitSizePositions = [(0, 1)]})
  [''FP]
  [''UnifiedSymOrd]

instance
  (DecideEvalMode mode, UnifiedSymOrd mode a, Integral a) =>
  UnifiedSymOrd mode (Ratio a)
  where
  withBaseSymOrd :: forall r.
(If (IsConMode mode) (Ord (Ratio a)) (SymOrd (Ratio a)) => r) -> r
withBaseSymOrd If (IsConMode mode) (Ord (Ratio a)) (SymOrd (Ratio a)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If (IsConMode mode) (Ord (Ratio a)) (SymOrd (Ratio a)) => r
r) (forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If (IsConMode mode) (Ord (Ratio a)) (SymOrd (Ratio a)) => r
r)
  {-# INLINE withBaseSymOrd #-}

-- Sum
instance
  ( DecideEvalMode mode,
    UnifiedSymOrd1 mode f,
    UnifiedSymOrd1 mode g,
    UnifiedSymOrd mode a
  ) =>
  UnifiedSymOrd mode (Sum f g a)
  where
  withBaseSymOrd :: forall r.
(If (IsConMode mode) (Ord (Sum f g a)) (SymOrd (Sum f g a)) => r)
-> r
withBaseSymOrd If (IsConMode mode) (Ord (Sum f g a)) (SymOrd (Sum f g a)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @f ((If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @g ((If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r) -> r)
-> (If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If (IsConMode mode) (Ord (Sum f g a)) (SymOrd (Sum f g a)) => r
r
      )
      ( forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @f ((If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @g ((If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r) -> r)
-> (If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r) -> r
forall a b. (a -> b) -> a -> b
$
            forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If (IsConMode mode) (Ord (Sum f g a)) (SymOrd (Sum f g a)) => r
r
      )
  {-# INLINE withBaseSymOrd #-}

instance
  (DecideEvalMode mode, UnifiedSymOrd1 mode f, UnifiedSymOrd1 mode g) =>
  UnifiedSymOrd1 mode (Sum f g)
  where
  withBaseSymOrd1 :: forall r.
(If (IsConMode mode) (Ord1 (Sum f g)) (SymOrd1 (Sum f g)) => r)
-> r
withBaseSymOrd1 If (IsConMode mode) (Ord1 (Sum f g)) (SymOrd1 (Sum f g)) => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @f ((If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @g r
If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r
If (IsConMode mode) (Ord1 (Sum f g)) (SymOrd1 (Sum f g)) => r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @f ((If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @g r
If (IsConMode mode) (Ord1 g) (SymOrd1 g) => r
If (IsConMode mode) (Ord1 (Sum f g)) (SymOrd1 (Sum f g)) => r
r)
  {-# INLINE withBaseSymOrd1 #-}

-- IdentityT
instance
  (DecideEvalMode mode, UnifiedSymOrd1 mode m, UnifiedSymOrd mode a) =>
  UnifiedSymOrd mode (IdentityT m a)
  where
  withBaseSymOrd :: forall r.
(If
   (IsConMode mode) (Ord (IdentityT m a)) (SymOrd (IdentityT m a)) =>
 r)
-> r
withBaseSymOrd If
  (IsConMode mode) (Ord (IdentityT m a)) (SymOrd (IdentityT m a)) =>
r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @m ((If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r) -> r)
-> (If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If
  (IsConMode mode) (Ord (IdentityT m a)) (SymOrd (IdentityT m a)) =>
r
r)
      (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @m ((If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r) -> r)
-> (If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (mode :: EvalModeTag) a r.
UnifiedSymOrd mode a =>
(If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
withBaseSymOrd @mode @a r
If (IsConMode mode) (Ord a) (SymOrd a) => r
If
  (IsConMode mode) (Ord (IdentityT m a)) (SymOrd (IdentityT m a)) =>
r
r)
  {-# INLINE withBaseSymOrd #-}

instance
  (DecideEvalMode mode, UnifiedSymOrd1 mode m) =>
  UnifiedSymOrd1 mode (IdentityT m)
  where
  withBaseSymOrd1 :: forall r.
(If
   (IsConMode mode) (Ord1 (IdentityT m)) (SymOrd1 (IdentityT m)) =>
 r)
-> r
withBaseSymOrd1 If (IsConMode mode) (Ord1 (IdentityT m)) (SymOrd1 (IdentityT m)) =>
r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @m r
If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r
If (IsConMode mode) (Ord1 (IdentityT m)) (SymOrd1 (IdentityT m)) =>
r
r) (forall (mode :: EvalModeTag) (f :: * -> *) r.
UnifiedSymOrd1 mode f =>
(If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
withBaseSymOrd1 @mode @m r
If (IsConMode mode) (Ord1 m) (SymOrd1 m) => r
If (IsConMode mode) (Ord1 (IdentityT m)) (SymOrd1 (IdentityT m)) =>
r
r)
  {-# INLINE withBaseSymOrd1 #-}