{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Bool (
  PBool (..),
  PEq (..),
  PPartialOrd (..),
  POrd,
  pif,
  pif',
  pnot,
  (#&&),
  (#||),
  por,
  pand,
  pand',
  por',
) 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.Internal (
  PDelayed,
  S,
  Term,
  pdelay,
  pforce,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom)
import Plutarch.Internal.Other (
  pto,
 )
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (PInner, PlutusType, pcon, pcon', pmatch, pmatch')
import Plutarch.Lift (
  DerivePConstantDirect (DerivePConstantDirect),
  PConstantDecl,
  PLifted,
  PUnsafeLiftDecl,
  pconstant,
 )
import Plutarch.Unsafe (punsafeBuiltin)
import PlutusCore qualified as PLC

-- | Plutus 'BuiltinBool'
data PBool (s :: S) = PTrue | PFalse
  deriving stock (Int -> PBool s -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: S). Int -> PBool s -> ShowS
forall (s :: S). [PBool s] -> ShowS
forall (s :: S). PBool s -> String
showList :: [PBool s] -> ShowS
$cshowList :: forall (s :: S). [PBool s] -> ShowS
show :: PBool s -> String
$cshow :: forall (s :: S). PBool s -> String
showsPrec :: Int -> PBool s -> ShowS
$cshowsPrec :: forall (s :: S). Int -> PBool s -> ShowS
Show)

instance PUnsafeLiftDecl PBool where type PLifted PBool = Bool
deriving via (DerivePConstantDirect Bool PBool) instance PConstantDecl Bool

instance PlutusType PBool where
  type PInner PBool = PBool
  pcon' :: forall (s :: S). PBool s -> Term s (PInner PBool)
pcon' PBool s
PTrue = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  pcon' PBool s
PFalse = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PBool) -> (PBool s -> Term s b) -> Term s b
pmatch' Term s (PInner PBool)
b PBool s -> Term s b
f = forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInner PBool)
b forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PBool s -> Term s b
f forall (s :: S). PBool s
PTrue) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PBool s -> Term s b
f forall (s :: S). PBool s
PFalse)

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 = forall (t :: PType) (s :: S).
(PGeneric t, PlutusType t, All2 @PType PEq (PCode t)) =>
Term s (t :--> (t :--> PBool))
gpeq forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s t
b

infix 4 #==

-- | Partial ordering relation.
class PEq t => PPartialOrd t where
  (#<=) :: Term s t -> Term s t -> Term s PBool
  default (#<=) :: (POrd (PInner t)) => Term s t -> Term s t -> Term s PBool
  Term s t
x #<= Term s t
y = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
x forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
y
  (#<) :: Term s t -> Term s t -> Term s PBool
  default (#<) :: (POrd (PInner t)) => Term s t -> Term s t -> Term s PBool
  Term s t
x #< Term s t
y = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
x forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s t
y

infix 4 #<=
infix 4 #<

-- | Total ordering relation.
class PPartialOrd t => POrd t

instance PEq PBool where
  Term s PBool
x #== :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#== Term s PBool
y' = forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PBool
y' forall a b. (a -> b) -> a -> b
$ \Term s PBool
y -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S). Term s (PBool :--> PBool)
pnot forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y

instance PPartialOrd PBool where
  Term s PBool
x #< :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#< Term s PBool
y = forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y
  Term s PBool
x #<= :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#<= Term s PBool
y = forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True

instance POrd PBool

{- | Strict version of 'pif'.
 Emits slightly less code.
-}
pif' :: Term s (PBool :--> a :--> a :--> a)
pif' :: forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IfThenElse

-- | Lazy if-then-else.
pif :: Term s PBool -> Term s a -> Term s a -> Term s a
pif :: forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
b Term s a
case_true Term s a
case_false = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PBool
b forall a b. (a -> b) -> a -> b
$ \case
  PBool s
PTrue -> Term s a
case_true
  PBool s
PFalse -> Term s a
case_false

-- | Boolean negation for 'PBool' terms.
pnot :: Term s (PBool :--> PBool)
pnot :: forall (s :: S). Term s (PBool :--> PBool)
pnot = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
x -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue

-- | Lazily evaluated boolean and for 'PBool' terms.
infixr 3 #&&

(#&&) :: Term s PBool -> Term s PBool -> Term s PBool
Term s PBool
x #&& :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s PBool
y = forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
pand forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y

-- | Lazily evaluated boolean or for 'PBool' terms.
infixr 2 #||

(#||) :: Term s PBool -> Term s PBool -> Term s PBool
Term s PBool
x #|| :: forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s PBool
y = forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
por forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y

-- | Hoisted, Plutarch level, lazily evaluated boolean and function.
pand :: Term s (PBool :--> PDelayed PBool :--> PDelayed PBool)
pand :: forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
pand = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
x Term s (PDelayed PBool)
y -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDelayed PBool)
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse)

-- | Hoisted, Plutarch level, strictly evaluated boolean and function.
pand' :: Term s (PBool :--> PBool :--> PBool)
pand' :: forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
pand' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
x Term s PBool
y -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse

-- | Hoisted, Plutarch level, lazily evaluated boolean or function.
por :: Term s (PBool :--> PDelayed PBool :--> PDelayed PBool)
por :: forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
por = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
x -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue)

-- | Hoisted, Plutarch level, strictly evaluated boolean or function.
por' :: Term s (PBool :--> PBool :--> PBool)
por' :: forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
por' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PBool
x -> forall (s :: S) (a :: PType).
Term s (PBool :--> (a :--> (a :--> a)))
pif' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue

-- | Like Haskell's `and` but for Plutarch terms
pands :: [Term s PBool] -> Term s PBool
pands :: forall (s :: S). [Term s PBool] -> Term s PBool
pands [Term s PBool]
ts' =
  case forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Term s PBool]
ts' of
    Maybe (NonEmpty (Term s PBool))
Nothing -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PTrue
    Just NonEmpty (Term s PBool)
ts -> forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
(#&&) NonEmpty (Term s PBool)
ts

-- | 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 =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s t
x Term s t
y ->
      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 forall a b. (a -> b) -> a -> b
$ \t s
x' ->
        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 forall a b. (a -> b) -> a -> b
$ \t s
y' ->
          forall (xss :: [[PType]]) (s :: S).
All2 @PType PEq xss =>
SOP @PType (Term s) xss -> SOP @PType (Term s) xss -> Term s PBool
gpeq' (forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom t s
x') (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) =
  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
Proxy @(All PEq)) (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (s :: S). PBool s
PFalse) forall (xs :: [PType]) (s :: S).
All @PType PEq xs =>
NP @PType (Term s) xs -> NP @PType (Term s) xs -> Term s PBool
eqProd (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon 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 =
  forall (s :: S). [Term s PBool] -> Term s PBool
pands forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy PEq) forall (s :: S) (a :: PType).
PEq a =>
Term s a -> Term s a -> K @PType (Term s PBool) a
eqTerm 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 =
      forall k a (b :: k). a -> K @k a b
K forall a b. (a -> b) -> a -> b
$ Term s a
a forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
b