{-# 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
  ( (.<=),
    (.<),
    (.>=),
    (.>),
    symCompare,
    liftSymCompare,
    symCompare1,
    liftSymCompare2,
    symCompare2,
    symMax,
    symMin,
    mrgMax,
    mrgMin,
  )
where

import Control.Monad.Except (ExceptT)
import Control.Monad.Identity (Identity (runIdentity), 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 (liftCompare),
    Ord2 (liftCompare2),
    compare1,
    compare2,
  )
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.BaseMonad (BaseMonad)
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 (.<=) #-}

-- | 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 (.<) #-}

-- | 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 (.>=) #-}

-- | 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 (.>) #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symCompare`.
symCompare ::
  forall mode a ctx.
  (DecideEvalMode mode, UnifiedSymOrd mode a, Monad ctx) =>
  a ->
  a ->
  BaseMonad mode Ordering
symCompare :: forall (mode :: EvalModeTag) a (ctx :: * -> *).
(DecideEvalMode mode, UnifiedSymOrd mode a, Monad ctx) =>
a -> a -> BaseMonad mode Ordering
symCompare 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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$ Ordering -> Identity Ordering
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Identity Ordering) -> Ordering -> Identity Ordering
forall a b. (a -> b) -> a -> b
$ a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare 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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
        a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
SymOrd.symCompare a
x a
y
    )
{-# INLINE symCompare #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.liftSymCompare`.
liftSymCompare ::
  forall mode f a b.
  (DecideEvalMode mode, UnifiedSymOrd1 mode f) =>
  (a -> b -> BaseMonad mode Ordering) ->
  f a ->
  f b ->
  BaseMonad mode Ordering
liftSymCompare :: forall (mode :: EvalModeTag) (f :: * -> *) a b.
(DecideEvalMode mode, UnifiedSymOrd1 mode f) =>
(a -> b -> BaseMonad mode Ordering)
-> f a -> f b -> BaseMonad mode Ordering
liftSymCompare a -> b -> BaseMonad mode Ordering
f f a
a f b
b =
  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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
        Ordering -> Identity Ordering
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Identity Ordering) -> Ordering -> Identity Ordering
forall a b. (a -> b) -> a -> b
$
          (a -> b -> Ordering) -> f a -> f b -> Ordering
forall a b. (a -> b -> Ordering) -> f a -> f b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare (\a
x b
y -> Identity Ordering -> Ordering
forall a. Identity a -> a
runIdentity (Identity Ordering -> Ordering) -> Identity Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ a -> b -> BaseMonad mode Ordering
f a
x b
y) f a
a f b
b
    )
    ( 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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
        (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
forall (f :: * -> *) a b.
SymOrd1 f =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
SymOrd.liftSymCompare a -> b -> Union Ordering
a -> b -> BaseMonad mode Ordering
f f a
a f b
b
    )
{-# INLINE liftSymCompare #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symCompare1`.
symCompare1 ::
  forall mode f a.
  (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) =>
  f a ->
  f a ->
  BaseMonad mode Ordering
symCompare1 :: forall (mode :: EvalModeTag) (f :: * -> *) a.
(DecideEvalMode mode, UnifiedSymOrd mode a,
 UnifiedSymOrd1 mode f) =>
f a -> f a -> BaseMonad mode Ordering
symCompare1 f a
a f a
b =
  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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 ((If (IsConMode mode) (Ord a) (SymOrd a) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$ Ordering -> Identity Ordering
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Identity Ordering) -> Ordering -> Identity Ordering
forall a b. (a -> b) -> a -> b
$ f a -> f a -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1 f a
a f a
b)
    ( 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) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 ((If (IsConMode mode) (Ord a) (SymOrd a) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
          f a -> f a -> Union Ordering
forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
SymOrd.symCompare1 f a
a f a
b
    )
{-# INLINE symCompare1 #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.liftSymCompare2`.
liftSymCompare2 ::
  forall mode f a b c d.
  (DecideEvalMode mode, UnifiedSymOrd2 mode f) =>
  (a -> b -> BaseMonad mode Ordering) ->
  (c -> d -> BaseMonad mode Ordering) ->
  f a c ->
  f b d ->
  BaseMonad mode Ordering
liftSymCompare2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b c d.
(DecideEvalMode mode, UnifiedSymOrd2 mode f) =>
(a -> b -> BaseMonad mode Ordering)
-> (c -> d -> BaseMonad mode Ordering)
-> f a c
-> f b d
-> BaseMonad mode Ordering
liftSymCompare2 a -> b -> BaseMonad mode Ordering
f c -> d -> BaseMonad mode Ordering
g f a c
a f b d
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymOrd2 mode f =>
(If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
withBaseSymOrd2 @mode @f ((If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
        Ordering -> Identity Ordering
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Identity Ordering) -> Ordering -> Identity Ordering
forall a b. (a -> b) -> a -> b
$
          (a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
forall a b c d.
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
forall (f :: * -> * -> *) a b c d.
Ord2 f =>
(a -> b -> Ordering)
-> (c -> d -> Ordering) -> f a c -> f b d -> Ordering
liftCompare2
            (\a
x b
y -> Identity Ordering -> Ordering
forall a. Identity a -> a
runIdentity (Identity Ordering -> Ordering) -> Identity Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ a -> b -> BaseMonad mode Ordering
f a
x b
y)
            (\c
x d
y -> Identity Ordering -> Ordering
forall a. Identity a -> a
runIdentity (Identity Ordering -> Ordering) -> Identity Ordering -> Ordering
forall a b. (a -> b) -> a -> b
$ c -> d -> BaseMonad mode Ordering
g c
x d
y)
            f a c
a
            f b d
b
    )
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymOrd2 mode f =>
(If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
withBaseSymOrd2 @mode @f ((If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
        (a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
forall (f :: * -> * -> *) a b c d.
SymOrd2 f =>
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
SymOrd.liftSymCompare2 a -> b -> Union Ordering
a -> b -> BaseMonad mode Ordering
f c -> d -> Union Ordering
c -> d -> BaseMonad mode Ordering
g f a c
a f b d
b
    )
{-# INLINE liftSymCompare2 #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symCompare2`.
symCompare2 ::
  forall mode f a b.
  ( DecideEvalMode mode,
    UnifiedSymOrd mode a,
    UnifiedSymOrd mode b,
    UnifiedSymOrd2 mode f
  ) =>
  f a b ->
  f a b ->
  BaseMonad mode Ordering
symCompare2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b.
(DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b,
 UnifiedSymOrd2 mode f) =>
f a b -> f a b -> BaseMonad mode Ordering
symCompare2 f a b
a f a b
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymOrd2 mode f =>
(If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
withBaseSymOrd2 @mode @f ((If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 ((If (IsConMode mode) (Ord a) (SymOrd a) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 @b ((If (IsConMode mode) (Ord b) (SymOrd b) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord b) (SymOrd b) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
            Ordering -> Identity Ordering
forall a. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ordering -> Identity Ordering) -> Ordering -> Identity Ordering
forall a b. (a -> b) -> a -> b
$
              f a b -> f a b -> Ordering
forall (f :: * -> * -> *) a b.
(Ord2 f, Ord a, Ord b) =>
f a b -> f a b -> Ordering
compare2 f a b
a f a b
b
    )
    ( forall (mode :: EvalModeTag) (f :: * -> * -> *) r.
UnifiedSymOrd2 mode f =>
(If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
withBaseSymOrd2 @mode @f ((If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 ((If (IsConMode mode) (Ord a) (SymOrd a) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
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 @b ((If (IsConMode mode) (Ord b) (SymOrd b) =>
  BaseMonad mode Ordering)
 -> BaseMonad mode Ordering)
-> (If (IsConMode mode) (Ord b) (SymOrd b) =>
    BaseMonad mode Ordering)
-> BaseMonad mode Ordering
forall a b. (a -> b) -> a -> b
$
            f a b -> f a b -> Union Ordering
forall (f :: * -> * -> *) a b.
(SymOrd2 f, SymOrd a, SymOrd b) =>
f a b -> f a b -> Union Ordering
SymOrd.symCompare2 f a b
a f a b
b
    )
{-# INLINE symCompare2 #-}

-- | 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 #-}