module Plutarch.Maybe (
  -- * Type
  PMaybe (..),

  -- * Functions

  -- ** Introduction
  pjust,
  pnothing,

  -- ** Predicates
  pisJust,

  -- ** Eliminators
  pfromJust,
  ptraceIfNothing,
  pfromMaybe,
  pmaybe,
  passertPJust,
  pmapMaybe,
) where

import Data.Kind (Type)
import GHC.Generics (Generic)
import Plutarch.Builtin.Bool (PBool)
import Plutarch.Internal.Eq (PEq)
import Plutarch.Internal.Lift (
  PLiftable (
    AsHaskell,
    PlutusRepr,
    fromPlutarch,
    fromPlutarchRepr,
    toPlutarch,
    toPlutarchRepr
  ),
  PLiftedClosed,
  fromPlutarchReprClosed,
  getPLifted,
  mkPLifted,
  pconstant,
  toPlutarchReprClosed,
 )
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  PlutusType,
  pcon,
  pmatch,
 )
import Plutarch.Internal.ScottEncoding (PlutusTypeScott)
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  (#),
  (:-->),
 )
import Plutarch.Show (PShow)
import Plutarch.String (PString)
import Plutarch.Trace (ptraceInfoError)

-- | Plutus Maybe type, with Scott-encoded repr
data PMaybe (a :: S -> Type) (s :: S)
  = PJust (Term s a)
  | PNothing
  deriving stock ((forall x. PMaybe a s -> Rep (PMaybe a s) x)
-> (forall x. Rep (PMaybe a s) x -> PMaybe a s)
-> Generic (PMaybe a s)
forall x. Rep (PMaybe a s) x -> PMaybe a s
forall x. PMaybe a s -> Rep (PMaybe a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x.
Rep (PMaybe a s) x -> PMaybe a s
forall (a :: S -> Type) (s :: S) x.
PMaybe a s -> Rep (PMaybe a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PMaybe a s -> Rep (PMaybe a s) x
from :: forall x. PMaybe a s -> Rep (PMaybe a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PMaybe a s) x -> PMaybe a s
to :: forall x. Rep (PMaybe a s) x -> PMaybe a s
Generic)
  deriving anyclass ((forall (s :: S). PMaybe a s -> Term s (PInner (PMaybe a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PMaybe a)) -> (PMaybe a s -> Term s b) -> Term s b)
-> PlutusType (PMaybe a)
forall (s :: S). PMaybe a s -> Term s (PInner (PMaybe a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PMaybe a)) -> (PMaybe a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PMaybe a s -> Term s (PInner (PMaybe a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PMaybe a)) -> (PMaybe a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PMaybe a s -> Term s (PInner (PMaybe a))
pcon' :: forall (s :: S). PMaybe a s -> Term s (PInner (PMaybe a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PMaybe a)) -> (PMaybe a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PMaybe a)) -> (PMaybe a s -> Term s b) -> Term s b
PlutusType, (forall (s :: S).
 Term s (PMaybe a) -> Term s (PMaybe a) -> Term s PBool)
-> PEq (PMaybe a)
forall (s :: S).
Term s (PMaybe a) -> Term s (PMaybe a) -> Term s PBool
forall (a :: S -> Type) (s :: S).
PEq a =>
Term s (PMaybe a) -> Term s (PMaybe a) -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (a :: S -> Type) (s :: S).
PEq a =>
Term s (PMaybe a) -> Term s (PMaybe a) -> Term s PBool
#== :: forall (s :: S).
Term s (PMaybe a) -> Term s (PMaybe a) -> Term s PBool
PEq, (forall (s :: S). Bool -> Term s (PMaybe a) -> Term s PString)
-> PShow (PMaybe a)
forall (s :: S). Bool -> Term s (PMaybe a) -> Term s PString
forall (a :: S -> Type) (s :: S).
PShow a =>
Bool -> Term s (PMaybe a) -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (a :: S -> Type) (s :: S).
PShow a =>
Bool -> Term s (PMaybe a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PMaybe a) -> Term s PString
PShow)

instance DerivePlutusType (PMaybe a) where type DPTStrat _ = PlutusTypeScott

-- | @since WIP
instance PLiftable a => PLiftable (PMaybe a) where
  type AsHaskell (PMaybe a) = Maybe (AsHaskell a)
  type PlutusRepr (PMaybe a) = PLiftedClosed (PMaybe a)

  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PMaybe a) -> PlutusRepr (PMaybe a)
toPlutarchRepr = AsHaskell (PMaybe a) -> PlutusRepr (PMaybe a)
forall (a :: S -> Type).
(PLiftable a,
 (PlutusRepr a :: Type) ~ (PLiftedClosed a :: Type)) =>
AsHaskell a -> PlutusRepr a
toPlutarchReprClosed

  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PMaybe a) -> PLifted @(S -> Type) s (PMaybe a)
toPlutarch (Just AsHaskell a
a) = Term s (PMaybe a) -> PLifted @(S -> Type) s (PMaybe a)
forall (s :: S) (a :: S -> Type).
Term s a -> PLifted @(S -> Type) s a
mkPLifted (Term s (PMaybe a) -> PLifted @(S -> Type) s (PMaybe a))
-> Term s (PMaybe a) -> PLifted @(S -> Type) s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ Term s (a :--> PMaybe a)
forall (a :: S -> Type) (s :: S). Term s (a :--> PMaybe a)
pjust Term s (a :--> PMaybe a) -> Term s a -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @a AsHaskell a
a
  toPlutarch Maybe (AsHaskell a)
AsHaskell (PMaybe a)
Nothing = Term s (PMaybe a) -> PLifted @(S -> Type) s (PMaybe a)
forall (s :: S) (a :: S -> Type).
Term s a -> PLifted @(S -> Type) s a
mkPLifted Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing

  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PMaybe a) -> Maybe (AsHaskell (PMaybe a))
fromPlutarchRepr = PlutusRepr (PMaybe a) -> Maybe (AsHaskell (PMaybe a))
forall (a :: S -> Type).
(PLiftable a,
 (PlutusRepr a :: Type) ~ (PLiftedClosed a :: Type)) =>
PlutusRepr a -> Maybe (AsHaskell a)
fromPlutarchReprClosed

  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @(S -> Type) s (PMaybe a))
-> Either LiftError (AsHaskell (PMaybe a))
fromPlutarch forall (s :: S). PLifted @(S -> Type) s (PMaybe a)
t = do
    Bool
isJust' <- (forall (s :: S). PLifted @(S -> Type) s PBool)
-> Either LiftError (AsHaskell PBool)
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted @(S -> Type) s a)
-> Either LiftError (AsHaskell a)
fromPlutarch ((forall (s :: S). PLifted @(S -> Type) s PBool)
 -> Either LiftError (AsHaskell PBool))
-> (forall (s :: S). PLifted @(S -> Type) s PBool)
-> Either LiftError (AsHaskell PBool)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> PLifted @(S -> Type) s PBool
forall (s :: S) (a :: S -> Type).
Term s a -> PLifted @(S -> Type) s a
mkPLifted (Term s PBool -> PLifted @(S -> Type) s PBool)
-> Term s PBool -> PLifted @(S -> Type) s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PMaybe a :--> PBool)
forall (a :: S -> Type) (s :: S). Term s (PMaybe a :--> PBool)
pisJust Term s (PMaybe a :--> PBool) -> Term s (PMaybe a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted @(S -> Type) s (PMaybe a) -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type).
PLifted @(S -> Type) s a -> Term s a
getPLifted PLifted @(S -> Type) s (PMaybe a)
forall (s :: S). PLifted @(S -> Type) s (PMaybe a)
t
    if Bool
isJust'
      then (AsHaskell a -> Maybe (AsHaskell a))
-> Either LiftError (AsHaskell a)
-> Either LiftError (Maybe (AsHaskell a))
forall a b. (a -> b) -> Either LiftError a -> Either LiftError b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap AsHaskell a -> Maybe (AsHaskell a)
forall a. a -> Maybe a
Just (Either LiftError (AsHaskell a)
 -> Either LiftError (Maybe (AsHaskell a)))
-> Either LiftError (AsHaskell a)
-> Either LiftError (Maybe (AsHaskell a))
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). PLifted @(S -> Type) s a)
-> Either LiftError (AsHaskell a)
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted @(S -> Type) s a)
-> Either LiftError (AsHaskell a)
fromPlutarch ((forall (s :: S). PLifted @(S -> Type) s a)
 -> Either LiftError (AsHaskell a))
-> (forall (s :: S). PLifted @(S -> Type) s a)
-> Either LiftError (AsHaskell a)
forall a b. (a -> b) -> a -> b
$ Term s a -> PLifted @(S -> Type) s a
forall (s :: S) (a :: S -> Type).
Term s a -> PLifted @(S -> Type) s a
mkPLifted (Term s a -> PLifted @(S -> Type) s a)
-> Term s a -> PLifted @(S -> Type) s a
forall a b. (a -> b) -> a -> b
$ Term s (PMaybe a :--> a)
forall (a :: S -> Type) (s :: S). Term s (PMaybe a :--> a)
pfromJust Term s (PMaybe a :--> a) -> Term s (PMaybe a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted @(S -> Type) s (PMaybe a) -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type).
PLifted @(S -> Type) s a -> Term s a
getPLifted PLifted @(S -> Type) s (PMaybe a)
forall (s :: S). PLifted @(S -> Type) s (PMaybe a)
t
      else Maybe (AsHaskell a) -> Either LiftError (Maybe (AsHaskell a))
forall a b. b -> Either a b
Right Maybe (AsHaskell a)
forall a. Maybe a
Nothing

-- | Extracts the element out of a 'PJust' and throws an error if its argument is 'PNothing'.
pfromJust ::
  forall (a :: S -> Type) (s :: S).
  Term s (PMaybe a :--> a)
pfromJust :: forall (a :: S -> Type) (s :: S). Term s (PMaybe a :--> a)
pfromJust = ClosedTerm (PMaybe a :--> a) -> Term s (PMaybe a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybe a :--> a) -> Term s (PMaybe a :--> a))
-> ClosedTerm (PMaybe a :--> a) -> Term s (PMaybe a :--> a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybe a) -> Term s a) -> Term s (PMaybe a :--> a)
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 a) -> Term s (c :--> a)
plam ((Term s (PMaybe a) -> Term s a) -> Term s (PMaybe a :--> a))
-> (Term s (PMaybe a) -> Term s a) -> Term s (PMaybe a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybe a)
t -> Term s (PMaybe a) -> (PMaybe a s -> Term s a) -> Term s a
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
t ((PMaybe a s -> Term s a) -> Term s a)
-> (PMaybe a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
    PMaybe a s
PNothing -> Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"pfromJust: found PNothing"
    PJust Term s a
x -> Term s a
x

{- | Extracts the element out of a 'PJust' and throws a custom error if it's given a 'PNothing'.

@since WIP
-}
ptraceIfNothing ::
  forall (a :: S -> Type) (s :: S).
  -- | The custom error message.
  Term s PString ->
  Term s (PMaybe a) ->
  Term s a
ptraceIfNothing :: forall (a :: S -> Type) (s :: S).
Term s PString -> Term s (PMaybe a) -> Term s a
ptraceIfNothing Term s PString
err Term s (PMaybe a)
t = Term s (PMaybe a) -> (PMaybe a s -> Term s a) -> Term s a
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
t ((PMaybe a s -> Term s a) -> Term s a)
-> (PMaybe a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
  PMaybe a s
PNothing -> Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
err
  PJust Term s a
x -> Term s a
x

{- | Yields true if the given 'PMaybe' value is of form @'PJust' _@.

@since WIP
-}
pisJust ::
  forall (a :: S -> Type) (s :: S).
  Term s (PMaybe a :--> PBool)
pisJust :: forall (a :: S -> Type) (s :: S). Term s (PMaybe a :--> PBool)
pisJust = ClosedTerm (PMaybe a :--> PBool) -> Term s (PMaybe a :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybe a :--> PBool) -> Term s (PMaybe a :--> PBool))
-> ClosedTerm (PMaybe a :--> PBool) -> Term s (PMaybe a :--> PBool)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybe a) -> Term s PBool) -> Term s (PMaybe a :--> 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 (PMaybe a) -> Term s PBool)
 -> Term s (PMaybe a :--> PBool))
-> (Term s (PMaybe a) -> Term s PBool)
-> Term s (PMaybe a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybe a)
v' ->
    Term s (PMaybe a) -> (PMaybe a s -> Term s PBool) -> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
v' ((PMaybe a s -> Term s PBool) -> Term s PBool)
-> (PMaybe a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
      PJust Term s a
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
      PMaybe a s
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False

{- | Extract a 'PMaybe' by providing a default value in case of 'PJust'.

@since WIP
-}
pfromMaybe ::
  forall (a :: S -> Type) (s :: S).
  Term s (a :--> PMaybe a :--> a)
pfromMaybe :: forall (a :: S -> Type) (s :: S). Term s (a :--> (PMaybe a :--> a))
pfromMaybe = ClosedTerm (a :--> (PMaybe a :--> a))
-> Term s (a :--> (PMaybe a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PMaybe a :--> a))
 -> Term s (a :--> (PMaybe a :--> a)))
-> ClosedTerm (a :--> (PMaybe a :--> a))
-> Term s (a :--> (PMaybe a :--> a))
forall a b. (a -> b) -> a -> b
$
  (Term s a -> Term s (PMaybe a) -> Term s a)
-> Term s (a :--> (PMaybe a :--> a))
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 (PMaybe a) -> Term s a)
-> Term s (c :--> (PMaybe a :--> a))
plam ((Term s a -> Term s (PMaybe a) -> Term s a)
 -> Term s (a :--> (PMaybe a :--> a)))
-> (Term s a -> Term s (PMaybe a) -> Term s a)
-> Term s (a :--> (PMaybe a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
e Term s (PMaybe a)
a -> Term s (PMaybe a) -> (PMaybe a s -> Term s a) -> Term s a
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
a ((PMaybe a s -> Term s a) -> Term s a)
-> (PMaybe a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
    PJust Term s a
a' -> Term s a
a'
    PMaybe a s
PNothing -> Term s a
e

{- | Construct a 'PJust' value.

@since WIP
-}
pjust ::
  forall (a :: S -> Type) (s :: S).
  Term s (a :--> PMaybe a)
pjust :: forall (a :: S -> Type) (s :: S). Term s (a :--> PMaybe a)
pjust = ClosedTerm (a :--> PMaybe a) -> Term s (a :--> PMaybe a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> PMaybe a) -> Term s (a :--> PMaybe a))
-> ClosedTerm (a :--> PMaybe a) -> Term s (a :--> PMaybe a)
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (PMaybe a)) -> Term s (a :--> PMaybe a)
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 (PMaybe a)) -> Term s (c :--> PMaybe a)
plam ((Term s a -> Term s (PMaybe a)) -> Term s (a :--> PMaybe a))
-> (Term s a -> Term s (PMaybe a)) -> Term s (a :--> PMaybe a)
forall a b. (a -> b) -> a -> b
$ PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe a s -> Term s (PMaybe a))
-> (Term s a -> PMaybe a s) -> Term s a -> Term s (PMaybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> PMaybe a s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust

{- | Construct a 'PNothing' value.

@since WIP
-}
pnothing ::
  forall (a :: S -> Type) (s :: S).
  Term s (PMaybe a)
pnothing :: forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing = ClosedTerm (PMaybe a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybe a) -> Term s (PMaybe a))
-> ClosedTerm (PMaybe a) -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe a s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing

{- | Given a default value, a function and a 'PMaybe' value, yields the default
value if the 'PMaybe' value is 'PNothing' and applies the function to the
value stored in the 'PJust' otherwise.

@since WIP
-}
pmaybe ::
  forall (b :: S -> Type) (a :: S -> Type) (s :: S).
  Term s (b :--> (a :--> b) :--> PMaybe a :--> b)
pmaybe :: forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
pmaybe = ClosedTerm (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
-> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
 -> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b))))
-> ClosedTerm (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
-> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
forall a b. (a -> b) -> a -> b
$
  (Term s b -> Term s (a :--> b) -> Term s (PMaybe a) -> Term s b)
-> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
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 (a :--> b) -> Term s (PMaybe a) -> Term s b)
-> Term s (c :--> ((a :--> b) :--> (PMaybe a :--> b)))
plam ((Term s b -> Term s (a :--> b) -> Term s (PMaybe a) -> Term s b)
 -> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b))))
-> (Term s b -> Term s (a :--> b) -> Term s (PMaybe a) -> Term s b)
-> Term s (b :--> ((a :--> b) :--> (PMaybe a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s b
d Term s (a :--> b)
f -> (Term s (PMaybe a) -> (PMaybe a s -> Term s b) -> Term s b)
-> (PMaybe a s -> Term s b) -> Term s (PMaybe a) -> Term s b
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term s (PMaybe a) -> (PMaybe a s -> Term s b) -> Term s b
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch ((PMaybe a s -> Term s b) -> Term s (PMaybe a) -> Term s b)
-> (PMaybe a s -> Term s b) -> Term s (PMaybe a) -> Term s b
forall a b. (a -> b) -> a -> b
$ \case
    PJust Term s a
v -> Term s (a :--> b)
f Term s (a :--> b) -> Term s a -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
v
    PMaybe a s
_ -> Term s b
d

{- | Extract the value stored in a 'PMaybe' container. If there's no value,
throw an error with the given message.

@since WIP
-}
passertPJust ::
  forall (a :: S -> Type) (s :: S).
  Term s (PString :--> PMaybe a :--> a)
passertPJust :: forall (a :: S -> Type) (s :: S).
Term s (PString :--> (PMaybe a :--> a))
passertPJust = ClosedTerm (PString :--> (PMaybe a :--> a))
-> Term s (PString :--> (PMaybe a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PString :--> (PMaybe a :--> a))
 -> Term s (PString :--> (PMaybe a :--> a)))
-> ClosedTerm (PString :--> (PMaybe a :--> a))
-> Term s (PString :--> (PMaybe a :--> a))
forall a b. (a -> b) -> a -> b
$
  (Term s PString -> Term s (PMaybe a) -> Term s a)
-> Term s (PString :--> (PMaybe a :--> a))
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 (PMaybe a) -> Term s a)
-> Term s (c :--> (PMaybe a :--> a))
plam ((Term s PString -> Term s (PMaybe a) -> Term s a)
 -> Term s (PString :--> (PMaybe a :--> a)))
-> (Term s PString -> Term s (PMaybe a) -> Term s a)
-> Term s (PString :--> (PMaybe a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PString
emsg Term s (PMaybe a)
mv' -> Term s (PMaybe a) -> (PMaybe a s -> Term s a) -> Term s a
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
mv' ((PMaybe a s -> Term s a) -> Term s a)
-> (PMaybe a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
    PJust Term s a
v -> Term s a
v
    PMaybe a s
_ -> Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
emsg

{- | Map underlying value if `PMaybe` is `PJust`, do nothing if it is `PNothing`

@since WIP
-}
pmapMaybe :: Term s ((a :--> b) :--> PMaybe a :--> PMaybe b)
pmapMaybe :: forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
pmapMaybe = ClosedTerm ((a :--> b) :--> (PMaybe a :--> PMaybe b))
-> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> b) :--> (PMaybe a :--> PMaybe b))
 -> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b)))
-> ClosedTerm ((a :--> b) :--> (PMaybe a :--> PMaybe b))
-> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
forall a b. (a -> b) -> a -> b
$
  (Term s (a :--> b) -> Term s (PMaybe a) -> Term s (PMaybe b))
-> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
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 (PMaybe a) -> Term s (PMaybe b))
-> Term s (c :--> (PMaybe a :--> PMaybe b))
plam ((Term s (a :--> b) -> Term s (PMaybe a) -> Term s (PMaybe b))
 -> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b)))
-> (Term s (a :--> b) -> Term s (PMaybe a) -> Term s (PMaybe b))
-> Term s ((a :--> b) :--> (PMaybe a :--> PMaybe b))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f Term s (PMaybe a)
mv -> Term s (PMaybe a)
-> (PMaybe a s -> Term s (PMaybe b)) -> Term s (PMaybe b)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe a)
mv ((PMaybe a s -> Term s (PMaybe b)) -> Term s (PMaybe b))
-> (PMaybe a s -> Term s (PMaybe b)) -> Term s (PMaybe b)
forall a b. (a -> b) -> a -> b
$ \case
    PJust Term s a
v -> Term s (b :--> PMaybe b)
forall (a :: S -> Type) (s :: S). Term s (a :--> PMaybe a)
pjust Term s (b :--> PMaybe b) -> Term s b -> Term s (PMaybe b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> b)
f Term s (a :--> b) -> Term s a -> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
v)
    PMaybe a s
PNothing -> Term s (PMaybe b)
forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing