{-# LANGUAGE UndecidableInstances #-}
module Plutarch.Builtin.Bool (
PBool (..),
pbuiltinIfThenElse,
pif',
pif,
pnot,
(#&&),
(#||),
por,
pand,
pand',
por',
pcond,
ptrue,
pfalse,
) where
import Data.Kind (Type)
import {-# SOURCE #-} Plutarch.Internal.PLam (plam)
import Plutarch.Internal.Term (
PDelayed,
S,
Term,
pdelay,
pforce,
phoistAcyclic,
punsafeBuiltin,
punsafeConstantInternal,
(#),
(:-->),
)
import PlutusCore qualified as PLC
data PBool (s :: S) = PTrue | PFalse
deriving stock
(
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 :: PType).
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 :: PType).
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
pbuiltinIfThenElse ::
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> a :--> a :--> PDelayed a)
pbuiltinIfThenElse :: forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> PDelayed a)))
pbuiltinIfThenElse = DefaultFun -> Term s (PBool :--> (a :--> (a :--> PDelayed a)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IfThenElse
pif' ::
forall (a :: S -> Type) (s :: S).
Term s (PBool :--> a :--> a :--> a)
pif' :: forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' = ClosedTerm (PBool :--> (a :--> (a :--> a)))
-> Term s (PBool :--> (a :--> (a :--> a)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBool :--> (a :--> (a :--> a)))
-> Term s (PBool :--> (a :--> (a :--> a))))
-> ClosedTerm (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 :: PType). 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 :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IfThenElse
pif ::
forall (a :: S -> Type) (s :: S).
Term s PBool ->
Term s a ->
Term s a ->
Term s a
pif :: forall (a :: PType) (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 (PDelayed a) -> Term s a
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed a) -> Term s a)
-> Term s (PDelayed a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> (PDelayed a :--> (PDelayed a :--> PDelayed a)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PDelayed a :--> (PDelayed a :--> PDelayed a)))
-> Term s PBool
-> Term s (PDelayed a :--> (PDelayed a :--> PDelayed a))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
cond Term s (PDelayed a :--> (PDelayed a :--> PDelayed a))
-> Term s (PDelayed a) -> Term s (PDelayed a :--> PDelayed a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s (PDelayed a)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s a
ifT Term s (PDelayed a :--> PDelayed a)
-> Term s (PDelayed a) -> Term s (PDelayed a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s (PDelayed a)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s a
ifF
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 :: PType) (s :: S).
HasCallStack =>
ClosedTerm 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 :: 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 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
x ->
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
forall (s :: S). Term s PBool
pfalse 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
forall (s :: S). Term s PBool
ptrue
(#&&) :: 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 :: PType). 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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y
infixr 3 #&&
(#||) :: 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 :: PType). 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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
y
infixr 2 #||
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 :: PType) (s :: S).
HasCallStack =>
ClosedTerm 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 :: 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 (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
:--> (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
s
(PBool
:--> (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s PBool
-> Term
s (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool))
-> Term s (PDelayed PBool)
-> Term s (PDelayed PBool :--> PDelayed PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDelayed PBool)
y Term s (PDelayed PBool :--> PDelayed PBool)
-> Term s (PDelayed PBool) -> Term s (PDelayed PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# ClosedTerm (PDelayed PBool) -> Term s (PDelayed PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
forall (s :: S). Term s PBool
pfalse)
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 :: PType) (s :: S).
HasCallStack =>
ClosedTerm 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 :: 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 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 :--> (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
forall (s :: S). Term s PBool
pfalse
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 :: PType) (s :: S).
HasCallStack =>
ClosedTerm 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 :--> PDelayed PBool))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed 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 (PDelayed PBool :--> PDelayed PBool))
-> Term s (c :--> (PDelayed PBool :--> PDelayed PBool))
plam ((Term s PBool -> Term s (PDelayed PBool :--> PDelayed PBool))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> (Term s PBool -> Term s (PDelayed PBool :--> PDelayed PBool))
-> Term s (PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PBool
x -> Term
s
(PBool
:--> (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term
s
(PBool
:--> (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool)))
-> Term s PBool
-> Term
s (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x Term s (PDelayed PBool :--> (PDelayed PBool :--> PDelayed PBool))
-> Term s (PDelayed PBool)
-> Term s (PDelayed PBool :--> PDelayed PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# ClosedTerm (PDelayed PBool) -> Term s (PDelayed PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (Term s PBool -> Term s (PDelayed PBool)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay Term s PBool
forall (s :: S). Term s PBool
ptrue)
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 :: PType) (s :: S).
HasCallStack =>
ClosedTerm 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 :--> PBool))
-> Term s (PBool :--> (PBool :--> 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 (PBool :--> PBool))
-> Term s (c :--> (PBool :--> PBool))
plam ((Term s PBool -> Term s (PBool :--> PBool))
-> Term s (PBool :--> (PBool :--> PBool)))
-> (Term s PBool -> Term s (PBool :--> PBool))
-> Term s (PBool :--> (PBool :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PBool
x -> 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
forall (s :: S). Term s PBool
ptrue
pcond ::
forall (a :: S -> Type) (s :: S).
[(Term s PBool, Term s a)] ->
Term s a ->
Term s a
pcond :: forall (a :: PType) (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 :: PType) (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 :: PType) (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)