{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Unified.UnifiedData
-- 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.Unified.UnifiedData
  ( UnifiedDataBase,
    GetData,
    BaseMonad,
    wrapData,
    extractData,
    UnifiedData,
    AllUnifiedData,
    symCompare,
    liftSymCompare,
    symCompare1,
    liftSymCompare2,
    symCompare2,
  )
where

import Control.DeepSeq (NFData)
import Control.Monad.Identity (Identity (Identity, runIdentity))
import Data.Bytes.Serial (Serial)
import Data.Functor.Classes (Ord1 (liftCompare), Ord2 (liftCompare2), compare1, compare2)
import Data.Hashable (Hashable)
import Data.Kind (Type)
import Grisette.Internal.Core.Data.Class.AsKey (KeyEq, KeyHashable)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp)
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp)
import Grisette.Internal.Core.Data.Class.UnionView (UnionView)
import Grisette.Internal.Internal.Decl.Core.Control.Monad.Union
  ( Union,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym
  ( EvalSym,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.ExtractSym
  ( ExtractSym,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
  ( Mergeable,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.PPrint
  ( PPrint,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym
  ( SubstSym,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq
  ( SymEq,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd
  ( SymOrd,
  )
import qualified Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd as SymOrd
import Grisette.Internal.Internal.Decl.Core.Data.Class.ToCon
  ( ToCon,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.ToSym
  ( ToSym,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.TryMerge
  ( TryMerge,
    mrgSingle,
  )
import Grisette.Internal.Internal.Decl.SymPrim.AllSyms (AllSyms)
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedITEOp
  ( UnifiedITEOp,
  )
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSimpleMergeable
  ( UnifiedBranching (withBaseBranching),
    UnifiedSimpleMergeable,
    UnifiedSimpleMergeable1,
  )
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymEq
  ( UnifiedSymEq,
  )
import Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymOrd
  ( UnifiedSymOrd (withBaseSymOrd),
    UnifiedSymOrd1 (withBaseSymOrd1),
    UnifiedSymOrd2 (withBaseSymOrd2),
  )
import Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp ()
import Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSimpleMergeable
  ( liftUnion,
  )
import Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq ()
import Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd ()
import Grisette.Internal.Unified.Class.UnionViewMode (UnionViewMode)
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S))
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)
import Instances.TH.Lift ()
import Language.Haskell.TH.Syntax (Lift)

-- | A type family that specifies the base monad for the evaluation mode.
--
-- Resolves to 'Identity' for `C` mode, and 'Union' for `S` mode.
type BaseMonad mode = GetData mode

class
  ( UnifiedSimpleMergeable1 mode (GetData mode),
    UnifiedBranching mode (GetData mode),
    UnionView (GetData mode),
    UnionViewMode mode (GetData mode),
    Monad (GetData mode),
    TryMerge (GetData mode)
  ) =>
  UnifiedDataBase mode
  where
  -- | Get a unified data type. Resolves to 'Identity' in 'C' mode, and 'Union'
  -- in 'S' mode.
  type GetData mode = (r :: Type -> Type) | r -> mode

class
  ( u ~ GetData mode v,
    (Mergeable v) => Mergeable u,
    (AllSyms v) => AllSyms u,
    (Eq v) => Eq u,
    (EvalSym v) => EvalSym u,
    (ExtractSym v) => ExtractSym u,
    (ITEOp v, Mergeable v) => ITEOp u,
    (PPrint v) => PPrint u,
    (Eq v) => KeyEq u,
    (Eq v, Hashable v) => KeyHashable u,
    (Lift v) => Lift u,
    (LogicalOp v, Mergeable v) => LogicalOp u,
    (NFData v) => NFData u,
    (Num v, Mergeable v) => Num u,
    (SymEq v) => SymEq u,
    (Show v) => Show u,
    (SymOrd v) => SymOrd u,
    (SubstSym v) => SubstSym u,
    (Serial v, Mergeable v) => Serial u,
    (UnifiedITEOp mode v, Mergeable v) => UnifiedITEOp mode u,
    (Mergeable v) => UnifiedSimpleMergeable mode u,
    (UnifiedSymEq mode v) => UnifiedSymEq mode u,
    (UnifiedSymOrd mode v) => UnifiedSymOrd mode u,
    forall a. (ToSym a v) => ToSym (Identity a) u,
    forall a. (ToSym v a) => ToSym u (Union a),
    forall a. (ToCon v a) => ToCon u (Identity a),
    forall a. (ToCon a v) => ToCon (Union a) u,
    UnifiedDataBase mode
  ) =>
  UnifiedDataImpl (mode :: EvalModeTag) v u
    | u -> mode v
  where
  -- type GetData mode = (r :: Type -> Type) | r -> mode

  -- | Wraps a value into the unified data type.
  wrapData :: (Mergeable v) => v -> u

  -- | Extracts a value from the unified data type.
  extractData :: (Mergeable v, Monad m, UnifiedBranching mode m) => u -> m v

instance UnifiedDataBase 'C where
  type GetData 'C = Identity

instance UnifiedDataImpl 'C v (Identity v) where
  wrapData :: Mergeable v => v -> Identity v
wrapData = v -> Identity v
forall a. a -> Identity a
Identity
  extractData ::
    forall m. (Mergeable v, Monad m, UnifiedBranching C m) => Identity v -> m v
  extractData :: forall (m :: * -> *).
(Mergeable v, Monad m, UnifiedBranching 'C m) =>
Identity v -> m v
extractData = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'C @m ((If (IsConMode 'C) (TryMerge m) (SymBranching m) =>
  Identity v -> m v)
 -> Identity v -> m v)
-> (If (IsConMode 'C) (TryMerge m) (SymBranching m) =>
    Identity v -> m v)
-> Identity v
-> m v
forall a b. (a -> b) -> a -> b
$ v -> m v
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (v -> m v) -> (Identity v -> v) -> Identity v -> m v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity v -> v
forall a. Identity a -> a
runIdentity

instance UnifiedDataBase 'S where
  type GetData 'S = Union

instance UnifiedDataImpl 'S v (Union v) where
  wrapData :: Mergeable v => v -> Union v
wrapData = v -> Union v
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle
  extractData ::
    forall m. (Mergeable v, Monad m, UnifiedBranching S m) => Union v -> m v
  extractData :: forall (m :: * -> *).
(Mergeable v, Monad m, UnifiedBranching 'S m) =>
Union v -> m v
extractData = Union v -> m v
forall (mode :: EvalModeTag) a (m :: * -> *) (u :: * -> *).
(Applicative m, UnifiedBranching mode m, Mergeable a, UnionView u,
 UnionViewMode mode u) =>
u a -> m a
liftUnion

-- | This class is needed as constraint in user code prior to GHC 9.2.1.
-- See the notes in 'Grisette.Internal.Unified.IsMode.IsMode'.
class (UnifiedDataImpl mode v (GetData mode v)) => UnifiedData mode v

instance (UnifiedDataImpl bool v (GetData bool v)) => UnifiedData bool v

class
  (UnifiedSimpleMergeable 'S (GetData 'S v)) =>
  UnifiedDataSimpleMergeable v

instance (Mergeable v) => UnifiedDataSimpleMergeable v

-- | Evaluation mode with unified data types.
class
  ( forall v. UnifiedData bool v,
    forall v. (Mergeable v) => UnifiedDataSimpleMergeable v
  ) =>
  AllUnifiedData bool

instance
  ( forall v. UnifiedData bool v,
    forall v. (Mergeable v) => UnifiedDataSimpleMergeable v
  ) =>
  AllUnifiedData bool

-- TODO: temporary instance for dependencies

-- | Unified `Grisette.Internal.Core.Data.Class.SymOrd.symCompare`.
symCompare ::
  forall mode a.
  (DecideEvalMode mode, UnifiedSymOrd mode a) =>
  a ->
  a ->
  GetData mode Ordering
symCompare :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedSymOrd mode a) =>
a -> a -> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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 -> GetData mode Ordering) ->
  f a ->
  f b ->
  GetData mode Ordering
liftSymCompare :: forall (mode :: EvalModeTag) (f :: * -> *) a b.
(DecideEvalMode mode, UnifiedSymOrd1 mode f) =>
(a -> b -> GetData mode Ordering)
-> f a -> f b -> GetData mode Ordering
liftSymCompare a -> b -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    GetData mode Ordering)
-> GetData 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 -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    GetData mode Ordering)
-> GetData 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 -> GetData 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 ->
  GetData mode Ordering
symCompare1 :: forall (mode :: EvalModeTag) (f :: * -> *) a.
(DecideEvalMode mode, UnifiedSymOrd mode a,
 UnifiedSymOrd1 mode f) =>
f a -> f a -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord1 f) (SymOrd1 f) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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 -> GetData mode Ordering) ->
  (c -> d -> GetData mode Ordering) ->
  f a c ->
  f b d ->
  GetData mode Ordering
liftSymCompare2 :: forall (mode :: EvalModeTag) (f :: * -> * -> *) a b c d.
(DecideEvalMode mode, UnifiedSymOrd2 mode f) =>
(a -> b -> GetData mode Ordering)
-> (c -> d -> GetData mode Ordering)
-> f a c
-> f b d
-> GetData mode Ordering
liftSymCompare2 a -> b -> GetData mode Ordering
f c -> d -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    GetData mode Ordering)
-> GetData 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 -> GetData 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 -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    GetData mode Ordering)
-> GetData 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 -> GetData mode Ordering
f c -> d -> Union Ordering
c -> d -> GetData 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 ->
  GetData 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 -> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord b) (SymOrd b) =>
    GetData mode Ordering)
-> GetData 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) =>
  GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord2 f) (SymOrd2 f) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord a) (SymOrd a) =>
    GetData mode Ordering)
-> GetData 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) => GetData mode Ordering)
 -> GetData mode Ordering)
-> (If (IsConMode mode) (Ord b) (SymOrd b) =>
    GetData mode Ordering)
-> GetData 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 #-}