{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE PolyKinds #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif
{-# LANGUAGE ScopedTypeVariables #-}
module Data.GADT.Compare
( module Data.GADT.Compare
#if MIN_VERSION_base(4,7,0)
, (:~:)(Refl)
#endif
) where
import Data.Maybe
import Data.GADT.Show
import Data.Typeable
#if MIN_VERSION_base(4,7,0)
type (:=) = (:~:)
#else
data a := b where
Refl :: a := a
deriving Typeable
instance Eq (a := b) where
Refl == Refl = True
instance Ord (a := b) where
compare Refl Refl = EQ
instance Show (a := b) where
showsPrec _ Refl = showString "Refl"
instance Read (a := a) where
readsPrec _ s = case con of
"Refl" -> [(Refl, rest)]
_ -> []
where (con,rest) = splitAt 4 s
#endif
instance GShow ((:=) a) where
gshowsPrec :: Int -> (a := a) -> ShowS
gshowsPrec _ Refl = String -> ShowS
showString "Refl"
instance GRead ((:=) a) where
greadsPrec :: Int -> GReadS ((:=) a)
greadsPrec p :: Int
p s :: String
s = Int -> ReadS (a := a)
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
s [(a := a, String)]
-> ((a := a, String) -> [(GReadResult ((:=) a), String)])
-> [(GReadResult ((:=) a), String)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a := a, String) -> [(GReadResult ((:=) a), String)]
forall k (x :: k).
(x := x, String) -> [(GReadResult ((:=) x), String)]
f
where
f :: forall x. (x := x, String) -> [(GReadResult ((:=) x), String)]
f :: (x := x, String) -> [(GReadResult ((:=) x), String)]
f (Refl, rest :: String
rest) = (GReadResult ((:=) x), String) -> [(GReadResult ((:=) x), String)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((forall b. (forall (a :: k). (x := a) -> b) -> b)
-> GReadResult ((:=) x)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). (x := a) -> b
x -> (x := x) -> b
forall (a :: k). (x := a) -> b
x x := x
forall k (a :: k). a :~: a
Refl) , String
rest)
class GEq f where
geq :: f a -> f b -> Maybe (a := b)
defaultEq :: GEq f => f a -> f b -> Bool
defaultEq :: f a -> f b -> Bool
defaultEq x :: f a
x y :: f b
y = Maybe (a := b) -> Bool
forall a. Maybe a -> Bool
isJust (f a -> f b -> Maybe (a := b)
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 :: f a -> f b -> Bool
defaultNeq x :: f a
x y :: f b
y = Maybe (a := b) -> Bool
forall a. Maybe a -> Bool
isNothing (f a -> f b -> Maybe (a := b)
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 :: (a := a) -> (a := b) -> Maybe (a := b)
geq (a := a
Refl :: a := b) (a := b
Refl :: a := c) = (a := b) -> Maybe (a := b)
forall a. a -> Maybe a
Just (a := b
forall k (a :: k). a :~: a
Refl :: b := c)
data GOrdering a b where
GLT :: GOrdering a b
GEQ :: GOrdering t t
GGT :: GOrdering a b
deriving Typeable
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering GLT = Ordering
LT
weakenOrdering GEQ = Ordering
EQ
weakenOrdering GGT = Ordering
GT
instance Eq (GOrdering a b) where
x :: GOrdering a b
x == :: GOrdering a b -> GOrdering a b -> Bool
== y :: GOrdering a b
y =
GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== GOrdering a b -> Ordering
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 x :: GOrdering a b
x y :: GOrdering a b
y = Ordering -> Ordering -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering GOrdering a b
x) (GOrdering a b -> Ordering
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 _ GGT = String -> ShowS
showString "GGT"
showsPrec _ GEQ = String -> ShowS
showString "GEQ"
showsPrec _ GLT = String -> ShowS
showString "GLT"
instance GShow (GOrdering a) where
gshowsPrec :: Int -> GOrdering a a -> ShowS
gshowsPrec = Int -> GOrdering a a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance GRead (GOrdering a) where
greadsPrec :: Int -> GReadS (GOrdering a)
greadsPrec _ s :: String
s = case String
con of
"GGT" -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a Any -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a Any
forall k (a :: k) (b :: k). GOrdering a b
GGT), String
rest)]
"GEQ" -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a a -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a a
forall k (t :: k). GOrdering t t
GEQ), String
rest)]
"GLT" -> [((forall b. (forall (a :: k). GOrdering a a -> b) -> b)
-> GReadResult (GOrdering a)
forall k (t :: k -> *).
(forall b. (forall (a :: k). t a -> b) -> b) -> GReadResult t
GReadResult (\x :: forall (a :: k). GOrdering a a -> b
x -> GOrdering a Any -> b
forall (a :: k). GOrdering a a -> b
x GOrdering a Any
forall k (a :: k) (b :: k). GOrdering a b
GLT), String
rest)]
_ -> []
where (con :: String
con, rest :: String
rest) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 3 String
s
class GEq f => GCompare f where
gcompare :: f a -> f b -> GOrdering a b
instance GCompare ((:=) a) where
gcompare :: (a := a) -> (a := b) -> GOrdering a b
gcompare Refl Refl = GOrdering a b
forall k (t :: k). GOrdering t t
GEQ
defaultCompare :: GCompare f => f a -> f b -> Ordering
defaultCompare :: f a -> f b -> Ordering
defaultCompare x :: f a
x y :: f b
y = GOrdering a b -> Ordering
forall k (a :: k) (b :: k). GOrdering a b -> Ordering
weakenOrdering (f a -> f b -> GOrdering a b
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare f a
x f b
y)