{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiWayIf #-}

{-|
Module      : Data.JoinSemilattice.Class.Boolean
Description : Relationships between boolean variables.
Copyright   : (c) Tom Harding, 2020
License     : MIT
-}
module Data.JoinSemilattice.Class.Boolean where

import Control.Applicative (liftA2)
import Data.JoinSemilattice.Class.Merge (Merge)
import Data.JoinSemilattice.Defined (Defined (..))
import Data.JoinSemilattice.Intersect (Intersect (..))
import qualified Data.JoinSemilattice.Intersect as Intersect
import Data.Kind (Type)

-- | Rather than the 'not', 'and', and 'or' functions we know and love, the
-- 'BooleanR' class presents /relationships/ that are analogous to these. The
-- main difference is that relationships are not one-way. For example, if I
-- tell you that the /output/ of @x && y@ is 'True', you can tell me what the
-- inputs are, even if your computer can't. The implementations of 'BooleanR'
-- should be such that all directions of inference are considered.
class Merge (f Bool) => BooleanR (f :: Type -> Type) where

  -- | An overloaded 'False' value.
  falseR :: f Bool

  -- | An overloaded 'True' value.
  trueR :: f Bool

  -- | A relationship between a boolean value and its opposite.
  notR :: ( f Bool, f Bool ) -> ( f Bool, f Bool )

  -- | A relationship between two boolean values and their conjunction.
  andR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool )

  -- | A relationship between two boolean values and their disjunction.
  orR :: ( f Bool, f Bool, f Bool ) -> ( f Bool, f Bool, f Bool )

instance BooleanR Defined where
  falseR :: Defined Bool
falseR = Bool -> Defined Bool
forall x. x -> Defined x
Exactly Bool
False
  trueR :: Defined Bool
trueR  = Bool -> Defined Bool
forall x. x -> Defined x
Exactly Bool
True

  notR :: (Defined Bool, Defined Bool) -> (Defined Bool, Defined Bool)
notR (Defined Bool
x, Defined Bool
y) = ( (Bool -> Bool) -> Defined Bool -> Defined Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not Defined Bool
y, (Bool -> Bool) -> Defined Bool -> Defined Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not Defined Bool
x )

  andR :: (Defined Bool, Defined Bool, Defined Bool)
-> (Defined Bool, Defined Bool, Defined Bool)
andR (Defined Bool
x, Defined Bool
y, Defined Bool
z)
    = ( if | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR                -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR Bool -> Bool -> Bool
&& Defined Bool
y Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Bool
otherwise                 -> Defined Bool
forall a. Monoid a => a
mempty

      , if | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR                -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR Bool -> Bool -> Bool
&& Defined Bool
x Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Bool
otherwise                 -> Defined Bool
forall a. Monoid a => a
mempty

      , (Bool -> Bool -> Bool)
-> Defined Bool -> Defined Bool -> Defined Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Defined Bool
x Defined Bool
y
      )

  orR :: (Defined Bool, Defined Bool, Defined Bool)
-> (Defined Bool, Defined Bool, Defined Bool)
orR (Defined Bool
x, Defined Bool
y, Defined Bool
z)
    = ( if | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR               -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR Bool -> Bool -> Bool
&& Defined Bool
y Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Bool
otherwise                 -> Defined Bool
forall a. Monoid a => a
mempty

      , if | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR               -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Defined Bool
z Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR Bool -> Bool -> Bool
&& Defined Bool
x Defined Bool -> Defined Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> Defined Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Bool
otherwise                 -> Defined Bool
forall a. Monoid a => a
mempty

      , (Bool -> Bool -> Bool)
-> Defined Bool -> Defined Bool -> Defined Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(||) Defined Bool
x Defined Bool
y
      )

instance BooleanR Intersect where
  falseR :: Intersect Bool
falseR = Bool -> Intersect Bool
forall x. Hashable x => x -> Intersect x
Intersect.singleton Bool
False
  trueR :: Intersect Bool
trueR  = Bool -> Intersect Bool
forall x. Hashable x => x -> Intersect x
Intersect.singleton Bool
True

  notR :: (Intersect Bool, Intersect Bool)
-> (Intersect Bool, Intersect Bool)
notR (Intersect Bool
x, Intersect Bool
y) = ( (Bool -> Bool) -> Intersect Bool -> Intersect Bool
forall y x.
(Eq y, Hashable y) =>
(x -> y) -> Intersect x -> Intersect y
Intersect.map Bool -> Bool
not Intersect Bool
y, (Bool -> Bool) -> Intersect Bool -> Intersect Bool
forall y x.
(Eq y, Hashable y) =>
(x -> y) -> Intersect x -> Intersect y
Intersect.map Bool -> Bool
not Intersect Bool
x )

  andR :: (Intersect Bool, Intersect Bool, Intersect Bool)
-> (Intersect Bool, Intersect Bool, Intersect Bool)
andR (Intersect Bool
x, Intersect Bool
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                -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR Bool -> Bool -> Bool
&& Intersect Bool
y Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Bool
otherwise                 -> Intersect Bool
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                -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR Bool -> Bool -> Bool
&& Intersect Bool
x Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Bool
otherwise                 -> Intersect Bool
forall a. Monoid a => a
mempty

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

  orR :: (Intersect Bool, Intersect Bool, Intersect Bool)
-> (Intersect Bool, Intersect Bool, Intersect Bool)
orR (Intersect Bool
x, Intersect Bool
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
falseR               -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR Bool -> Bool -> Bool
&& Intersect Bool
y Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Bool
otherwise                 -> Intersect Bool
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
falseR               -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR
           | Intersect Bool
z Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR Bool -> Bool -> Bool
&& Intersect Bool
x Intersect Bool -> Intersect Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
falseR -> Intersect Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR
           | Bool
otherwise                 -> Intersect Bool
forall a. Monoid a => a
mempty

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