-- Required for class constraints of form: c (ValueType t) :: Constraint
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DefaultSignatures #-}

module Language.Hasmtlib.Equatable where

import Prelude hiding (not, (&&))
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Boolean
import Data.Int
import Data.Word
import Data.Void
import qualified Data.Vector.Sized as V
import Numeric.Natural
import GHC.Generics

-- | Test two as on equality as SMT-Expression.
--
-- @
--     x <- var @RealType
--     y <- var
--     assert $ y === x && not (y /== x)
-- @
--
class Equatable a where
  -- | Test whether two values are equal in the SMT-Problem.
  (===) :: a -> a -> Expr BoolSort
  default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort
  a
a === a
b = a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
a Rep a Any -> Rep a Any -> Expr 'BoolSort
forall a. Rep a a -> Rep a a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
b

  -- | Test whether two values are not equal in the SMT-Problem.
  (/==) :: a -> a -> Expr BoolSort
  a
x /== a
y = Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not (Expr 'BoolSort -> Expr 'BoolSort)
-> Expr 'BoolSort -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== a
y

infix 4 ===, /==

instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where
  Expr t
x === :: Expr t -> Expr t -> Expr 'BoolSort
=== Expr t
y = Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
EQU (Vector (0 + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ (Expr t, Expr t) -> Vector (0 + 2) (Expr t)
forall input (length :: Nat) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
x,Expr t
y)
  {-# INLINE (===) #-}
  Expr t
x /== :: Expr t -> Expr t -> Expr 'BoolSort
/== Expr t
y = Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall (t1 :: SMTSort) (n :: Nat).
(Eq (HaskellType t1), KnownSMTSort t1, KnownNat n) =>
Vector (n + 2) (Expr t1) -> Expr 'BoolSort
Distinct (Vector (0 + 2) (Expr t) -> Expr 'BoolSort)
-> Vector (0 + 2) (Expr t) -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ (Expr t, Expr t) -> Vector (0 + 2) (Expr t)
forall input (length :: Nat) ty.
(IndexedListLiterals input length ty, KnownNat length) =>
input -> Vector length ty
V.fromTuple (Expr t
x,Expr t
y)
  {-# INLINE (/==) #-}

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

instance GEquatable U1 where
  U1 a
U1 ===# :: forall (a :: k). U1 a -> U1 a -> Expr 'BoolSort
===# U1 a
U1 = Expr 'BoolSort
forall b. Boolean b => b
true

instance GEquatable V1 where
  V1 a
x ===# :: forall (a :: k). V1 a -> V1 a -> Expr 'BoolSort
===# V1 a
y = V1 a
x V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` V1 a
y V1 a -> Expr 'BoolSort -> Expr 'BoolSort
forall a b. a -> b -> b
`seq` [Char] -> Expr 'BoolSort
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 :: k). (:*:) f g a -> (:*:) f g a -> Expr 'BoolSort
===# (f a
c :*: g a
d) = (f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# f a
c) Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
&& (g a
b g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# g a
d)

instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where
  L1 f a
a ===# :: forall (a :: k). (:+:) f g a -> (:+:) f g a -> Expr 'BoolSort
===# L1 f a
b = f a
a f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# f a
b
  R1 g a
a ===# R1 g a
b = g a
a g a -> g a -> Expr 'BoolSort
forall (a :: k). g a -> g a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# g a
b
  (:+:) f g a
_ ===# (:+:) f g a
_ = Expr 'BoolSort
forall b. Boolean b => b
false

instance GEquatable f => GEquatable (M1 i c f) where
  M1 f a
x ===# :: forall (a :: k). M1 i c f a -> M1 i c f a -> Expr 'BoolSort
===# M1 f a
y = f a
x f a -> f a -> Expr 'BoolSort
forall (a :: k). f a -> f a -> Expr 'BoolSort
forall {k} (f :: k -> *) (a :: k).
GEquatable f =>
f a -> f a -> Expr 'BoolSort
===# f a
y

instance Equatable a => GEquatable (K1 i a) where
  K1 a
a ===# :: forall (a :: k). K1 i a a -> K1 i a a -> Expr 'BoolSort
===# K1 a
b = a
a a -> a -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
=== a
b

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