{-# 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

-- Helpers

-- | Generic version of (#==)
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

-- | @since WIP
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
      -- 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 =
        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

-- | @since WIP
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

-- | @since WIP
deriving anyclass instance PEq PEndianness