module Plutarch.Internal.Eq (
  PEq (..),
) where

import Data.List.NonEmpty (nonEmpty)
import Generics.SOP (
  All,
  All2,
  HCollapse (hcollapse),
  K (K),
  NP,
  Proxy (Proxy),
  SOP (SOP),
  ccompare_NS,
  hcliftA2,
 )
import Plutarch.Builtin.Bool (
  PBool (PFalse, PTrue),
  pif',
  pnot,
  (#&&),
 )
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  PlutusType,
  pcon,
  pmatch,
 )
import Plutarch.Internal.Term (
  Term,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  (:-->),
 )

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