{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module Data.GADT.Internal where
import Control.Applicative (Applicative (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import Data.Kind (Type)
import Data.Maybe (isJust, isNothing)
import Data.Monoid (Monoid (..))
import Data.Semigroup (Semigroup (..))
import Data.Type.Equality (TestEquality (..), (:~:) (..), (:~~:) (..))
import GHC.Generics ((:*:) (..), (:+:) (..))
import qualified Type.Reflection as TR
#if __GLASGOW_HASKELL__ >= 810
import Data.Kind (Constraint)
#endif
#if MIN_VERSION_base(4,18,0)
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif
#if __GLASGOW_HASKELL__ >= 810
type GShow :: (k -> Type) -> Constraint
#endif
class GShow t where
gshowsPrec :: Int -> t a -> ShowS
defaultGshowsPrec :: Show (t a) => Int -> t a -> ShowS
defaultGshowsPrec :: forall {k} (t :: k -> *) (a :: k).
Show (t a) =>
Int -> t a -> ShowS
defaultGshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
gshows :: GShow t => t a -> ShowS
gshows :: forall {k} (t :: k -> *) (a :: k). GShow t => t a -> ShowS
gshows = forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec (-Int
1)
gshow :: (GShow t) => t a -> String
gshow :: forall {k} (t :: k -> *) (a :: k). GShow t => t a -> String
gshow t a
x = forall {k} (t :: k -> *) (a :: k). GShow t => t a -> ShowS
gshows t a
x String
""
instance GShow ((:~:) a) where
gshowsPrec :: forall (a :: k). Int -> (a :~: a) -> ShowS
gshowsPrec Int
_ a :~: a
Refl = String -> ShowS
showString String
"Refl"
instance GShow ((:~~:) a) where
gshowsPrec :: forall (a :: k). Int -> (a :~~: a) -> ShowS
gshowsPrec Int
_ a :~~: a
HRefl = String -> ShowS
showString String
"HRefl"
instance GShow TR.TypeRep where
gshowsPrec :: forall (a :: k). Int -> TypeRep a -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
#if MIN_VERSION_base(4,18,0)
instance GShow TL.SChar where
gshowsPrec = showsPrec
instance GShow TL.SSymbol where
gshowsPrec = showsPrec
instance GShow TN.SNat where
gshowsPrec = showsPrec
#endif
instance (GShow a, GShow b) => GShow (Sum a b) where
gshowsPrec :: forall (a :: k). Int -> Sum a b a -> ShowS
gshowsPrec Int
d = \Sum a b a
s -> case Sum a b a
s of
InL a a
x -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) (String -> ShowS
showString String
"InL " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 a a
x)
InR b a
x -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) (String -> ShowS
showString String
"InR " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 b a
x)
instance (GShow a, GShow b) => GShow (Product a b) where
gshowsPrec :: forall (a :: k). Int -> Product a b a -> ShowS
gshowsPrec Int
d (Pair a a
x b a
y) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Pair "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 a a
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> ShowS
showChar Char
' '
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 b a
y
instance (GShow a, GShow b) => GShow (a :+: b) where
gshowsPrec :: forall (a :: k). Int -> (:+:) a b a -> ShowS
gshowsPrec Int
d = \(:+:) a b a
s -> case (:+:) a b a
s of
L1 a a
x -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) (String -> ShowS
showString String
"L1 " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 a a
x)
R1 b a
x -> Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) (String -> ShowS
showString String
"R1 " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 b a
x)
instance (GShow a, GShow b) => GShow (a :*: b) where
gshowsPrec :: forall (a :: k). Int -> (:*:) a b a -> ShowS
gshowsPrec Int
d (a a
x :*: b a
y) = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
6)
forall a b. (a -> b) -> a -> b
$ forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
6 a a
x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :*: "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
6 b a
y
#if __GLASGOW_HASKELL__ >= 810
type GReadS :: (k -> Type) -> Type
#endif
type GReadS t = String -> [(Some t, String)]
getGReadResult :: Some tag -> (forall a. tag a -> b) -> b
getGReadResult :: forall {k} (tag :: k -> *) b.
Some tag -> (forall (a :: k). tag a -> b) -> b
getGReadResult Some tag
t forall (a :: k). tag a -> b
k = forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
t forall (a :: k). tag a -> b
k
mkGReadResult :: tag a -> Some tag
mkGReadResult :: forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkGReadResult = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome
#if __GLASGOW_HASKELL__ >= 810
type GRead :: (k -> Type) -> Constraint
#endif
class GRead t where
greadsPrec :: Int -> GReadS t
greads :: GRead t => GReadS t
greads :: forall {k} (t :: k -> *). GRead t => GReadS t
greads = forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec (-Int
1)
gread :: GRead t => String -> (forall a. t a -> b) -> b
gread :: forall {k} (t :: k -> *) b.
GRead t =>
String -> (forall (a :: k). t a -> b) -> b
gread String
s forall (a :: k). t a -> b
g = forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome (forall {a}. [a] -> a
hd [Some t
f | (Some t
f, String
"") <- forall {k} (t :: k -> *). GRead t => GReadS t
greads String
s]) forall (a :: k). t a -> b
g where
hd :: [a] -> a
hd (a
x:[a]
_) = a
x
hd [a]
_ = forall a. HasCallStack => String -> a
error String
"gread: no parse"
greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b
greadMaybe :: forall {k} (t :: k -> *) b.
GRead t =>
String -> (forall (a :: k). t a -> b) -> Maybe b
greadMaybe String
s forall (a :: k). t a -> b
g = case [Some t
f | (Some t
f, String
"") <- forall {k} (t :: k -> *). GRead t => GReadS t
greads String
s] of
(Some t
x : [Some t]
_) -> forall a. a -> Maybe a
Just (forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some t
x forall (a :: k). t a -> b
g)
[Some t]
_ -> forall a. Maybe a
Nothing
instance GRead ((:~:) a) where
greadsPrec :: Int -> GReadS ((:~:) a)
greadsPrec Int
_ = forall a. Bool -> ReadS a -> ReadS a
readParen Bool
False (\String
s ->
[ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k). (a :~: a) -> r
k -> forall (a :: k). (a :~: a) -> r
k (forall {k} (a :: k). a :~: a
Refl :: a :~: a), String
t)
| (String
"Refl", String
t) <- ReadS String
lex String
s
])
instance k1 ~ k2 => GRead ((:~~:) (a :: k1) :: k2 -> Type) where
greadsPrec :: Int -> GReadS ((:~~:) a)
greadsPrec Int
_ = forall a. Bool -> ReadS a -> ReadS a
readParen Bool
False (\String
s ->
[ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k2). (a :~~: a) -> r
k -> forall (a :: k2). (a :~~: a) -> r
k (forall {k1} (a :: k1). a :~~: a
HRefl :: a :~~: a), String
t)
| (String
"HRefl", String
t) <- ReadS String
lex String
s
])
instance (GRead a, GRead b) => GRead (Sum a b) where
greadsPrec :: Int -> GReadS (Sum a b)
greadsPrec Int
d String
s =
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
(\String
s1 -> [ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k). Sum a b a -> r
k -> forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some a
r (forall (a :: k). Sum a b a -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL), String
t)
| (String
"InL", String
s2) <- ReadS String
lex String
s1
, (Some a
r, String
t) <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
s2 ]) String
s
forall a. [a] -> [a] -> [a]
++
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
(\String
s1 -> [ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k). Sum a b a -> r
k -> forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some b
r (forall (a :: k). Sum a b a -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR), String
t)
| (String
"InR", String
s2) <- ReadS String
lex String
s1
, (Some b
r, String
t) <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
s2 ]) String
s
instance (GRead a, GRead b) => GRead (a :+: b) where
greadsPrec :: Int -> GReadS (a :+: b)
greadsPrec Int
d String
s =
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
(\String
s1 -> [ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k). (:+:) a b a -> r
k -> forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some a
r (forall (a :: k). (:+:) a b a -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1), String
t)
| (String
"L1", String
s2) <- ReadS String
lex String
s1
, (Some a
r, String
t) <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
s2 ]) String
s
forall a. [a] -> [a] -> [a]
++
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10)
(\String
s1 -> [ (forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S forall a b. (a -> b) -> a -> b
$ \forall (a :: k). (:+:) a b a -> r
k -> forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some b
r (forall (a :: k). (:+:) a b a -> r
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1), String
t)
| (String
"R1", String
s2) <- ReadS String
lex String
s1
, (Some b
r, String
t) <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
s2 ]) String
s
#if __GLASGOW_HASKELL__ >= 810
type GEq :: (k -> Type) -> Constraint
#endif
class GEq f where
geq :: f a -> f b -> Maybe (a :~: b)
defaultGeq :: GCompare f => f a -> f b -> Maybe (a :~: b)
defaultGeq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Maybe (a :~: b)
defaultGeq f a
a f b
b = case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare f a
a f b
b of
GOrdering a b
GEQ -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
GOrdering a b
_ -> forall a. Maybe a
Nothing
defaultEq :: GEq f => f a -> f b -> Bool
defaultEq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq f a
x f b
y = forall a. Maybe a -> Bool
isJust (forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq f a
x f b
y)
defaultNeq :: GEq f => f a -> f b -> Bool
defaultNeq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultNeq f a
x f b
y = forall a. Maybe a -> Bool
isNothing (forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq f a
x f b
y)
instance GEq ((:~:) a) where
geq :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> Maybe (a :~: b)
geq (a :~: a
Refl :: a :~: b) (a :~: b
Refl :: a :~: c) = forall a. a -> Maybe a
Just (forall {k} (a :: k). a :~: a
Refl :: b :~: c)
instance GEq ((:~~:) a) where
geq :: forall (a :: k) (b :: k).
(a :~~: a) -> (a :~~: b) -> Maybe (a :~: b)
geq (a :~~: a
HRefl :: a :~~: b) (a :~~: b
HRefl :: a :~~: c) = forall a. a -> Maybe a
Just (forall {k} (a :: k). a :~: a
Refl :: b :~: c)
instance (GEq a, GEq b) => GEq (Sum a b) where
geq :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> Maybe (a :~: b)
geq (InL a a
x) (InL a b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq a a
x a b
y
geq (InR b a
x) (InR b b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq b a
x b b
y
geq Sum a b a
_ Sum a b b
_ = forall a. Maybe a
Nothing
instance (GEq a, GEq b) => GEq (Product a b) where
geq :: forall (a :: k) (b :: k).
Product a b a -> Product a b b -> Maybe (a :~: b)
geq (Pair a a
x b a
y) (Pair a b
x' b b
y') = do
a :~: b
Refl <- forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq a a
x a b
x'
a :~: b
Refl <- forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq b a
y b b
y'
forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
instance (GEq f, GEq g) => GEq (f :+: g) where
geq :: forall (a :: k) (b :: k).
(:+:) f g a -> (:+:) f g b -> Maybe (a :~: b)
geq (L1 f a
x) (L1 f b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq f a
x f b
y
geq (R1 g a
x) (R1 g b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq g a
x g b
y
geq (:+:) f g a
_ (:+:) f g b
_ = forall a. Maybe a
Nothing
instance (GEq a, GEq b) => GEq (a :*: b) where
geq :: forall (a :: k) (b :: k).
(:*:) a b a -> (:*:) a b b -> Maybe (a :~: b)
geq (a a
x :*: b a
y) (a b
x' :*: b b
y') = do
a :~: b
Refl <- forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq a a
x a b
x'
a :~: b
Refl <- forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq b a
y b b
y'
forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
instance GEq TR.TypeRep where
geq :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
geq = forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality
#if MIN_VERSION_base(4,18,0)
instance GEq TL.SChar where
geq = testEquality
instance GEq TL.SSymbol where
geq = testEquality
instance GEq TN.SNat where
geq = testEquality
#endif
#if __GLASGOW_HASKELL__ >= 810
type GOrdering :: k -> k -> Type
#endif
data GOrdering a b where
GLT :: GOrdering a b
GEQ :: GOrdering t t
GGT :: GOrdering a b
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering :: forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
GLT = Ordering
LT
weakenOrdering GOrdering a b
GEQ = Ordering
EQ
weakenOrdering GOrdering a b
GGT = Ordering
GT
instance Eq (GOrdering a b) where
GOrdering a b
x == :: GOrdering a b -> GOrdering a b -> Bool
== GOrdering a b
y = forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x forall a. Eq a => a -> a -> Bool
== forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
y
instance Ord (GOrdering a b) where
compare :: GOrdering a b -> GOrdering a b -> Ordering
compare GOrdering a b
x GOrdering a b
y = forall a. Ord a => a -> a -> Ordering
compare (forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x) (forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
y)
instance Show (GOrdering a b) where
showsPrec :: Int -> GOrdering a b -> ShowS
showsPrec Int
_ GOrdering a b
GGT = String -> ShowS
showString String
"GGT"
showsPrec Int
_ GOrdering a b
GEQ = String -> ShowS
showString String
"GEQ"
showsPrec Int
_ GOrdering a b
GLT = String -> ShowS
showString String
"GLT"
instance GShow (GOrdering a) where
gshowsPrec :: forall (a :: k). Int -> GOrdering a a -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance GRead (GOrdering a) where
greadsPrec :: Int -> GReadS (GOrdering a)
greadsPrec Int
_ String
s = case String
con of
String
"GGT" -> [(forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome forall {k} (a :: k) (b :: k). GOrdering a b
GGT, String
rest)]
String
"GEQ" -> [(forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome forall {k} (t :: k). GOrdering t t
GEQ, String
rest)]
String
"GLT" -> [(forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome forall {k} (a :: k) (b :: k). GOrdering a b
GLT, String
rest)]
String
_ -> []
where (String
con, String
rest) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
3 String
s
#if __GLASGOW_HASKELL__ >= 810
type GCompare :: (k -> Type) -> Constraint
#endif
class GEq f => GCompare f where
gcompare :: f a -> f b -> GOrdering a b
instance GCompare ((:~:) a) where
gcompare :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> GOrdering a b
gcompare a :~: a
Refl a :~: b
Refl = forall {k} (t :: k). GOrdering t t
GEQ
instance GCompare ((:~~:) a) where
gcompare :: forall (a :: k) (b :: k). (a :~~: a) -> (a :~~: b) -> GOrdering a b
gcompare a :~~: a
HRefl a :~~: b
HRefl = forall {k} (t :: k). GOrdering t t
GEQ
instance GCompare TR.TypeRep where
gcompare :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> GOrdering a b
gcompare = forall {k} (f :: k -> *) c (a :: k) (b :: k).
(TestEquality f, Ord c) =>
String
-> (forall (x :: k). f x -> c) -> f a -> f b -> GOrdering a b
gcompareSing String
"TypeRep" forall k (a :: k). TypeRep a -> SomeTypeRep
TR.SomeTypeRep
#if MIN_VERSION_base(4,18,0)
instance GCompare TL.SChar where
gcompare = gcompareSing "SChar" TL.fromSChar
instance GCompare TL.SSymbol where
gcompare = gcompareSing "SSymbol" TL.fromSSymbol
instance GCompare TN.SNat where
gcompare = gcompareSing "SNat" TN.fromSNat
#endif
defaultCompare :: GCompare f => f a -> f b -> Ordering
defaultCompare :: forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare f a
x f b
y = forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering (forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare f a
x f b
y)
gcompareSing :: (TestEquality f, Ord c)
=> String
-> (forall x. f x -> c)
-> f a -> f b -> GOrdering a b
gcompareSing :: forall {k} (f :: k -> *) c (a :: k) (b :: k).
(TestEquality f, Ord c) =>
String
-> (forall (x :: k). f x -> c) -> f a -> f b -> GOrdering a b
gcompareSing String
singName forall (x :: k). f x -> c
toOrd f a
t1 f b
t2 =
case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
t1 f b
t2 of
Just a :~: b
Refl -> forall {k} (t :: k). GOrdering t t
GEQ
Maybe (a :~: b)
Nothing ->
case forall a. Ord a => a -> a -> Ordering
compare (forall (x :: k). f x -> c
toOrd f a
t1) (forall (x :: k). f x -> c
toOrd f b
t2) of
Ordering
LT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
Ordering
GT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
Ordering
EQ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"impossible: 'testEquality' and 'compare' are inconsistent for "
forall a. [a] -> [a] -> [a]
++ String
singName
forall a. [a] -> [a] -> [a]
++ String
"; report this as a GHC bug"
instance (GCompare a, GCompare b) => GCompare (Sum a b) where
gcompare :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> GOrdering a b
gcompare (InL a a
x) (InL a b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare a a
x a b
y
gcompare (InL a a
_) (InR b b
_) = forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare (InR b a
_) (InL a b
_) = forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare (InR b a
x) (InR b b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare b a
x b b
y
instance (GCompare a, GCompare b) => GCompare (Product a b) where
gcompare :: forall (a :: k) (b :: k).
Product a b a -> Product a b b -> GOrdering a b
gcompare (Pair a a
x b a
y) (Pair a b
x' b b
y') = case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare a a
x a b
x' of
GOrdering a b
GLT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering a b
GGT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
GOrdering a b
GEQ -> case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare b a
y b b
y' of
GOrdering a b
GLT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering a b
GEQ -> forall {k} (t :: k). GOrdering t t
GEQ
GOrdering a b
GGT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
instance (GCompare f, GCompare g) => GCompare (f :+: g) where
gcompare :: forall (a :: k) (b :: k).
(:+:) f g a -> (:+:) f g b -> GOrdering a b
gcompare (L1 f a
x) (L1 f b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare f a
x f b
y
gcompare (L1 f a
_) (R1 g b
_) = forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare (R1 g a
_) (L1 f b
_) = forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare (R1 g a
x) (R1 g b
y) = forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare g a
x g b
y
instance (GCompare a, GCompare b) => GCompare (a :*: b) where
gcompare :: forall (a :: k) (b :: k).
(:*:) a b a -> (:*:) a b b -> GOrdering a b
gcompare (a a
x :*: b a
y) (a b
x' :*: b b
y') = case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare a a
x a b
x' of
GOrdering a b
GLT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering a b
GGT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
GOrdering a b
GEQ -> case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare b a
y b b
y' of
GOrdering a b
GLT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering a b
GEQ -> forall {k} (t :: k). GOrdering t t
GEQ
GOrdering a b
GGT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT
#if __GLASGOW_HASKELL__ >= 810
type Some :: (k -> Type) -> Type
#endif
newtype Some tag = S
{
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome :: forall r. (forall a. tag a -> r) -> r
}
type role Some representational
mkSome :: tag a -> Some tag
mkSome :: forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome tag a
t = forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S (\forall (a :: k). tag a -> r
f -> forall (a :: k). tag a -> r
f tag a
t)
mapSome :: (forall x. f x -> g x) -> Some f -> Some g
mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Some f -> Some g
mapSome forall (x :: k). f x -> g x
nt (S forall r. (forall (a :: k). f a -> r) -> r
fx) = forall k (tag :: k -> *).
(forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
S (\forall (a :: k). g a -> r
f -> forall r. (forall (a :: k). f a -> r) -> r
fx (forall (a :: k). g a -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: k). f x -> g x
nt))
foldSome :: (forall a. tag a -> b) -> Some tag -> b
foldSome :: forall {k} (tag :: k -> *) b.
(forall (a :: k). tag a -> b) -> Some tag -> b
foldSome forall (a :: k). tag a -> b
some (S forall r. (forall (a :: k). tag a -> r) -> r
thing) = forall r. (forall (a :: k). tag a -> r) -> r
thing forall (a :: k). tag a -> b
some
traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
traverseSome :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
Functor m =>
(forall (a :: k). f a -> m (g a)) -> Some f -> m (Some g)
traverseSome forall (a :: k). f a -> m (g a)
f Some f
x = forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some f
x forall a b. (a -> b) -> a -> b
$ \f a
x' -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome (forall (a :: k). f a -> m (g a)
f f a
x')
withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r
withSomeM :: forall {k} (m :: * -> *) (tag :: k -> *) r.
Monad m =>
m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r
withSomeM m (Some tag)
m forall (a :: k). tag a -> m r
k = m (Some tag)
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Some tag
s -> forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
s forall (a :: k). tag a -> m r
k
instance GShow tag => Show (Some tag) where
showsPrec :: Int -> Some tag -> ShowS
showsPrec Int
p Some tag
some = forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
some forall a b. (a -> b) -> a -> b
$ \tag a
thing -> Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10)
( String -> ShowS
showString String
"mkSome "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 tag a
thing
)
instance GRead f => Read (Some f) where
readsPrec :: Int -> ReadS (Some f)
readsPrec Int
p = forall a. Bool -> ReadS a -> ReadS a
readParen (Int
pforall a. Ord a => a -> a -> Bool
>Int
10) forall a b. (a -> b) -> a -> b
$ \String
s ->
[ (forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some f
withTag forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome, String
rest')
| (String
con, String
rest) <- ReadS String
lex String
s
, String
con forall a. Eq a => a -> a -> Bool
== String
"Some" Bool -> Bool -> Bool
|| String
con forall a. Eq a => a -> a -> Bool
== String
"mkSome"
, (Some f
withTag, String
rest') <- forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec Int
11 String
rest
]
instance GEq tag => Eq (Some tag) where
Some tag
x == :: Some tag -> Some tag -> Bool
== Some tag
y =
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
x forall a b. (a -> b) -> a -> b
$ \tag a
x' ->
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
y forall a b. (a -> b) -> a -> b
$ \tag a
y' -> forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq tag a
x' tag a
y'
instance GCompare tag => Ord (Some tag) where
compare :: Some tag -> Some tag -> Ordering
compare Some tag
x Some tag
y =
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
x forall a b. (a -> b) -> a -> b
$ \tag a
x' ->
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
y forall a b. (a -> b) -> a -> b
$ \tag a
y' -> forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare tag a
x' tag a
y'
instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
Some m
m <> :: Some m -> Some m -> Some m
<> Some m
n =
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some m
m forall a b. (a -> b) -> a -> b
$ \m a
m' ->
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some m
n forall a b. (a -> b) -> a -> b
$ \m a
n' ->
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome (m a
m' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m a
n')
instance Applicative m => Data.Monoid.Monoid (Some m) where
mempty :: Some m
mempty = forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome (forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
mappend :: Some m -> Some m -> Some m
mappend = forall a. Semigroup a => a -> a -> a
(<>)