{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
module Data.GADT.Compare.Monad
    ( GComparing
    , runGComparing
    , geq'
    , compare'
    ) where

import Control.Applicative
import Control.Monad
import Data.GADT.Compare
import Data.Type.Equality ((:~:) (..))

-- A monad allowing gcompare to be defined in the same style as geq
newtype GComparing a b t = GComparing (Either (GOrdering a b) t)

instance Functor (GComparing a b) where fmap :: forall a b. (a -> b) -> GComparing a b a -> GComparing a b b
fmap a -> b
f (GComparing Either (GOrdering a b) a
x) = forall {k} (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. a -> Either a b
Left (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) Either (GOrdering a b) a
x)
instance Monad (GComparing a b) where
    return :: forall a. a -> GComparing a b a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    GComparing (Left  GOrdering a b
x) >>= :: forall a b.
GComparing a b a -> (a -> GComparing a b b) -> GComparing a b b
>>= a -> GComparing a b b
f = forall {k} (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (forall a b. a -> Either a b
Left GOrdering a b
x)
    GComparing (Right a
x) >>= a -> GComparing a b b
f = a -> GComparing a b b
f a
x
instance Applicative (GComparing a b) where
    pure :: forall a. a -> GComparing a b a
pure = forall {k} (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right
    <*> :: forall a b.
GComparing a b (a -> b) -> GComparing a b a -> GComparing a b b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

geq' :: GCompare t => t a -> t b -> GComparing x y (a :~: b)
geq' :: forall {k} {k} (t :: k -> *) (a :: k) (b :: k) (x :: k) (y :: k).
GCompare t =>
t a -> t b -> GComparing x y (a :~: b)
geq' t a
x t b
y = forall {k} (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (case forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
gcompare t a
x t b
y of
    GOrdering a b
GLT -> forall a b. a -> Either a b
Left forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    GOrdering a b
GEQ -> forall a b. b -> Either a b
Right forall {k} (a :: k). a :~: a
Refl
    GOrdering a b
GGT -> forall a b. a -> Either a b
Left forall {k} (a :: k) (b :: k). GOrdering a b
GGT)

compare' :: a -> a -> GComparing a b ()
compare' a
x a
y = forall {k} (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing forall a b. (a -> b) -> a -> b
$ case forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
    Ordering
LT -> forall a b. a -> Either a b
Left forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> forall a b. b -> Either a b
Right ()
    Ordering
GT -> forall a b. a -> Either a b
Left forall {k} (a :: k) (b :: k). GOrdering a b
GGT

runGComparing :: GComparing a b (GOrdering a b) -> GOrdering a b
runGComparing (GComparing Either (GOrdering a b) (GOrdering a b)
x) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id forall a. a -> a
id Either (GOrdering a b) (GOrdering a b)
x