{-# 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 Data.IntMap (IntMap)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap

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 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 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