-- editorconfig-checker-disable-file
{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module UntypedPlutusCore.Core.Instance.Eq () where

import PlutusPrelude

import UntypedPlutusCore.Core.Type

import PlutusCore.DeBruijn
import PlutusCore.Eq
import PlutusCore.Name.Unique
import PlutusCore.Rename.Monad

import Universe

import Data.Hashable
import Data.Vector qualified as V

instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
            Eq (Term Name uni fun ann) where
    Term Name uni fun ann
term1 == :: Term Name uni fun ann -> Term Name uni fun ann -> Bool
== Term Name uni fun ann
term2 = EqRename (Renaming TermUnique) -> Bool
forall ren. Monoid ren => EqRename ren -> Bool
runEqRename (EqRename (Renaming TermUnique) -> Bool)
-> EqRename (Renaming TermUnique) -> Bool
forall a b. (a -> b) -> a -> b
$ Term Name uni fun ann
-> Term Name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term Name uni fun ann
term1 Term Name uni fun ann
term2

type HashableTermConstraints uni fun ann =
  ( GEq uni
  , Closed uni
  , uni `Everywhere` Eq
  , uni `Everywhere` Hashable
  , Hashable ann
  , Hashable fun
  )

-- This instance is the only logical one, and exists also in the package `vector-instances`.
-- Since this is the same implementation as that one, there isn't even much risk of incoherence.
instance Hashable a => Hashable (V.Vector a) where
  hashWithSalt :: Int -> Vector a -> Int
hashWithSalt Int
s = Int -> [a] -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s ([a] -> Int) -> (Vector a -> [a]) -> Vector a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector a -> [a]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance HashableTermConstraints uni fun ann => Hashable (Term Name uni fun ann)

-- Simple Structural Equality of a `Term NamedDeBruijn`. This implies three things:
-- a) We ignore the name part of the nameddebruijn
-- b) We do not do equality "modulo init index, see deBruijnInitIndex". E.g. `LamAbs 0 (Var 0) /= LamAbs 1 (Var 1)`.
-- c) We do not do equality ""modulo annotations".
-- If a user wants to ignore annotations he must prior do `void <$> term`, to throw away any annotations.
deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term NamedDeBruijn uni fun ann)

instance HashableTermConstraints uni fun ann => Hashable (Term NamedDeBruijn uni fun ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term FakeNamedDeBruijn uni fun ann)

instance HashableTermConstraints uni fun ann => Hashable (Term FakeNamedDeBruijn uni fun ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term DeBruijn uni fun ann)

instance HashableTermConstraints uni fun ann => Hashable (Term DeBruijn uni fun ann)

deriving stock instance (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann,
                  Eq (Term name uni fun ann)
                  ) =>  Eq (Program name uni fun ann)

-- | Check equality of two 'Term's.
eqTermM
    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann, HasUnique name TermUnique)
    => Term name uni fun ann -> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM :: forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM (Constant ann
ann1 Some (ValueOf uni)
con1) (Constant ann
ann2 Some (ValueOf uni)
con2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Some (ValueOf uni)
-> Some (ValueOf uni) -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM Some (ValueOf uni)
con1 Some (ValueOf uni)
con2
eqTermM (Builtin ann
ann1 fun
bi1) (Builtin ann
ann2 fun
bi2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    fun -> fun -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM fun
bi1 fun
bi2
eqTermM (Var ann
ann1 name
name1) (Var ann
ann2 name
name2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    name -> name -> EqRename (Renaming TermUnique)
forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM name
name1 name
name2
eqTermM (LamAbs ann
ann1 name
name1 Term name uni fun ann
body1) (LamAbs ann
ann2 name
name2 Term name uni fun ann
body2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    name
-> name
-> EqRename (Renaming TermUnique)
-> EqRename (Renaming TermUnique)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings name
name1 name
name2 (EqRename (Renaming TermUnique) -> EqRename (Renaming TermUnique))
-> EqRename (Renaming TermUnique) -> EqRename (Renaming TermUnique)
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
body1 Term name uni fun ann
body2
eqTermM (Apply ann
ann1 Term name uni fun ann
fun1 Term name uni fun ann
arg1) (Apply ann
ann2 Term name uni fun ann
fun2 Term name uni fun ann
arg2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
fun1 Term name uni fun ann
fun2
    Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
arg1 Term name uni fun ann
arg2
eqTermM (Delay ann
ann1 Term name uni fun ann
term1) (Delay ann
ann2 Term name uni fun ann
term2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
term1 Term name uni fun ann
term2
eqTermM (Force ann
ann1 Term name uni fun ann
term1) (Force ann
ann2 Term name uni fun ann
term2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
term1 Term name uni fun ann
term2
eqTermM (Error ann
ann1) (Error ann
ann2) = ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
eqTermM (Constr ann
ann1 Word64
i1 [Term name uni fun ann]
args1) (Constr ann
ann2 Word64
i2 [Term name uni fun ann]
args2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Word64 -> Word64 -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM Word64
i1 Word64
i2
    case [Term name uni fun ann]
-> [Term name uni fun ann]
-> Maybe [(Term name uni fun ann, Term name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term name uni fun ann]
args1 [Term name uni fun ann]
args2 of
        Just [(Term name uni fun ann, Term name uni fun ann)]
ps -> [(Term name uni fun ann, Term name uni fun ann)]
-> ((Term name uni fun ann, Term name uni fun ann)
    -> EqRename (Renaming TermUnique))
-> EqRename (Renaming TermUnique)
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term name uni fun ann, Term name uni fun ann)]
ps (((Term name uni fun ann, Term name uni fun ann)
  -> EqRename (Renaming TermUnique))
 -> EqRename (Renaming TermUnique))
-> ((Term name uni fun ann, Term name uni fun ann)
    -> EqRename (Renaming TermUnique))
-> EqRename (Renaming TermUnique)
forall a b. (a -> b) -> a -> b
$ \(Term name uni fun ann
t1, Term name uni fun ann
t2) -> Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
t1 Term name uni fun ann
t2
        Maybe [(Term name uni fun ann, Term name uni fun ann)]
Nothing -> EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM (Case ann
ann1 Term name uni fun ann
a1 Vector (Term name uni fun ann)
cs1) (Case ann
ann2 Term name uni fun ann
a2 Vector (Term name uni fun ann)
cs2) = do
    ann -> ann -> EqRename (Renaming TermUnique)
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
a1 Term name uni fun ann
a2
    case [Term name uni fun ann]
-> [Term name uni fun ann]
-> Maybe [(Term name uni fun ann, Term name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact (Vector (Term name uni fun ann) -> [Term name uni fun ann]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Vector (Term name uni fun ann)
cs1) (Vector (Term name uni fun ann) -> [Term name uni fun ann]
forall a. Vector a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Vector (Term name uni fun ann)
cs2) of
        Just [(Term name uni fun ann, Term name uni fun ann)]
ps -> [(Term name uni fun ann, Term name uni fun ann)]
-> ((Term name uni fun ann, Term name uni fun ann)
    -> EqRename (Renaming TermUnique))
-> EqRename (Renaming TermUnique)
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term name uni fun ann, Term name uni fun ann)]
ps (((Term name uni fun ann, Term name uni fun ann)
  -> EqRename (Renaming TermUnique))
 -> EqRename (Renaming TermUnique))
-> ((Term name uni fun ann, Term name uni fun ann)
    -> EqRename (Renaming TermUnique))
-> EqRename (Renaming TermUnique)
forall a b. (a -> b) -> a -> b
$ \(Term name uni fun ann
t1, Term name uni fun ann
t2) -> Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
forall (uni :: * -> *) fun ann name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann,
 HasUnique name TermUnique) =>
Term name uni fun ann
-> Term name uni fun ann -> EqRename (Renaming TermUnique)
eqTermM Term name uni fun ann
t1 Term name uni fun ann
t2
        Maybe [(Term name uni fun ann, Term name uni fun ann)]
Nothing -> EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constant{} Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Builtin{}  Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Var{}      Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM LamAbs{}   Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Apply{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Delay{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Force{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Error{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constr{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Case{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall a. RenameT (Bilateral (Renaming TermUnique)) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty