-- | 'Eq' instances for core data types.

{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module PlutusCore.Core.Instance.Eq () where

import PlutusPrelude

import PlutusCore.Core.Type
import PlutusCore.DeBruijn
import PlutusCore.Eq
import PlutusCore.Name
import PlutusCore.Rename.Monad

import Universe

instance (GEq uni, Eq ann) => Eq (Type TyName uni ann) where
    Type TyName uni ann
ty1 == :: Type TyName uni ann -> Type TyName uni ann -> Bool
== Type TyName uni ann
ty2 = Monoid TypeRenaming => EqRename TypeRenaming -> Bool
forall ren. Monoid ren => EqRename ren -> Bool
runEqRename @TypeRenaming (EqRename TypeRenaming -> Bool) -> EqRename TypeRenaming -> Bool
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ann -> EqRename TypeRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type TyName uni ann
ty1 Type TyName uni ann
ty2

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

-- Simple Structural Equality of a `Term NamedDeBruijn`. This implies three things:
-- b) We do not do equality "modulo starting index". E.g. `LamAbs 0 (Var 0) /= LamAbs 1 (Var 1)`.
-- c) We do not do equality ""modulo annotations".
-- Note that we ignore the name part in case of the nameddebruijn
-- 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 NamedTyDeBruijn NamedDeBruijn uni fun ann)

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

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) =>
   Eq (Type NamedTyDeBruijn uni ann)

deriving stock instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq ann) =>
   Eq (Type TyDeBruijn uni ann)

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

type EqRenameOf ren a = HasUniques a => a -> a -> EqRename ren

-- See Note [Modulo alpha].
-- See Note [Scope tracking]
-- See Note [Side tracking]
-- See Note [No catch-all].
-- | Check equality of two 'Type's.
eqTypeM :: (HasRenaming ren TypeUnique, GEq uni, Eq ann) => EqRenameOf ren (Type tyname uni ann)
eqTypeM :: Type tyname uni ann -> Type tyname uni ann -> EqRename ren
eqTypeM (TyVar ann
ann1 tyname
name1) (TyVar ann
ann2 tyname
name2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    tyname -> tyname -> EqRename ren
forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM tyname
name1 tyname
name2
eqTypeM (TyLam ann
ann1 tyname
name1 Kind ann
kind1 Type tyname uni ann
ty1) (TyLam ann
ann2 tyname
name2 Kind ann
kind2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname -> tyname -> EqRename ren -> EqRename ren
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 tyname
name1 tyname
name2 (EqRename ren -> EqRename ren) -> EqRename ren -> EqRename ren
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTypeM (TyForall ann
ann1 tyname
name1 Kind ann
kind1 Type tyname uni ann
ty1) (TyForall ann
ann2 tyname
name2 Kind ann
kind2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname -> tyname -> EqRename ren -> EqRename ren
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 tyname
name1 tyname
name2 (EqRename ren -> EqRename ren) -> EqRename ren -> EqRename ren
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTypeM (TyIFix ann
ann1 Type tyname uni ann
pat1 Type tyname uni ann
arg1) (TyIFix ann
ann2 Type tyname uni ann
pat2 Type tyname uni ann
arg2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
pat1 Type tyname uni ann
pat2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
eqTypeM (TyApp ann
ann1 Type tyname uni ann
fun1 Type tyname uni ann
arg1) (TyApp ann
ann2 Type tyname uni ann
fun2 Type tyname uni ann
arg2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
fun1 Type tyname uni ann
fun2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
eqTypeM (TyFun ann
ann1 Type tyname uni ann
dom1 Type tyname uni ann
cod1) (TyFun ann
ann2 Type tyname uni ann
dom2 Type tyname uni ann
cod2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
dom1 Type tyname uni ann
dom2
    Type tyname uni ann -> Type tyname uni ann -> EqRename ren
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
cod1 Type tyname uni ann
cod2
eqTypeM (TyBuiltin ann
ann1 SomeTypeIn uni
bi1) (TyBuiltin ann
ann2 SomeTypeIn uni
bi2) = do
    ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    SomeTypeIn uni -> SomeTypeIn uni -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM SomeTypeIn uni
bi1 SomeTypeIn uni
bi2
eqTypeM TyVar{}     Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyLam{}     Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyForall{}  Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyIFix{}    Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyApp{}     Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyFun{}     Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyBuiltin{} Type tyname uni ann
_ = EqRename ren
forall (f :: * -> *) a. Alternative f => f a
empty

-- See Note [Modulo alpha].
-- See Note [Scope tracking]
-- See Note [Side tracking]
-- See Note [No catch-all].
-- | Check equality of two 'Term's.
eqTermM
    :: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann)
    => EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM :: Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
eqTermM (LamAbs ann
ann1 name
name1 Type tyname uni ann
ty1 Term tyname name uni fun ann
body1) (LamAbs ann
ann2 name
name2 Type tyname uni ann
ty2 Term tyname name uni fun ann
body2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
    name -> name -> EqRename ScopedRenaming -> EqRename ScopedRenaming
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 ScopedRenaming -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
body1 Term tyname name uni fun ann
body2
eqTermM (TyAbs ann
ann1 tyname
name1 Kind ann
kind1 Term tyname name uni fun ann
body1) (TyAbs ann
ann2 tyname
name2 Kind ann
kind2 Term tyname name uni fun ann
body2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Kind ann -> Kind ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM Kind ann
kind1 Kind ann
kind2
    tyname
-> tyname -> EqRename ScopedRenaming -> EqRename ScopedRenaming
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 tyname
name1 tyname
name2 (EqRename ScopedRenaming -> EqRename ScopedRenaming)
-> EqRename ScopedRenaming -> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
body1 Term tyname name uni fun ann
body2
eqTermM (IWrap ann
ann1 Type tyname uni ann
pat1 Type tyname uni ann
arg1 Term tyname name uni fun ann
term1) (IWrap ann
ann2 Type tyname uni ann
pat2 Type tyname uni ann
arg2 Term tyname name uni fun ann
term2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
pat1 Type tyname uni ann
pat2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
arg1 Type tyname uni ann
arg2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
eqTermM (Apply ann
ann1 Term tyname name uni fun ann
fun1 Term tyname name uni fun ann
arg1) (Apply ann
ann2 Term tyname name uni fun ann
fun2 Term tyname name uni fun ann
arg2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
fun1 Term tyname name uni fun ann
fun2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
arg1 Term tyname name uni fun ann
arg2
eqTermM (Unwrap ann
ann1 Term tyname name uni fun ann
term1) (Unwrap ann
ann2 Term tyname name uni fun ann
term2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
eqTermM (Error ann
ann1 Type tyname uni ann
ty1) (Error ann
ann2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTermM (TyInst ann
ann1 Term tyname name uni fun ann
term1 Type tyname uni ann
ty1) (TyInst ann
ann2 Term tyname name uni fun ann
term2 Type tyname uni ann
ty2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Term tyname name uni fun ann
-> Term tyname name uni fun ann -> EqRename ScopedRenaming
forall (uni :: * -> *) fun ann tyname name.
(GEq uni, Closed uni, Everywhere uni Eq, Eq fun, Eq ann) =>
EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM Term tyname name uni fun ann
term1 Term tyname name uni fun ann
term2
    Type tyname uni ann
-> Type tyname uni ann -> EqRename ScopedRenaming
forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
eqTypeM Type tyname uni ann
ty1 Type tyname uni ann
ty2
eqTermM (Var ann
ann1 name
name1) (Var ann
ann2 name
name2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    name -> name -> EqRename ScopedRenaming
forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM name
name1 name
name2
eqTermM (Constant ann
ann1 Some (ValueOf uni)
con1) (Constant ann
ann2 Some (ValueOf uni)
con2) = do
    ann -> ann -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    Some (ValueOf uni) -> Some (ValueOf uni) -> EqRename ScopedRenaming
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 ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
    fun -> fun -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM fun
bi1 fun
bi2
eqTermM LamAbs{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyAbs{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM IWrap{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Apply{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Unwrap{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Error{}    Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyInst{}   Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Var{}      Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constant{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Builtin{}  Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall (f :: * -> *) a. Alternative f => f a
empty