{-# LANGUAGE TypeOperators #-}
{-|
  Provides instances of EqHF and OrdHF for 'Data.Comp.Multi.:&:'.

  The reason we have not yet suggested these be merged into compdata is that it is unclear
  how annotations should in general be treated. In particular, for efficiency, we may at one point
  wish to use annotations and ignore terms for the EqHF and OrdHF instances.
 -}

module Cubix.Sin.Compdata.Instances (
  ) where

import Data.Comp.Multi.Equality ( EqHF(..) )
import Data.Comp.Multi.Ops ( (:&:)(..) )
import Data.Comp.Multi.Ordering ( OrdHF(..) )

instance (EqHF f, Eq a) => EqHF (f :&: a) where
  (v1 :: f g i
v1 :&: c1 :: a
c1) eqHF :: (:&:) f a g i -> (:&:) f a g j -> Bool
`eqHF` (v2 :: f g j
v2 :&: c2 :: a
c2) = (f g i
v1 f g i -> f g j -> Bool
forall (f :: (* -> *) -> * -> *) (g :: * -> *) i j.
(EqHF f, KEq g) =>
f g i -> f g j -> Bool
`eqHF` f g j
v2) Bool -> Bool -> Bool
&& (a
c1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c2)

instance (OrdHF f, Ord a) => OrdHF (f :&: a) where
  (v1 :: f a i
v1 :&: c1 :: a
c1) compareHF :: (:&:) f a a i -> (:&:) f a a j -> Ordering
`compareHF` (v2 :: f a j
v2 :&: c2 :: a
c2) = case f a i
v1 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 j
v2 of
                                          EQ -> a
c1 a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
c2
                                          x :: Ordering
x -> Ordering
x