{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeApplications     #-}
{-# 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.Type.Equality
import Data.Comp.Multi.Equality
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
import Data.Comp.Dict
import Data.Comp.Elem

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 x :: f i
x) (E y :: f i
y) = f i -> f i -> Ordering
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 :: K a i -> K a j -> Ordering
kcompare (K x :: a
x) (K y :: a
y) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y

{-| 'OrdHF' is propagated through sums. -}
instance ( All OrdHF fs
         , EqHF (Sum fs)
         ) => OrdHF (Sum fs) where
    compareHF :: Sum fs a i -> Sum fs a j -> Ordering
compareHF (Sum wit1 :: Elem f fs
wit1 x :: f a i
x) (Sum wit2 :: Elem f fs
wit2 y :: f a j
y) =
      case Elem f fs -> Elem f fs -> Maybe (f :~: f)
forall k (f :: k) (g :: k) (fs :: [k]).
Elem f fs -> Elem g fs -> Maybe (f :~: g)
elemEq Elem f fs
wit1 Elem f fs
wit2 of
        Just Refl -> f a i -> f a j -> Ordering
forall (f :: (* -> *) -> * -> *) (a :: * -> *) i j.
(OrdHF f, KOrd a) =>
f a i -> f a j -> Ordering
compareHF f a i
x f a j
f a j
y (OrdHF f => Ordering) -> Dict OrdHF f -> Ordering
forall k (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
\\ Elem f fs -> Dict OrdHF f
forall k (c :: k -> Constraint) (f :: k) (fs :: [k]).
All c fs =>
Elem f fs -> Dict c f
dictFor @OrdHF Elem f fs
wit1
        Nothing   -> Elem f fs -> Elem f fs -> Ordering
forall k (f :: k) (fs :: [k]) (g :: k).
Elem f fs -> Elem g fs -> Ordering
comparePos Elem f fs
wit1 Elem f fs
wit2

{-| 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 :: Cxt h f a i -> Cxt h f a j -> Ordering
compareHF (Term e1 :: f (Cxt h f a) i
e1) (Term e2 :: f (Cxt h f a) j
e2) = f (Cxt h f a) i -> f (Cxt h f a) j -> Ordering
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 h1 :: a i
h1) (Hole h2 :: a j
h2) = a i -> a j -> Ordering
forall (f :: * -> *) i j. KOrd f => f i -> f j -> Ordering
kcompare a i
h1 a j
h2
    compareHF (Term _) _ = Ordering
LT
    compareHF (Hole _) (Term _) = Ordering
GT

instance (HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a) where
    kcompare :: Cxt h f a i -> Cxt h f a j -> Ordering
kcompare = Cxt h f a i -> Cxt h f a j -> Ordering
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 = Cxt h f a i -> Cxt h f a i -> Ordering
forall (f :: * -> *) i j. KOrd f => f i -> f j -> Ordering
kcompare