{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd
(
SymOrd (..),
SymOrd1 (..),
symCompare1,
SymOrd2 (..),
symCompare2,
symMax,
symMin,
mrgMax,
mrgMin,
SymOrdArgs (..),
GSymOrd (..),
genericSymCompare,
genericLiftSymCompare,
)
where
import Data.Kind (Type)
import Generics.Deriving
( Default (Default),
Default1 (Default1),
Generic (Rep, from),
Generic1 (Rep1, from1),
K1 (K1),
M1 (M1),
Par1 (Par1),
Rec1 (Rec1),
U1,
V1,
(:.:) (Comp1),
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp, symIte)
import Grisette.Internal.Core.Data.Class.LogicalOp
( LogicalOp (symNot),
)
import Grisette.Internal.Core.Data.Class.PlainUnion
( simpleMerge,
)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Internal.Decl.Core.Control.Monad.Union (Union)
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
( Mergeable,
)
import Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable
( SymBranching,
mrgIf,
)
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq
( GSymEq,
SymEq ((.==)),
SymEq1,
SymEq2,
)
import Grisette.Internal.Internal.Decl.Core.Data.Class.TryMerge
( mrgSingle,
)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.Utils.Derive (Arity0, Arity1)
class (SymEq a) => SymOrd a where
(.<) :: a -> a -> SymBool
infix 4 .<
(.<=) :: a -> a -> SymBool
infix 4 .<=
(.>) :: a -> a -> SymBool
infix 4 .>
(.>=) :: a -> a -> SymBool
infix 4 .>=
a
x .< a
y =
Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$
a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare a
x a
y Union Ordering -> (Ordering -> Union SymBool) -> Union SymBool
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Ordering
LT -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
True
Ordering
EQ -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
False
Ordering
GT -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
False
{-# INLINE (.<) #-}
a
x .<= a
y = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> a
y)
{-# INLINE (.<=) #-}
a
x .> a
y = a
y a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
x
{-# INLINE (.>) #-}
a
x .>= a
y = a
y a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= a
x
{-# INLINE (.>=) #-}
symCompare :: a -> a -> Union Ordering
symCompare a
l a
r =
SymBool -> Union Ordering -> Union Ordering -> Union Ordering
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(a
l a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
r)
(Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT)
(SymBool -> Union Ordering -> Union Ordering -> Union Ordering
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
l a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
r) (Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ) (Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT))
{-# INLINE symCompare #-}
{-# MINIMAL (.<) | symCompare #-}
class (SymEq1 f, forall a. (SymOrd a) => SymOrd (f a)) => SymOrd1 f where
liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering
symCompare1 :: forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1 = (a -> a -> Union Ordering) -> f a -> f a -> 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
liftSymCompare a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare
{-# INLINE symCompare1 #-}
class (SymEq2 f, forall a. (SymOrd a) => SymOrd1 (f a)) => SymOrd2 f where
liftSymCompare2 ::
(a -> b -> Union Ordering) ->
(c -> d -> Union Ordering) ->
f a c ->
f b d ->
Union Ordering
symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering
symCompare2 :: forall (f :: * -> * -> *) a b.
(SymOrd2 f, SymOrd a, SymOrd b) =>
f a b -> f a b -> Union Ordering
symCompare2 = (a -> a -> Union Ordering)
-> (b -> b -> Union Ordering) -> f a b -> f a b -> 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
liftSymCompare2 a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare b -> b -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare
{-# INLINE symCompare2 #-}
symMax :: (SymOrd a, ITEOp a) => a -> a -> a
symMax :: forall a. (SymOrd a, ITEOp a) => a -> a -> a
symMax a
x a
y = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) a
x a
y
{-# INLINE symMax #-}
symMin :: (SymOrd a, ITEOp a) => a -> a -> a
symMin :: forall a. (SymOrd a, ITEOp a) => a -> a -> a
symMin a
x a
y = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) a
y a
x
{-# INLINE symMin #-}
mrgMax ::
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a ->
a ->
m a
mrgMax :: forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
mrgMax a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y)
{-# INLINE mrgMax #-}
mrgMin ::
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a ->
a ->
m a
mrgMin :: forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
mrgMin a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
{-# INLINE mrgMin #-}
data family SymOrdArgs arity a b :: Type
data instance SymOrdArgs Arity0 _ _ = SymOrdArgs0
newtype instance SymOrdArgs Arity1 a b
= SymOrdArgs1 (a -> b -> Union Ordering)
class GSymOrd arity f where
gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering
instance GSymOrd arity V1 where
gsymCompare :: forall a b. SymOrdArgs arity a b -> V1 a -> V1 b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ V1 a
_ V1 b
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
{-# INLINE gsymCompare #-}
instance GSymOrd arity U1 where
gsymCompare :: forall a b. SymOrdArgs arity a b -> U1 a -> U1 b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ U1 a
_ U1 b
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
{-# INLINE gsymCompare #-}
instance
(GSymOrd arity a, GSymOrd arity b) =>
GSymOrd arity (a :*: b)
where
gsymCompare :: forall a b.
SymOrdArgs arity a b
-> (:*:) a b a -> (:*:) a b b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (a a
a1 :*: b a
b1) (a b
a2 :*: b b
b2) = do
l <- SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a1 a b
a2
case l of
Ordering
EQ -> SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall a b. SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args b a
b1 b b
b2
Ordering
_ -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
l
{-# INLINE gsymCompare #-}
instance
(GSymOrd arity a, GSymOrd arity b) =>
GSymOrd arity (a :+: b)
where
gsymCompare :: forall a b.
SymOrdArgs arity a b
-> (:+:) a b a -> (:+:) a b b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (L1 a a
a) (L1 a b
b) = SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a a b
b
gsymCompare SymOrdArgs arity a b
_ (L1 a a
_) (R1 b b
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
gsymCompare SymOrdArgs arity a b
args (R1 b a
a) (R1 b b
b) = SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall a b. SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args b a
a b b
b
gsymCompare SymOrdArgs arity a b
_ (R1 b a
_) (L1 a b
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
{-# INLINE gsymCompare #-}
instance (GSymOrd arity a) => GSymOrd arity (M1 i c a) where
gsymCompare :: forall a b.
SymOrdArgs arity a b -> M1 i c a a -> M1 i c a b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (M1 a a
a) (M1 a b
b) = SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a a b
b
{-# INLINE gsymCompare #-}
instance (SymOrd a) => GSymOrd arity (K1 i a) where
gsymCompare :: forall a b.
SymOrdArgs arity a b -> K1 i a a -> K1 i a b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ (K1 a
a) (K1 a
b) = a
a a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
`symCompare` a
b
{-# INLINE gsymCompare #-}
instance GSymOrd Arity1 Par1 where
gsymCompare :: forall a b.
SymOrdArgs Arity1 a b -> Par1 a -> Par1 b -> Union Ordering
gsymCompare (SymOrdArgs1 a -> b -> Union Ordering
c) (Par1 a
a) (Par1 b
b) = a -> b -> Union Ordering
c a
a b
b
{-# INLINE gsymCompare #-}
instance (SymOrd1 f) => GSymOrd Arity1 (Rec1 f) where
gsymCompare :: forall a b.
SymOrdArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> Union Ordering
gsymCompare (SymOrdArgs1 a -> b -> Union Ordering
c) (Rec1 f a
a) (Rec1 f b
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
liftSymCompare a -> b -> Union Ordering
c f a
a f b
b
{-# INLINE gsymCompare #-}
instance (SymOrd1 f, GSymOrd Arity1 g) => GSymOrd Arity1 (f :.: g) where
gsymCompare :: forall a b.
SymOrdArgs Arity1 a b
-> (:.:) f g a -> (:.:) f g b -> Union Ordering
gsymCompare SymOrdArgs Arity1 a b
targs (Comp1 f (g a)
a) (Comp1 f (g b)
b) = (g a -> g b -> Union Ordering)
-> f (g a) -> f (g 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
liftSymCompare (SymOrdArgs Arity1 a b -> g a -> g b -> Union Ordering
forall a b. SymOrdArgs Arity1 a b -> g a -> g b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs Arity1 a b
targs) f (g a)
a f (g b)
b
{-# INLINE gsymCompare #-}
instance
(Generic a, GSymOrd Arity0 (Rep a), GSymEq Arity0 (Rep a)) =>
SymOrd (Default a)
where
symCompare :: Default a -> Default a -> Union Ordering
symCompare (Default a
l) (Default a
r) = a -> a -> Union Ordering
forall a.
(Generic a, GSymOrd Arity0 (Rep a)) =>
a -> a -> Union Ordering
genericSymCompare a
l a
r
{-# INLINE symCompare #-}
genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering
genericSymCompare :: forall a.
(Generic a, GSymOrd Arity0 (Rep a)) =>
a -> a -> Union Ordering
genericSymCompare a
l a
r = SymOrdArgs Arity0 Any Any
-> Rep a Any -> Rep a Any -> Union Ordering
forall a b.
SymOrdArgs Arity0 a b -> Rep a a -> Rep a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs Arity0 Any Any
forall _ _. SymOrdArgs Arity0 _ _
SymOrdArgs0 (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
l) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
r)
{-# INLINE genericSymCompare #-}
instance
(Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f), SymOrd a) =>
SymOrd (Default1 f a)
where
symCompare :: Default1 f a -> Default1 f a -> Union Ordering
symCompare = Default1 f a -> Default1 f a -> Union Ordering
forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1
{-# INLINE symCompare #-}
instance
(Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f)) =>
SymOrd1 (Default1 f)
where
liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> Default1 f a -> Default1 f b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
c (Default1 f a
l) (Default1 f b
r) = (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
forall (f :: * -> *) a b.
(Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
genericLiftSymCompare a -> b -> Union Ordering
c f a
l f b
r
{-# INLINE liftSymCompare #-}
genericLiftSymCompare ::
(Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
(a -> b -> Union Ordering) ->
f a ->
f b ->
Union Ordering
genericLiftSymCompare :: forall (f :: * -> *) a b.
(Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
genericLiftSymCompare a -> b -> Union Ordering
c f a
l f b
r = SymOrdArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> Union Ordering
forall a b.
SymOrdArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare ((a -> b -> Union Ordering) -> SymOrdArgs Arity1 a b
forall a b. (a -> b -> Union Ordering) -> SymOrdArgs Arity1 a b
SymOrdArgs1 a -> b -> Union Ordering
c) (f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a
l) (f b -> Rep1 f b
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f b
r)
{-# INLINE genericLiftSymCompare #-}