{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.JoinSemilattice.Class.Eq where
import Control.Applicative (liftA2)
import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
import Data.JoinSemilattice.Class.Merge (Merge)
import Data.JoinSemilattice.Defined (Defined (..))
import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
import qualified Data.JoinSemilattice.Intersect as Intersect
import Data.Kind (Constraint, Type)
class EqC f x => EqC' f x
instance EqC f x => EqC' f x
class (forall x. EqC' f x => Merge (f x), BooleanR f)
=> EqR (f :: Type -> Type) where
type EqC f :: Type -> Constraint
eqR :: EqC' f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
neR :: (EqR f, EqC' f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
neR ( x, y, z )
= let ( notZ', _ ) = notR ( mempty, z )
( x', y', notZR ) = eqR ( x, y, notZ' )
( _, z' ) = notR ( notZR, mempty )
in ( x', y', z' )
instance EqR Defined where
type EqC Defined = Eq
eqR ( x, y, z )
= ( if z == trueR then y else mempty
, if z == trueR then x else mempty
, liftA2 (==) x y
)
instance EqR Intersect where
type EqC Intersect = Intersectable
eqR ( x, y, z )
= ( if | z == trueR -> y
| z == falseR && Intersect.size y == 1 -> Intersect.except y
| otherwise -> mempty
, if | z == trueR -> x
| z == falseR && Intersect.size x == 1 -> Intersect.except x
| otherwise -> mempty
, Intersect.lift2 (==) x y
)