{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Builtin.Bool (
  -- * Type
  PBool (..),

  -- * Builtin
  pbuiltinIfThenElse,

  -- * Functions
  pif',
  pif,
  pnot,
  (#&&),
  (#||),
  por,
  pand,
  pand',
  por',
  pcond,
  ptrue,
  pfalse,
) where

import Data.Kind (Type)
import Plutarch.Builtin.Opaque (popaque)
import Plutarch.Internal.Case (punsafeCase)
import {-# SOURCE #-} Plutarch.Internal.PLam (plam)
import Plutarch.Internal.Term (
  PDelayed,
  S,
  Term,
  pdelay,
  pforce,
  phoistAcyclic,
  punsafeBuiltin,
  punsafeConstantInternal,
  (#),
  (:-->),
 )
import PlutusCore qualified as PLC

{- | Builtin Plutus boolean.

@since 1.10.0
-}
data PBool (s :: S) = PTrue | PFalse
  deriving stock
    ( -- | @since 1.10.0
      Int -> PBool s -> ShowS
[PBool s] -> ShowS
PBool s -> String
(Int -> PBool s -> ShowS)
-> (PBool s -> String) -> ([PBool s] -> ShowS) -> Show (PBool s)
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
$cshowsPrec :: forall (s :: S). Int -> PBool s -> ShowS
showsPrec :: Int -> PBool s -> ShowS
$cshow :: forall (s :: S). PBool s -> String
show :: PBool s -> String
$cshowList :: forall (s :: S). [PBool s] -> ShowS
showList :: [PBool s] -> ShowS
Show
    )

ptrue :: Term (s :: S) PBool
ptrue :: forall (s :: S). Term s PBool
ptrue = Some @Type (ValueOf DefaultUni) -> Term s PBool
forall (s :: S) (a :: S -> Type).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal (Some @Type (ValueOf DefaultUni) -> Term s PBool)
-> Some @Type (ValueOf DefaultUni) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Bool -> Some @Type (ValueOf DefaultUni)
forall a (uni :: Type -> Type).
Contains @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue Bool
True

pfalse :: Term (s :: S) PBool
pfalse :: forall (s :: S). Term s PBool
pfalse = Some @Type (ValueOf DefaultUni) -> Term s PBool
forall (s :: S) (a :: S -> Type).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal (Some @Type (ValueOf DefaultUni) -> Term s PBool)
-> Some @Type (ValueOf DefaultUni) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Bool -> Some @Type (ValueOf DefaultUni)
forall a (uni :: Type -> Type).
Contains @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue Bool
False

-- | @since 1.10.0
pbuiltinIfThenElse ::
  forall (a :: S -> Type) (s :: S).
  Term s (PBool :--> a :--> a :--> PDelayed a)
pbuiltinIfThenElse :: forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> PDelayed a)))
pbuiltinIfThenElse = DefaultFun -> Term s (PBool :--> (a :--> (a :--> PDelayed a)))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IfThenElse

{- | Strict if-then-else. Emits slightly less code than the lazy version.

@since 1.10.0
-}
{-# DEPRECATED pif' "Use pif instead" #-}
pif' ::
  forall (a :: S -> Type) (s :: S).
  Term s (PBool :--> a :--> a :--> a)
pif' :: forall (a :: S -> Type) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' = (forall (s' :: S). Term s' (PBool :--> (a :--> (a :--> a))))
-> Term s (PBool :--> (a :--> (a :--> a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBool :--> (a :--> (a :--> a))))
 -> Term s (PBool :--> (a :--> (a :--> a))))
-> (forall (s' :: S). Term s' (PBool :--> (a :--> (a :--> a))))
-> Term s (PBool :--> (a :--> (a :--> a)))
forall a b. (a -> b) -> a -> b
$ Term s' (PDelayed (PBool :--> (a :--> (a :--> a))))
-> Term s' (PBool :--> (a :--> (a :--> a)))
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce (Term s' (PDelayed (PBool :--> (a :--> (a :--> a))))
 -> Term s' (PBool :--> (a :--> (a :--> a))))
-> Term s' (PDelayed (PBool :--> (a :--> (a :--> a))))
-> Term s' (PBool :--> (a :--> (a :--> a)))
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Term s' (PDelayed (PBool :--> (a :--> (a :--> a))))
forall (s :: S) (a :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IfThenElse

{- | Lazy if-then-else.

@since 1.10.0
-}
pif ::
  forall (a :: S -> Type) (s :: S).
  Term s PBool ->
  Term s a ->
  Term s a ->
  Term s a
pif :: forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
cond Term s a
ifT Term s a
ifF = Term s PBool -> [Term s POpaque] -> Term s a
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase Term s PBool
cond [Term s a -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque Term s a
ifF, Term s a -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque Term s a
ifT]

{- | Boolean negation.

@since 1.10.0
-}
pnot ::
  forall (s :: S).
  Term s (PBool :--> PBool)
pnot :: forall (s :: S). Term s (PBool :--> PBool)
pnot = (forall (s :: S). Term s (PBool :--> PBool))
-> Term s (PBool :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PBool :--> PBool))
 -> Term s (PBool :--> PBool))
-> (forall (s :: S). Term s (PBool :--> PBool))
-> Term s (PBool :--> PBool)
forall a b. (a -> b) -> a -> b
$ (Term s' PBool -> Term s' PBool) -> Term s' (PBool :--> 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' PBool) -> Term s' (c :--> PBool)
plam ((Term s' PBool -> Term s' PBool) -> Term s' (PBool :--> PBool))
-> (Term s' PBool -> Term s' PBool) -> Term s' (PBool :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s' PBool
b ->
  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
b Term s' PBool
forall (s :: S). Term s PBool
pfalse Term s' PBool
forall (s :: S). Term s PBool
ptrue

{- | Lazy AND for terms.

@since 1.10.0
-}
(#&&) :: forall (s :: S). 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 = Term s (PDelayed PBool) -> Term s PBool
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed PBool) -> Term s PBool)
-> Term s (PDelayed PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
pand Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
-> Term s PBool -> Term s (PDelayed PBool :--> PDelayed PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PDelayed PBool :--> PDelayed PBool)
-> Term s (PDelayed PBool) -> Term s (PDelayed PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y

infixr 3 #&&

{- | Lazy OR for terms.

@since 1.10.0
-}
(#||) :: forall (s :: S). 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 = Term s (PDelayed PBool) -> Term s PBool
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed PBool) -> Term s PBool)
-> Term s (PDelayed PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
por Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
-> Term s PBool -> Term s (PDelayed PBool :--> PDelayed PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PDelayed PBool :--> PDelayed PBool)
-> Term s (PDelayed PBool) -> Term s (PDelayed PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y

infixr 2 #||

{- | Hoisted lazy AND at the Plutarch level.

@since 1.10.0
-}
pand :: forall (s :: S). Term s (PBool :--> PDelayed PBool :--> PDelayed PBool)
pand :: forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
pand = (forall (s :: S).
 Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
 -> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> (forall (s :: S).
    Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall a b. (a -> b) -> a -> b
$ (Term s' PBool
 -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (PBool :--> (PDelayed PBool :--> PDelayed 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' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (c :--> (PDelayed PBool :--> PDelayed PBool))
plam ((Term s' PBool
  -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
 -> Term s' (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> (Term s' PBool
    -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall a b. (a -> b) -> a -> b
$ \Term s' PBool
x Term s' (PDelayed PBool)
y -> Term s' PBool -> Term s' (PDelayed PBool)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay (Term s' PBool -> Term s' (PDelayed PBool))
-> Term s' PBool -> Term s' (PDelayed PBool)
forall a b. (a -> b) -> a -> b
$ 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' (PDelayed PBool) -> Term s' PBool
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce Term s' (PDelayed PBool)
y) Term s' PBool
x

{- | As 'pand', but strict.

@since 1.10.0
-}
pand' :: forall (s :: S). Term s (PBool :--> PBool :--> PBool)
pand' :: forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
pand' = (forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
-> Term s (PBool :--> (PBool :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
 -> Term s (PBool :--> (PBool :--> PBool)))
-> (forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
-> Term s (PBool :--> (PBool :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s' PBool -> Term s' PBool -> Term s' PBool)
-> Term s' (PBool :--> (PBool :--> 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' PBool -> Term s' PBool)
-> Term s' (c :--> (PBool :--> PBool))
plam ((Term s' PBool -> Term s' PBool -> Term s' PBool)
 -> Term s' (PBool :--> (PBool :--> PBool)))
-> (Term s' PBool -> Term s' PBool -> Term s' PBool)
-> Term s' (PBool :--> (PBool :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s' PBool
x 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
x

{- | Hoisted lazy OR at the Plutarch level.

@since 1.10.0
-}
por :: forall (s :: S). Term s (PBool :--> PDelayed PBool :--> PDelayed PBool)
por :: forall (s :: S).
Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
por = (forall (s :: S).
 Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
 -> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> (forall (s :: S).
    Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall a b. (a -> b) -> a -> b
$ (Term s' PBool
 -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (PBool :--> (PDelayed PBool :--> PDelayed 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' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (c :--> (PDelayed PBool :--> PDelayed PBool))
plam ((Term s' PBool
  -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
 -> Term s' (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> (Term s' PBool
    -> Term s' (PDelayed PBool) -> Term s' (PDelayed PBool))
-> Term s' (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall a b. (a -> b) -> a -> b
$ \Term s' PBool
x -> Term s' PBool
-> Term s' (PDelayed PBool)
-> Term s' (PDelayed PBool)
-> Term s' (PDelayed PBool)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s' PBool
x ((forall (s' :: S). Term s' (PDelayed PBool))
-> Term s' (PDelayed PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic (Term s' PBool -> Term s' (PDelayed PBool)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay Term s' PBool
forall (s :: S). Term s PBool
ptrue))

{- | As 'por', but strict.

@since 1.10.0
-}
por' :: Term s (PBool :--> PBool :--> PBool)
por' :: forall (s :: S). Term s (PBool :--> (PBool :--> PBool))
por' = (forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
-> Term s (PBool :--> (PBool :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
 -> Term s (PBool :--> (PBool :--> PBool)))
-> (forall (s :: S). Term s (PBool :--> (PBool :--> PBool)))
-> Term s (PBool :--> (PBool :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s' PBool -> Term s' PBool -> Term s' PBool)
-> Term s' (PBool :--> (PBool :--> 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' PBool -> Term s' PBool)
-> Term s' (c :--> (PBool :--> PBool))
plam ((Term s' PBool -> Term s' PBool -> Term s' PBool)
 -> Term s' (PBool :--> (PBool :--> PBool)))
-> (Term s' PBool -> Term s' PBool -> Term s' PBool)
-> Term s' (PBool :--> (PBool :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s' PBool
x -> 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
forall (s :: S). Term s PBool
ptrue

{- | Essentially multi-way 'pif'. More precisely, given a list of
condition-action pairs, and an \'action of last resort\', construct a
left-to-right \'chain\' of @pif@s, using the conditions to determine which
action gets taken. The \'action of last resort\' finishes the \'chain\'. For
example:

> pcond [(cond1, act1), (cond2, act2)] act3

does the same thing as

> pif cond1 act1 (pif cond2 act2 act3)

@since 1.10.0
-}
pcond ::
  forall (a :: S -> Type) (s :: S).
  [(Term s PBool, Term s a)] ->
  Term s a ->
  Term s a
pcond :: forall (a :: S -> Type) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond [(Term s PBool, Term s a)]
conds Term s a
lastResort = case [(Term s PBool, Term s a)]
conds of
  [] -> Term s a
lastResort
  (Term s PBool
cond, Term s a
action) : [(Term s PBool, Term s a)]
conds' -> 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 PBool
cond Term s a
action ([(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
pcond [(Term s PBool, Term s a)]
conds' Term s a
lastResort)