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

module Plutarch.Builtin (
  PData,
  pfstBuiltin,
  psndBuiltin,
  pasConstr,
  pasMap,
  pasList,
  pasInt,
  plistData,
  pconstantData,
  pconstrBuiltin,
  pasByteStr,
  PBuiltinPair,
  PBuiltinList (..),
  pdataLiteral,
  PIsData (..),
  pdata,
  pfromData,
  PAsData,
  pforgetData,
  prememberData,
  prememberData',
  pserialiseData,
  ppairDataBuiltin,
  pchooseListBuiltin,
  pchooseData,
  PDataNewtype (..),
) where

import Data.Functor.Const (Const)
import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Generics (Generic)
import Plutarch.Builtin.Bool (PBool, pif, pif', (#&&), (#||))
import Plutarch.ByteString (PByteString)
import Plutarch.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Lift (
  DeriveBuiltinPLiftable,
  PLiftable (AsHaskell, PlutusRepr, fromPlutarch, fromPlutarchRepr, toPlutarch, toPlutarchRepr),
  PLifted (PLifted),
  fromPlutarchUni,
  getPLifted,
  pconstant,
  toPlutarchUni,
  unsafeToUni,
 )
import Plutarch.Internal.Newtype (PlutusTypeNewtype)
import Plutarch.Internal.Ord (POrd, PPartialOrd ((#<), (#<=)))
import Plutarch.Internal.Other (POpaque, pfix, pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  PCovariant,
  PVariant,
  PlutusType (PContravariant', PCovariant', PInner, PVariant', pcon', pmatch'),
  pcon,
  pmatch,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  pdelay,
  pforce,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.TermCont (runTermCont, tcont, unTermCont)
import Plutarch.Internal.Witness (witness)
import Plutarch.List (
  PListLike (
    PElemConstraint,
    pcons,
    pelimList,
    phead,
    pnil,
    pnull,
    ptail
  ),
  pfoldr',
  phead,
  plistEquals,
  pmap,
  pshowList,
  ptail,
 )
import Plutarch.Show (PShow (pshow'), pshow)
import Plutarch.String (PString)
import Plutarch.Trace (ptraceInfoError)
import Plutarch.TryFrom (PSubtype, PTryFrom, PTryFromExcess, ptryFrom, ptryFrom', pupcast, pupcastF)
import Plutarch.Unit (PUnit)
import Plutarch.Unsafe (punsafeBuiltin, punsafeCoerce, punsafeDowncast)
import PlutusCore qualified as PLC
import PlutusTx (Data (Constr), ToData)
import PlutusTx qualified
import PlutusTx.Builtins.Internal (BuiltinByteString (BuiltinByteString), BuiltinData (BuiltinData))

-- | Plutus 'BuiltinPair'
newtype PBuiltinPair (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PBuiltinPair (Term s (PBuiltinPair a b))

instance PlutusType (PBuiltinPair a b) where
  type PInner (PBuiltinPair a b) = PBuiltinPair a b
  type PCovariant' (PBuiltinPair a b) = (PCovariant' a, PCovariant' b)
  type PContravariant' (PBuiltinPair a b) = (PContravariant' a, PContravariant' b)
  type PVariant' (PBuiltinPair a b) = (PVariant' a, PVariant' b)
  pcon' :: forall (s :: S).
PBuiltinPair a b s -> Term s (PInner (PBuiltinPair a b))
pcon' (PBuiltinPair Term s (PBuiltinPair a b)
x) = Term s (PInner (PBuiltinPair a b))
Term s (PBuiltinPair a b)
x
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PBuiltinPair a b))
-> (PBuiltinPair a b s -> Term s b) -> Term s b
pmatch' Term s (PInner (PBuiltinPair a b))
x PBuiltinPair a b s -> Term s b
f = PBuiltinPair a b s -> Term s b
f (Term s (PBuiltinPair a b) -> PBuiltinPair a b s
forall (a :: PType) (b :: PType) (s :: S).
Term s (PBuiltinPair a b) -> PBuiltinPair a b s
PBuiltinPair Term s (PInner (PBuiltinPair a b))
Term s (PBuiltinPair a b)
x)

-- | @since WIP
instance
  ( PLiftable a
  , PLC.Contains PLC.DefaultUni (PlutusRepr a)
  , PLiftable b
  , PLC.Contains PLC.DefaultUni (PlutusRepr b)
  ) =>
  PLiftable (PBuiltinPair a b)
  where
  type AsHaskell (PBuiltinPair a b) = (AsHaskell a, AsHaskell b)
  type PlutusRepr (PBuiltinPair a b) = (PlutusRepr a, PlutusRepr b)

  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PBuiltinPair a b) -> PlutusRepr (PBuiltinPair a b)
toPlutarchRepr (AsHaskell a
a, AsHaskell b
b) = (forall (a :: PType). PLiftable a => AsHaskell a -> PlutusRepr a
toPlutarchRepr @a AsHaskell a
a, forall (a :: PType). PLiftable a => AsHaskell a -> PlutusRepr a
toPlutarchRepr @b AsHaskell b
b)

  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PBuiltinPair a b) -> PLifted @PType s (PBuiltinPair a b)
toPlutarch = AsHaskell (PBuiltinPair a b) -> PLifted @PType s (PBuiltinPair a b)
forall (a :: PType) (s :: S).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
AsHaskell a -> PLifted @PType s a
toPlutarchUni

  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PBuiltinPair a b)
-> Maybe (AsHaskell (PBuiltinPair a b))
fromPlutarchRepr (PlutusRepr a
ar, PlutusRepr b
br) = do
    AsHaskell a
a <- forall (a :: PType).
PLiftable a =>
PlutusRepr a -> Maybe (AsHaskell a)
fromPlutarchRepr @a PlutusRepr a
ar
    AsHaskell b
b <- forall (a :: PType).
PLiftable a =>
PlutusRepr a -> Maybe (AsHaskell a)
fromPlutarchRepr @b PlutusRepr b
br
    (AsHaskell a, AsHaskell b) -> Maybe (AsHaskell a, AsHaskell b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AsHaskell a
a, AsHaskell b
b)

  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @PType s (PBuiltinPair a b))
-> Either LiftError (AsHaskell (PBuiltinPair a b))
fromPlutarch = (forall (s :: S). PLifted @PType s (PBuiltinPair a b))
-> Either LiftError (AsHaskell (PBuiltinPair a b))
forall (a :: PType).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
(forall (s :: S). PLifted @PType s a)
-> Either LiftError (AsHaskell a)
fromPlutarchUni

pfstBuiltin :: Term s (PBuiltinPair a b :--> a)
pfstBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin = ClosedTerm (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b :--> a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinPair a b :--> a)
 -> Term s (PBuiltinPair a b :--> a))
-> ClosedTerm (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b :--> a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinPair a b :--> a))
-> Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinPair a b :--> a))
 -> Term s (PBuiltinPair a b :--> a))
-> (DefaultFun -> Term s (PDelayed (PBuiltinPair a b :--> a)))
-> DefaultFun
-> Term s (PBuiltinPair a b :--> a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
-> Term s (PDelayed (PBuiltinPair a b :--> a))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
 -> Term s (PDelayed (PBuiltinPair a b :--> a)))
-> (DefaultFun
    -> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a))))
-> DefaultFun
-> Term s (PDelayed (PBuiltinPair a b :--> a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun
-> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin (DefaultFun -> Term s (PBuiltinPair a b :--> a))
-> DefaultFun -> Term s (PBuiltinPair a b :--> a)
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.FstPair

psndBuiltin :: Term s (PBuiltinPair a b :--> b)
psndBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin = ClosedTerm (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b :--> b)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinPair a b :--> b)
 -> Term s (PBuiltinPair a b :--> b))
-> ClosedTerm (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b :--> b)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinPair a b :--> b))
-> Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinPair a b :--> b))
 -> Term s (PBuiltinPair a b :--> b))
-> (DefaultFun -> Term s (PDelayed (PBuiltinPair a b :--> b)))
-> DefaultFun
-> Term s (PBuiltinPair a b :--> b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
-> Term s (PDelayed (PBuiltinPair a b :--> b))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
 -> Term s (PDelayed (PBuiltinPair a b :--> b)))
-> (DefaultFun
    -> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b))))
-> DefaultFun
-> Term s (PDelayed (PBuiltinPair a b :--> b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun
-> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin (DefaultFun -> Term s (PBuiltinPair a b :--> b))
-> DefaultFun -> Term s (PBuiltinPair a b :--> b)
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.SndPair

{- | Construct a builtin pair of 'PData' elements.

Uses 'PAsData' to preserve more information about the underlying 'PData'.
-}
ppairDataBuiltin :: Term s (PAsData a :--> PAsData b :--> PBuiltinPair (PAsData a) (PAsData b))
ppairDataBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin = DefaultFun
-> Term
     s
     (PAsData a
      :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkPairData

-- | Plutus 'BuiltinList'
data PBuiltinList (a :: S -> Type) (s :: S)
  = PCons (Term s a) (Term s (PBuiltinList a))
  | PNil

instance
  ( PShow a
  , PLC.Contains PLC.DefaultUni (PlutusRepr a)
  ) =>
  PShow (PBuiltinList a)
  where
  pshow' :: forall (s :: S). Bool -> Term s (PBuiltinList a) -> Term s PString
pshow' Bool
_ Term s (PBuiltinList a)
x = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList @PBuiltinList @a Term s (PBuiltinList a :--> PString)
-> Term s (PBuiltinList a) -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
x

pheadBuiltin :: Term s (PBuiltinList a :--> a)
pheadBuiltin :: forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> a)
pheadBuiltin = ClosedTerm (PBuiltinList a :--> a)
-> Term s (PBuiltinList a :--> a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> a)
 -> Term s (PBuiltinList a :--> a))
-> ClosedTerm (PBuiltinList a :--> a)
-> Term s (PBuiltinList a :--> a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> a))
-> Term s (PBuiltinList a :--> a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> a))
 -> Term s (PBuiltinList a :--> a))
-> Term s (PDelayed (PBuiltinList a :--> a))
-> Term s (PBuiltinList a :--> a)
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Term s (PDelayed (PBuiltinList a :--> a))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.HeadList

ptailBuiltin :: Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin :: forall (s :: S) (a :: PType).
Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin = ClosedTerm (PBuiltinList a :--> PBuiltinList a)
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> PBuiltinList a)
 -> Term s (PBuiltinList a :--> PBuiltinList a))
-> ClosedTerm (PBuiltinList a :--> PBuiltinList a)
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
 -> Term s (PBuiltinList a :--> PBuiltinList a))
-> Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.TailList

pchooseListBuiltin :: Term s (PBuiltinList a :--> b :--> b :--> b)
pchooseListBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin = ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
 -> Term s (PBuiltinList a :--> (b :--> (b :--> b))))
-> ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
 -> Term s (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall a b. (a -> b) -> a -> b
$ Term
  s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term
   s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
 -> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term
     s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term
     s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ChooseList

pnullBuiltin :: Term s (PBuiltinList a :--> PBool)
pnullBuiltin :: forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> PBool)
pnullBuiltin = ClosedTerm (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a :--> PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> PBool)
 -> Term s (PBuiltinList a :--> PBool))
-> ClosedTerm (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a :--> PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> PBool))
 -> Term s (PBuiltinList a :--> PBool))
-> Term s (PDelayed (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a :--> PBool)
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Term s (PDelayed (PBuiltinList a :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.NullList

pconsBuiltin :: Term s (a :--> PBuiltinList a :--> PBuiltinList a)
pconsBuiltin :: forall (s :: S) (a :: PType).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin = ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkCons

instance PLC.Contains PLC.DefaultUni (PlutusRepr a) => PlutusType (PBuiltinList a) where
  type PInner (PBuiltinList a) = PBuiltinList a
  type PCovariant' (PBuiltinList a) = PCovariant' a
  type PContravariant' (PBuiltinList a) = PContravariant' a
  type PVariant' (PBuiltinList a) = PVariant' a
  pcon' :: forall (s :: S).
PBuiltinList a s -> Term s (PInner (PBuiltinList a))
pcon' (PCons Term s a
x Term s (PBuiltinList a)
xs) = Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: PType).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s a -> Term s (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (PBuiltinList a :--> PBuiltinList a)
-> Term s (PBuiltinList a) -> Term s (PBuiltinList a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs
  pcon' PBuiltinList a s
PNil = PLifted @PType s (PInner (PBuiltinList a))
-> Term s (PInner (PBuiltinList a))
forall (s :: S) (a :: PType). PLifted @PType s a -> Term s a
getPLifted (PLifted @PType s (PInner (PBuiltinList a))
 -> Term s (PInner (PBuiltinList a)))
-> PLifted @PType s (PInner (PBuiltinList a))
-> Term s (PInner (PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ forall h (a :: PType) (s :: S).
Includes @Type DefaultUni h =>
h -> PLifted @PType s a
unsafeToUni @[PlutusRepr a] []
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PBuiltinList a))
-> (PBuiltinList a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PBuiltinList a))
xs' PBuiltinList a s -> Term s b
f = Term s (PInner (PBuiltinList a))
-> (Term s (PInner (PBuiltinList a)) -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PInner (PBuiltinList a))
xs' ((Term s (PInner (PBuiltinList a)) -> Term s b) -> Term s b)
-> (Term s (PInner (PBuiltinList a)) -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \Term s (PInner (PBuiltinList a))
xs ->
    Term s (PDelayed b) -> Term s b
forall (s :: S) (a :: PType). 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
  (PBuiltinList a
   :--> (PDelayed b :--> (PDelayed b :--> PDelayed b)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin
        # xs
        # pdelay (f PNil)
        # pdelay (f (PCons (pheadBuiltin # xs) (ptailBuiltin # xs)))

-- | @since WIP
instance (PLiftable a, PLC.Contains PLC.DefaultUni (PlutusRepr a)) => PLiftable (PBuiltinList a) where
  type AsHaskell (PBuiltinList a) = [AsHaskell a]
  type PlutusRepr (PBuiltinList a) = [PlutusRepr a]

  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PBuiltinList a) -> PlutusRepr (PBuiltinList a)
toPlutarchRepr = (AsHaskell a -> PlutusRepr a) -> [AsHaskell a] -> [PlutusRepr a]
forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: PType). PLiftable a => AsHaskell a -> PlutusRepr a
toPlutarchRepr @a)

  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PBuiltinList a) -> PLifted @PType s (PBuiltinList a)
toPlutarch = AsHaskell (PBuiltinList a) -> PLifted @PType s (PBuiltinList a)
forall (a :: PType) (s :: S).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
AsHaskell a -> PLifted @PType s a
toPlutarchUni

  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PBuiltinList a) -> Maybe (AsHaskell (PBuiltinList a))
fromPlutarchRepr = (PlutusRepr a -> Maybe (AsHaskell a))
-> [PlutusRepr a] -> Maybe [AsHaskell a]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (forall (a :: PType).
PLiftable a =>
PlutusRepr a -> Maybe (AsHaskell a)
fromPlutarchRepr @a)

  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @PType s (PBuiltinList a))
-> Either LiftError (AsHaskell (PBuiltinList a))
fromPlutarch = (forall (s :: S). PLifted @PType s (PBuiltinList a))
-> Either LiftError (AsHaskell (PBuiltinList a))
forall (a :: PType).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
(forall (s :: S). PLifted @PType s a)
-> Either LiftError (AsHaskell a)
fromPlutarchUni

instance PListLike PBuiltinList where
  type PElemConstraint PBuiltinList a = (PLC.Contains PLC.DefaultUni (PlutusRepr a))

  pelimList :: forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint PBuiltinList a =>
(Term s a -> Term s (PBuiltinList a) -> Term s r)
-> Term s r -> Term s (PBuiltinList a) -> Term s r
pelimList Term s a -> Term s (PBuiltinList a) -> Term s r
match_cons Term s r
match_nil Term s (PBuiltinList a)
ls = Term s (PBuiltinList a)
-> (PBuiltinList a s -> Term s r) -> Term s r
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinList a)
ls ((PBuiltinList a s -> Term s r) -> Term s r)
-> (PBuiltinList a s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
    PCons Term s a
x Term s (PBuiltinList a)
xs -> Term s a -> Term s (PBuiltinList a) -> Term s r
match_cons Term s a
x Term s (PBuiltinList a)
xs
    PBuiltinList a s
PNil -> Term s r
match_nil

  pcons :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pcons = (Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (c :--> (PBuiltinList a :--> PBuiltinList a))
plam ((Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> (Term s a -> Term s (PBuiltinList a) -> Term s (PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PBuiltinList a)
xs -> PBuiltinList a s -> Term s (PBuiltinList a)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
forall (a :: PType) (s :: S).
Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
PCons Term s a
x Term s (PBuiltinList a)
xs)
  pnil :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
pnil = PBuiltinList a s -> Term s (PBuiltinList a)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBuiltinList a s
forall (a :: PType) (s :: S). PBuiltinList a s
PNil
  phead :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
phead = Term s (PBuiltinList a :--> a)
forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> a)
pheadBuiltin
  ptail :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
ptail = Term s (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: PType).
Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin
  pnull :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBool)
pnull = Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> PBool)
pnullBuiltin

type family F (a :: S -> Type) :: Bool where
  F PData = 'True
  F (PAsData _) = 'True
  F _ = 'False

class Fc (x :: Bool) (a :: S -> Type) where
  fc :: Proxy x -> Term s (PBuiltinList a) -> Term s (PBuiltinList a) -> Term s PBool

instance (PEq a, PLC.Contains PLC.DefaultUni (PlutusRepr a)) => Fc 'False a where
  fc :: forall (s :: S).
Proxy @Bool 'False
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc Proxy @Bool 'False
_ Term s (PBuiltinList a)
xs Term s (PBuiltinList a)
ys = Term s (PBuiltinList a :--> (PBuiltinList a :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals Term s (PBuiltinList a :--> (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a) -> Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs Term s (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
ys

instance PIsData (PBuiltinList a) => Fc 'True a where
  fc :: forall (s :: S).
Proxy @Bool 'True
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc Proxy @Bool 'True
_ Term s (PBuiltinList a)
xs Term s (PBuiltinList a)
ys = Term s (PBuiltinList a) -> Term s (PAsData (PBuiltinList a))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList a)
xs Term s (PAsData (PBuiltinList a))
-> Term s (PAsData (PBuiltinList a)) -> Term s PBool
forall (s :: S).
Term s (PAsData (PBuiltinList a))
-> Term s (PAsData (PBuiltinList a)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinList a) -> Term s (PAsData (PBuiltinList a))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList a)
ys

instance Fc (F a) a => PEq (PBuiltinList a) where
  #== :: forall (s :: S).
Term s (PBuiltinList a) -> Term s (PBuiltinList a) -> Term s PBool
(#==) = Proxy @Bool (F a)
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
forall (x :: Bool) (a :: PType) (s :: S).
Fc x a =>
Proxy @Bool x
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
forall (s :: S).
Proxy @Bool (F a)
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc (forall (t :: Bool). Proxy @Bool t
forall {k} (t :: k). Proxy @k t
Proxy @(F a))

newtype PData (s :: S) = PData (Term s PData)

instance PShow PData where
  pshow' :: forall (s :: S). Bool -> Term s PData -> Term s PString
pshow' Bool
b Term s PData
t0 = Term s PString -> Term s PString
wrap (Term s (PData :--> PString)
forall (s :: S). Term s (PData :--> PString)
go0 Term s (PData :--> PString) -> Term s PData -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
t0)
    where
      wrap :: Term s PString -> Term s PString
wrap Term s PString
s = Term s PBool -> Term s PString -> Term s PString -> Term s PString
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
b) (Term s PString
"(" Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
s Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
")") Term s PString
s
      go0 :: Term s (PData :--> PString)
      go0 :: forall (s :: S). Term s (PData :--> PString)
go0 = (forall (s :: S). Term s (PData :--> PString))
-> Term s (PData :--> PString)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PData :--> PString))
 -> Term s (PData :--> PString))
-> (forall (s :: S). Term s (PData :--> PString))
-> Term s (PData :--> PString)
forall a b. (a -> b) -> a -> b
$
        Term
  s
  (((PData :--> PString) :--> (PData :--> PString))
   :--> (PData :--> PString))
forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((PData :--> PString) :--> (PData :--> PString))
   :--> (PData :--> PString))
-> Term s ((PData :--> PString) :--> (PData :--> PString))
-> Term s (PData :--> PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PData :--> PString) -> Term s PData -> Term s PString)
-> Term s ((PData :--> PString) :--> (PData :--> PString))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PData -> Term s PString)
-> Term s (c :--> (PData :--> PString))
plam ((Term s (PData :--> PString) -> Term s PData -> Term s PString)
 -> Term s ((PData :--> PString) :--> (PData :--> PString)))
-> (Term s (PData :--> PString) -> Term s PData -> Term s PString)
-> Term s ((PData :--> PString) :--> (PData :--> PString))
forall a b. (a -> b) -> a -> b
$ \Term s (PData :--> PString)
go Term s PData
t ->
          let pshowConstr :: Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PString
pshowConstr Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp0 = Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s PString)
-> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp0 ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
  -> Term s PString)
 -> Term s PString)
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s PString)
-> Term s PString
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp ->
                Term s PString
"Constr "
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Bool -> Term s PInteger -> Term s PString
forall (s :: S). Bool -> Term s PInteger -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
False (Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp)
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
" "
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (PBuiltinList PString :--> PString)
forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString Term s (PBuiltinList PString :--> PString)
-> Term s (PBuiltinList PString) -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  ((PData :--> PString)
   :--> (PBuiltinList PData :--> PBuiltinList PString))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap Term
  s
  ((PData :--> PString)
   :--> (PBuiltinList PData :--> PBuiltinList PString))
-> Term s (PData :--> PString)
-> Term s (PBuiltinList PData :--> PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PString)
go Term s (PBuiltinList PData :--> PBuiltinList PString)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp))
              pshowMap :: Term s (PBuiltinList (PBuiltinPair PData PData)) -> Term s PString
pshowMap Term s (PBuiltinList (PBuiltinPair PData PData))
pplist =
                Term s PString
"Map " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (PBuiltinList PString :--> PString)
forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString Term s (PBuiltinList PString :--> PString)
-> Term s (PBuiltinList PString) -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  ((PBuiltinPair PData PData :--> PString)
   :--> (PBuiltinList (PBuiltinPair PData PData)
         :--> PBuiltinList PString))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap Term
  s
  ((PBuiltinPair PData PData :--> PString)
   :--> (PBuiltinList (PBuiltinPair PData PData)
         :--> PBuiltinList PString))
-> Term s (PBuiltinPair PData PData :--> PString)
-> Term
     s
     (PBuiltinList (PBuiltinPair PData PData) :--> PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData :--> PString)
pshowPair Term
  s
  (PBuiltinList (PBuiltinPair PData PData) :--> PBuiltinList PString)
-> Term s (PBuiltinList (PBuiltinPair PData PData))
-> Term s (PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair PData PData))
pplist)
              pshowPair :: Term s (PBuiltinPair PData PData :--> PString)
pshowPair = (Term s (PBuiltinPair PData PData) -> Term s PString)
-> Term s (PBuiltinPair PData PData :--> PString)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PString) -> Term s (c :--> PString)
plam ((Term s (PBuiltinPair PData PData) -> Term s PString)
 -> Term s (PBuiltinPair PData PData :--> PString))
-> (Term s (PBuiltinPair PData PData) -> Term s PString)
-> Term s (PBuiltinPair PData PData :--> PString)
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PData PData)
pp0 -> Term s (PBuiltinPair PData PData)
-> (Term s (PBuiltinPair PData PData) -> Term s PString)
-> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PBuiltinPair PData PData)
pp0 ((Term s (PBuiltinPair PData PData) -> Term s PString)
 -> Term s PString)
-> (Term s (PBuiltinPair PData PData) -> Term s PString)
-> Term s PString
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PData PData)
pp ->
                Term s PString
"("
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> (Term s (PData :--> PString)
go Term s (PData :--> PString) -> Term s PData -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PBuiltinPair PData PData :--> PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PData PData :--> PData)
-> Term s (PBuiltinPair PData PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pp))
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
", "
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> (Term s (PData :--> PString)
go Term s (PData :--> PString) -> Term s PData -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PBuiltinPair PData PData :--> PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair PData PData :--> PData)
-> Term s (PBuiltinPair PData PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pp))
                  Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
")"
              pshowList :: Term s (PBuiltinList PData) -> Term s PString
pshowList Term s (PBuiltinList PData)
xs = Term s PString
"List " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (PBuiltinList PString :--> PString)
forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString Term s (PBuiltinList PString :--> PString)
-> Term s (PBuiltinList PString) -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
  s
  ((PData :--> PString)
   :--> (PBuiltinList PData :--> PBuiltinList PString))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap Term
  s
  ((PData :--> PString)
   :--> (PBuiltinList PData :--> PBuiltinList PString))
-> Term s (PData :--> PString)
-> Term s (PBuiltinList PData :--> PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PString)
go Term s (PBuiltinList PData :--> PBuiltinList PString)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
xs)
              pshowListPString :: Term s (list PString :--> PString)
pshowListPString = ClosedTerm (list PString :--> PString)
-> Term s (list PString :--> PString)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list PString :--> PString)
 -> Term s (list PString :--> PString))
-> ClosedTerm (list PString :--> PString)
-> Term s (list PString :--> PString)
forall a b. (a -> b) -> a -> b
$
                (Term s (list PString) -> Term s PString)
-> Term s (list PString :--> PString)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PString) -> Term s (c :--> PString)
plam ((Term s (list PString) -> Term s PString)
 -> Term s (list PString :--> PString))
-> (Term s (list PString) -> Term s PString)
-> Term s (list PString :--> PString)
forall a b. (a -> b) -> a -> b
$ \Term s (list PString)
plist ->
                  Term s PString
"["
                    Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> (Term s PString -> Term s (list PString) -> Term s PString)
-> Term s PString -> Term s (list PString) -> Term s PString
forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
                      ( \Term s PString
x0 Term s (list PString)
xs0 ->
                          Term s PString
x0 Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> ((forall (s1 :: S).
 Term s1 PString -> Term s1 PString -> Term s1 PString)
-> Term s (PString :--> (list PString :--> PString))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
PIsListLike list a =>
(forall (s1 :: S). Term s1 a -> Term s1 b -> Term s1 b)
-> Term s (b :--> (list a :--> b))
pfoldr' (\Term s1 PString
x Term s1 PString
r -> Term s1 PString
", " Term s1 PString -> Term s1 PString -> Term s1 PString
forall a. Semigroup a => a -> a -> a
<> Term s1 PString
x Term s1 PString -> Term s1 PString -> Term s1 PString
forall a. Semigroup a => a -> a -> a
<> Term s1 PString
r) Term s (PString :--> (list PString :--> PString))
-> Term s PString -> Term s (list PString :--> PString)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PString
forall {s :: S}. Term s PString
"" :: Term s PString) Term s (list PString :--> PString)
-> Term s (list PString) -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list PString)
xs0)
                      )
                      Term s PString
""
                      Term s (list PString)
plist
                    Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
"]"
           in Term s (PDelayed PString) -> Term s PString
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed PString) -> Term s PString)
-> Term s (PDelayed PString) -> Term s PString
forall a b. (a -> b) -> a -> b
$
                Term
  s
  (PData
   :--> (PDelayed PString
         :--> (PDelayed PString
               :--> (PDelayed PString
                     :--> (PDelayed PString
                           :--> (PDelayed PString :--> PDelayed PString))))))
forall (s :: S) (a :: PType).
Term s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
pchooseData
                  # t
                  # pdelay (pshowConstr (pasConstr # t))
                  # pdelay (pshowMap (pasMap # t))
                  # pdelay (pshowList (pasList # t))
                  # pdelay ("I " <> pshow (pasInt # t))
                  # pdelay ("B " <> pshow (pasByteStr # t))

instance PlutusType PData where
  type PInner PData = PData
  type PCovariant' PData = ()
  type PContravariant' PData = ()
  type PVariant' PData = ()
  pcon' :: forall (s :: S). PData s -> Term s (PInner PData)
pcon' (PData Term s PData
t) = Term s (PInner PData)
Term s PData
t
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PData) -> (PData s -> Term s b) -> Term s b
pmatch' Term s (PInner PData)
t PData s -> Term s b
f = PData s -> Term s b
f (Term s PData -> PData s
forall (s :: S). Term s PData -> PData s
PData Term s (PInner PData)
Term s PData
t)

-- | @since WIP
deriving via
  DeriveBuiltinPLiftable PData Data
  instance
    PLiftable PData

instance PEq PData where
  Term s PData
x #== :: forall (s :: S). Term s PData -> Term s PData -> Term s PBool
#== Term s PData
y = DefaultFun -> Term s (PData :--> (PData :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData Term s (PData :--> (PData :--> PBool))
-> Term s PData -> Term s (PData :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x Term s (PData :--> PBool) -> Term s PData -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
y

pchooseData :: Term s (PData :--> a :--> a :--> a :--> a :--> a :--> a)
pchooseData :: forall (s :: S) (a :: PType).
Term s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
pchooseData = ClosedTerm
  (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
 -> Term
      s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> ClosedTerm
     (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDelayed
     (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term
   s
   (PDelayed
      (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
 -> Term
      s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s
     (PDelayed
        (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term
     s
     (PDelayed
        (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ChooseData

pasConstr :: Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr :: forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr = DefaultFun
-> Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnConstrData

pasMap :: Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap :: forall (s :: S).
Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap = DefaultFun
-> Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnMapData

plistData :: Term s (PBuiltinList PData :--> PData)
plistData :: forall (s :: S). Term s (PBuiltinList PData :--> PData)
plistData = DefaultFun -> Term s (PBuiltinList PData :--> PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ListData

pasList :: Term s (PData :--> PBuiltinList PData)
pasList :: forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList = DefaultFun -> Term s (PData :--> PBuiltinList PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnListData

pasInt :: Term s (PData :--> PInteger)
pasInt :: forall (s :: S). Term s (PData :--> PInteger)
pasInt = DefaultFun -> Term s (PData :--> PInteger)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnIData

pasByteStr :: Term s (PData :--> PByteString)
pasByteStr :: forall (s :: S). Term s (PData :--> PByteString)
pasByteStr = DefaultFun -> Term s (PData :--> PByteString)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnBData

-- | Serialise any builtin data to its cbor represented by a builtin bytestring
pserialiseData :: Term s (PData :--> PByteString)
pserialiseData :: forall (s :: S). Term s (PData :--> PByteString)
pserialiseData = DefaultFun -> Term s (PData :--> PByteString)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.SerialiseData

{-# DEPRECATED pdataLiteral "Use `pconstant` instead." #-}
pdataLiteral :: Data -> Term s PData
pdataLiteral :: forall (s :: S). Data -> Term s PData
pdataLiteral = Data -> Term s PData
AsHaskell PData -> Term s PData
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant

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

instance PIsData a => PlutusType (PAsData a) where
  type PInner (PAsData a) = IfSameThenData a (PInner a)
  type PCovariant' (PAsData a) = PCovariant' a
  type PContravariant' (PAsData a) = PContravariant' a
  type PVariant' (PAsData a) = PVariant' a
  pcon' :: forall (s :: S). PAsData a s -> Term s (PInner (PAsData a))
pcon' (PAsData Term s a
t) = Term s (PAsData a) -> Term s (PInner (PAsData a))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s (PAsData a) -> Term s (PInner (PAsData a)))
-> Term s (PAsData a) -> Term s (PInner (PAsData a))
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PAsData a)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s a
t
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PAsData a))
-> (PAsData a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PAsData a))
t PAsData a s -> Term s b
f = PAsData a s -> Term s b
f (Term s a -> PAsData a s
forall (a :: PType) (s :: S). Term s a -> PAsData a s
PAsData (Term s a -> PAsData a s) -> Term s a -> PAsData a s
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData a) -> Term s a) -> Term s (PAsData a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s (PInner (PAsData a)) -> Term s (PAsData a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PAsData a))
t)

instance {-# OVERLAPPING #-} PLiftable (PAsData PByteString) where
  type AsHaskell (PAsData PByteString) = AsHaskell PByteString
  type PlutusRepr (PAsData PByteString) = Data
  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PAsData PByteString) -> PlutusRepr (PAsData PByteString)
toPlutarchRepr = BuiltinByteString -> Data
forall a. ToData a => a -> Data
PlutusTx.toData (BuiltinByteString -> Data)
-> (ByteString -> BuiltinByteString) -> ByteString -> Data
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> BuiltinByteString
BuiltinByteString
  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PAsData PByteString)
-> PLifted @PType s (PAsData PByteString)
toPlutarch = AsHaskell (PAsData PByteString)
-> PLifted @PType s (PAsData PByteString)
forall (a :: PType) (s :: S).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
AsHaskell a -> PLifted @PType s a
toPlutarchUni
  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PAsData PByteString)
-> Maybe (AsHaskell (PAsData PByteString))
fromPlutarchRepr PlutusRepr (PAsData PByteString)
x = (\(BuiltinByteString ByteString
str) -> ByteString
AsHaskell (PAsData PByteString)
str) (BuiltinByteString -> AsHaskell (PAsData PByteString))
-> Maybe BuiltinByteString
-> Maybe (AsHaskell (PAsData PByteString))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Data -> Maybe BuiltinByteString
forall a. FromData a => Data -> Maybe a
PlutusTx.fromData Data
PlutusRepr (PAsData PByteString)
x
  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @PType s (PAsData PByteString))
-> Either LiftError (AsHaskell (PAsData PByteString))
fromPlutarch = (forall (s :: S). PLifted @PType s (PAsData PByteString))
-> Either LiftError (AsHaskell (PAsData PByteString))
forall (a :: PType).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
(forall (s :: S). PLifted @PType s a)
-> Either LiftError (AsHaskell a)
fromPlutarchUni

instance {-# OVERLAPPING #-} PLiftable (PAsData PData) where
  type AsHaskell (PAsData PData) = AsHaskell PData
  type PlutusRepr (PAsData PData) = Data
  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PAsData PData) -> PlutusRepr (PAsData PData)
toPlutarchRepr = BuiltinData -> Data
forall a. ToData a => a -> Data
PlutusTx.toData (BuiltinData -> Data) -> (Data -> BuiltinData) -> Data -> Data
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Data -> BuiltinData
BuiltinData
  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PAsData PData) -> PLifted @PType s (PAsData PData)
toPlutarch = AsHaskell (PAsData PData) -> PLifted @PType s (PAsData PData)
forall (a :: PType) (s :: S).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
AsHaskell a -> PLifted @PType s a
toPlutarchUni
  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PAsData PData) -> Maybe (AsHaskell (PAsData PData))
fromPlutarchRepr PlutusRepr (PAsData PData)
x = (\(BuiltinData Data
str) -> Data
AsHaskell (PAsData PData)
str) (BuiltinData -> AsHaskell (PAsData PData))
-> Maybe BuiltinData -> Maybe (AsHaskell (PAsData PData))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Data -> Maybe BuiltinData
forall a. FromData a => Data -> Maybe a
PlutusTx.fromData Data
PlutusRepr (PAsData PData)
x
  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @PType s (PAsData PData))
-> Either LiftError (AsHaskell (PAsData PData))
fromPlutarch = (forall (s :: S). PLifted @PType s (PAsData PData))
-> Either LiftError (AsHaskell (PAsData PData))
forall (a :: PType).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
(forall (s :: S). PLifted @PType s a)
-> Either LiftError (AsHaskell a)
fromPlutarchUni

instance (PlutusTx.ToData (AsHaskell a), PlutusTx.FromData (AsHaskell a), PIsData a) => PLiftable (PAsData a) where
  type AsHaskell (PAsData a) = AsHaskell a
  type PlutusRepr (PAsData a) = Data

  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell (PAsData a) -> PlutusRepr (PAsData a)
toPlutarchRepr = AsHaskell (PAsData a) -> Data
AsHaskell (PAsData a) -> PlutusRepr (PAsData a)
forall a. ToData a => a -> Data
PlutusTx.toData

  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S).
AsHaskell (PAsData a) -> PLifted @PType s (PAsData a)
toPlutarch = AsHaskell (PAsData a) -> PLifted @PType s (PAsData a)
forall (a :: PType) (s :: S).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
AsHaskell a -> PLifted @PType s a
toPlutarchUni

  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr (PAsData a) -> Maybe (AsHaskell (PAsData a))
fromPlutarchRepr = Data -> Maybe (AsHaskell (PAsData a))
PlutusRepr (PAsData a) -> Maybe (AsHaskell (PAsData a))
forall a. FromData a => Data -> Maybe a
PlutusTx.fromData

  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted @PType s (PAsData a))
-> Either LiftError (AsHaskell (PAsData a))
fromPlutarch = (forall (s :: S). PLifted @PType s (PAsData a))
-> Either LiftError (AsHaskell (PAsData a))
forall (a :: PType).
(PLiftable a, Includes @Type DefaultUni (PlutusRepr a)) =>
(forall (s :: S). PLifted @PType s a)
-> Either LiftError (AsHaskell a)
fromPlutarchUni

instance PEq (PAsData a) where
  Term s (PAsData a)
x #== :: forall (s :: S).
Term s (PAsData a) -> Term s (PAsData a) -> Term s PBool
#== Term s (PAsData a)
y = DefaultFun -> Term s (PAsData a :--> (PAsData a :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData Term s (PAsData a :--> (PAsData a :--> PBool))
-> Term s (PAsData a) -> Term s (PAsData a :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
x Term s (PAsData a :--> PBool) -> Term s (PAsData a) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
y

instance (PIsData a, PShow a) => PShow (PAsData a) where
  pshow' :: forall (s :: S). Bool -> Term s (PAsData a) -> Term s PString
pshow' Bool
w Term s (PAsData a)
x = Bool -> Term s a -> Term s PString
forall (s :: S). Bool -> Term s a -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
w (Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
x)

type family IfSameThenData (a :: S -> Type) (b :: S -> Type) :: S -> Type where
  IfSameThenData a a = PData
  IfSameThenData _ POpaque = PData
  IfSameThenData _ b = PAsData b

pforgetData :: forall s a. Term s (PAsData a) -> Term s PData
pforgetData :: forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData = Term s (PAsData a) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- FIXME: remove, broken

{- | Like 'pforgetData', except it works for complex types.
 Equivalent to 'pupcastF'.
-}
pforgetData' ::
  forall a (p :: (S -> Type) -> S -> Type) (s :: S).
  PCovariant p =>
  Proxy p ->
  Term s (p (PAsData a)) ->
  Term s (p PData)
pforgetData' :: forall (a :: PType) (p :: PType -> PType) (s :: S).
PCovariant p =>
Proxy @(PType -> PType) p
-> Term s (p (PAsData a)) -> Term s (p PData)
pforgetData' Proxy @(PType -> PType) p
_ = let ()
_ = Proxy @Constraint (PCovariant p) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PCovariant p)) in Term s (p (PAsData a)) -> Term s (p PData)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | Inverse of 'pforgetData''.
prememberData ::
  forall (p :: (S -> Type) -> S -> Type) (s :: S).
  PVariant p =>
  Proxy p ->
  Term s (p PData) ->
  Term s (p (PAsData PData))
prememberData :: forall (p :: PType -> PType) (s :: S).
PVariant p =>
Proxy @(PType -> PType) p
-> Term s (p PData) -> Term s (p (PAsData PData))
prememberData Proxy @(PType -> PType) p
Proxy = let ()
_ = Proxy @Constraint (PVariant p) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PVariant p)) in Term s (p PData) -> Term s (p (PAsData PData))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | Like 'prememberData' but generalised.
prememberData' ::
  forall a (p :: (S -> Type) -> S -> Type) (s :: S).
  (PSubtype PData a, PVariant p) =>
  Proxy p ->
  Term s (p a) ->
  Term s (p (PAsData a))
prememberData' :: forall (a :: PType) (p :: PType -> PType) (s :: S).
(PSubtype PData a, PVariant p) =>
Proxy @(PType -> PType) p -> Term s (p a) -> Term s (p (PAsData a))
prememberData' Proxy @(PType -> PType) p
Proxy = let ()
_ = Proxy @Constraint (PSubtype PData a, PVariant p) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PSubtype PData a, PVariant p)) in Term s (p a) -> Term s (p (PAsData a))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

{- | Laws:
 - If @PSubtype PData a@, then @pdataImpl a@ must be `pupcast`.
 - pdataImpl . pupcast . pfromDataImpl ≡ id
 - pfromDataImpl . punsafeDowncast . pdataImpl ≡ id
-}
class PIsData a where
  pfromDataImpl :: Term s (PAsData a) -> Term s a
  default pfromDataImpl :: PIsData (PInner a) => Term s (PAsData a) -> Term s a
  pfromDataImpl Term s (PAsData a)
x = Term s (PInner a) -> Term s a
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner a) -> Term s a) -> Term s (PInner a) -> Term s a
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PInner a)) -> Term s (PInner a)
forall (s :: S). Term s (PAsData (PInner a)) -> Term s (PInner a)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromDataImpl (Term s (PAsData a) -> Term s (PAsData (PInner a))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PAsData a)
x :: Term _ (PAsData (PInner a)))

  pdataImpl :: Term s a -> Term s PData
  default pdataImpl :: PIsData (PInner a) => Term s a -> Term s PData
  pdataImpl Term s a
x = Term s (PInner a) -> Term s PData
forall (s :: S). Term s (PInner a) -> Term s PData
forall (a :: PType) (s :: S). PIsData a => Term s a -> Term s PData
pdataImpl (Term s (PInner a) -> Term s PData)
-> Term s (PInner a) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s a
x

pfromData :: PIsData a => Term s (PAsData a) -> Term s a
pfromData :: forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData = Term s (PAsData a) -> Term s a
forall (s :: S). Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromDataImpl
pdata :: PIsData a => Term s a -> Term s (PAsData a)
pdata :: forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata = Term s PData -> Term s (PAsData a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s (PAsData a))
-> (Term s a -> Term s PData) -> Term s a -> Term s (PAsData a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s PData
forall (s :: S). Term s a -> Term s PData
forall (a :: PType) (s :: S). PIsData a => Term s a -> Term s PData
pdataImpl

instance PIsData PData where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PData) -> Term s PData
pfromDataImpl = Term s (PAsData PData) -> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast
  pdataImpl :: forall (s :: S). Term s PData -> Term s PData
pdataImpl = Term s PData -> Term s PData
forall a. a -> a
id

instance forall (a :: S -> Type). PSubtype PData a => PIsData (PBuiltinList a) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinList a)) -> Term s (PBuiltinList a)
pfromDataImpl Term s (PAsData (PBuiltinList a))
x = Term s (PBuiltinList PData) -> Term s (PBuiltinList a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData) -> Term s (PBuiltinList a))
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinList PData)
forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList Term s (PData :--> PBuiltinList PData)
-> Term s PData -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinList a)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData (PBuiltinList a))
x
  pdataImpl :: forall (s :: S). Term s (PBuiltinList a) -> Term s PData
pdataImpl Term s (PBuiltinList a)
x = Term s (PBuiltinList PData :--> PData)
forall (s :: S). Term s (PBuiltinList PData :--> PData)
plistData Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: PType) (b :: PType) (p :: PType -> PType) (s :: S).
(PSubtype a b, PCovariant p) =>
Proxy @(PType -> PType) p -> Term s (p b) -> Term s (p a)
pupcastF @PData @a (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @PBuiltinList) Term s (PBuiltinList a)
x

newtype Helper2 f a s = Helper2 (Term s (PAsData (f a)))
  deriving stock ((forall x. Helper2 @k f a s -> Rep (Helper2 @k f a s) x)
-> (forall x. Rep (Helper2 @k f a s) x -> Helper2 @k f a s)
-> Generic (Helper2 @k f a s)
forall x. Rep (Helper2 @k f a s) x -> Helper2 @k f a s
forall x. Helper2 @k f a s -> Rep (Helper2 @k f a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k -> PType) (a :: k) (s :: S) x.
Rep (Helper2 @k f a s) x -> Helper2 @k f a s
forall k (f :: k -> PType) (a :: k) (s :: S) x.
Helper2 @k f a s -> Rep (Helper2 @k f a s) x
$cfrom :: forall k (f :: k -> PType) (a :: k) (s :: S) x.
Helper2 @k f a s -> Rep (Helper2 @k f a s) x
from :: forall x. Helper2 @k f a s -> Rep (Helper2 @k f a s) x
$cto :: forall k (f :: k -> PType) (a :: k) (s :: S) x.
Rep (Helper2 @k f a s) x -> Helper2 @k f a s
to :: forall x. Rep (Helper2 @k f a s) x -> Helper2 @k f a s
Generic)
  deriving anyclass ((forall (s :: S).
 Helper2 @k f a s -> Term s (PInner (Helper2 @k f a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (Helper2 @k f a))
    -> (Helper2 @k f a s -> Term s b) -> Term s b)
-> PlutusType (Helper2 @k f a)
forall k (f :: k -> PType) (a :: k) (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
forall k (f :: k -> PType) (a :: k) (s :: S) (b :: PType).
Term s (PInner (Helper2 @k f a))
-> (Helper2 @k f a s -> Term s b) -> Term s b
forall (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
forall (s :: S) (b :: PType).
Term s (PInner (Helper2 @k f a))
-> (Helper2 @k f a s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
$cpcon' :: forall k (f :: k -> PType) (a :: k) (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
pcon' :: forall (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
$cpmatch' :: forall k (f :: k -> PType) (a :: k) (s :: S) (b :: PType).
Term s (PInner (Helper2 @k f a))
-> (Helper2 @k f a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (Helper2 @k f a))
-> (Helper2 @k f a s -> Term s b) -> Term s b
PlutusType)
instance DerivePlutusType (Helper2 f a) where type DPTStrat _ = PlutusTypeNewtype

instance PIsData PInteger where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PInteger) -> Term s PInteger
pfromDataImpl Term s (PAsData PInteger)
x = Term s (PData :--> PInteger)
forall (s :: S). Term s (PData :--> PInteger)
pasInt Term s (PData :--> PInteger) -> Term s PData -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PInteger) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData PInteger)
x
  pdataImpl :: forall (s :: S). Term s PInteger -> Term s PData
pdataImpl Term s PInteger
x = DefaultFun -> Term s (PInteger :--> PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IData Term s (PInteger :--> PData) -> Term s PInteger -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x

instance PIsData PByteString where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PByteString) -> Term s PByteString
pfromDataImpl Term s (PAsData PByteString)
x = Term s (PData :--> PByteString)
forall (s :: S). Term s (PData :--> PByteString)
pasByteStr Term s (PData :--> PByteString)
-> Term s PData -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PByteString) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData PByteString)
x
  pdataImpl :: forall (s :: S). Term s PByteString -> Term s PData
pdataImpl Term s PByteString
x = DefaultFun -> Term s (PByteString :--> PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.BData Term s (PByteString :--> PData)
-> Term s PByteString -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PByteString
x

{- |
  Instance for PBool following the Plutus IsData repr
  given by @makeIsDataIndexed ''Bool [('False,0),('True,1)]@,
  which is used in 'TxInfo' via 'Closure'.
-}
instance PIsData PBool where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PBool) -> Term s PBool
pfromDataImpl Term s (PAsData PBool)
x =
    ClosedTerm (PData :--> PBool) -> Term s (PData :--> PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((Term s PData -> Term s PBool) -> Term s (PData :--> PBool)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PBool) -> Term s (c :--> PBool)
plam Term s PData -> Term s PBool
forall (s :: S). Term s PData -> Term s PBool
toBool) Term s (PData :--> PBool) -> Term s PData -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData PBool)
x
    where
      toBool :: Term s PData -> Term s PBool
      toBool :: forall (s :: S). Term s PData -> Term s PBool
toBool Term s PData
d = Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
d) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1

  pdataImpl :: forall (s :: S). Term s PBool -> Term s PData
pdataImpl Term s PBool
x =
    ClosedTerm (PBool :--> PData) -> Term s (PBool :--> PData)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((Term s PBool -> Term s PData) -> Term s (PBool :--> PData)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PData) -> Term s (c :--> PData)
plam Term s PBool -> Term s PData
forall (s :: S). Term s PBool -> Term s PData
toData) Term s (PBool :--> PData) -> Term s PBool -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
x
    where
      toData :: Term s PBool -> Term s PData
      toData :: forall (s :: S). Term s PBool -> Term s PData
toData Term s PBool
b =
        DefaultFun
-> Term s (PInteger :--> (PBuiltinList PData :--> PData))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ConstrData
          # (pif' # b # 1 # (0 :: Term s PInteger))
          # nil

      nil :: Term s (PBuiltinList PData)
      nil :: forall (s :: S). Term s (PBuiltinList PData)
nil = Term s (PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

instance PIsData (PBuiltinPair (PAsData a) (PAsData b)) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PBuiltinPair (PAsData a) (PAsData b))
pfromDataImpl Term s (PAsData (PBuiltinPair (PAsData a) (PAsData b)))
x = Term
  s
  (PAsData (PBuiltinPair (PAsData a) (PAsData b))
   :--> PBuiltinPair (PAsData a) (PAsData b))
forall {s :: S} {a :: PType} {a :: PType} {b :: PType}.
Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
f Term
  s
  (PAsData (PBuiltinPair (PAsData a) (PAsData b))
   :--> PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PAsData (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PBuiltinPair (PAsData a) (PAsData b))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinPair (PAsData a) (PAsData b)))
x
    where
      f :: Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
f = ClosedTerm (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
 -> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b)))
-> ClosedTerm (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
forall a b. (a -> b) -> a -> b
$
        (Term s (PAsData a)
 -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (c :--> PBuiltinPair (PAsData a) (PAsData b))
plam ((Term s (PAsData a)
  -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
 -> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b)))
-> (Term s (PAsData a)
    -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
pairDat -> Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData)
    -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PBuiltinPair (PAsData a) (PAsData b))
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData a)
pairDat) ((Term s (PBuiltinList PData)
  -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
 -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> (Term s (PBuiltinList PData)
    -> Term s (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PBuiltinPair (PAsData a) (PAsData b))
forall a b. (a -> b) -> a -> b
$
          \Term s (PBuiltinList PData)
pd -> Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PAsData a)
-> Term s (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData -> Term s (PAsData a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData :--> PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
pd) Term s (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PAsData b)
-> Term s (PBuiltinPair (PAsData a) (PAsData b))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s PData -> Term s (PAsData b)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData :--> PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
pd)
  pdataImpl :: forall (s :: S).
Term s (PBuiltinPair (PAsData a) (PAsData b)) -> Term s PData
pdataImpl Term s (PBuiltinPair (PAsData a) (PAsData b))
x = Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
target
    where
      target :: Term _ (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
      target :: Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
target = Term
  s
  (PBuiltinPair PData PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall {s :: S}.
Term
  s
  (PBuiltinPair PData PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
f Term
  s
  (PBuiltinPair PData PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinPair PData PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PBuiltinPair PData PData)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinPair (PAsData a) (PAsData b))
x
      f :: Term
  s
  (PBuiltinPair PData PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
f = (forall {s :: S}.
 Term
   s
   (PBuiltinPair PData PData
    :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term
     s
     (PBuiltinPair PData PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall {s :: S}.
  Term
    s
    (PBuiltinPair PData PData
     :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
 -> Term
      s
      (PBuiltinPair PData PData
       :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> (forall {s :: S}.
    Term
      s
      (PBuiltinPair PData PData
       :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term
     s
     (PBuiltinPair PData PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$
        (Term s (PBuiltinPair PData PData)
 -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term
     s
     (PBuiltinPair PData PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
 -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term
     s (c :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
plam ((Term s (PBuiltinPair PData PData)
  -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
 -> Term
      s
      (PBuiltinPair PData PData
       :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PData PData)
    -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term
     s
     (PBuiltinPair PData PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$
          \Term s (PBuiltinPair PData PData)
pair -> 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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PBuiltinPair PData PData :--> PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PData PData :--> PData)
-> Term s (PBuiltinPair PData PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pair) Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PBuiltinPair PData PData :--> PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair PData PData :--> PData)
-> Term s (PBuiltinPair PData PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pair) Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

newtype Helper3 f b a s = Helper3 (Term s (PAsData (f a b)))
  deriving stock ((forall x. Helper3 @k @k f b a s -> Rep (Helper3 @k @k f b a s) x)
-> (forall x.
    Rep (Helper3 @k @k f b a s) x -> Helper3 @k @k f b a s)
-> Generic (Helper3 @k @k f b a s)
forall x. Rep (Helper3 @k @k f b a s) x -> Helper3 @k @k f b a s
forall x. Helper3 @k @k f b a s -> Rep (Helper3 @k @k f b a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Rep (Helper3 @k @k f b a s) x -> Helper3 @k @k f b a s
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Helper3 @k @k f b a s -> Rep (Helper3 @k @k f b a s) x
$cfrom :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Helper3 @k @k f b a s -> Rep (Helper3 @k @k f b a s) x
from :: forall x. Helper3 @k @k f b a s -> Rep (Helper3 @k @k f b a s) x
$cto :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Rep (Helper3 @k @k f b a s) x -> Helper3 @k @k f b a s
to :: forall x. Rep (Helper3 @k @k f b a s) x -> Helper3 @k @k f b a s
Generic)
  deriving anyclass ((forall (s :: S).
 Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (Helper3 @k @k f b a))
    -> (Helper3 @k @k f b a s -> Term s b) -> Term s b)
-> PlutusType (Helper3 @k @k f b a)
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b a))
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S)
       (b :: PType).
Term s (PInner (Helper3 @k @k f b a))
-> (Helper3 @k @k f b a s -> Term s b) -> Term s b
forall (s :: S).
Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b a))
forall (s :: S) (b :: PType).
Term s (PInner (Helper3 @k @k f b a))
-> (Helper3 @k @k f b a s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
$cpcon' :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b a))
pcon' :: forall (s :: S).
Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b a))
$cpmatch' :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S)
       (b :: PType).
Term s (PInner (Helper3 @k @k f b a))
-> (Helper3 @k @k f b a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (Helper3 @k @k f b a))
-> (Helper3 @k @k f b a s -> Term s b) -> Term s b
PlutusType)
instance DerivePlutusType (Helper3 f b a) where type DPTStrat _ = PlutusTypeNewtype

newtype Helper4 f b a s = Helper4 (Term s (f a b))
  deriving stock ((forall x. Helper4 @k @k f b a s -> Rep (Helper4 @k @k f b a s) x)
-> (forall x.
    Rep (Helper4 @k @k f b a s) x -> Helper4 @k @k f b a s)
-> Generic (Helper4 @k @k f b a s)
forall x. Rep (Helper4 @k @k f b a s) x -> Helper4 @k @k f b a s
forall x. Helper4 @k @k f b a s -> Rep (Helper4 @k @k f b a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Rep (Helper4 @k @k f b a s) x -> Helper4 @k @k f b a s
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Helper4 @k @k f b a s -> Rep (Helper4 @k @k f b a s) x
$cfrom :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Helper4 @k @k f b a s -> Rep (Helper4 @k @k f b a s) x
from :: forall x. Helper4 @k @k f b a s -> Rep (Helper4 @k @k f b a s) x
$cto :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S) x.
Rep (Helper4 @k @k f b a s) x -> Helper4 @k @k f b a s
to :: forall x. Rep (Helper4 @k @k f b a s) x -> Helper4 @k @k f b a s
Generic)
  deriving anyclass ((forall (s :: S).
 Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b a)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (Helper4 @k @k f b a))
    -> (Helper4 @k @k f b a s -> Term s b) -> Term s b)
-> PlutusType (Helper4 @k @k f b a)
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b a))
forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S)
       (b :: PType).
Term s (PInner (Helper4 @k @k f b a))
-> (Helper4 @k @k f b a s -> Term s b) -> Term s b
forall (s :: S).
Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b a))
forall (s :: S) (b :: PType).
Term s (PInner (Helper4 @k @k f b a))
-> (Helper4 @k @k f b a s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
$cpcon' :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b a))
pcon' :: forall (s :: S).
Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b a))
$cpmatch' :: forall k k (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S)
       (b :: PType).
Term s (PInner (Helper4 @k @k f b a))
-> (Helper4 @k @k f b a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (Helper4 @k @k f b a))
-> (Helper4 @k @k f b a s -> Term s b) -> Term s b
PlutusType)
instance DerivePlutusType (Helper4 f b a) where type DPTStrat _ = PlutusTypeNewtype

instance PIsData (PBuiltinPair PData PData) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PBuiltinPair PData PData)
pfromDataImpl = Term s (PBuiltinPair (PAsData PData) (PAsData PData))
-> Term s (PBuiltinPair PData PData)
forall (s :: S).
Term s (PBuiltinPair (PAsData PData) (PAsData PData))
-> Term s (PBuiltinPair PData PData)
f (Term s (PBuiltinPair (PAsData PData) (PAsData PData))
 -> Term s (PBuiltinPair PData PData))
-> (Term s (PAsData (PBuiltinPair PData PData))
    -> Term s (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PBuiltinPair PData PData)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
 -> Term s (PBuiltinPair (PAsData PData) (PAsData PData)))
-> (Term s (PAsData (PBuiltinPair PData PData))
    -> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData))))
-> Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
forall (s :: S).
Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
g
    where
      g :: Term s (PAsData (PBuiltinPair PData PData)) -> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
      g :: forall (s :: S).
Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
g Term s (PAsData (PBuiltinPair PData PData))
x = Term
  s
  (Helper3
     @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
-> Term
     s
     (PInner
        (Helper3
           @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term
   s
   (Helper3
      @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
 -> Term
      s
      (PInner
         (Helper3
            @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))))
-> Term
     s
     (Helper3
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
-> Term
     s
     (PInner
        (Helper3
           @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
forall a b. (a -> b) -> a -> b
$ Proxy
  @(PType -> PType)
  (Helper3 @PType @PType PBuiltinPair (PAsData PData))
-> Term
     s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData)
-> Term
     s
     (Helper3
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
forall (p :: PType -> PType) (s :: S).
PVariant p =>
Proxy @(PType -> PType) p
-> Term s (p PData) -> Term s (p (PAsData PData))
prememberData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper3 PBuiltinPair (PAsData PData))) (Term s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData)
 -> Term
      s
      (Helper3
         @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term
     s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData)
-> Term
     s
     (Helper3
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s
-> Term
     s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s
 -> Term
      s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData))
-> Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s
-> Term
     s (Helper3 @PType @PType PBuiltinPair (PAsData PData) PData)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PBuiltinPair PData (PAsData PData)))
-> Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s
forall {k} {k} (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Term s (PAsData (f a b)) -> Helper3 @k @k f b a s
Helper3 (Term s (PAsData (PBuiltinPair PData (PAsData PData)))
 -> Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s)
-> Term s (PAsData (PBuiltinPair PData (PAsData PData)))
-> Helper3 @PType @PType PBuiltinPair (PAsData PData) PData s
forall a b. (a -> b) -> a -> b
$ Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData))
-> Term
     s (PInner (Helper2 @PType (PBuiltinPair PData) (PAsData PData)))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData))
 -> Term
      s (PInner (Helper2 @PType (PBuiltinPair PData) (PAsData PData))))
-> Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData))
-> Term
     s (PInner (Helper2 @PType (PBuiltinPair PData) (PAsData PData)))
forall a b. (a -> b) -> a -> b
$ Proxy @(PType -> PType) (Helper2 @PType (PBuiltinPair PData))
-> Term s (Helper2 @PType (PBuiltinPair PData) PData)
-> Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData))
forall (p :: PType -> PType) (s :: S).
PVariant p =>
Proxy @(PType -> PType) p
-> Term s (p PData) -> Term s (p (PAsData PData))
prememberData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper2 (PBuiltinPair PData))) (Term s (Helper2 @PType (PBuiltinPair PData) PData)
 -> Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData)))
-> Term s (Helper2 @PType (PBuiltinPair PData) PData)
-> Term s (Helper2 @PType (PBuiltinPair PData) (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Helper2 @PType (PBuiltinPair PData) PData s
-> Term s (Helper2 @PType (PBuiltinPair PData) PData)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper2 @PType (PBuiltinPair PData) PData s
 -> Term s (Helper2 @PType (PBuiltinPair PData) PData))
-> Helper2 @PType (PBuiltinPair PData) PData s
-> Term s (Helper2 @PType (PBuiltinPair PData) PData)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PBuiltinPair PData PData))
-> Helper2 @PType (PBuiltinPair PData) PData s
forall {k} (f :: k -> PType) (a :: k) (s :: S).
Term s (PAsData (f a)) -> Helper2 @k f a s
Helper2 Term s (PAsData (PBuiltinPair PData PData))
x

      f :: Term s (PBuiltinPair (PAsData PData) (PAsData PData)) -> Term s (PBuiltinPair PData PData)
      f :: forall (s :: S).
Term s (PBuiltinPair (PAsData PData) (PAsData PData))
-> Term s (PBuiltinPair PData PData)
f Term s (PBuiltinPair (PAsData PData) (PAsData PData))
x = Term s (Helper4 @PType @PType PBuiltinPair PData PData)
-> Term s (PInner (Helper4 @PType @PType PBuiltinPair PData PData))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s (Helper4 @PType @PType PBuiltinPair PData PData)
 -> Term
      s (PInner (Helper4 @PType @PType PBuiltinPair PData PData)))
-> Term s (Helper4 @PType @PType PBuiltinPair PData PData)
-> Term s (PInner (Helper4 @PType @PType PBuiltinPair PData PData))
forall a b. (a -> b) -> a -> b
$ Proxy @(PType -> PType) (Helper4 @PType @PType PBuiltinPair PData)
-> Term
     s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData))
-> Term s (Helper4 @PType @PType PBuiltinPair PData PData)
forall (a :: PType) (p :: PType -> PType) (s :: S).
PCovariant p =>
Proxy @(PType -> PType) p
-> Term s (p (PAsData a)) -> Term s (p PData)
pforgetData' (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper4 PBuiltinPair PData)) (Term s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData))
 -> Term s (Helper4 @PType @PType PBuiltinPair PData PData))
-> Term
     s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData))
-> Term s (Helper4 @PType @PType PBuiltinPair PData PData)
forall a b. (a -> b) -> a -> b
$ Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s
-> Term
     s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData))
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s
 -> Term
      s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData)))
-> Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s
-> Term
     s (Helper4 @PType @PType PBuiltinPair PData (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData PData) PData)
-> Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s
forall {k} {k} (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Term s (f a b) -> Helper4 @k @k f b a s
Helper4 (Term s (PBuiltinPair (PAsData PData) PData)
 -> Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s)
-> Term s (PBuiltinPair (PAsData PData) PData)
-> Helper4 @PType @PType PBuiltinPair PData (PAsData PData) s
forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (p :: PType -> PType) (s :: S).
PCovariant p =>
Proxy @(PType -> PType) p
-> Term s (p (PAsData a)) -> Term s (p PData)
pforgetData' @PData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(PBuiltinPair (PAsData PData))) Term s (PBuiltinPair (PAsData PData) (PAsData PData))
x
  pdataImpl :: forall (s :: S). Term s (PBuiltinPair PData PData) -> Term s PData
pdataImpl = Term s (PAsData (PBuiltinPair PData PData)) -> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast (Term s (PAsData (PBuiltinPair PData PData)) -> Term s PData)
-> (Term s (PBuiltinPair PData PData)
    -> Term s (PAsData (PBuiltinPair PData PData)))
-> Term s (PBuiltinPair PData PData)
-> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PAsData (PBuiltinPair PData PData))
forall (s :: S).
Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PAsData (PBuiltinPair PData PData))
f (Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
 -> Term s (PAsData (PBuiltinPair PData PData)))
-> (Term s (PBuiltinPair PData PData)
    -> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData))))
-> Term s (PBuiltinPair PData PData)
-> Term s (PAsData (PBuiltinPair PData PData))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair (PAsData PData) (PAsData PData))
-> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (PBuiltinPair (PAsData PData) (PAsData PData))
 -> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData))))
-> (Term s (PBuiltinPair PData PData)
    -> Term s (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PBuiltinPair PData PData)
-> Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PData PData)
-> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
forall (s :: S).
Term s (PBuiltinPair PData PData)
-> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
g
    where
      g :: Term s (PBuiltinPair PData PData) -> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
      g :: forall (s :: S).
Term s (PBuiltinPair PData PData)
-> Term s (PBuiltinPair (PAsData PData) (PAsData PData))
g Term s (PBuiltinPair PData PData)
x = Term
  s
  (Helper4
     @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
-> Term
     s
     (PInner
        (Helper4
           @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term
   s
   (Helper4
      @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
 -> Term
      s
      (PInner
         (Helper4
            @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))))
-> Term
     s
     (Helper4
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
-> Term
     s
     (PInner
        (Helper4
           @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
forall a b. (a -> b) -> a -> b
$ Proxy
  @(PType -> PType)
  (Helper4 @PType @PType PBuiltinPair (PAsData PData))
-> Term
     s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData)
-> Term
     s
     (Helper4
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
forall (p :: PType -> PType) (s :: S).
PVariant p =>
Proxy @(PType -> PType) p
-> Term s (p PData) -> Term s (p (PAsData PData))
prememberData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper4 PBuiltinPair (PAsData PData))) (Term s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData)
 -> Term
      s
      (Helper4
         @PType @PType PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term
     s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData)
-> Term
     s
     (Helper4
        @PType @PType PBuiltinPair (PAsData PData) (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s
-> Term
     s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s
 -> Term
      s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData))
-> Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s
-> Term
     s (Helper4 @PType @PType PBuiltinPair (PAsData PData) PData)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PData (PAsData PData))
-> Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s
forall {k} {k} (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Term s (f a b) -> Helper4 @k @k f b a s
Helper4 (Term s (PBuiltinPair PData (PAsData PData))
 -> Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s)
-> Term s (PBuiltinPair PData (PAsData PData))
-> Helper4 @PType @PType PBuiltinPair (PAsData PData) PData s
forall a b. (a -> b) -> a -> b
$ Proxy @(PType -> PType) (PBuiltinPair PData)
-> Term s (PBuiltinPair PData PData)
-> Term s (PBuiltinPair PData (PAsData PData))
forall (p :: PType -> PType) (s :: S).
PVariant p =>
Proxy @(PType -> PType) p
-> Term s (p PData) -> Term s (p (PAsData PData))
prememberData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(PBuiltinPair PData)) Term s (PBuiltinPair PData PData)
x

      f :: Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData))) -> Term s (PAsData (PBuiltinPair PData PData))
      f :: forall (s :: S).
Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PAsData (PBuiltinPair PData PData))
f Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
x = Term s (Helper3 @PType @PType PBuiltinPair PData PData)
-> Term s (PInner (Helper3 @PType @PType PBuiltinPair PData PData))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s (Helper3 @PType @PType PBuiltinPair PData PData)
 -> Term
      s (PInner (Helper3 @PType @PType PBuiltinPair PData PData)))
-> Term s (Helper3 @PType @PType PBuiltinPair PData PData)
-> Term s (PInner (Helper3 @PType @PType PBuiltinPair PData PData))
forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (p :: PType -> PType) (s :: S).
PCovariant p =>
Proxy @(PType -> PType) p
-> Term s (p (PAsData a)) -> Term s (p PData)
pforgetData' @PData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper3 PBuiltinPair PData)) (Term s (Helper3 @PType @PType PBuiltinPair PData (PAsData PData))
 -> Term s (Helper3 @PType @PType PBuiltinPair PData PData))
-> Term
     s (Helper3 @PType @PType PBuiltinPair PData (PAsData PData))
-> Term s (Helper3 @PType @PType PBuiltinPair PData PData)
forall a b. (a -> b) -> a -> b
$ Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s
-> Term
     s (Helper3 @PType @PType PBuiltinPair PData (PAsData PData))
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s
 -> Term
      s (Helper3 @PType @PType PBuiltinPair PData (PAsData PData)))
-> Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s
-> Term
     s (Helper3 @PType @PType PBuiltinPair PData (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PBuiltinPair (PAsData PData) PData))
-> Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s
forall {k} {k} (f :: k -> k -> PType) (b :: k) (a :: k) (s :: S).
Term s (PAsData (f a b)) -> Helper3 @k @k f b a s
Helper3 (Term s (PAsData (PBuiltinPair (PAsData PData) PData))
 -> Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s)
-> Term s (PAsData (PBuiltinPair (PAsData PData) PData))
-> Helper3 @PType @PType PBuiltinPair PData (PAsData PData) s
forall a b. (a -> b) -> a -> b
$ Term s (Helper2 @PType (PBuiltinPair (PAsData PData)) PData)
-> Term
     s (PInner (Helper2 @PType (PBuiltinPair (PAsData PData)) PData))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s (Helper2 @PType (PBuiltinPair (PAsData PData)) PData)
 -> Term
      s (PInner (Helper2 @PType (PBuiltinPair (PAsData PData)) PData)))
-> Term s (Helper2 @PType (PBuiltinPair (PAsData PData)) PData)
-> Term
     s (PInner (Helper2 @PType (PBuiltinPair (PAsData PData)) PData))
forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (p :: PType -> PType) (s :: S).
PCovariant p =>
Proxy @(PType -> PType) p
-> Term s (p (PAsData a)) -> Term s (p PData)
pforgetData' @PData (forall {k} (t :: k). Proxy @k t
forall (t :: PType -> PType). Proxy @(PType -> PType) t
Proxy @(Helper2 (PBuiltinPair (PAsData PData)))) (Term
   s (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData))
 -> Term s (Helper2 @PType (PBuiltinPair (PAsData PData)) PData))
-> Term
     s (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData))
-> Term s (Helper2 @PType (PBuiltinPair (PAsData PData)) PData)
forall a b. (a -> b) -> a -> b
$ Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData) s
-> Term
     s (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData))
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData) s
 -> Term
      s (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData)))
-> Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData) s
-> Term
     s (Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData))
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Helper2 @PType (PBuiltinPair (PAsData PData)) (PAsData PData) s
forall {k} (f :: k -> PType) (a :: k) (s :: S).
Term s (PAsData (f a)) -> Helper2 @k f a s
Helper2 Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
x

instance (PShow a, PShow b) => PShow (PBuiltinPair a b) where
  pshow' :: forall (s :: S).
Bool -> Term s (PBuiltinPair a b) -> Term s PString
pshow' Bool
_ Term s (PBuiltinPair a b)
pair = Term s PString
"(" Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s a -> Term s PString
forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow (Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
pair) Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
"," Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s b -> Term s PString
forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow (Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
pair) Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
")"

instance (PEq a, PEq b) => PEq (PBuiltinPair a b) where
  Term s (PBuiltinPair a b)
p1 #== :: forall (s :: S).
Term s (PBuiltinPair a b)
-> Term s (PBuiltinPair a b) -> Term s PBool
#== Term s (PBuiltinPair a b)
p2 = Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b) -> Term s a
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p2 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 Term s b -> Term s b -> Term s PBool
forall (s :: S). Term s b -> Term s b -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term s (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p2

instance PIsData PUnit where
  pfromDataImpl :: forall (s :: S). Term s (PAsData (PUnit @S)) -> Term s (PUnit @S)
pfromDataImpl Term s (PAsData (PUnit @S))
_ = AsHaskell (PUnit @S) -> Term s (PUnit @S)
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant ()
  pdataImpl :: forall (s :: S). Term s (PUnit @S) -> Term s PData
pdataImpl Term s (PUnit @S)
_ = AsHaskell PData -> Term s PData
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (Integer -> [Data] -> Data
Constr Integer
0 [])

-- This instance is kind of useless. There's no safe way to use 'pdata'.
instance PIsData (PBuiltinPair PInteger (PBuiltinList PData)) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
pfromDataImpl Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
x = 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
x
  pdataImpl :: forall (s :: S).
Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s PData
pdataImpl Term s (PBuiltinPair PInteger (PBuiltinList PData))
x' = Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast (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 (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PBuiltinPair PInteger (PBuiltinList PData))
x' ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
  -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
 -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
x -> 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x) Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x

pconstrBuiltin :: Term s (PInteger :--> PBuiltinList PData :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
pconstrBuiltin :: forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin = DefaultFun
-> Term
     s
     (PInteger
      :--> (PBuiltinList PData
            :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ConstrData

{- | Create a Plutarch-level 'PAsData' constant, from a Haskell value.
Example:
> pconstantData @PInteger 42
-}
pconstantData ::
  forall (p :: S -> Type) (h :: Type) (s :: S).
  (ToData h, AsHaskell p ~ h) =>
  h ->
  Term s (PAsData p)
pconstantData :: forall (p :: PType) h (s :: S).
(ToData h, (AsHaskell p :: Type) ~ (h :: Type)) =>
h -> Term s (PAsData p)
pconstantData h
x = let ()
_ = Proxy @Constraint ((AsHaskell p :: Type) ~ (h :: Type)) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(AsHaskell p ~ h)) in Term s PData -> Term s (PAsData p)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s (PAsData p))
-> Term s PData -> Term s (PAsData p)
forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PData (AsHaskell PData -> Term s PData)
-> AsHaskell PData -> Term s PData
forall a b. (a -> b) -> a -> b
$ h -> Data
forall a. ToData a => a -> Data
PlutusTx.toData h
x

newtype Flip f a b = Flip (f b a) deriving stock ((forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x)
-> (forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b)
-> Generic (Flip @k @k f a b)
forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
from :: forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
to :: forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
Generic)

instance PTryFrom PData (PAsData PInteger) where
  type PTryFromExcess PData (PAsData PInteger) = Flip Term PInteger
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PInteger),
   Reduce (PTryFromExcess PData (PAsData PInteger) s))
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PInteger),
    Reduce (PTryFromExcess PData (PAsData PInteger) s))
 -> ((Term s (PAsData PInteger),
      Reduce (PTryFromExcess PData (PAsData PInteger) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PInteger),
      Reduce (PTryFromExcess PData (PAsData PInteger) s))
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PInteger
ver <- ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PInteger -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PInteger))
-> ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PInteger)
forall (s :: S). Term s (PData :--> PInteger)
pasInt Term s (PData :--> PInteger) -> Term s PData -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData PInteger), Term s PInteger)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PInteger)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PInteger
ver)

instance PTryFrom PData (PAsData PByteString) where
  type PTryFromExcess PData (PAsData PByteString) = Flip Term PByteString
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PByteString),
   Reduce (PTryFromExcess PData (PAsData PByteString) s))
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PByteString),
    Reduce (PTryFromExcess PData (PAsData PByteString) s))
 -> ((Term s (PAsData PByteString),
      Reduce (PTryFromExcess PData (PAsData PByteString) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PByteString),
      Reduce (PTryFromExcess PData (PAsData PByteString) s))
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PByteString
ver <- ((Term s PByteString -> Term s r) -> Term s r)
-> TermCont @r s (Term s PByteString)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PByteString -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PByteString))
-> ((Term s PByteString -> Term s r) -> Term s r)
-> TermCont @r s (Term s PByteString)
forall a b. (a -> b) -> a -> b
$ Term s PByteString -> (Term s PByteString -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PByteString)
forall (s :: S). Term s (PData :--> PByteString)
pasByteStr Term s (PData :--> PByteString)
-> Term s PData -> Term s PByteString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData PByteString), Term s PByteString)
-> TermCont @r s (Term s (PAsData PByteString), Term s PByteString)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PByteString)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PByteString
ver)

{- |
    This verifies a list to be indeed a list but doesn't recover the inner data
    use this instance instead of the one for `PData (PAsData (PBuiltinList (PAsData a)))`
    as this is O(1) instead of O(n)
-}

-- TODO: add the excess inner type list
instance PTryFrom PData (PAsData (PBuiltinList PData)) where
  type PTryFromExcess PData (PAsData (PBuiltinList PData)) = Flip Term (PBuiltinList PData)
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinList PData)),
   Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinList PData)),
    Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
 -> ((Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList PData)
ver <- ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList PData)))
-> ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinList PData)
forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList Term s (PData :--> PBuiltinList PData)
-> Term s PData -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData (PBuiltinList PData)),
 Term s (PBuiltinList PData))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Term s (PBuiltinList PData))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinList PData)
ver)

{- |
    Recover a `PBuiltinList (PAsData a)`
-}
instance
  ( PTryFrom PData (PAsData a)
  , PIsData a
  ) =>
  PTryFrom PData (PAsData (PBuiltinList (PAsData a)))
  where
  type PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) = Flip Term (PBuiltinList (PAsData a))
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinList (PAsData a))),
   Reduce
     (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinList (PAsData a))),
    Reduce
      (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
 -> ((Term s (PAsData (PBuiltinList (PAsData a))),
      Reduce
        (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList (PAsData a))),
      Reduce
        (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    let lst :: Term _ (PBuiltinList PData)
        lst :: Term s (PBuiltinList PData)
lst = Term s (PData :--> PBuiltinList PData)
forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList Term s (PData :--> PBuiltinList PData)
-> Term s PData -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
        verify :: Term _ (PData :--> PAsData a)
        verify :: Term s (PData :--> PAsData a)
verify = (Term s PData -> Term s (PAsData a))
-> Term s (PData :--> PAsData a)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PAsData a)) -> Term s (c :--> PAsData a)
plam ((Term s PData -> Term s (PAsData a))
 -> Term s (PData :--> PAsData a))
-> (Term s PData -> Term s (PAsData a))
-> Term s (PData :--> PAsData a)
forall a b. (a -> b) -> a -> b
$ \Term s PData
e ->
          TermCont @(PAsData a) s (Term s (PAsData a)) -> Term s (PAsData a)
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @(PAsData a) s (Term s (PAsData a))
 -> Term s (PAsData a))
-> TermCont @(PAsData a) s (Term s (PAsData a))
-> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ do
            (Term s (PAsData a)
wrapped, GReduce
  (PTryFromExcess PData (PAsData a) s)
  (Rep (PTryFromExcess PData (PAsData a) s))
_) <- (((Term s (PAsData a),
   GReduce
     (PTryFromExcess PData (PAsData a) s)
     (Rep (PTryFromExcess PData (PAsData a) s)))
  -> Term s (PAsData a))
 -> Term s (PAsData a))
-> TermCont
     @(PAsData a)
     s
     (Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData a),
    GReduce
      (PTryFromExcess PData (PAsData a) s)
      (Rep (PTryFromExcess PData (PAsData a) s)))
   -> Term s (PAsData a))
  -> Term s (PAsData a))
 -> TermCont
      @(PAsData a)
      s
      (Term s (PAsData a),
       GReduce
         (PTryFromExcess PData (PAsData a) s)
         (Rep (PTryFromExcess PData (PAsData a) s))))
-> (((Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
     -> Term s (PAsData a))
    -> Term s (PAsData a))
-> TermCont
     @(PAsData a)
     s
     (Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData a) (Term s PData
 -> ((Term s (PAsData a),
      Reduce (PTryFromExcess PData (PAsData a) s))
     -> Term s (PAsData a))
 -> Term s (PAsData a))
-> Term s PData
-> ((Term s (PAsData a),
     Reduce (PTryFromExcess PData (PAsData a) s))
    -> Term s (PAsData a))
-> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ Term s PData
e
            Term s (PAsData a) -> TermCont @(PAsData a) s (Term s (PAsData a))
forall a. a -> TermCont @(PAsData a) s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s (PAsData a)
wrapped
    Term s (PBuiltinList (PAsData a))
ver <- ((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList (PAsData a)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList (PAsData a))))
-> ((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList (PAsData a)))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList (PAsData a))
-> (Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinList (PAsData a))
 -> (Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> Term s (PBuiltinList (PAsData a))
-> (Term s (PBuiltinList (PAsData a)) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term
  s
  ((PData :--> PAsData a)
   :--> (PBuiltinList PData :--> PBuiltinList (PAsData a)))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap Term
  s
  ((PData :--> PAsData a)
   :--> (PBuiltinList PData :--> PBuiltinList (PAsData a)))
-> Term s (PData :--> PAsData a)
-> Term s (PBuiltinList PData :--> PBuiltinList (PAsData a))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PAsData a)
forall {s :: S}. Term s (PData :--> PAsData a)
verify Term s (PBuiltinList PData :--> PBuiltinList (PAsData a))
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList (PAsData a))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
lst
    (Term s (PAsData (PBuiltinList (PAsData a))),
 Term s (PBuiltinList (PAsData a)))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList (PAsData a))),
      Term s (PBuiltinList (PAsData a)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PBuiltinList (PAsData a)))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinList (PAsData a))
ver)

{- |
    Recover a `PAsData (PBuiltinPair a b)`
-}
instance
  ( PTryFrom PData a
  , a ~ PAsData a'
  , PIsData a'
  , PTryFrom PData b
  , b ~ PAsData b'
  , PIsData b'
  ) =>
  PTryFrom PData (PAsData (PBuiltinPair a b))
  where
  type PTryFromExcess PData (PAsData (PBuiltinPair a b)) = Flip Term (PBuiltinPair a b)
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinPair a b)),
   Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinPair a b)),
    Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
 -> ((Term s (PAsData (PBuiltinPair a b)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinPair a b)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup <- ((Term
    s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term
        s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term
         s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))))
-> ((Term
       s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term
        s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> (Term
      s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PAsData
     (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
   s
   (PAsData
      (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
 -> Term
      s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s
     (PAsData
        (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
forall a b. (a -> b) -> a -> b
$ Term s PData
-> Term
     s
     (PAsData
        (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq)
    let fst' :: Term _ a
        fst' :: Term s a
fst' = TermCont @a s (Term s a) -> Term s a
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @a s (Term s a) -> Term s a)
-> TermCont @a s (Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ (Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a
forall a b. (a, b) -> a
fst ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
-> TermCont @a s (Term s a, Reduce (PTryFromExcess PData a s))
-> TermCont @a s (Term s a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
 -> Term s a)
-> TermCont @a s (Term s a, Reduce (PTryFromExcess PData a s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @a (Term s PData
 -> ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
 -> Term s a)
-> Term s PData
-> ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
-> Term s a
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (Any @PType)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (Any @PType)) -> Term s PData)
-> Term s (PAsData (Any @PType)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> Term s (PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup)
        snd' :: Term _ b
        snd' :: Term s b
snd' = TermCont @b s (Term s b) -> Term s b
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ (Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b
forall a b. (a, b) -> a
fst ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
-> TermCont @b s (Term s b, Reduce (PTryFromExcess PData b s))
-> TermCont @b s (Term s b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
 -> Term s b)
-> TermCont @b s (Term s b, Reduce (PTryFromExcess PData b s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @b (Term s PData
 -> ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
 -> Term s b)
-> Term s PData
-> ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
-> Term s b
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (Any @PType)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (Any @PType)) -> Term s PData)
-> Term s (PAsData (Any @PType)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> Term s (PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup)
    Term s (PBuiltinPair (PAsData a') (PAsData b'))
ver <- ((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
 -> Term s r)
-> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
  -> Term s r)
 -> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b'))))
-> ((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
    -> Term s r)
-> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData a') (PAsData b'))
-> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
-> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair (PAsData a') (PAsData b'))
 -> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
 -> Term s r)
-> Term s (PBuiltinPair (PAsData a') (PAsData b'))
-> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PAsData a'
   :--> (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b')))
forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin Term
  s
  (PAsData a'
   :--> (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b')))
-> Term s (PAsData a')
-> Term s (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b'))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
Term s (PAsData a')
fst' Term s (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b'))
-> Term s (PAsData b')
-> Term s (PBuiltinPair (PAsData a') (PAsData b'))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
Term s (PAsData b')
snd'
    (Term s (PAsData (PBuiltinPair (PAsData a') (PAsData b'))),
 Term s (PBuiltinPair (PAsData a') (PAsData b')))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinPair (PAsData a') (PAsData b'))),
      Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData
-> Term s (PAsData (PBuiltinPair (PAsData a') (PAsData b')))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinPair (PAsData a') (PAsData b'))
ver)

----------------------- other utility functions -----------------------------------------

instance PTryFrom PData (PAsData PData) where
  type PTryFromExcess PData (PAsData PData) = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PData),
   Reduce (PTryFromExcess PData (PAsData PData) s))
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PData),
    Reduce (PTryFromExcess PData (PAsData PData) s))
 -> ((Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData PData),
 Reduce (PTryFromExcess PData (PAsData PData) s))
-> TermCont
     @r
     s
     (Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PData)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PData
opq, ())

instance PTryFrom PData PData where
  type PTryFromExcess PData PData = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s PData, Reduce (PTryFromExcess PData PData s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq (Term s PData, Reduce (PTryFromExcess PData PData s)) -> Term s r
f = (Term s PData, Reduce (PTryFromExcess PData PData s)) -> Term s r
f (Term s PData
opq, ())

-- | @since 1.7.0
newtype PDataNewtype (a :: S -> Type) (s :: S) = PDataNewtype (Term s (PAsData a))
  deriving stock
    ( -- | @since 1.7.0
      (forall x. PDataNewtype a s -> Rep (PDataNewtype a s) x)
-> (forall x. Rep (PDataNewtype a s) x -> PDataNewtype a s)
-> Generic (PDataNewtype a s)
forall x. Rep (PDataNewtype a s) x -> PDataNewtype a s
forall x. PDataNewtype a s -> Rep (PDataNewtype a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x.
Rep (PDataNewtype a s) x -> PDataNewtype a s
forall (a :: PType) (s :: S) x.
PDataNewtype a s -> Rep (PDataNewtype a s) x
$cfrom :: forall (a :: PType) (s :: S) x.
PDataNewtype a s -> Rep (PDataNewtype a s) x
from :: forall x. PDataNewtype a s -> Rep (PDataNewtype a s) x
$cto :: forall (a :: PType) (s :: S) x.
Rep (PDataNewtype a s) x -> PDataNewtype a s
to :: forall x. Rep (PDataNewtype a s) x -> PDataNewtype a s
Generic
    )

-- | @since 1.7.0
instance PlutusType (PDataNewtype a) where
  type PInner (PDataNewtype a) = PData
  pcon' :: forall (s :: S).
PDataNewtype a s -> Term s (PInner (PDataNewtype a))
pcon' (PDataNewtype Term s (PAsData a)
a) = Term s (PAsData a) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData a)
a
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PDataNewtype a))
-> (PDataNewtype a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PDataNewtype a))
x' PDataNewtype a s -> Term s b
f = PDataNewtype a s -> Term s b
f (Term s (PAsData a) -> PDataNewtype a s
forall (a :: PType) (s :: S).
Term s (PAsData a) -> PDataNewtype a s
PDataNewtype (Term s (PInner (PDataNewtype a)) -> Term s (PAsData a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataNewtype a))
x'))

-- | @since 1.7.0
instance PIsData (PDataNewtype a) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PDataNewtype a)) -> Term s (PDataNewtype a)
pfromDataImpl = Term s (PAsData (PDataNewtype a)) -> Term s (PDataNewtype a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce
  pdataImpl :: forall (s :: S). Term s (PDataNewtype a) -> Term s PData
pdataImpl = Term s (PDataNewtype a) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | @since 1.7.0
instance PEq (PDataNewtype a) where
  Term s (PDataNewtype a)
a #== :: forall (s :: S).
Term s (PDataNewtype a) -> Term s (PDataNewtype a) -> Term s PBool
#== Term s (PDataNewtype a)
b = Term s (PDataNewtype a) -> Term s (PInner (PDataNewtype a))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataNewtype a)
a Term s (PInner (PDataNewtype a))
-> Term s (PInner (PDataNewtype a)) -> Term s PBool
forall (s :: S).
Term s (PInner (PDataNewtype a))
-> Term s (PInner (PDataNewtype a)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PDataNewtype a) -> Term s (PInner (PDataNewtype a))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataNewtype a)
b

-- | @since 1.7.0
instance (PIsData a, PPartialOrd a) => PPartialOrd (PDataNewtype a) where
  Term s (PDataNewtype a)
a #<= :: forall (s :: S).
Term s (PDataNewtype a) -> Term s (PDataNewtype a) -> Term s PBool
#<= Term s (PDataNewtype a)
b =
    Term s (PDataNewtype a)
-> (PDataNewtype a s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataNewtype a)
a \(PDataNewtype Term s (PAsData a)
a') ->
      Term s (PDataNewtype a)
-> (PDataNewtype a s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataNewtype a)
b \(PDataNewtype Term s (PAsData a)
b') ->
        Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
a' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
b'
  Term s (PDataNewtype a)
a #< :: forall (s :: S).
Term s (PDataNewtype a) -> Term s (PDataNewtype a) -> Term s PBool
#< Term s (PDataNewtype a)
b =
    Term s (PDataNewtype a)
-> (PDataNewtype a s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataNewtype a)
a \(PDataNewtype Term s (PAsData a)
a') ->
      Term s (PDataNewtype a)
-> (PDataNewtype a s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataNewtype a)
b \(PDataNewtype Term s (PAsData a)
b') ->
        Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
a' Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
b'

-- | @since 1.7.0
instance (PIsData a, PPartialOrd a) => POrd (PDataNewtype a)

-- | @since 1.7.0
instance (PIsData a, PShow a) => PShow (PDataNewtype a) where
  pshow' :: forall (s :: S). Bool -> Term s (PDataNewtype a) -> Term s PString
pshow' Bool
x Term s (PDataNewtype a)
t =
    Term s (PDataNewtype a)
-> (PDataNewtype a s -> Term s PString) -> Term s PString
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataNewtype a)
t \(PDataNewtype Term s (PAsData a)
t') -> Bool -> Term s a -> Term s PString
forall (s :: S). Bool -> Term s a -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
x (Term s a -> Term s PString) -> Term s a -> Term s PString
forall a b. (a -> b) -> a -> b
$ Term s (PAsData a) -> Term s a
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
t'

-- | @since 1.7.0
instance (PIsData a, PTryFrom PData (PAsData a)) => PTryFrom PData (PDataNewtype a)

-- | @since 1.7.0
instance PTryFrom PData (PAsData (PDataNewtype a))

-- | @since 1.7.0
instance PTryFrom PData (PAsData PBool) where
  type PTryFromExcess PData (PAsData PBool) = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PBool),
   Reduce (PTryFromExcess PData (PAsData PBool) s))
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PBool),
    Reduce (PTryFromExcess PData (PAsData PBool) s))
 -> ((Term s (PAsData PBool),
      Reduce (PTryFromExcess PData (PAsData PBool) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PBool),
      Reduce (PTryFromExcess PData (PAsData PBool) s))
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr <- ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
        -> Term s r)
    -> Term s r)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @r 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    let ix :: Term s PInteger
ix = Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((() -> Term s r) -> Term s r) -> TermCont @r s ())
-> ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a b. (a -> b) -> a -> b
$ \() -> Term s r
f ->
      Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PInteger
ix Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s PInteger
ix Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1)
        (() -> Term s r
f ())
        (Term s PString -> Term s r
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"PTryFrom(PAsData PBool): invalid constructor tag")
    let dat :: Term s (PBuiltinList PData)
dat = Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((() -> Term s r) -> Term s r) -> TermCont @r s ())
-> ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a b. (a -> b) -> a -> b
$ \() -> Term s r
f ->
      Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PBuiltinList PData :--> PBool)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBool)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull Term s (PBuiltinList PData :--> PBool)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
dat)
        (() -> Term s r
f ())
        (Term s PString -> Term s r
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"PTryFrom(PAsData PBool): non-empty constructor list")
    (Term s (PAsData PBool), ())
-> TermCont @r s (Term s (PAsData PBool), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PBool)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, ())