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

{-# 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
import PlutusCore.Rename.Monad

import Universe

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

-- 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 instance
   (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
   Eq (Term NamedDeBruijn uni fun ann)

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

deriving 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 :: 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 Constant{} Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Builtin{}  Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Var{}      Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM LamAbs{}   Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Apply{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Delay{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Force{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Error{}    Term name uni fun ann
_ = EqRename (Renaming TermUnique)
forall (f :: * -> *) a. Alternative f => f a
empty