{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-|
Module      : Data.JoinSemilattice.Class.Ord
Description : Relationships between values and their comparison results.
Copyright   : (c) Tom Harding, 2020
License     : MIT
-}
module Data.JoinSemilattice.Class.Ord where

import Control.Applicative (liftA2)
import Data.JoinSemilattice.Defined (Defined (..))
import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)
import qualified Data.JoinSemilattice.Intersect as Intersect
import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
import Data.JoinSemilattice.Class.Eq (EqR (..), EqC')
import Data.Kind (Constraint, Type)

-- | Comparison relationships between two values and their comparison result.
-- See 'Data.JoinSemilattice.Class.Eq.EqR' for more information on the design
-- of this class, and a full apology for the constraints involved.
class (EqR f, forall x. OrdC f x => EqC' f x) => OrdR (f :: Type -> Type) where
  type OrdC f :: Type -> Constraint
  type OrdC f = EqC f

  -- | A relationship between two values and whether the left is less than or
  -- equal to the right.
  lteR :: OrdC f x => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )

-- | Comparison between two values and their '(>)' result.
gtR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
gtR :: (f x, f x, f Bool) -> (f x, f x, f Bool)
gtR ( f x
x, f x
y, f Bool
z ) = let ( f x
y', f x
x', f Bool
z' ) = (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
ltR ( f x
y, f x
x, f Bool
z ) in ( f x
x', f x
y', f Bool
z' )

-- | Comparison between two values and their '(>=)' result.
gteR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
gteR :: (f x, f x, f Bool) -> (f x, f x, f Bool)
gteR ( f x
x, f x
y, f Bool
z ) = let ( f x
y', f x
x', f Bool
z' ) = (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
lteR ( f x
y, f x
x, f Bool
z ) in ( f x
x', f x
y', f Bool
z' )

-- | Comparison between two values and their '(<)' result.
ltR :: (OrdR f, OrdC f x) => ( f x, f x, f Bool ) -> ( f x, f x, f Bool )
ltR :: (f x, f x, f Bool) -> (f x, f x, f Bool)
ltR ( f x
x, f x
y, f Bool
z )
  = let ( f Bool
notZ', f Bool
_ ) = (f Bool, f Bool) -> (f Bool, f Bool)
forall (f :: * -> *).
BooleanR f =>
(f Bool, f Bool) -> (f Bool, f Bool)
notR ( f Bool
forall a. Monoid a => a
mempty, f Bool
z )
        ( f x
x', f x
y', f Bool
notZR ) = (f x, f x, f Bool) -> (f x, f x, f Bool)
forall (f :: * -> *) x.
(OrdR f, OrdC f x) =>
(f x, f x, f Bool) -> (f x, f x, f Bool)
gteR ( f x
x, f x
y, f Bool
notZ' )
        ( f Bool
_, f Bool
z' ) = (f Bool, f Bool) -> (f Bool, f Bool)
forall (f :: * -> *).
BooleanR f =>
(f Bool, f Bool) -> (f Bool, f Bool)
notR ( f Bool
notZR, f Bool
forall a. Monoid a => a
mempty )

    in ( f x
x', f x
y', f Bool
z' )

instance OrdR Defined where
  type OrdC Defined = Ord

  lteR :: (Defined x, Defined x, Defined Bool)
-> (Defined x, Defined x, Defined Bool)
lteR ( Defined x
x, Defined x
y, Defined Bool
_ ) = ( Defined x
forall a. Monoid a => a
mempty, Defined x
forall a. Monoid a => a
mempty, (x -> x -> Bool) -> Defined x -> Defined x -> Defined Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 x -> x -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Defined x
x Defined x
y )

class (Ord x, Intersectable x) => OrdIntersectable (x :: Type)
instance (Ord x, Intersectable x) => OrdIntersectable x

instance OrdR Intersect where
  type OrdC Intersect = OrdIntersectable

  lteR :: (Intersect x, Intersect x, Intersect Bool)
-> (Intersect x, Intersect x, Intersect Bool)
lteR ( Intersect x
x, Intersect x
y, Intersect Bool
z )
    = ( if | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR  -> (x -> Bool) -> Intersect x -> Intersect x
forall x. (x -> Bool) -> Intersect x -> Intersect x
Intersect.filter (x -> x -> Bool
forall a. Ord a => a -> a -> Bool
<= Intersect x -> x
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Intersect x
y) Intersect x
x
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> (x -> Bool) -> Intersect x -> Intersect x
forall x. (x -> Bool) -> Intersect x -> Intersect x
Intersect.filter ( x -> x -> Bool
forall a. Ord a => a -> a -> Bool
> Intersect x -> x
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Intersect x
y) Intersect x
x
           | Bool
otherwise   -> Intersect x
forall a. Monoid a => a
mempty

      , if | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR  -> (x -> Bool) -> Intersect x -> Intersect x
forall x. (x -> Bool) -> Intersect x -> Intersect x
Intersect.filter (x -> x -> Bool
forall a. Ord a => a -> a -> Bool
>= Intersect x -> x
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum Intersect x
x) Intersect x
y
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> (x -> Bool) -> Intersect x -> Intersect x
forall x. (x -> Bool) -> Intersect x -> Intersect x
Intersect.filter ( x -> x -> Bool
forall a. Ord a => a -> a -> Bool
< Intersect x -> x
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum Intersect x
x) Intersect x
y
           | Bool
otherwise   -> Intersect x
forall a. Monoid a => a
mempty

      , (x -> x -> Bool) -> Intersect x -> Intersect x -> Intersect Bool
forall this that result.
(Intersectable this, Intersectable that, Intersectable result) =>
(this -> that -> result)
-> Intersect this -> Intersect that -> Intersect result
Intersect.lift2 x -> x -> Bool
forall a. Ord a => a -> a -> Bool
(<=) Intersect x
x Intersect x
y
      )