{-# 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 :: (a -> b) -> GComparing a b a -> GComparing a b b
fmap a -> b
f (GComparing Either (GOrdering a b) a
x) = Either (GOrdering a b) b -> GComparing a b b
forall k (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing ((GOrdering a b -> Either (GOrdering a b) b)
-> (a -> Either (GOrdering a b) b)
-> Either (GOrdering a b) a
-> Either (GOrdering a b) b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GOrdering a b -> Either (GOrdering a b) b
forall a b. a -> Either a b
Left (b -> Either (GOrdering a b) b
forall a b. b -> Either a b
Right (b -> Either (GOrdering a b) b)
-> (a -> b) -> a -> Either (GOrdering a b) b
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 :: a -> GComparing a b a
return = a -> GComparing a b a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    GComparing (Left  GOrdering a b
x) >>= :: GComparing a b a -> (a -> GComparing a b b) -> GComparing a b b
>>= a -> GComparing a b b
f = Either (GOrdering a b) b -> GComparing a b b
forall k (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (GOrdering a b -> Either (GOrdering a b) b
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 :: a -> GComparing a b a
pure = Either (GOrdering a b) a -> GComparing a b a
forall k (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (Either (GOrdering a b) a -> GComparing a b a)
-> (a -> Either (GOrdering a b) a) -> a -> GComparing a b a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either (GOrdering a b) a
forall a b. b -> Either a b
Right
    <*> :: GComparing a b (a -> b) -> GComparing a b a -> GComparing a b 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' :: t a -> t b -> GComparing x y (a :~: b)
geq' t a
x t b
y = Either (GOrdering x y) (a :~: b) -> GComparing x y (a :~: b)
forall k (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (case t a -> t b -> GOrdering a b
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 -> GOrdering x y -> Either (GOrdering x y) (a :~: b)
forall a b. a -> Either a b
Left GOrdering x y
forall k (a :: k) (b :: k). GOrdering a b
GLT
    GOrdering a b
GEQ -> (a :~: a) -> Either (GOrdering x y) (a :~: a)
forall a b. b -> Either a b
Right a :~: a
forall k (a :: k). a :~: a
Refl
    GOrdering a b
GGT -> GOrdering x y -> Either (GOrdering x y) (a :~: b)
forall a b. a -> Either a b
Left GOrdering x y
forall k (a :: k) (b :: k). GOrdering a b
GGT)

compare' :: a -> a -> GComparing a b ()
compare' a
x a
y = Either (GOrdering a b) () -> GComparing a b ()
forall k (a :: k) (b :: k) t.
Either (GOrdering a b) t -> GComparing a b t
GComparing (Either (GOrdering a b) () -> GComparing a b ())
-> Either (GOrdering a b) () -> GComparing a b ()
forall a b. (a -> b) -> a -> b
$ case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
    Ordering
LT -> GOrdering a b -> Either (GOrdering a b) ()
forall a b. a -> Either a b
Left GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> () -> Either (GOrdering a b) ()
forall a b. b -> Either a b
Right ()
    Ordering
GT -> GOrdering a b -> Either (GOrdering a b) ()
forall a b. a -> Either a b
Left GOrdering a b
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) = (GOrdering a b -> GOrdering a b)
-> (GOrdering a b -> GOrdering a b)
-> Either (GOrdering a b) (GOrdering a b)
-> GOrdering a b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either GOrdering a b -> GOrdering a b
forall a. a -> a
id GOrdering a b -> GOrdering a b
forall a. a -> a
id Either (GOrdering a b) (GOrdering a b)
x