{-# 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 = forall a x. Generic a => a -> Rep a x
from t
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# 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 = forall b. Boolean b => b -> b
not (t
a forall t. Equatable t => t -> t -> Bit
=== t
b)

instance Equatable Bit where
  Bit
a === :: Bit -> Bit -> Bit
=== Bit
b = forall b. Boolean b => b -> b
not (forall b. Boolean b => b -> b -> b
xor Bit
a Bit
b)
  /== :: 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
    | forall k a. Map k a -> [k]
Map.keys Map k v
x forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> [k]
Map.keys Map k v
y = forall k a. Map k a -> [a]
Map.elems Map k v
x forall t. Equatable t => t -> t -> Bit
=== forall k a. Map k a -> [a]
Map.elems Map k v
y
    | Bool
otherwise                = forall b. Boolean b => b
false

instance Equatable v => Equatable (IntMap v) where
  IntMap v
x === :: IntMap v -> IntMap v -> Bit
=== IntMap v
y
    | forall a. IntMap a -> [Int]
IntMap.keys IntMap v
x forall a. Eq a => a -> a -> Bool
== forall a. IntMap a -> [Int]
IntMap.keys IntMap v
y = forall a. IntMap a -> [a]
IntMap.elems IntMap v
x forall t. Equatable t => t -> t -> Bit
=== forall a. IntMap a -> [a]
IntMap.elems IntMap v
y
    | Bool
otherwise                      = 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
    | forall a. Seq a -> Int
Seq.length Seq v
x forall a. Eq a => a -> a -> Bool
== forall a. Seq a -> Int
Seq.length Seq v
y = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
x forall t. Equatable t => t -> t -> Bit
=== forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq v
y
    | Bool
otherwise                    = 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 [Tree a]
xs === :: Tree a -> Tree a -> Bit
=== Tree.Node a
y [Tree a]
ys = a
x forall t. Equatable t => t -> t -> Bit
=== a
y forall b. Boolean b => b -> b -> b
&& [Tree a]
xs forall t. Equatable t => t -> t -> Bit
=== [Tree 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 ===# :: forall a. U1 a -> U1 a -> Bit
===# U1 a
U1 = forall b. Boolean b => b
true

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

instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where
  (f a
a :*: g a
b) ===# :: forall a. (:*:) f g a -> (:*:) f g a -> Bit
===# (f a
c :*: g a
d) = (f a
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
c) forall b. Boolean b => b -> b -> b
&& (g a
b 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 ===# :: forall a. (:+:) f g a -> (:+:) f g a -> Bit
===# L1 f a
b = f a
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# f a
b
  R1 g a
a ===# R1 g a
b = g a
a forall (f :: * -> *) a. GEquatable f => f a -> f a -> Bit
===# g a
b
  (:+:) f g a
_ ===# (:+:) f g a
_ = forall b. Boolean b => b
false

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

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