{-# 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, pnot, (#&&))
import Plutarch.Builtin.ByteString (
  PByte,
  PByteString,
  PEndianness,
  PLogicOpSemantics,
 )
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PBuiltinPair (PBuiltinPair),
  PData,
 )
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 :: S -> Type) (s :: S).
(PGeneric t, PlutusType t, All2 @(S -> Type) 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
x Term s PBool
y (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y)

-- Helpers

-- | Generic version of (#==)
gpeq ::
  forall t s.
  ( PGeneric t
  , PlutusType t
  , All2 PEq (PCode t)
  ) =>
  Term s (t :--> t :--> PBool)
gpeq :: forall (t :: S -> Type) (s :: S).
(PGeneric t, PlutusType t, All2 @(S -> Type) PEq (PCode t)) =>
Term s (t :--> (t :--> PBool))
gpeq =
  (forall (s' :: S). Term s' (t :--> (t :--> PBool)))
-> Term s (t :--> (t :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (t :--> (t :--> PBool)))
 -> Term s (t :--> (t :--> PBool)))
-> (forall (s' :: S). Term s' (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 :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
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 :: S -> Type) (s :: S) (b :: S -> Type).
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 :: S -> Type) (s :: S) (b :: S -> Type).
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 @(S -> Type) (Term s') (PCode t)
-> SOP @(S -> Type) (Term s') (PCode t) -> Term s' PBool
forall (xss :: [[S -> Type]]) (s :: S).
All2 @(S -> Type) PEq xss =>
SOP @(S -> Type) (Term s) xss
-> SOP @(S -> Type) (Term s) xss -> Term s PBool
gpeq' (t s' -> SOP @(S -> Type) (Term s') (PCode t)
forall (a :: S -> Type) (s :: S).
PGeneric a =>
a s -> SOP @(S -> Type) (Term s) (PCode a)
gpfrom t s'
x') (t s' -> SOP @(S -> Type) (Term s') (PCode t)
forall (a :: S -> Type) (s :: S).
PGeneric a =>
a s -> SOP @(S -> Type) (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 :: [[S -> Type]]) (s :: S).
All2 @(S -> Type) PEq xss =>
SOP @(S -> Type) (Term s) xss
-> SOP @(S -> Type) (Term s) xss -> Term s PBool
gpeq' (SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) xss
c1) (SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) xss
c2) =
  Proxy @([S -> Type] -> Constraint) (All @(S -> Type) PEq)
-> Term s PBool
-> (forall (x :: [S -> Type]).
    All @(S -> Type) PEq x =>
    NP @(S -> Type) (Term s) x
    -> NP @(S -> Type) (Term s) x -> Term s PBool)
-> Term s PBool
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) xss
-> NS @[S -> Type] (NP @(S -> Type) (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 :: [S -> Type] -> Constraint).
Proxy @([S -> Type] -> Constraint) t
Proxy @(All PEq)) (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse) NP @(S -> Type) (Term s) x
-> NP @(S -> Type) (Term s) x -> Term s PBool
forall (x :: [S -> Type]).
All @(S -> Type) PEq x =>
NP @(S -> Type) (Term s) x
-> NP @(S -> Type) (Term s) x -> Term s PBool
forall (xs :: [S -> Type]) (s :: S).
All @(S -> Type) PEq xs =>
NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (Term s) xs -> Term s PBool
eqProd (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse) NS @[S -> Type] (NP @(S -> Type) (Term s)) xss
c1 NS @[S -> Type] (NP @(S -> Type) (Term s)) xss
c2

eqProd :: All PEq xs => NP (Term s) xs -> NP (Term s) xs -> Term s PBool
eqProd :: forall (xs :: [S -> Type]) (s :: S).
All @(S -> Type) PEq xs =>
NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (Term s) xs -> Term s PBool
eqProd NP @(S -> Type) (Term s) xs
p1 NP @(S -> Type) (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 @(S -> Type) (K @(S -> Type) (Term s PBool)) xs
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool)
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> Type)) 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 @(S -> Type) (K @(S -> Type) (Term s PBool)) xs
 -> CollapseTo
      @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool))
-> NP @(S -> Type) (K @(S -> Type) (Term s PBool)) xs
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PEq
-> (forall (a :: S -> Type).
    PEq a =>
    Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a)
-> Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s) xs
-> NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (K @(S -> Type) (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 @((S -> Type) -> Constraint) PEq
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy PEq) Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a
forall (s :: S) (a :: S -> Type).
PEq a =>
Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a
forall (a :: S -> Type).
PEq a =>
Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a
eqTerm Prod @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s) xs
NP @(S -> Type) (Term s) xs
p1 NP @(S -> Type) (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 :: S -> Type).
PEq a =>
Term s a -> Term s a -> K @(S -> Type) (Term s PBool) a
eqTerm Term s a
a Term s a
b =
      Term s PBool -> K @(S -> Type) (Term s PBool) a
forall k a (b :: k). a -> K @k a b
K (Term s PBool -> K @(S -> Type) (Term s PBool) a)
-> Term s PBool -> K @(S -> Type) (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 :: S -> Type) (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 :: S -> Type) (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

-- | @since 1.10.0
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData Term s (PData :--> (PData :--> PBool))
-> Term s PData -> Term s (PData :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type} {list :: (S -> Type) -> S -> Type}
       {a :: S -> Type} {list :: (S -> Type) -> S -> Type} {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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
ys
    where
      -- TODO: This is copied from ListLike. See if there's a way to not do this
      plistEquals :: Term s (list a :--> (list a :--> a))
plistEquals =
        (forall (s' :: S). Term s' (list a :--> (list a :--> a)))
-> Term s (list a :--> (list a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (list a :--> (list a :--> a)))
 -> Term s (list a :--> (list a :--> a)))
-> (forall (s' :: S). Term s' (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))
 -> Term s' (list a :--> (list a :--> a)))
-> Term s' (list a :--> (list a :--> a))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s' (list a :--> (list a :--> a))
  -> Term s' (list a :--> (list a :--> a)))
 -> Term s' (list a :--> (list a :--> a)))
-> (Term s' (list a :--> (list a :--> a))
    -> Term s' (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))
self -> (Term s' (list a) -> Term s' (list a) -> Term s' a)
-> Term s' (list a :--> (list a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' (list a) -> Term s' a)
-> Term s' (c :--> (list a :--> a))
plam ((Term s' (list a) -> Term s' (list a) -> Term s' 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))
forall a b. (a -> b) -> a -> b
$ \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 :: S -> Type) (s :: S) (r :: S -> Type).
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 :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 :: S -> Type) (s :: S) (r :: S -> Type).
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 :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (list a)
ys) (AsHaskell a -> Term s' a
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
False)) (AsHaskell a -> Term s' a
forall (a :: S -> Type) (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 :: S -> Type) (s :: S) (r :: S -> Type).
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 :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(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 :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell a
False) (AsHaskell a -> Term s' a
forall (a :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinList a) -> Term s (PAsData (PBuiltinList a))
forall (a :: S -> Type) (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 :: S -> Type) (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)
-> (PBuiltinPair a b s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinPair a b)
p1 ((PBuiltinPair a b s -> Term s PBool) -> Term s PBool)
-> (PBuiltinPair a b s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s a
p1x Term s b
p1y) ->
    Term s (PBuiltinPair a b)
-> (PBuiltinPair a b s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinPair a b)
p2 ((PBuiltinPair a b s -> Term s PBool) -> Term s PBool)
-> (PBuiltinPair a b s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s a
p2x Term s b
p2y) ->
      Term s a
p1x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
p2x Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s b
p1y Term s b -> Term s b -> Term s PBool
forall (s :: S). Term s b -> Term s b -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s b
p2y

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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsByteString Term s (PByteString :--> (PByteString :--> PBool))
-> Term s PByteString -> Term s (PByteString :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
y

-- | @since 1.10.0
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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsInteger Term s (PByte :--> (PByte :--> PBool))
-> Term s PByte -> Term s (PByte :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsString Term s (PString :--> (PString :--> PBool))
-> Term s PString -> Term s (PString :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBuiltinBLS12_381_G2_Element
y

-- | @since 1.10.0
deriving anyclass instance PEq PEndianness