{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Ordering
-- Copyright   :  (c) 2011 Patrick Bahr, Tom Hvitved
-- License     :  BSD3
-- Maintainer  :  Tom Hvitved <hvitved@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines ordering of signatures, which lifts to ordering of
-- terms and contexts.
--
--------------------------------------------------------------------------------
module Data.Comp.Multi.Ordering
    (
     KOrd(..),
     OrdHF(..)
    ) where

import Data.Comp.Multi.Equality
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term

class KEq f => KOrd f where
    kcompare :: f i -> f j -> Ordering

{-| Signature ordering. An instance @OrdHF f@ gives rise to an instance
  @Ord (Term f)@. -}
class EqHF f => OrdHF f where
    compareHF :: KOrd a => f a i -> f a j -> Ordering

instance KOrd f => Ord (E f) where
    compare :: E f -> E f -> Ordering
compare (E f i
x) (E f i
y) = forall (f :: * -> *) i j. KOrd f => f i -> f j -> Ordering
kcompare f i
x f i
y

instance Ord a => KOrd (K a) where
    kcompare :: forall i j. K a i -> K a j -> Ordering
kcompare (K a
x) (K a
y) = forall a. Ord a => a -> a -> Ordering
compare a
x a
y

{-| 'OrdHF' is propagated through sums. -}
instance (OrdHF f, OrdHF g) => OrdHF (f :+: g) where
    compareHF :: forall (a :: * -> *) i j.
KOrd a =>
(:+:) f g a i -> (:+:) f g a j -> Ordering
compareHF (Inl f a i
x) (Inl f a j
y) = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i j.
(OrdHF f, KOrd a) =>
f a i -> f a j -> Ordering
compareHF f a i
x f a j
y
    compareHF (Inl f a i
_) (Inr g a j
_) = Ordering
LT
    compareHF (Inr g a i
x) (Inr g a j
y) = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i j.
(OrdHF f, KOrd a) =>
f a i -> f a j -> Ordering
compareHF g a i
x g a j
y
    compareHF (Inr g a i
_) (Inl f a j
_) = Ordering
GT

{-| From an 'OrdHF' difunctor an 'Ord' instance of the corresponding term type
  can be derived. -}
instance (HFunctor f, OrdHF f) => OrdHF (Cxt h f) where
    compareHF :: forall (a :: * -> *) i j.
KOrd a =>
Cxt h f a i -> Cxt h f a j -> Ordering
compareHF (Term f (Cxt h f a) i
e1) (Term f (Cxt h f a) j
e2) = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i j.
(OrdHF f, KOrd a) =>
f a i -> f a j -> Ordering
compareHF f (Cxt h f a) i
e1 f (Cxt h f a) j
e2
    compareHF (Hole a i
h1) (Hole a j
h2) = forall (f :: * -> *) i j. KOrd f => f i -> f j -> Ordering
kcompare a i
h1 a j
h2
    compareHF (Term f (Cxt h f a) i
_) Cxt h f a j
_ = Ordering
LT
    compareHF (Hole a i
_) (Term f (Cxt h f a) j
_) = Ordering
GT

instance (HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a) where
    kcompare :: forall i j. Cxt h f a i -> Cxt h f a j -> Ordering
kcompare = forall (f :: (* -> *) -> * -> *) (a :: * -> *) i j.
(OrdHF f, KOrd a) =>
f a i -> f a j -> Ordering
compareHF

{-| Ordering of terms. -}
instance (HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i) where
    compare :: Cxt h f a i -> Cxt h f a i -> Ordering
compare = forall (f :: * -> *) i j. KOrd f => f i -> f j -> Ordering
kcompare