{-# 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.Unique
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 = 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
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
eqTypeM :: (HasRenaming ren TypeUnique, GEq uni, Eq ann) => EqRenameOf ren (Type tyname uni ann)
eqTypeM :: forall ren (uni :: * -> *) ann tyname.
(HasRenaming ren TypeUnique, GEq uni, Eq ann) =>
EqRenameOf ren (Type tyname uni ann)
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
someUni1) (TyBuiltin ann
ann2 SomeTypeIn uni
someUni2) = 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
someUni1 SomeTypeIn uni
someUni2
eqTypeM (TySOP ann
ann1 [[Type tyname uni ann]]
tyls1) (TySOP ann
ann2 [[Type tyname uni ann]]
tyls2) = do
ann -> ann -> EqRename ren
forall a ren. Eq a => a -> a -> EqRename ren
eqM ann
ann1 ann
ann2
case [[Type tyname uni ann]]
-> [[Type tyname uni ann]]
-> Maybe [([Type tyname uni ann], [Type tyname uni ann])]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [[Type tyname uni ann]]
tyls1 [[Type tyname uni ann]]
tyls2 of
Just [([Type tyname uni ann], [Type tyname uni ann])]
ps -> [([Type tyname uni ann], [Type tyname uni ann])]
-> (([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
-> EqRename ren
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [([Type tyname uni ann], [Type tyname uni ann])]
ps ((([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
-> EqRename ren)
-> (([Type tyname uni ann], [Type tyname uni ann]) -> EqRename ren)
-> EqRename ren
forall a b. (a -> b) -> a -> b
$ \([Type tyname uni ann]
ptys1, [Type tyname uni ann]
ptys2) -> case [Type tyname uni ann]
-> [Type tyname uni ann]
-> Maybe [(Type tyname uni ann, Type tyname uni ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Type tyname uni ann]
ptys1 [Type tyname uni ann]
ptys2 of
Just [(Type tyname uni ann, Type tyname uni ann)]
tys -> [(Type tyname uni ann, Type tyname uni ann)]
-> ((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
-> EqRename ren
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Type tyname uni ann, Type tyname uni ann)]
tys (((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
-> EqRename ren)
-> ((Type tyname uni ann, Type tyname uni ann) -> EqRename ren)
-> EqRename ren
forall a b. (a -> b) -> a -> b
$ \(Type tyname uni ann
ty1, Type tyname uni ann
ty2) -> 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
Maybe [(Type tyname uni ann, Type tyname uni ann)]
Nothing -> EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
Maybe [([Type tyname uni ann], [Type tyname uni ann])]
Nothing -> EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyVar{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyLam{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyForall{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyIFix{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyApp{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyFun{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TyBuiltin{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTypeM TySOP{} Type tyname uni ann
_ = EqRename ren
forall a. RenameT (Bilateral ren) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM
:: (GEq uni, Closed uni, uni `Everywhere` Eq, Eq fun, Eq ann)
=> EqRenameOf ScopedRenaming (Term tyname name uni fun ann)
eqTermM :: 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 (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 (Constr ann
ann1 Type tyname uni ann
ty1 Word64
i1 [Term tyname name uni fun ann]
args1) (Constr ann
ann2 Type tyname uni ann
ty2 Word64
i2 [Term tyname name uni fun ann]
args2) = 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
Word64 -> Word64 -> EqRename ScopedRenaming
forall a ren. Eq a => a -> a -> EqRename ren
eqM Word64
i1 Word64
i2
case [Term tyname name uni fun ann]
-> [Term tyname name uni fun ann]
-> Maybe
[(Term tyname name uni fun ann, Term tyname name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term tyname name uni fun ann]
args1 [Term tyname name uni fun ann]
args2 of
Just [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps -> [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps (((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming)
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ \(Term tyname name uni fun ann
t1, Term tyname name uni fun ann
t2) -> 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
t1 Term tyname name uni fun ann
t2
Maybe
[(Term tyname name uni fun ann, Term tyname name uni fun ann)]
Nothing -> EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM (Case ann
ann1 Type tyname uni ann
ty1 Term tyname name uni fun ann
a1 [Term tyname name uni fun ann]
cs1) (Case ann
ann2 Type tyname uni ann
ty2 Term tyname name uni fun ann
a2 [Term tyname name uni fun ann]
cs2) = 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
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
a1 Term tyname name uni fun ann
a2
case [Term tyname name uni fun ann]
-> [Term tyname name uni fun ann]
-> Maybe
[(Term tyname name uni fun ann, Term tyname name uni fun ann)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
zipExact [Term tyname name uni fun ann]
cs1 [Term tyname name uni fun ann]
cs2 of
Just [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps -> [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(Term tyname name uni fun ann, Term tyname name uni fun ann)]
ps (((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming)
-> ((Term tyname name uni fun ann, Term tyname name uni fun ann)
-> EqRename ScopedRenaming)
-> EqRename ScopedRenaming
forall a b. (a -> b) -> a -> b
$ \(Term tyname name uni fun ann
t1, Term tyname name uni fun ann
t2) -> 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
t1 Term tyname name uni fun ann
t2
Maybe
[(Term tyname name uni fun ann, Term tyname name uni fun ann)]
Nothing -> EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM LamAbs{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyAbs{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM IWrap{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Apply{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Unwrap{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Error{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM TyInst{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Var{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constant{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Builtin{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Constr{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
eqTermM Case{} Term tyname name uni fun ann
_ = EqRename ScopedRenaming
forall a. RenameT (Bilateral ScopedRenaming) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty