{-# 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
deriving stock instance
(GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
Eq (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)
deriving stock instance
(GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann) =>
Eq (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)
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