{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Equatable
  ( Equatable(..)
  , GEquatable(..)
  ) where

import Prelude hiding ((&&),(||),not,and,or,all,any)

import Ersatz.Bit
import GHC.Generics
import Numeric.Natural
import Data.IntMap (IntMap)
import Data.Foldable (toList)
import Data.Map (Map)
import Data.Int
import Data.Word
import Data.Void
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import qualified Data.Sequence as Seq
import qualified Data.Tree as Tree

infix  4 ===, /==

-- | Instances for this class for arbitrary types can be automatically derived from 'Generic'.
class Equatable t where
  -- | Compare for equality within the SAT problem.
  (===) :: t -> t -> Bit
  default (===) :: (Generic t, GEquatable (Rep t)) => t -> t -> Bit
  t
a === t
b = t -> Rep t Any
forall a x. Generic a => a -> Rep a x
from t
a Rep t Any -> Rep t Any -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# t -> Rep t Any
forall a x. Generic a => a -> Rep a x
from t
b

  -- | Compare for inequality within the SAT problem.
  (/==) :: t -> t -> Bit

  t
a /== t
b = Bit -> Bit
forall b. Boolean b => b -> b
not (t
a t -> t -> Bit
forall t. Equatable t => t -> t -> Bit
=== t
b)

instance Equatable Bit where
  Bit
a === :: Bit -> Bit -> Bit
=== Bit
b = Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
xor Bit
a Bit
b)
  /== :: Bit -> Bit -> Bit
(/==) = Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
xor

instance (Eq k, Equatable v) => Equatable (Map k v) where
  Map k v
x === :: Map k v -> Map k v -> Bit
=== Map k v
y
    | Map k v -> [k]
forall k a. Map k a -> [k]
Map.keys Map k v
x [k] -> [k] -> Bool
forall a. Eq a => a -> a -> Bool
== Map k v -> [k]
forall k a. Map k a -> [k]
Map.keys Map k v
y = Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
x [v] -> [v] -> Bit
forall t. Equatable t => t -> t -> Bit
=== Map k v -> [v]
forall k a. Map k a -> [a]
Map.elems Map k v
y
    | Bool
otherwise                = Bit
forall b. Boolean b => b
false

instance Equatable v => Equatable (IntMap v) where
  IntMap v
x === :: IntMap v -> IntMap v -> Bit
=== IntMap v
y
    | IntMap v -> [Key]
forall a. IntMap a -> [Key]
IntMap.keys IntMap v
x [Key] -> [Key] -> Bool
forall a. Eq a => a -> a -> Bool
== IntMap v -> [Key]
forall a. IntMap a -> [Key]
IntMap.keys IntMap v
y = IntMap v -> [v]
forall a. IntMap a -> [a]
IntMap.elems IntMap v
x [v] -> [v] -> Bit
forall t. Equatable t => t -> t -> Bit
=== IntMap v -> [v]
forall a. IntMap a -> [a]
IntMap.elems IntMap v
y
    | Bool
otherwise                      = Bit
forall b. Boolean b => b
false

instance Equatable v => Equatable (Seq.Seq v) where
  Seq v
x === :: Seq v -> Seq v -> Bit
=== Seq v
y
    | Seq v -> Key
forall a. Seq a -> Key
Seq.length Seq v
x Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Seq v -> Key
forall a. Seq a -> Key
Seq.length Seq v
y = Seq v -> [v]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
x [v] -> [v] -> Bit
forall t. Equatable t => t -> t -> Bit
=== Seq v -> [v]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
y
    | Bool
otherwise                    = Bit
forall b. Boolean b => b
false

-- manually written because ancient GHC didn't have the generics instance
instance Equatable a => Equatable (Tree.Tree a) where
  Tree.Node a
x Forest a
xs === :: Tree a -> Tree a -> Bit
=== Tree.Node a
y Forest a
ys = a
x a -> a -> Bit
forall t. Equatable t => t -> t -> Bit
=== a
y Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& Forest a
xs Forest a -> Forest a -> Bit
forall t. Equatable t => t -> t -> Bit
=== Forest a
ys

instance (Equatable a, Equatable b) => Equatable (a,b)
instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)
instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)
instance Equatable a => Equatable (Maybe a)
instance Equatable a => Equatable [a]
instance Equatable a => Equatable (NonEmpty a)
instance (Equatable a, Equatable b) => Equatable (Either a b)

class GEquatable f where
  (===#) :: f a -> f a -> Bit

instance GEquatable U1 where
  U1 a
U1 ===# :: U1 a -> U1 a -> Bit
===# U1 a
U1 = Bit
forall b. Boolean b => b
true

instance GEquatable V1 where
  V1 a
x ===# :: V1 a -> V1 a -> Bit
===# V1 a
y = V1 a
x V1 a -> Bit -> Bit
`seq` V1 a
y V1 a -> Bit -> Bit
`seq` [Char] -> Bit
forall a. HasCallStack => [Char] -> a
error [Char]
"GEquatable[V1].===#"

instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where
  (f a
a :*: g a
b) ===# :: (:*:) f g a -> (:*:) f g a -> Bit
===# (f a
c :*: g a
d) = (f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c) Bit -> Bit -> Bit
forall b. Boolean b => b -> b -> b
&& (g a
b g a -> g a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# g a
d)

instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where
  L1 f a
a ===# :: (:+:) f g a -> (:+:) f g a -> Bit
===# L1 f a
b = f a
a f a -> f a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
b
  R1 g a
a ===# R1 g a
b = g a
a g a -> g a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# g a
b
  (:+:) f g a
_ ===# (:+:) f g a
_ = Bit
forall b. Boolean b => b
false

instance GEquatable f => GEquatable (M1 i c f) where
  M1 f a
x ===# :: M1 i c f a -> M1 i c f a -> Bit
===# M1 f a
y = f a
x f a -> f a -> Bit
forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
y

instance Equatable a => GEquatable (K1 i a) where
  K1 a
a ===# :: K1 i a a -> K1 i a a -> Bit
===# K1 a
b = a
a a -> a -> Bit
forall t. Equatable t => t -> t -> Bit
=== a
b

-- Boring instances that end up being useful when deriving Equatable with Generics

instance Equatable ()       where ()
_ === :: () -> () -> Bit
=== ()
_ = Bit
forall b. Boolean b => b
true
instance Equatable Void     where Void
x === :: Void -> Void -> Bit
=== Void
y = Void
x Void -> Bit -> Bit
`seq` Void
y Void -> Bit -> Bit
`seq` [Char] -> Bit
forall a. HasCallStack => [Char] -> a
error [Char]
"Equatable[Void].==="
instance Equatable Int      where Key
x === :: Key -> Key -> Bit
=== Key
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Key
x Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
y)
instance Equatable Integer  where Integer
x === :: Integer -> Integer -> Bit
=== Integer
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y)
instance Equatable Natural  where Natural
x === :: Natural -> Natural -> Bit
=== Natural
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Natural
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
y)
instance Equatable Word     where Word
x === :: Word -> Word -> Bit
=== Word
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Word
x Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
y)
instance Equatable Word8    where Word8
x === :: Word8 -> Word8 -> Bit
=== Word8
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Word8
x Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
y)
instance Equatable Word16   where Word16
x === :: Word16 -> Word16 -> Bit
=== Word16
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Word16
x Word16 -> Word16 -> Bool
forall a. Eq a => a -> a -> Bool
== Word16
y)
instance Equatable Word32   where Word32
x === :: Word32 -> Word32 -> Bit
=== Word32
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Word32
x Word32 -> Word32 -> Bool
forall a. Eq a => a -> a -> Bool
== Word32
y)
instance Equatable Word64   where Word64
x === :: Word64 -> Word64 -> Bit
=== Word64
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Word64
x Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
y)
instance Equatable Int8     where Int8
x === :: Int8 -> Int8 -> Bit
=== Int8
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Int8
x Int8 -> Int8 -> Bool
forall a. Eq a => a -> a -> Bool
== Int8
y)
instance Equatable Int16    where Int16
x === :: Int16 -> Int16 -> Bit
=== Int16
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Int16
x Int16 -> Int16 -> Bool
forall a. Eq a => a -> a -> Bool
== Int16
y)
instance Equatable Int32    where Int32
x === :: Int32 -> Int32 -> Bit
=== Int32
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Int32
x Int32 -> Int32 -> Bool
forall a. Eq a => a -> a -> Bool
== Int32
y)
instance Equatable Int64    where Int64
x === :: Int64 -> Int64 -> Bit
=== Int64
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Int64
x Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
y)
instance Equatable Char     where Char
x === :: Char -> Char -> Bit
=== Char
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
y)
instance Equatable Float    where Float
x === :: Float -> Float -> Bit
=== Float
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Float
x Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== Float
y)
instance Equatable Double   where Double
x === :: Double -> Double -> Bit
=== Double
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Double
x Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
y)
instance Equatable Ordering where Ordering
x === :: Ordering -> Ordering -> Bit
=== Ordering
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Ordering
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
y)
instance Equatable Bool     where Bool
x === :: Bool -> Bool -> Bit
=== Bool
y = Bool -> Bit
forall b. Boolean b => Bool -> b
bool (Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y)