{-# 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.Unrestricted.Linear
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 a %1 -> a %1 -> Bool
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 a %1 -> a %1 -> Bool
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 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) -> Bool
forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> 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) -> Bool
forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \(Ur (a
a, a
b)) ->
      a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
Prelude./= a
b