{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{- | Useful tools that aren't part of the Plutarch API per se, but get used in
multiple places.
-}
module Plutarch.LedgerApi.Utils (
  -- * Types
  Mret (..),
  PMaybeData (..),
  PRationalData (..),
  PSBool (..),

  -- * Functions

  -- ** PMaybeData
  pfromDJust,
  pisDJust,
  pmaybeData,
  pdjust,
  pdnothing,
  pmaybeToMaybeData,
  pmaybeDataToMaybe,
  passertPDJust,

  -- ** PRationalData
  prationalFromData,

  -- ** PSBool
  pmatchStrict,
  pstrue,
  psfalse,
  psif,
  psif',
  psnot,
  psand,
  psand',
  psor,
  psor',
) where

import Data.Bifunctor (first)
import Plutarch.Builtin (
  PIsData (pdataImpl, pfromDataImpl),
  pasConstr,
  pconstrBuiltin,
  pforgetData,
 )
import Plutarch.DataRepr (PDataFields)
import Plutarch.Internal.Lift (DeriveDataPLiftable)
import Plutarch.Internal.PlutusType (PlutusType (pcon', pmatch'))
import Plutarch.Positive (PPositive)
import Plutarch.Prelude
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
import Plutarch.Unsafe (punsafeCoerce)
import PlutusLedgerApi.V3 qualified as Plutus

{- | 'Term', but with its type arguments flipped. This is a useful helper for
defining 'PTryFrom' instances.

For example, consider the 'PTryFrom' instance for 'PTokenName':

@
instance PTryFrom PData (PAsData PTokenName) where
   type PTryFromExcess PData (PAsData PTokenName) = Mret PTokenName
@

We need to do this because 'PTryFromExcess' expects something of kind @S ->
Type@, but 'Term' has kind @S -> (S -> Type) -> Type@, which doesn't quite
fit. By using 'Mret', we end up with something of kind @(S -> Type)
-> S -> Type@, which fits.

The name is just 'Term' written backwards.

@since 2.0.0
-}
newtype Mret (a :: S -> Type) (s :: S) = Mret (Term s a)
  deriving stock
    ( -- | @since 2.0.0
      (forall x. Mret a s -> Rep (Mret a s) x)
-> (forall x. Rep (Mret a s) x -> Mret a s) -> Generic (Mret a s)
forall x. Rep (Mret a s) x -> Mret a s
forall x. Mret a s -> Rep (Mret 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 (Mret a s) x -> Mret a s
forall (a :: S -> Type) (s :: S) x. Mret a s -> Rep (Mret a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x. Mret a s -> Rep (Mret a s) x
from :: forall x. Mret a s -> Rep (Mret a s) x
$cto :: forall (a :: S -> Type) (s :: S) x. Rep (Mret a s) x -> Mret a s
to :: forall x. Rep (Mret a s) x -> Mret a s
Generic
    )

-- | @since WIP
data PMaybeData (a :: S -> Type) (s :: S)
  = PDJust (Term s (PAsData a))
  | PDNothing
  deriving stock
    ( -- | @since 2.0.0
      (forall x. PMaybeData a s -> Rep (PMaybeData a s) x)
-> (forall x. Rep (PMaybeData a s) x -> PMaybeData a s)
-> Generic (PMaybeData a s)
forall x. Rep (PMaybeData a s) x -> PMaybeData a s
forall x. PMaybeData a s -> Rep (PMaybeData 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 (PMaybeData a s) x -> PMaybeData a s
forall (a :: S -> Type) (s :: S) x.
PMaybeData a s -> Rep (PMaybeData a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x.
PMaybeData a s -> Rep (PMaybeData a s) x
from :: forall x. PMaybeData a s -> Rep (PMaybeData a s) x
$cto :: forall (a :: S -> Type) (s :: S) x.
Rep (PMaybeData a s) x -> PMaybeData a s
to :: forall x. Rep (PMaybeData a s) x -> PMaybeData a s
Generic
    )
  deriving anyclass
    ( -- | @since 2.0.0
      (forall (s :: S).
 Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool)
-> PEq (PMaybeData a)
forall (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
forall (a :: S -> Type) (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
$c#== :: forall (a :: S -> Type) (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
#== :: forall (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
PEq
    , -- | @since 2.0.0
      (forall (s :: S). Bool -> Term s (PMaybeData a) -> Term s PString)
-> PShow (PMaybeData a)
forall (s :: S). Bool -> Term s (PMaybeData a) -> Term s PString
forall (a :: S -> Type) (s :: S).
(PIsData a, PShow a) =>
Bool -> Term s (PMaybeData 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).
(PIsData a, PShow a) =>
Bool -> Term s (PMaybeData a) -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s (PMaybeData a) -> Term s PString
PShow
    )

-- | @since WIP
instance PlutusType (PMaybeData a) where
  type PInner (PMaybeData a) = PData
  {-# INLINEABLE pcon' #-}
  pcon' :: forall (s :: S). PMaybeData a s -> Term s (PInner (PMaybeData a))
pcon' = \case
    PDJust Term s (PAsData a)
t ->
      Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
 -> Term s PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s PInteger
-> Term
     s
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0 Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData a)
t Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
    PMaybeData a s
PDNothing ->
      Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
 -> Term s PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s PInteger
-> Term
     s
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
1 Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
  {-# INLINEABLE pmatch' #-}
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PMaybeData a))
-> (PMaybeData a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PMaybeData a))
t PMaybeData a s -> Term s b
f = Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s b)
-> Term s b
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInner (PMaybeData a))
Term s PData
t) ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s b)
 -> Term s b)
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s b)
-> Term s b
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr ->
    Term s PBool -> Term s b -> Term s b -> Term s b
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      ((Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1)
      (PMaybeData a s -> Term s b
f PMaybeData a s
forall (a :: S -> Type) (s :: S). PMaybeData a s
PDNothing)
      (PMaybeData a s -> Term s b
f (PMaybeData a s -> Term s b)
-> (Term s PData -> PMaybeData a s) -> Term s PData -> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData a) -> PMaybeData a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PMaybeData a s
PDJust (Term s (PAsData a) -> PMaybeData a s)
-> (Term s PData -> Term s (PAsData a))
-> Term s PData
-> PMaybeData a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PData -> Term s (PAsData a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s b) -> Term s PData -> Term s b
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr)

-- | @since WIP
deriving via
  DeriveDataPLiftable (PMaybeData a) (Maybe (AsHaskell a))
  instance
    (Plutus.ToData (AsHaskell a), Plutus.FromData (AsHaskell a)) => PLiftable (PMaybeData a)

-- | @since WIP
instance PIsData (PMaybeData a) where
  {-# INLINEABLE pdataImpl #-}
  pdataImpl :: forall (s :: S). Term s (PMaybeData a) -> Term s PData
pdataImpl = Term s (PMaybeData a) -> Term s (PInner (PMaybeData a))
Term s (PMaybeData a) -> Term s PData
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto
  {-# INLINEABLE pfromDataImpl #-}
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PMaybeData a)) -> Term s (PMaybeData a)
pfromDataImpl = Term s (PAsData (PMaybeData a)) -> Term s (PMaybeData a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> Term s b
punsafeCoerce

-- | @since 2.0.0
instance PTryFrom PData a => PTryFrom PData (PMaybeData a)

-- | @since 2.0.0
instance PTryFrom PData a => PTryFrom PData (PAsData (PMaybeData a))

-- | @since 2.0.0
instance (PIsData a, PPartialOrd a) => PPartialOrd (PMaybeData a) where
  {-# INLINEABLE (#<=) #-}
  Term s (PMaybeData a)
t1 #<= :: forall (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
#<= Term s (PMaybeData a)
t2 = Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
t1 ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue
    PDJust Term s (PAsData a)
t1' -> Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
t2 ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
      PMaybeData a s
PDNothing -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse
      PDJust Term s (PAsData a)
t2' -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t1' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t2'
  {-# INLINEABLE (#<) #-}
  Term s (PMaybeData a)
t1 #< :: forall (s :: S).
Term s (PMaybeData a) -> Term s (PMaybeData a) -> Term s PBool
#< Term s (PMaybeData a)
t2 = Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
t1 ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
t2 ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
      PMaybeData a s
PDNothing -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse
      PDJust Term s (PAsData a)
_ -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue
    PDJust Term s (PAsData a)
t1' -> Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
t2 ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
      PMaybeData a s
PDNothing -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse
      PDJust Term s (PAsData a)
t2' -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t1' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t2'

-- | @since 2.0.0
instance (PIsData a, PPartialOrd a) => POrd (PMaybeData a) where
  {-# INLINEABLE pmin #-}
  pmin :: forall (s :: S).
Term s (PMaybeData a)
-> Term s (PMaybeData a) -> Term s (PMaybeData a)
pmin Term s (PMaybeData a)
t1 Term s (PMaybeData a)
t2 = Term s (PMaybeData a)
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData 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 (PMaybeData a)
t1 ((PMaybeData a s -> Term s (PMaybeData a))
 -> Term s (PMaybeData a))
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> Term s (PMaybeData a)
t1
    PDJust Term s (PAsData a)
t1' -> Term s (PMaybeData a)
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData 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 (PMaybeData a)
t2 ((PMaybeData a s -> Term s (PMaybeData a))
 -> Term s (PMaybeData a))
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \case
      PMaybeData a s
PDNothing -> Term s (PMaybeData a)
t2
      PDJust Term s (PAsData a)
t2' ->
        Term s PBool
-> Term s (PMaybeData a)
-> Term s (PMaybeData a)
-> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t1' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t2')
          Term s (PMaybeData a)
t1
          Term s (PMaybeData a)
t2
  {-# INLINEABLE pmax #-}
  pmax :: forall (s :: S).
Term s (PMaybeData a)
-> Term s (PMaybeData a) -> Term s (PMaybeData a)
pmax Term s (PMaybeData a)
t1 Term s (PMaybeData a)
t2 = Term s (PMaybeData a)
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData 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 (PMaybeData a)
t1 ((PMaybeData a s -> Term s (PMaybeData a))
 -> Term s (PMaybeData a))
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> Term s (PMaybeData a)
t2
    PDJust Term s (PAsData a)
t1' -> Term s (PMaybeData a)
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData 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 (PMaybeData a)
t2 ((PMaybeData a s -> Term s (PMaybeData a))
 -> Term s (PMaybeData a))
-> (PMaybeData a s -> Term s (PMaybeData a))
-> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \case
      PMaybeData a s
PDNothing -> Term s (PMaybeData a)
t1
      PDJust Term s (PAsData a)
t2' ->
        Term s PBool
-> Term s (PMaybeData a)
-> Term s (PMaybeData a)
-> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t1' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t2')
          Term s (PMaybeData a)
t2
          Term s (PMaybeData a)
t1

{-
instance (PIsData a, POrd a) => PPartialOrd (PMaybeData a) where
  x #< y = pmaybeLT False (#<) # x # y
  x #<= y = pmaybeLT True (#<=) # x # y

-- | @since 2.0.0
instance (PIsData a, POrd a) => POrd (PMaybeData a)
-}

{- | A Rational type that corresponds to the data encoding used by 'Plutus.Rational'.

@since 3.1.0
-}
newtype PRationalData s
  = PRationalData
      ( Term
          s
          ( PDataRecord
              '[ "numerator" ':= PInteger
               , "denominator" ':= PPositive
               ]
          )
      )
  deriving stock
    ( -- | @since 3.1.0
      (forall x. PRationalData s -> Rep (PRationalData s) x)
-> (forall x. Rep (PRationalData s) x -> PRationalData s)
-> Generic (PRationalData s)
forall x. Rep (PRationalData s) x -> PRationalData s
forall x. PRationalData s -> Rep (PRationalData s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PRationalData s) x -> PRationalData s
forall (s :: S) x. PRationalData s -> Rep (PRationalData s) x
$cfrom :: forall (s :: S) x. PRationalData s -> Rep (PRationalData s) x
from :: forall x. PRationalData s -> Rep (PRationalData s) x
$cto :: forall (s :: S) x. Rep (PRationalData s) x -> PRationalData s
to :: forall x. Rep (PRationalData s) x -> PRationalData s
Generic
    )
  deriving anyclass
    ( -- | @since 3.1.0
      (forall (s :: S). PRationalData s -> Term s (PInner PRationalData))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner PRationalData)
    -> (PRationalData s -> Term s b) -> Term s b)
-> PlutusType PRationalData
forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
forall (s :: S) (b :: S -> Type).
Term s (PInner PRationalData)
-> (PRationalData 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
$cpcon' :: forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
pcon' :: forall (s :: S). PRationalData s -> Term s (PInner PRationalData)
$cpmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner PRationalData)
-> (PRationalData s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner PRationalData)
-> (PRationalData s -> Term s b) -> Term s b
PlutusType
    , -- | @since 3.1.0
      (forall (s :: S).
 Term s (PAsData PRationalData) -> Term s PRationalData)
-> (forall (s :: S). Term s PRationalData -> Term s PData)
-> PIsData PRationalData
forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
forall (s :: S). Term s PRationalData -> Term s PData
forall (a :: S -> Type).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
$cpfromDataImpl :: forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
pfromDataImpl :: forall (s :: S).
Term s (PAsData PRationalData) -> Term s PRationalData
$cpdataImpl :: forall (s :: S). Term s PRationalData -> Term s PData
pdataImpl :: forall (s :: S). Term s PRationalData -> Term s PData
PIsData
    , -- | @since 3.1.0
      (forall (s :: S).
 Term s PRationalData
 -> Term s (PDataRecord (PFields PRationalData)))
-> PDataFields PRationalData
forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
forall (a :: S -> Type).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
$cptoFields :: forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
ptoFields :: forall (s :: S).
Term s PRationalData
-> Term s (PDataRecord (PFields PRationalData))
PDataFields
    , -- | @since 3.1.0
      (forall (s :: S).
 Term s PRationalData -> Term s PRationalData -> Term s PBool)
-> PEq PRationalData
forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (t :: S -> Type).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
#== :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
PEq
    , -- | @since 3.1.0
      (forall (s :: S). Bool -> Term s PRationalData -> Term s PString)
-> PShow PRationalData
forall (s :: S). Bool -> Term s PRationalData -> Term s PString
forall (t :: S -> Type).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
$cpshow' :: forall (s :: S). Bool -> Term s PRationalData -> Term s PString
pshow' :: forall (s :: S). Bool -> Term s PRationalData -> Term s PString
PShow
    )

-- | @since 3.1.0
instance PPartialOrd PRationalData where
  #<= :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
(#<=) = (forall (s :: S).
 Term s PInteger -> Term s PInteger -> Term s PBool)
-> Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (s :: S).
(forall (s :: S).
 Term s PInteger -> Term s PInteger -> Term s PBool)
-> Term s PRationalData -> Term s PRationalData -> Term s PBool
liftCompareOp Term s' PInteger -> Term s' PInteger -> Term s' PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
(#<=)
  #< :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
(#<) = (forall (s :: S).
 Term s PInteger -> Term s PInteger -> Term s PBool)
-> Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (s :: S).
(forall (s :: S).
 Term s PInteger -> Term s PInteger -> Term s PBool)
-> Term s PRationalData -> Term s PRationalData -> Term s PBool
liftCompareOp Term s' PInteger -> Term s' PInteger -> Term s' PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
(#<)

-- | @since 3.1.0
instance POrd PRationalData

-- | @since 3.1.0
instance DerivePlutusType PRationalData where
  type DPTStrat _ = PlutusTypeData

-- | @since WIP
deriving via
  DeriveDataPLiftable PRationalData Plutus.Rational
  instance
    PLiftable PRationalData

-- | @since 3.1.0
instance PTryFrom PData PRationalData where
  type PTryFromExcess PData PRationalData = Mret PPositive
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s PRationalData,
     Reduce (PTryFromExcess PData PRationalData s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq (Term s PRationalData,
 Reduce (PTryFromExcess PData PRationalData s))
-> Term s r
cont = forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PRationalData) Term s PData
opq ((Term s PRationalData, Term s PPositive) -> Term s r
(Term s PRationalData,
 Reduce (PTryFromExcess PData PRationalData s))
-> Term s r
cont ((Term s PRationalData, Term s PPositive) -> Term s r)
-> ((Term s (PAsData PRationalData), Term s PPositive)
    -> (Term s PRationalData, Term s PPositive))
-> (Term s (PAsData PRationalData), Term s PPositive)
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term s (PAsData PRationalData) -> Term s PRationalData)
-> (Term s (PAsData PRationalData), Term s PPositive)
-> (Term s PRationalData, Term s PPositive)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Term s (PAsData PRationalData) -> Term s PRationalData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> Term s b
punsafeCoerce)

{- | This instance produces a verified positive denominator as the excess output.

@since 3.1.0
-}
instance PTryFrom PData (PAsData PRationalData) where
  type PTryFromExcess PData (PAsData PRationalData) = Mret PPositive
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PRationalData),
     Reduce (PTryFromExcess PData (PAsData PRationalData) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  s
  (Term s (PAsData PRationalData),
   Reduce (PTryFromExcess PData (PAsData PRationalData) s))
-> ((Term s (PAsData PRationalData),
     Reduce (PTryFromExcess PData (PAsData PRationalData) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   s
   (Term s (PAsData PRationalData),
    Reduce (PTryFromExcess PData (PAsData PRationalData) s))
 -> ((Term s (PAsData PRationalData),
      Reduce (PTryFromExcess PData (PAsData PRationalData) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     s
     (Term s (PAsData PRationalData),
      Reduce (PTryFromExcess PData (PAsData PRationalData) s))
-> ((Term s (PAsData PRationalData),
     Reduce (PTryFromExcess PData (PAsData PRationalData) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq' <- Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    Term s PString -> Term s PBool -> TermCont s ()
forall {r :: S -> Type} (s :: S).
Term s PString -> Term s PBool -> TermCont s ()
pguardC Term s PString
"ptryFrom(PRationalData): invalid constructor id" (Term s PBool -> TermCont s ()) -> Term s PBool -> TermCont s ()
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0
    Term s (PBuiltinList PData)
flds <- Term s (PBuiltinList PData)
-> TermCont s (Term s (PBuiltinList PData))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (PBuiltinList PData)
 -> TermCont s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
opq'
    Term s PInteger
_numr <- Term s PInteger -> TermCont s (Term s PInteger)
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s PInteger -> TermCont s (Term s PInteger))
-> Term s PInteger -> TermCont s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PInteger) (Term s (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
flds) (Term s (PAsData PInteger), Term s PInteger) -> Term s PInteger
(Term s (PAsData PInteger),
 Reduce (PTryFromExcess PData (PAsData PInteger) s))
-> Term s PInteger
forall a b. (a, b) -> b
snd
    Term s (PBuiltinList PData)
ratTail <- Term s (PBuiltinList PData)
-> TermCont s (Term s (PBuiltinList PData))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s (PBuiltinList PData)
 -> TermCont s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
flds
    Term s PPositive
denm <- Term s PPositive -> TermCont s (Term s PPositive)
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont s (Term s a)
pletC (Term s PPositive -> TermCont s (Term s PPositive))
-> Term s PPositive -> TermCont s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PPositive) (Term s (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ratTail) (Term s (PAsData PPositive), Term s PPositive) -> Term s PPositive
(Term s (PAsData PPositive),
 Reduce (PTryFromExcess PData (PAsData PPositive) s))
-> Term s PPositive
forall a b. (a, b) -> b
snd
    Term s PString -> Term s PBool -> TermCont s ()
forall {r :: S -> Type} (s :: S).
Term s PString -> Term s PBool -> TermCont s ()
pguardC Term s PString
"ptryFrom(PRationalData): constructor fields len > 2" (Term s PBool -> TermCont s ()) -> Term s PBool -> TermCont s ()
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ratTail Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (s :: S).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
    (Term s (PAsData PRationalData), Term s PPositive)
-> TermCont s (Term s (PAsData PRationalData), Term s PPositive)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PRationalData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PPositive
denm)

-- | @since 3.1.0
prationalFromData :: ClosedTerm (PRationalData :--> PRational)
prationalFromData :: ClosedTerm (PRationalData :--> PRational)
prationalFromData = ClosedTerm (PRationalData :--> PRational)
-> Term s (PRationalData :--> PRational)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PRationalData :--> PRational)
 -> Term s (PRationalData :--> PRational))
-> ClosedTerm (PRationalData :--> PRational)
-> Term s (PRationalData :--> PRational)
forall a b. (a -> b) -> a -> b
$
  (Term s PRationalData -> Term s PRational)
-> Term s (PRationalData :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRationalData -> Term s PRational)
 -> Term s (PRationalData :--> PRational))
-> (Term s PRationalData -> Term s PRational)
-> Term s (PRationalData :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRationalData
x -> TermCont s (Term s PRational) -> Term s PRational
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s (Term s PRational) -> Term s PRational)
-> TermCont s (Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ do
    HRec
  '[ '("numerator", Term s (PAsData PInteger)),
     '("denominator", Term s (PAsData PPositive))]
l <- forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> TermCont s (HRec (BoundTerms ps bs s))
pletFieldsC @'["numerator", "denominator"] Term s PRationalData
x
    Term s PRational -> TermCont s (Term s PRational)
forall a. a -> TermCont s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PRational -> TermCont s (Term s PRational))
-> (PRational s -> Term s PRational)
-> PRational s
-> TermCont s (Term s PRational)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRational s -> Term s PRational
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> TermCont s (Term s PRational))
-> PRational s -> TermCont s (Term s PRational)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"numerator" HRec
  '[ '("numerator", Term s (PAsData PInteger)),
     '("denominator", Term s (PAsData PPositive))]
l) (forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"denominator" HRec
  '[ '("numerator", Term s (PAsData PInteger)),
     '("denominator", Term s (PAsData PPositive))]
l)

{- | Extracts the element out of a 'PDJust' and throws an error if its
argument is 'PDNothing'.

@since 2.1.1
-}
pfromDJust ::
  forall (a :: S -> Type) (s :: S).
  PIsData a =>
  Term s (PMaybeData a :--> a)
pfromDJust :: forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PMaybeData a :--> a)
pfromDJust = ClosedTerm (PMaybeData a :--> a) -> Term s (PMaybeData a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybeData a :--> a) -> Term s (PMaybeData a :--> a))
-> ClosedTerm (PMaybeData a :--> a) -> Term s (PMaybeData a :--> a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybeData a) -> Term s a) -> Term s (PMaybeData 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 (PMaybeData a) -> Term s a)
 -> Term s (PMaybeData a :--> a))
-> (Term s (PMaybeData a) -> Term s a)
-> Term s (PMaybeData a :--> a)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybeData a)
t -> Term s (PMaybeData a) -> (PMaybeData 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 (PMaybeData a)
t ((PMaybeData a s -> Term s a) -> Term s a)
-> (PMaybeData a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"pfromDJust: found PDNothing"
    PDJust Term s (PAsData a)
x -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
x

{- | Yield 'PTrue' if a given 'PMaybeData' is of the form @'PDJust' _@.

@since 2.1.1
-}
pisDJust ::
  forall (a :: S -> Type) (s :: S).
  Term s (PMaybeData a :--> PBool)
pisDJust :: forall (a :: S -> Type) (s :: S). Term s (PMaybeData a :--> PBool)
pisDJust = ClosedTerm (PMaybeData a :--> PBool)
-> Term s (PMaybeData a :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybeData a :--> PBool)
 -> Term s (PMaybeData a :--> PBool))
-> ClosedTerm (PMaybeData a :--> PBool)
-> Term s (PMaybeData a :--> PBool)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybeData a) -> Term s PBool)
-> Term s (PMaybeData 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 (PMaybeData a) -> Term s PBool)
 -> Term s (PMaybeData a :--> PBool))
-> (Term s (PMaybeData a) -> Term s PBool)
-> Term s (PMaybeData a :--> PBool)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybeData a)
x -> Term s (PMaybeData a)
-> (PMaybeData 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 (PMaybeData a)
x ((PMaybeData a s -> Term s PBool) -> Term s PBool)
-> (PMaybeData a s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
    PDJust Term s (PAsData a)
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
    PMaybeData 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

{- | Special version of 'pmaybe' that works with 'PMaybeData'.

@since 2.1.1
-}
pmaybeData ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  PIsData a =>
  Term s (b :--> (a :--> b) :--> PMaybeData a :--> b)
pmaybeData :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PIsData a =>
Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
pmaybeData = ClosedTerm (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
-> Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
 -> Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b))))
-> ClosedTerm (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
-> Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
forall a b. (a -> b) -> a -> b
$
  (Term s b
 -> Term s (a :--> b) -> Term s (PMaybeData a) -> Term s b)
-> Term s (b :--> ((a :--> b) :--> (PMaybeData 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 (PMaybeData a) -> Term s b)
-> Term s (c :--> ((a :--> b) :--> (PMaybeData a :--> b)))
plam ((Term s b
  -> Term s (a :--> b) -> Term s (PMaybeData a) -> Term s b)
 -> Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b))))
-> (Term s b
    -> Term s (a :--> b) -> Term s (PMaybeData a) -> Term s b)
-> Term s (b :--> ((a :--> b) :--> (PMaybeData a :--> b)))
forall a b. (a -> b) -> a -> b
$ \Term s b
d Term s (a :--> b)
f Term s (PMaybeData a)
m -> Term s (PMaybeData a) -> (PMaybeData 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 Term s (PMaybeData a)
m ((PMaybeData a s -> Term s b) -> Term s b)
-> (PMaybeData a s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$
    \case
      PDJust Term s (PAsData a)
x -> 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 (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
x
      PMaybeData a s
_ -> Term s b
d

{- | Construct a 'PDJust' value.

@since 2.1.1
-}
pdjust ::
  forall (a :: S -> Type) (s :: S).
  PIsData a =>
  Term s (a :--> PMaybeData a)
pdjust :: forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (a :--> PMaybeData a)
pdjust = ClosedTerm (a :--> PMaybeData a) -> Term s (a :--> PMaybeData a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> PMaybeData a) -> Term s (a :--> PMaybeData a))
-> ClosedTerm (a :--> PMaybeData a) -> Term s (a :--> PMaybeData a)
forall a b. (a -> b) -> a -> b
$
  (Term s a -> Term s (PMaybeData a)) -> Term s (a :--> PMaybeData 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 (PMaybeData a)) -> Term s (c :--> PMaybeData a)
plam ((Term s a -> Term s (PMaybeData a))
 -> Term s (a :--> PMaybeData a))
-> (Term s a -> Term s (PMaybeData a))
-> Term s (a :--> PMaybeData a)
forall a b. (a -> b) -> a -> b
$
    \Term s a
x -> PMaybeData a s -> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybeData a s -> Term s (PMaybeData a))
-> (Term s a -> PMaybeData a s)
-> Term s a
-> Term s (PMaybeData a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData a) -> PMaybeData a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PMaybeData a s
PDJust (Term s (PAsData a) -> PMaybeData a s)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> PMaybeData a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s a -> Term s (PMaybeData a))
-> Term s a -> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ Term s a
x

{- | Construct a 'PDNothing' value.

@since 2.1.1
-}
pdnothing ::
  forall (a :: S -> Type) (s :: S).
  Term s (PMaybeData a)
pdnothing :: forall (a :: S -> Type) (s :: S). Term s (PMaybeData a)
pdnothing = PMaybeData a s -> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybeData a s
forall (a :: S -> Type) (s :: S). PMaybeData a s
PDNothing

{- | Construct a 'PMaybeData' given a 'PMaybe'. Could be useful if you want to
"lift" from 'PMaybe' to 'Maybe'.

@since 2.1.1
-}
pmaybeToMaybeData ::
  forall (a :: S -> Type) (s :: S).
  PIsData a =>
  Term s (PMaybe a :--> PMaybeData a)
pmaybeToMaybeData :: forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PMaybe a :--> PMaybeData a)
pmaybeToMaybeData = ClosedTerm (PMaybe a :--> PMaybeData a)
-> Term s (PMaybe a :--> PMaybeData a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybe a :--> PMaybeData a)
 -> Term s (PMaybe a :--> PMaybeData a))
-> ClosedTerm (PMaybe a :--> PMaybeData a)
-> Term s (PMaybe a :--> PMaybeData a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybe a) -> Term s (PMaybeData a))
-> Term s (PMaybe a :--> PMaybeData 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 (PMaybeData a)) -> Term s (c :--> PMaybeData a)
plam ((Term s (PMaybe a) -> Term s (PMaybeData a))
 -> Term s (PMaybe a :--> PMaybeData a))
-> (Term s (PMaybe a) -> Term s (PMaybeData a))
-> Term s (PMaybe a :--> PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybe a)
t -> Term s (PMaybe a)
-> (PMaybe a s -> Term s (PMaybeData a)) -> Term s (PMaybeData 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 (PMaybeData a)) -> Term s (PMaybeData a))
-> (PMaybe a s -> Term s (PMaybeData a)) -> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ \case
    PMaybe a s
PNothing -> PMaybeData a s -> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybeData a s
forall (a :: S -> Type) (s :: S). PMaybeData a s
PDNothing
    PJust Term s a
x -> PMaybeData a s -> Term s (PMaybeData a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybeData a s -> Term s (PMaybeData a))
-> (Term s a -> PMaybeData a s)
-> Term s a
-> Term s (PMaybeData a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData a) -> PMaybeData a s
forall (a :: S -> Type) (s :: S).
Term s (PAsData a) -> PMaybeData a s
PDJust (Term s (PAsData a) -> PMaybeData a s)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> PMaybeData a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s a -> Term s (PMaybeData a))
-> Term s a -> Term s (PMaybeData a)
forall a b. (a -> b) -> a -> b
$ Term s a
x

{- | Inverse of `pmaybeToMaybeData`

@since WIP
-}
pmaybeDataToMaybe ::
  forall (a :: S -> Type) (s :: S).
  PIsData a =>
  Term s (PMaybeData a :--> PMaybe a)
pmaybeDataToMaybe :: forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PMaybeData a :--> PMaybe a)
pmaybeDataToMaybe = ClosedTerm (PMaybeData a :--> PMaybe a)
-> Term s (PMaybeData a :--> PMaybe a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PMaybeData a :--> PMaybe a)
 -> Term s (PMaybeData a :--> PMaybe a))
-> ClosedTerm (PMaybeData a :--> PMaybe a)
-> Term s (PMaybeData a :--> PMaybe a)
forall a b. (a -> b) -> a -> b
$
  (Term s (PMaybeData a) -> Term s (PMaybe a))
-> Term s (PMaybeData 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 (PMaybeData a) -> Term s (PMaybe a))
 -> Term s (PMaybeData a :--> PMaybe a))
-> (Term s (PMaybeData a) -> Term s (PMaybe a))
-> Term s (PMaybeData a :--> PMaybe a)
forall a b. (a -> b) -> a -> b
$ \Term s (PMaybeData a)
t -> Term s (PMaybeData a)
-> (PMaybeData a s -> Term s (PMaybe a)) -> Term s (PMaybe 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 (PMaybeData a)
t ((PMaybeData a s -> Term s (PMaybe a)) -> Term s (PMaybe a))
-> (PMaybeData a s -> Term s (PMaybe a)) -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ \case
    PMaybeData a s
PDNothing -> 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
    PDJust Term s (PAsData a)
x -> 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 (PAsData a) -> PMaybe a s)
-> Term s (PAsData 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 (Term s a -> PMaybe a s)
-> (Term s (PAsData a) -> Term s a)
-> Term s (PAsData a)
-> PMaybe a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData a) -> Term s (PMaybe a))
-> Term s (PAsData a) -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a)
x

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

@since 2.1.1
-}
passertPDJust ::
  forall (a :: S -> Type) (s :: S).
  PIsData a =>
  Term s (PString :--> PMaybeData a :--> a)
passertPDJust :: forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PString :--> (PMaybeData a :--> a))
passertPDJust = ClosedTerm (PString :--> (PMaybeData a :--> a))
-> Term s (PString :--> (PMaybeData a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PString :--> (PMaybeData a :--> a))
 -> Term s (PString :--> (PMaybeData a :--> a)))
-> ClosedTerm (PString :--> (PMaybeData a :--> a))
-> Term s (PString :--> (PMaybeData a :--> a))
forall a b. (a -> b) -> a -> b
$
  (Term s PString -> Term s (PMaybeData a) -> Term s a)
-> Term s (PString :--> (PMaybeData 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 (PMaybeData a) -> Term s a)
-> Term s (c :--> (PMaybeData a :--> a))
plam ((Term s PString -> Term s (PMaybeData a) -> Term s a)
 -> Term s (PString :--> (PMaybeData a :--> a)))
-> (Term s PString -> Term s (PMaybeData a) -> Term s a)
-> Term s (PString :--> (PMaybeData a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PString
emsg Term s (PMaybeData a)
t -> Term s (PMaybeData a) -> (PMaybeData 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 (PMaybeData a)
t ((PMaybeData a s -> Term s a) -> Term s a)
-> (PMaybeData a s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
    PDJust Term s (PAsData a)
t' -> Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t'
    PMaybeData a s
PDNothing -> Term s PString -> Term s a
forall (a :: S -> Type) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
emsg

{- | Scott-encoded boolean.

@since WIP
-}
data PSBool (s :: S)
  = PSTrue
  | PSFalse
  deriving stock
    ( -- | @since WIP
      PSBool s -> PSBool s -> Bool
(PSBool s -> PSBool s -> Bool)
-> (PSBool s -> PSBool s -> Bool) -> Eq (PSBool s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: S). PSBool s -> PSBool s -> Bool
$c== :: forall (s :: S). PSBool s -> PSBool s -> Bool
== :: PSBool s -> PSBool s -> Bool
$c/= :: forall (s :: S). PSBool s -> PSBool s -> Bool
/= :: PSBool s -> PSBool s -> Bool
Eq
    , -- | @since WIP
      Eq (PSBool s)
Eq (PSBool s) =>
(PSBool s -> PSBool s -> Ordering)
-> (PSBool s -> PSBool s -> Bool)
-> (PSBool s -> PSBool s -> Bool)
-> (PSBool s -> PSBool s -> Bool)
-> (PSBool s -> PSBool s -> Bool)
-> (PSBool s -> PSBool s -> PSBool s)
-> (PSBool s -> PSBool s -> PSBool s)
-> Ord (PSBool s)
PSBool s -> PSBool s -> Bool
PSBool s -> PSBool s -> Ordering
PSBool s -> PSBool s -> PSBool s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (s :: S). Eq (PSBool s)
forall (s :: S). PSBool s -> PSBool s -> Bool
forall (s :: S). PSBool s -> PSBool s -> Ordering
forall (s :: S). PSBool s -> PSBool s -> PSBool s
$ccompare :: forall (s :: S). PSBool s -> PSBool s -> Ordering
compare :: PSBool s -> PSBool s -> Ordering
$c< :: forall (s :: S). PSBool s -> PSBool s -> Bool
< :: PSBool s -> PSBool s -> Bool
$c<= :: forall (s :: S). PSBool s -> PSBool s -> Bool
<= :: PSBool s -> PSBool s -> Bool
$c> :: forall (s :: S). PSBool s -> PSBool s -> Bool
> :: PSBool s -> PSBool s -> Bool
$c>= :: forall (s :: S). PSBool s -> PSBool s -> Bool
>= :: PSBool s -> PSBool s -> Bool
$cmax :: forall (s :: S). PSBool s -> PSBool s -> PSBool s
max :: PSBool s -> PSBool s -> PSBool s
$cmin :: forall (s :: S). PSBool s -> PSBool s -> PSBool s
min :: PSBool s -> PSBool s -> PSBool s
Ord
    , -- | @since WIP
      Int -> PSBool s -> ShowS
[PSBool s] -> ShowS
PSBool s -> String
(Int -> PSBool s -> ShowS)
-> (PSBool s -> String) -> ([PSBool s] -> ShowS) -> Show (PSBool s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: S). Int -> PSBool s -> ShowS
forall (s :: S). [PSBool s] -> ShowS
forall (s :: S). PSBool s -> String
$cshowsPrec :: forall (s :: S). Int -> PSBool s -> ShowS
showsPrec :: Int -> PSBool s -> ShowS
$cshow :: forall (s :: S). PSBool s -> String
show :: PSBool s -> String
$cshowList :: forall (s :: S). [PSBool s] -> ShowS
showList :: [PSBool s] -> ShowS
Show
    )

-- | @since WIP
instance PlutusType PSBool where
  type PInner PSBool = PForall PSBoolRaw
  {-# INLINEABLE pcon' #-}
  pcon' :: forall (s :: S). PSBool s -> Term s (PInner PSBool)
pcon' = \case
    PSBool s
PSTrue -> PInner PSBool s -> Term s (PInner PSBool)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInner PSBool s -> Term s (PInner PSBool))
-> PInner PSBool s -> Term s (PInner PSBool)
forall a b. (a -> b) -> a -> b
$ (forall (x :: S -> Type). Term s (PSBoolRaw x))
-> PForall PSBoolRaw s
forall a (b :: a -> S -> Type) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall b s
PForall ((forall (x :: S -> Type). Term s (PSBoolRaw x))
 -> PForall PSBoolRaw s)
-> (forall (x :: S -> Type). Term s (PSBoolRaw x))
-> PForall PSBoolRaw s
forall a b. (a -> b) -> a -> b
$ PSBoolRaw x s -> Term s (PSBoolRaw x)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSBoolRaw x s -> Term s (PSBoolRaw x))
-> PSBoolRaw x s -> Term s (PSBoolRaw x)
forall a b. (a -> b) -> a -> b
$ Term s (x :--> (x :--> x)) -> PSBoolRaw x s
forall (a :: S -> Type) (s :: S).
Term s (a :--> (a :--> a)) -> PSBoolRaw a s
PSBoolRaw ((Term s x -> Term s x -> Term s x) -> Term s (x :--> (x :--> x))
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 x -> Term s x) -> Term s (c :--> (x :--> x))
plam Term s x -> Term s x -> Term s x
forall a b. a -> b -> a
const)
    PSBool s
PSFalse -> PInner PSBool s -> Term s (PInner PSBool)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInner PSBool s -> Term s (PInner PSBool))
-> PInner PSBool s -> Term s (PInner PSBool)
forall a b. (a -> b) -> a -> b
$ (forall (x :: S -> Type). Term s (PSBoolRaw x))
-> PForall PSBoolRaw s
forall a (b :: a -> S -> Type) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall b s
PForall ((forall (x :: S -> Type). Term s (PSBoolRaw x))
 -> PForall PSBoolRaw s)
-> (forall (x :: S -> Type). Term s (PSBoolRaw x))
-> PForall PSBoolRaw s
forall a b. (a -> b) -> a -> b
$ PSBoolRaw x s -> Term s (PSBoolRaw x)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSBoolRaw x s -> Term s (PSBoolRaw x))
-> PSBoolRaw x s -> Term s (PSBoolRaw x)
forall a b. (a -> b) -> a -> b
$ Term s (x :--> (x :--> x)) -> PSBoolRaw x s
forall (a :: S -> Type) (s :: S).
Term s (a :--> (a :--> a)) -> PSBoolRaw a s
PSBoolRaw ((Term s x -> Term s x -> Term s x) -> Term s (x :--> (x :--> x))
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 x -> Term s x) -> Term s (c :--> (x :--> x))
plam ((Term s x -> Term s x) -> Term s x -> Term s x -> Term s x
forall a b. a -> b -> a
const Term s x -> Term s x
forall a. a -> a
id))
  {-# INLINEABLE pmatch' #-}
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner PSBool) -> (PSBool s -> Term s b) -> Term s b
pmatch' Term s (PInner PSBool)
x' PSBool s -> Term s b
f =
    Term s (PForall PSBoolRaw)
-> (PForall PSBoolRaw 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 Term s (PInner PSBool)
Term s (PForall PSBoolRaw)
x' ((PForall PSBoolRaw s -> Term s b) -> Term s b)
-> (PForall PSBoolRaw s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(PForall forall (x :: S -> Type). Term s (PSBoolRaw x)
raw) ->
      Term s (PSBoolRaw (PDelayed b))
-> (PSBoolRaw (PDelayed b) 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 Term s (PSBoolRaw (PDelayed b))
forall (x :: S -> Type). Term s (PSBoolRaw x)
raw ((PSBoolRaw (PDelayed b) s -> Term s b) -> Term s b)
-> (PSBoolRaw (PDelayed b) s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(PSBoolRaw Term s (PDelayed b :--> (PDelayed b :--> PDelayed b))
x) ->
        Term s (PDelayed b) -> Term s b
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed b) -> Term s b)
-> Term s (PDelayed b) -> Term s b
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed b :--> (PDelayed b :--> PDelayed b))
x Term s (PDelayed b :--> (PDelayed b :--> PDelayed b))
-> Term s (PDelayed b) -> Term s (PDelayed b :--> PDelayed b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay (PSBool s -> Term s b
f PSBool s
forall (s :: S). PSBool s
PSTrue) Term s (PDelayed b :--> PDelayed b)
-> Term s (PDelayed b) -> Term s (PDelayed b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay (PSBool s -> Term s b
f PSBool s
forall (s :: S). PSBool s
PSFalse)

{- | Strict version of 'pmatch' for 'PSBool'.

@since WIP
-}
pmatchStrict ::
  forall (r :: S -> Type) (s :: S).
  Term s PSBool ->
  (PSBool s -> Term s r) ->
  Term s r
pmatchStrict :: forall (r :: S -> Type) (s :: S).
Term s PSBool -> (PSBool s -> Term s r) -> Term s r
pmatchStrict Term s PSBool
x' PSBool s -> Term s r
f =
  Term s (PForall PSBoolRaw)
-> (PForall PSBoolRaw s -> Term s r) -> Term s r
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 PSBool -> Term s (PInner PSBool)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PSBool
x') ((PForall PSBoolRaw s -> Term s r) -> Term s r)
-> (PForall PSBoolRaw s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \(PForall forall (x :: S -> Type). Term s (PSBoolRaw x)
raw) ->
    Term s (PSBoolRaw r) -> (PSBoolRaw r s -> Term s r) -> Term s r
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 (PSBoolRaw r)
forall (x :: S -> Type). Term s (PSBoolRaw x)
raw ((PSBoolRaw r s -> Term s r) -> Term s r)
-> (PSBoolRaw r s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \(PSBoolRaw Term s (r :--> (r :--> r))
x) ->
      Term s (r :--> (r :--> r))
x Term s (r :--> (r :--> r)) -> Term s r -> Term s (r :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# PSBool s -> Term s r
f PSBool s
forall (s :: S). PSBool s
PSTrue Term s (r :--> r) -> Term s r -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# PSBool s -> Term s r
f PSBool s
forall (s :: S). PSBool s
PSFalse

-- | @since WIP
pstrue :: forall (s :: S). Term s PSBool
pstrue :: forall (s :: S). Term s PSBool
pstrue = PSBool s -> Term s PSBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PSBool s
forall (s :: S). PSBool s
PSTrue

-- | @since WIP
psfalse :: forall (s :: S). Term s PSBool
psfalse :: forall (s :: S). Term s PSBool
psfalse = PSBool s -> Term s PSBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PSBool s
forall (s :: S). PSBool s
PSFalse

{- | Strict @if@ on Scott-encoded bool.

@since WIP
-}
psif' ::
  forall (s :: S) (a :: S -> Type).
  Term s PSBool ->
  Term s a ->
  Term s a ->
  Term s a
psif' :: forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif' Term s PSBool
b Term s a
t Term s a
f = Term s PSBool -> (PSBool s -> Term s a) -> Term s a
forall (r :: S -> Type) (s :: S).
Term s PSBool -> (PSBool s -> Term s r) -> Term s r
pmatchStrict Term s PSBool
b ((PSBool s -> Term s a) -> Term s a)
-> (PSBool s -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \case
  PSBool s
PSTrue -> Term s a
t
  PSBool s
PSFalse -> Term s a
f

{- | Lazy @if@ on Scott-encoded bool.

@since WIP
-}
psif ::
  forall (s :: S) (a :: S -> Type).
  Term s PSBool ->
  Term s a ->
  Term s a ->
  Term s a
psif :: forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif Term s PSBool
b Term s a
t Term s a
f = Term s (PDelayed a) -> Term s a
forall (s :: S) (a :: S -> Type). 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 PSBool
-> Term s (PDelayed a)
-> Term s (PDelayed a)
-> Term s (PDelayed a)
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif' Term s PSBool
b (Term s a -> Term s (PDelayed a)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay Term s a
t) (Term s a -> Term s (PDelayed a)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay Term s a
f)

{- | @not@ on Scott-encoded bool.

@since WIP
-}
psnot :: forall (s :: S). Term s PSBool -> Term s PSBool
psnot :: forall (s :: S). Term s PSBool -> Term s PSBool
psnot Term s PSBool
b = Term s PSBool -> Term s PSBool -> Term s PSBool -> Term s PSBool
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif' Term s PSBool
b Term s PSBool
forall (s :: S). Term s PSBool
psfalse Term s PSBool
forall (s :: S). Term s PSBool
pstrue

{- | Strict AND on Scott-encoded bool.

@since WIP
-}
psand' :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psand' :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psand' Term s PSBool
a Term s PSBool
b = Term s PSBool -> Term s PSBool -> Term s PSBool -> Term s PSBool
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif' Term s PSBool
a Term s PSBool
b Term s PSBool
forall (s :: S). Term s PSBool
psfalse

-- | Lazy AND on Scott-encoded bool.
psand :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psand :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psand Term s PSBool
a Term s PSBool
b = Term s PSBool -> Term s PSBool -> Term s PSBool -> Term s PSBool
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif Term s PSBool
a Term s PSBool
b Term s PSBool
forall (s :: S). Term s PSBool
psfalse

{- | Strict OR on Scott-encoded bool.

@since WIP
-}
psor' :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psor' :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psor' Term s PSBool
a = Term s PSBool -> Term s PSBool -> Term s PSBool -> Term s PSBool
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif' Term s PSBool
a Term s PSBool
forall (s :: S). Term s PSBool
pstrue

{- | Lazy OR on Scott-encoded bool

@since WIP
-}
psor :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psor :: forall (s :: S). Term s PSBool -> Term s PSBool -> Term s PSBool
psor Term s PSBool
a = Term s PSBool -> Term s PSBool -> Term s PSBool -> Term s PSBool
forall (s :: S) (a :: S -> Type).
Term s PSBool -> Term s a -> Term s a -> Term s a
psif Term s PSBool
a Term s PSBool
forall (s :: S). Term s PSBool
pstrue

-- Helpers

newtype PSBoolRaw (a :: S -> Type) (s :: S)
  = PSBoolRaw (Term s (a :--> a :--> a))

instance PlutusType (PSBoolRaw a) where
  type PInner (PSBoolRaw a) = a :--> a :--> a
  pcon' :: forall (s :: S). PSBoolRaw a s -> Term s (PInner (PSBoolRaw a))
pcon' (PSBoolRaw Term s (a :--> (a :--> a))
x) = Term s (a :--> (a :--> a))
Term s (PInner (PSBoolRaw a))
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PSBoolRaw a))
-> (PSBoolRaw a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PSBoolRaw a))
x PSBoolRaw a s -> Term s b
f = PSBoolRaw a s -> Term s b
f (Term s (a :--> (a :--> a)) -> PSBoolRaw a s
forall (a :: S -> Type) (s :: S).
Term s (a :--> (a :--> a)) -> PSBoolRaw a s
PSBoolRaw Term s (a :--> (a :--> a))
Term s (PInner (PSBoolRaw a))
x)

liftCompareOp ::
  forall (s :: S).
  (forall (s' :: S). Term s' PInteger -> Term s' PInteger -> Term s' PBool) ->
  Term s PRationalData ->
  Term s PRationalData ->
  Term s PBool
liftCompareOp :: forall (s :: S).
(forall (s :: S).
 Term s PInteger -> Term s PInteger -> Term s PBool)
-> Term s PRationalData -> Term s PRationalData -> Term s PBool
liftCompareOp forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
f Term s PRationalData
x Term s PRationalData
y = ClosedTerm (PRationalData :--> (PRationalData :--> PBool))
-> Term s (PRationalData :--> (PRationalData :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((Term s PRationalData -> Term s PRationalData -> Term s PBool)
-> Term s (PRationalData :--> (PRationalData :--> 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 PRationalData -> Term s PBool)
-> Term s (c :--> (PRationalData :--> PBool))
plam Term s PRationalData -> Term s PRationalData -> Term s PBool
forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
go) Term s (PRationalData :--> (PRationalData :--> PBool))
-> Term s PRationalData -> Term s (PRationalData :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRationalData
x Term s (PRationalData :--> PBool)
-> Term s PRationalData -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRationalData
y
  where
    go ::
      forall (s' :: S).
      Term s' PRationalData ->
      Term s' PRationalData ->
      Term s' PBool
    go :: forall (s :: S).
Term s PRationalData -> Term s PRationalData -> Term s PBool
go Term s' PRationalData
l Term s' PRationalData
r = TermCont s' (Term s' PBool) -> Term s' PBool
forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont (TermCont s' (Term s' PBool) -> Term s' PBool)
-> TermCont s' (Term s' PBool) -> Term s' PBool
forall a b. (a -> b) -> a -> b
$ do
      HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
l' <- forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> TermCont s (HRec (BoundTerms ps bs s))
pletFieldsC @'["numerator", "denominator"] Term s' PRationalData
l
      HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
r' <- forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps fs,
 BindFields ps bs) =>
Term s a -> TermCont s (HRec (BoundTerms ps bs s))
pletFieldsC @'["numerator", "denominator"] Term s' PRationalData
r
      let ln :: Term s' PInteger
ln = Term s' (PAsData PInteger) -> Term s' PInteger
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s' (PAsData PInteger) -> Term s' PInteger)
-> Term s' (PAsData PInteger) -> Term s' PInteger
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"numerator" HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
l'
      let ld :: Term s' PPositive
ld = Term s' (PAsData PPositive) -> Term s' PPositive
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s' (PAsData PPositive) -> Term s' PPositive)
-> Term s' (PAsData PPositive) -> Term s' PPositive
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"denominator" HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
l'
      let rn :: Term s' PInteger
rn = Term s' (PAsData PInteger) -> Term s' PInteger
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s' (PAsData PInteger) -> Term s' PInteger)
-> Term s' (PAsData PInteger) -> Term s' PInteger
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"numerator" HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
r'
      let rd :: Term s' PPositive
rd = Term s' (PAsData PPositive) -> Term s' PPositive
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s' (PAsData PPositive) -> Term s' PPositive)
-> Term s' (PAsData PPositive) -> Term s' PPositive
forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k) r a. HasField x r a => r -> a
forall (x :: Symbol) r a. HasField x r a => r -> a
getField @"denominator" HRec
  '[ '("numerator", Term s' (PAsData PInteger)),
     '("denominator", Term s' (PAsData PPositive))]
r'
      Term s' PBool -> TermCont s' (Term s' PBool)
forall a. a -> TermCont s' a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s' PBool -> TermCont s' (Term s' PBool))
-> Term s' PBool -> TermCont s' (Term s' PBool)
forall a b. (a -> b) -> a -> b
$ Term s' PInteger -> Term s' PInteger -> Term s' PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
f (Term s' PInteger
ln Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
* Term s' PPositive -> Term s' (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s' PPositive
rd) (Term s' PInteger
rn Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
* Term s' PPositive -> Term s' (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s' PPositive
ld)