{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}

-- | This module provides a linear 'Eq' class for testing equality between
-- values, along with standard instances.
module Data.Ord.Linear.Internal.Eq
  ( Eq(..)
  )
  where

import Data.Bool.Linear
import qualified Prelude
import Prelude.Linear.Internal
import Data.Unrestricted.Linear

-- | Testing equality on values.
--
-- The laws are that (==) and (/=) are compatible
-- and (==) is an equivalence relation. So, for all @x@, @y@, @z@,
--
-- * @x == x@ always
-- * @x == y@ implies @y == x@
-- * @x == y@ and @y == z@ implies @x == z@
-- * @(x == y)@ ≌ @not (x /= y)@
--
class Eq a where
  {-# MINIMAL (==) | (/=) #-}
  (==) :: a %1-> a %1-> Bool
  a
x == a
y = Bool %1 -> Bool
not (a
x a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
/= a
y)
  (/=) :: a %1-> a %1-> Bool
  a
x /= a
y = Bool %1 -> Bool
not (a
x a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
y)
  infix 4 ==, /=

-- * Instances

instance Prelude.Eq a => Eq (Ur a) where
  Ur a
x == :: Ur a %1 -> Ur a %1 -> Bool
== Ur a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Prelude.== a
y
  Ur a
x /= :: Ur a %1 -> Ur a %1 -> Bool
/= Ur a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Prelude./= a
y

instance (Consumable a, Eq a) => Eq [a] where
  [] == :: [a] %1 -> [a] %1 -> Bool
== [] = Bool
True
  (a
x:[a]
xs) == (a
y:[a]
ys) = a
x a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
y Bool %1 -> Bool %1 -> Bool
&& [a]
xs [a] %1 -> [a] %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== [a]
ys
  [a]
xs == [a]
ys = ([a]
xs, [a]
ys) ([a], [a]) %1 -> Bool %1 -> Bool
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` Bool
False

instance (Consumable a, Eq a) => Eq (Prelude.Maybe a) where
  Maybe a
Prelude.Nothing == :: Maybe a %1 -> Maybe a %1 -> Bool
== Maybe a
Prelude.Nothing = Bool
True
  Prelude.Just a
x == Prelude.Just a
y = a
x a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
y
  Maybe a
x == Maybe a
y = (Maybe a
x, Maybe a
y) (Maybe a, Maybe a) %1 -> Bool %1 -> Bool
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` Bool
False

instance (Consumable a, Consumable b, Eq a, Eq b)
  => Eq (Prelude.Either a b) where
  Prelude.Left a
x == :: Either a b %1 -> Either a b %1 -> Bool
== Prelude.Left a
y = a
x a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
y
  Prelude.Right b
x == Prelude.Right b
y = b
x b %1 -> b %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== b
y
  Either a b
x == Either a b
y = (Either a b
x, Either a b
y) (Either a b, Either a b) %1 -> Bool %1 -> Bool
forall a b. Consumable a => a %1 -> b %1 -> b
`lseq` Bool
False

instance (Eq a, Eq b) => Eq (a, b) where
  (a
a, b
b) == :: (a, b) %1 -> (a, b) %1 -> Bool
== (a
a', b
b') =
    a
a a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b b %1 -> b %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== b
b'

instance (Eq a, Eq b, Eq c) => Eq (a, b, c) where
  (a
a, b
b, c
c) == :: (a, b, c) %1 -> (a, b, c) %1 -> Bool
== (a
a', b
b', c
c') =
    a
a a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b b %1 -> b %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== b
b' Bool %1 -> Bool %1 -> Bool
&& c
c c %1 -> c %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== c
c'

instance (Eq a, Eq b, Eq c, Eq d) => Eq (a, b, c, d) where
  (a
a, b
b, c
c, d
d) == :: (a, b, c, d) %1 -> (a, b, c, d) %1 -> Bool
== (a
a', b
b', c
c', d
d') =
    a
a a %1 -> a %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b b %1 -> b %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== b
b' Bool %1 -> Bool %1 -> Bool
&& c
c c %1 -> c %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== c
c' Bool %1 -> Bool %1 -> Bool
&& d
d d %1 -> d %1 -> Bool
forall a. Eq a => a %1 -> a %1 -> Bool
== d
d'

deriving via MovableEq () instance Eq ()
deriving via MovableEq Prelude.Int instance Eq Prelude.Int
deriving via MovableEq Prelude.Double instance Eq Prelude.Double
deriving via MovableEq Prelude.Bool instance Eq Prelude.Bool
deriving via MovableEq Prelude.Char instance Eq Prelude.Char
deriving via MovableEq Prelude.Ordering instance Eq Prelude.Ordering

newtype MovableEq a = MovableEq a

instance (Prelude.Eq a, Movable a) => Eq (MovableEq a) where
  MovableEq a
ar == :: MovableEq a %1 -> MovableEq a %1 -> Bool
== MovableEq a
br
    = (a, a) %1 -> Ur (a, a)
forall a. Movable a => a %1 -> Ur a
move (a
ar, a
br) Ur (a, a) %1 -> (Ur (a, a) %1 -> Bool) %1 -> Bool
forall a b. a %1 -> (a %1 -> b) %1 -> b
& \(Ur (a
a, a
b)) ->
        a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Prelude.== a
b

  MovableEq a
ar /= :: MovableEq a %1 -> MovableEq a %1 -> Bool
/= MovableEq a
br
    = (a, a) %1 -> Ur (a, a)
forall a. Movable a => a %1 -> Ur a
move (a
ar, a
br) Ur (a, a) %1 -> (Ur (a, a) %1 -> Bool) %1 -> Bool
forall a b. a %1 -> (a %1 -> b) %1 -> b
& \(Ur (a
a, a
b)) ->
        a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Prelude./= a
b