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

-- | 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 Data.Int (Int16, Int32, Int64, Int8)
import Data.Unrestricted.Linear
import Data.Word (Word16, Word32, Word64, Word8)
import Prelude.Linear.Internal
import qualified Prelude

-- | 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 forall a. Eq a => a %1 -> a %1 -> Bool
/= a
y)
  infix 4 == -- same fixity as base.==
  (/=) :: a %1 -> a %1 -> Bool
  a
x /= a
y = Bool %1 -> Bool
not (a
x forall a. Eq a => a %1 -> a %1 -> Bool
== a
y)
  infix 4 /= -- same fixity as base./=

-- * Instances

instance (Prelude.Eq a) => Eq (Ur a) where
  Ur a
x == :: Ur a %1 -> Ur a %1 -> Bool
== Ur a
y = a
x 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 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
y Bool %1 -> Bool %1 -> Bool
&& [a]
xs forall a. Eq a => a %1 -> a %1 -> Bool
== [a]
ys
  [a]
xs == [a]
ys = ([a]
xs, [a]
ys) 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
y
  Maybe a
x == Maybe a
y = (Maybe a
x, Maybe a
y) 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
y
  Prelude.Right b
x == Prelude.Right b
y = b
x 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) 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b forall a. Eq a => a %1 -> a %1 -> Bool
== b
b' Bool %1 -> Bool %1 -> Bool
&& c
c 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 forall a. Eq a => a %1 -> a %1 -> Bool
== a
a' Bool %1 -> Bool %1 -> Bool
&& b
b forall a. Eq a => a %1 -> a %1 -> Bool
== b
b' Bool %1 -> Bool %1 -> Bool
&& c
c forall a. Eq a => a %1 -> a %1 -> Bool
== c
c' Bool %1 -> Bool %1 -> Bool
&& d
d 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

deriving via MovableEq Int16 instance Eq Int16

deriving via MovableEq Int32 instance Eq Int32

deriving via MovableEq Int64 instance Eq Int64

deriving via MovableEq Int8 instance Eq Int8

deriving via MovableEq Word16 instance Eq Word16

deriving via MovableEq Word32 instance Eq Word32

deriving via MovableEq Word64 instance Eq Word64

deriving via MovableEq Word8 instance Eq Word8

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 =
    forall a. Movable a => a %1 -> Ur a
move (a
ar, a
br) forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \(Ur (a
a, a
b)) ->
      a
a forall a. Eq a => a -> a -> Bool
Prelude.== a
b

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