{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Plutarch.Internal.Eq (
PEq (..),
) where
import Plutarch.Builtin.BLS (
PBuiltinBLS12_381_G1_Element,
PBuiltinBLS12_381_G2_Element,
)
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pif, pif', pnot, (#&&))
import Plutarch.Builtin.ByteString (
PByte,
PByteString,
PEndianness,
PLogicOpSemantics,
)
import Plutarch.Builtin.Data (
PAsData,
PBuiltinList,
PBuiltinPair,
PData,
pfstBuiltin,
psndBuiltin,
)
import Plutarch.Builtin.Integer (PInteger, peqInteger)
import Plutarch.Builtin.String (PString)
import Plutarch.Builtin.Unit (PUnit)
import Data.Kind (Type)
import Data.List.NonEmpty (nonEmpty)
import Generics.SOP (
All,
All2,
HCollapse (hcollapse),
K (K),
NP,
Proxy (Proxy),
SOP (SOP),
ccompare_NS,
hcliftA2,
)
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom)
import {-# SOURCE #-} Plutarch.Internal.IsData (PIsData, pdata)
import Plutarch.Internal.Lift (PLiftable (PlutusRepr), pconstant)
import Plutarch.Internal.ListLike (PListLike (pelimList))
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
PlutusType,
pcon,
pmatch,
)
import Plutarch.Internal.Term (
S,
Term,
phoistAcyclic,
plet,
punsafeBuiltin,
(#),
(#$),
(:-->),
)
import PlutusCore qualified as PLC
class PEq t where
(#==) :: Term s t -> Term s t -> Term s PBool
default (#==) ::
(PGeneric t, PlutusType t, All2 PEq (PCode t)) =>
Term s t ->
Term s t ->
Term s PBool
Term s t
a #== Term s t
b = Term s (t :--> (t :--> PBool))
forall (t :: PType) (s :: S).
(PGeneric t, PlutusType t, All2 @PType PEq (PCode t)) =>
Term s (t :--> (t :--> PBool))
gpeq Term s (t :--> (t :--> PBool)) -> Term s t -> Term s (t :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
a Term s (t :--> PBool) -> Term s t -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
b
infix 4 #==
instance PEq PBool where
{-# INLINEABLE (#==) #-}
Term s PBool
x #== :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#== Term s PBool
y' = Term s PBool -> (Term s PBool -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PBool
y' ((Term s PBool -> Term s PBool) -> Term s PBool)
-> (Term s PBool -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \Term s PBool
y -> Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PBool :--> (PBool :--> PBool)))
-> Term s PBool -> Term s (PBool :--> (PBool :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PBool :--> (PBool :--> PBool))
-> Term s PBool -> Term s (PBool :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y
gpeq ::
forall t s.
( PGeneric t
, PlutusType t
, All2 PEq (PCode t)
) =>
Term s (t :--> t :--> PBool)
gpeq :: forall (t :: PType) (s :: S).
(PGeneric t, PlutusType t, All2 @PType PEq (PCode t)) =>
Term s (t :--> (t :--> PBool))
gpeq =
ClosedTerm (t :--> (t :--> PBool))
-> Term s (t :--> (t :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (t :--> (t :--> PBool))
-> Term s (t :--> (t :--> PBool)))
-> ClosedTerm (t :--> (t :--> PBool))
-> Term s (t :--> (t :--> PBool))
forall a b. (a -> b) -> a -> b
$
(Term s t -> Term s t -> Term s PBool)
-> Term s (t :--> (t :--> PBool))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s t -> Term s PBool)
-> Term s (c :--> (t :--> PBool))
plam ((Term s t -> Term s t -> Term s PBool)
-> Term s (t :--> (t :--> PBool)))
-> (Term s t -> Term s t -> Term s PBool)
-> Term s (t :--> (t :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s t
x Term s t
y ->
Term s t -> (t s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s t
x ((t s -> Term s PBool) -> Term s PBool)
-> (t s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \t s
x' ->
Term s t -> (t s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s t
y ((t s -> Term s PBool) -> Term s PBool)
-> (t s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \t s
y' ->
SOP @PType (Term s) (PCode t)
-> SOP @PType (Term s) (PCode t) -> Term s PBool
forall (xss :: [[PType]]) (s :: S).
All2 @PType PEq xss =>
SOP @PType (Term s) xss -> SOP @PType (Term s) xss -> Term s PBool
gpeq' (t s -> SOP @PType (Term s) (PCode t)
forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom t s
x') (t s -> SOP @PType (Term s) (PCode t)
forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom t s
y')
gpeq' :: All2 PEq xss => SOP (Term s) xss -> SOP (Term s) xss -> Term s PBool
gpeq' :: forall (xss :: [[PType]]) (s :: S).
All2 @PType PEq xss =>
SOP @PType (Term s) xss -> SOP @PType (Term s) xss -> Term s PBool
gpeq' (SOP NS @[PType] (NP @PType (Term s)) xss
c1) (SOP NS @[PType] (NP @PType (Term s)) xss
c2) =
Proxy @([PType] -> Constraint) (All @PType PEq)
-> Term s PBool
-> (forall (x :: [PType]).
All @PType PEq x =>
NP @PType (Term s) x -> NP @PType (Term s) x -> Term s PBool)
-> Term s PBool
-> NS @[PType] (NP @PType (Term s)) xss
-> NS @[PType] (NP @PType (Term s)) xss
-> Term s PBool
forall {k} (c :: k -> Constraint)
(proxy :: (k -> Constraint) -> Type) r (f :: k -> Type)
(g :: k -> Type) (xs :: [k]).
All @k c xs =>
proxy c
-> r
-> (forall (x :: k). c x => f x -> g x -> r)
-> r
-> NS @k f xs
-> NS @k g xs
-> r
ccompare_NS (forall {k} (t :: k). Proxy @k t
forall (t :: [PType] -> Constraint).
Proxy @([PType] -> Constraint) t
Proxy @(All PEq)) (PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse) NP @PType (Term s) x -> NP @PType (Term s) x -> Term s PBool
forall (x :: [PType]).
All @PType PEq x =>
NP @PType (Term s) x -> NP @PType (Term s) x -> Term s PBool
forall (xs :: [PType]) (s :: S).
All @PType PEq xs =>
NP @PType (Term s) xs -> NP @PType (Term s) xs -> Term s PBool
eqProd (PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse) NS @[PType] (NP @PType (Term s)) xss
c1 NS @[PType] (NP @PType (Term s)) xss
c2
eqProd :: All PEq xs => NP (Term s) xs -> NP (Term s) xs -> Term s PBool
eqProd :: forall (xs :: [PType]) (s :: S).
All @PType PEq xs =>
NP @PType (Term s) xs -> NP @PType (Term s) xs -> Term s PBool
eqProd NP @PType (Term s) xs
p1 NP @PType (Term s) xs
p2 =
[Term s PBool] -> Term s PBool
forall (s :: S). [Term s PBool] -> Term s PBool
pands ([Term s PBool] -> Term s PBool) -> [Term s PBool] -> Term s PBool
forall a b. (a -> b) -> a -> b
$ NP @PType (K @PType (Term s PBool)) xs
-> CollapseTo @PType @[PType] (NP @PType) (Term s PBool)
forall (xs :: [PType]) a.
SListIN @PType @[PType] (NP @PType) xs =>
NP @PType (K @PType a) xs
-> CollapseTo @PType @[PType] (NP @PType) a
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
hcollapse (NP @PType (K @PType (Term s PBool)) xs
-> CollapseTo @PType @[PType] (NP @PType) (Term s PBool))
-> NP @PType (K @PType (Term s PBool)) xs
-> CollapseTo @PType @[PType] (NP @PType) (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Proxy @(PType -> Constraint) PEq
-> (forall (a :: PType).
PEq a =>
Term s a -> Term s a -> K @PType (Term s PBool) a)
-> Prod @PType @[PType] (NP @PType) (Term s) xs
-> NP @PType (Term s) xs
-> NP @PType (K @PType (Term s PBool)) xs
forall {k} {l} (h :: (k -> Type) -> l -> Type)
(c :: k -> Constraint) (xs :: l)
(proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
(f' :: k -> Type) (f'' :: k -> Type).
(AllN @k @l (Prod @k @l h) c xs, HAp @k @l h,
HAp @k @l (Prod @k @l h)) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a -> f'' a)
-> Prod @k @l h f xs
-> h f' xs
-> h f'' xs
hcliftA2 (Proxy @(PType -> Constraint) PEq
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy PEq) Term s a -> Term s a -> K @PType (Term s PBool) a
forall (s :: S) (a :: PType).
PEq a =>
Term s a -> Term s a -> K @PType (Term s PBool) a
forall (a :: PType).
PEq a =>
Term s a -> Term s a -> K @PType (Term s PBool) a
eqTerm Prod @PType @[PType] (NP @PType) (Term s) xs
NP @PType (Term s) xs
p1 NP @PType (Term s) xs
p2
where
eqTerm :: forall s a. PEq a => Term s a -> Term s a -> K (Term s PBool) a
eqTerm :: forall (s :: S) (a :: PType).
PEq a =>
Term s a -> Term s a -> K @PType (Term s PBool) a
eqTerm Term s a
a Term s a
b =
Term s PBool -> K @PType (Term s PBool) a
forall k a (b :: k). a -> K @k a b
K (Term s PBool -> K @PType (Term s PBool) a)
-> Term s PBool -> K @PType (Term s PBool) a
forall a b. (a -> b) -> a -> b
$ Term s a
a Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
b
pands :: [Term s PBool] -> Term s PBool
pands :: forall (s :: S). [Term s PBool] -> Term s PBool
pands [Term s PBool]
ts' =
case [Term s PBool] -> Maybe (NonEmpty (Term s PBool))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Term s PBool]
ts' of
Maybe (NonEmpty (Term s PBool))
Nothing -> PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue
Just NonEmpty (Term s PBool)
ts -> (Term s PBool -> Term s PBool -> Term s PBool)
-> NonEmpty (Term s PBool) -> Term s PBool
forall a. (a -> a -> a) -> NonEmpty a -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
(#&&) NonEmpty (Term s PBool)
ts
instance PEq PInteger where
{-# INLINEABLE (#==) #-}
Term s PInteger
x #== :: forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
#== Term s PInteger
y = Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PBool))
peqInteger Term s (PInteger :--> (PInteger :--> PBool))
-> Term s PInteger -> Term s (PInteger :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PBool) -> Term s PInteger -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y
instance PEq PData where
Term s PData
x #== :: forall (s :: S). Term s PData -> Term s PData -> Term s PBool
#== Term s PData
y = DefaultFun -> Term s (PData :--> (PData :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData Term s (PData :--> (PData :--> PBool))
-> Term s PData -> Term s (PData :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x Term s (PData :--> PBool) -> Term s PData -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
y
instance PEq (PAsData a) where
Term s (PAsData a)
x #== :: forall (s :: S).
Term s (PAsData a) -> Term s (PAsData a) -> Term s PBool
#== Term s (PAsData a)
y = DefaultFun -> Term s (PAsData a :--> (PAsData a :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData Term s (PAsData a :--> (PAsData a :--> PBool))
-> Term s (PAsData a) -> Term s (PAsData a :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
x Term s (PAsData a :--> PBool) -> Term s (PAsData a) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
y
type family F (a :: S -> Type) :: Bool where
F PData = 'True
F (PAsData _) = 'True
F _ = 'False
class Fc (x :: Bool) (a :: S -> Type) where
fc :: Proxy x -> Term s (PBuiltinList a) -> Term s (PBuiltinList a) -> Term s PBool
instance (PEq a, PLC.Contains PLC.DefaultUni (PlutusRepr a)) => Fc 'False a where
fc :: forall (s :: S).
Proxy @Bool 'False
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc Proxy @Bool 'False
_ Term s (PBuiltinList a)
xs Term s (PBuiltinList a)
ys = Term s (PBuiltinList a :--> (PBuiltinList a :--> PBool))
forall {a :: PType} {list :: PType -> PType} {a :: PType}
{list :: PType -> PType} {s :: S}.
((AsHaskell a :: Type) ~ (Bool :: Type), PElemConstraint list a,
PElemConstraint list a, PListLike list, PListLike list, PEq a,
PLiftable a) =>
Term s (list a :--> (list a :--> a))
plistEquals Term s (PBuiltinList a :--> (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a) -> Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs Term s (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
ys
where
plistEquals :: Term s (list a :--> (list a :--> a))
plistEquals =
ClosedTerm (list a :--> (list a :--> a))
-> Term s (list a :--> (list a :--> a))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list a :--> a))
-> Term s (list a :--> (list a :--> a)))
-> ClosedTerm (list a :--> (list a :--> a))
-> Term s (list a :--> (list a :--> a))
forall a b. (a -> b) -> a -> b
$
Term
s
(((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a)))
:--> (list a :--> (list a :--> a)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s
(((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a)))
:--> (list a :--> (list a :--> a)))
-> Term
s
((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a)))
-> Term s (list a :--> (list a :--> a))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list a :--> a))
-> Term s (list a) -> Term s (list a) -> Term s a)
-> Term
s
((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a)))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (list a) -> Term s (list a) -> Term s a)
-> Term s (c :--> (list a :--> (list a :--> a)))
plam ((Term s (list a :--> (list a :--> a))
-> Term s (list a) -> Term s (list a) -> Term s a)
-> Term
s
((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a))))
-> (Term s (list a :--> (list a :--> a))
-> Term s (list a) -> Term s (list a) -> Term s a)
-> Term
s
((list a :--> (list a :--> a)) :--> (list a :--> (list a :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list a :--> a))
self Term s (list a)
xlist Term s (list a)
ylist ->
(Term s a -> Term s (list a) -> Term s a)
-> Term s a -> Term s (list a) -> Term s a
forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
( \Term s a
x Term s (list a)
xs ->
(Term s a -> Term s (list a) -> Term s a)
-> Term s a -> Term s (list a) -> Term s a
forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
y Term s (list a)
ys -> Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
y) (Term s (list a :--> (list a :--> a))
self Term s (list a :--> (list a :--> a))
-> Term s (list a) -> Term s (list a :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list a :--> a) -> Term s (list a) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
ys) (AsHaskell a -> Term s a
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
False)) (AsHaskell a -> Term s a
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
False) Term s (list a)
ylist
)
((Term s a -> Term s (list a) -> Term s a)
-> Term s a -> Term s (list a) -> Term s a
forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
_ Term s (list a)
_ -> AsHaskell a -> Term s a
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
False) (AsHaskell a -> Term s a
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
True) Term s (list a)
ylist)
Term s (list a)
xlist
instance PIsData (PBuiltinList a) => Fc 'True a where
fc :: forall (s :: S).
Proxy @Bool 'True
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc Proxy @Bool 'True
_ Term s (PBuiltinList a)
xs Term s (PBuiltinList a)
ys = Term s (PBuiltinList a) -> Term s (PAsData (PBuiltinList a))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList a)
xs Term s (PAsData (PBuiltinList a))
-> Term s (PAsData (PBuiltinList a)) -> Term s PBool
forall (s :: S).
Term s (PAsData (PBuiltinList a))
-> Term s (PAsData (PBuiltinList a)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinList a) -> Term s (PAsData (PBuiltinList a))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList a)
ys
instance Fc (F a) a => PEq (PBuiltinList a) where
#== :: forall (s :: S).
Term s (PBuiltinList a) -> Term s (PBuiltinList a) -> Term s PBool
(#==) = Proxy @Bool (F a)
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
forall (x :: Bool) (a :: PType) (s :: S).
Fc x a =>
Proxy @Bool x
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
forall (s :: S).
Proxy @Bool (F a)
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc (forall (t :: Bool). Proxy @Bool t
forall {k} (t :: k). Proxy @k t
Proxy @(F a))
instance (PEq a, PEq b) => PEq (PBuiltinPair a b) where
Term s (PBuiltinPair a b)
p1 #== :: forall (s :: S).
Term s (PBuiltinPair a b)
-> Term s (PBuiltinPair a b) -> Term s PBool
#== Term s (PBuiltinPair a b)
p2 = Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p2 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 Term s b -> Term s b -> Term s PBool
forall (s :: S). Term s b -> Term s b -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p2
instance PEq PByteString where
Term s PByteString
x #== :: forall (s :: S).
Term s PByteString -> Term s PByteString -> Term s PBool
#== Term s PByteString
y = DefaultFun -> Term s (PByteString :--> (PByteString :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsByteString Term s (PByteString :--> (PByteString :--> PBool))
-> Term s PByteString -> Term s (PByteString :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
x Term s (PByteString :--> PBool)
-> Term s PByteString -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
y
instance PEq PByte where
{-# INLINEABLE (#==) #-}
Term s PByte
x #== :: forall (s :: S). Term s PByte -> Term s PByte -> Term s PBool
#== Term s PByte
y = DefaultFun -> Term s (PByte :--> (PByte :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsInteger Term s (PByte :--> (PByte :--> PBool))
-> Term s PByte -> Term s (PByte :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
x Term s (PByte :--> PBool) -> Term s PByte -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByte
y
deriving anyclass instance PEq PLogicOpSemantics
instance PEq PUnit where
Term s PUnit
x #== :: forall (s :: S). Term s PUnit -> Term s PUnit -> Term s PBool
#== Term s PUnit
y = Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
x \Term s PUnit
_ -> Term s PUnit -> (Term s PUnit -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PUnit
y \Term s PUnit
_ -> PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue
instance PEq PString where
Term s PString
x #== :: forall (s :: S). Term s PString -> Term s PString -> Term s PBool
#== Term s PString
y = DefaultFun -> Term s (PString :--> (PString :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsString Term s (PString :--> (PString :--> PBool))
-> Term s PString -> Term s (PString :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PString
x Term s (PString :--> PBool) -> Term s PString -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PString
y
instance PEq PBuiltinBLS12_381_G1_Element where
Term s PBuiltinBLS12_381_G1_Element
x #== :: forall (s :: S).
Term s PBuiltinBLS12_381_G1_Element
-> Term s PBuiltinBLS12_381_G1_Element -> Term s PBool
#== Term s PBuiltinBLS12_381_G1_Element
y = DefaultFun
-> Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PBuiltinBLS12_381_G1_Element :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.Bls12_381_G1_equal Term
s
(PBuiltinBLS12_381_G1_Element
:--> (PBuiltinBLS12_381_G1_Element :--> PBool))
-> Term s PBuiltinBLS12_381_G1_Element
-> Term s (PBuiltinBLS12_381_G1_Element :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
x Term s (PBuiltinBLS12_381_G1_Element :--> PBool)
-> Term s PBuiltinBLS12_381_G1_Element -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G1_Element
y
instance PEq PBuiltinBLS12_381_G2_Element where
Term s PBuiltinBLS12_381_G2_Element
x #== :: forall (s :: S).
Term s PBuiltinBLS12_381_G2_Element
-> Term s PBuiltinBLS12_381_G2_Element -> Term s PBool
#== Term s PBuiltinBLS12_381_G2_Element
y = DefaultFun
-> Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PBuiltinBLS12_381_G2_Element :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.Bls12_381_G2_equal Term
s
(PBuiltinBLS12_381_G2_Element
:--> (PBuiltinBLS12_381_G2_Element :--> PBool))
-> Term s PBuiltinBLS12_381_G2_Element
-> Term s (PBuiltinBLS12_381_G2_Element :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
x Term s (PBuiltinBLS12_381_G2_Element :--> PBool)
-> Term s PBuiltinBLS12_381_G2_Element -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
y
deriving anyclass instance PEq PEndianness