{-# 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,
) where

import Data.Functor.Const (Const)
import Data.Proxy (Proxy (Proxy))
import GHC.Generics (Generic)
import Plutarch (
  DPTStrat,
  DerivePlutusType,
  PContravariant',
  PCovariant,
  PCovariant',
  PInner,
  PType,
  PVariant,
  PVariant',
  PlutusType,
  PlutusTypeNewtype,
  S,
  Term,
  pcon,
  pdelay,
  pfix,
  pforce,
  phoistAcyclic,
  plam,
  plet,
  pmatch,
  pto,
  (#),
  (#$),
  type (:-->),
 )
import Plutarch.Bool (PBool (..), PEq, pif, pif', (#&&), (#==))
import Plutarch.ByteString (PByteString)
import Plutarch.Integer (PInteger)
import Plutarch.Internal.PlutusType (pcon', pmatch')
import Plutarch.Internal.Witness (witness)
import Plutarch.Lift (
  DerivePConstantDirect (DerivePConstantDirect),
  PConstant,
  PConstantDecl,
  PConstantRepr,
  PConstanted,
  PLift,
  PLifted,
  PUnsafeLiftDecl,
  pconstant,
  pconstantFromRepr,
  pconstantToRepr,
 )
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.TermCont (TermCont (runTermCont), tcont, unTermCont)
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

-- | Plutus 'BuiltinPair'
newtype PBuiltinPair (a :: PType) (b :: PType) (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 (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 (forall (a :: PType) (b :: PType) (s :: S).
Term s (PBuiltinPair a b) -> PBuiltinPair a b s
PBuiltinPair Term s (PInner (PBuiltinPair a b))
x)

instance (PLift a, PLift b) => PUnsafeLiftDecl (PBuiltinPair a b) where
  type PLifted (PBuiltinPair a b) = (PLifted a, PLifted b)

-- FIXME: figure out good way of deriving this
instance (PConstant a, PConstant b) => PConstantDecl (a, b) where
  type PConstantRepr (a, b) = (PConstantRepr a, PConstantRepr b)
  type PConstanted (a, b) = PBuiltinPair (PConstanted a) (PConstanted b)
  pconstantToRepr :: (a, b) -> PConstantRepr (a, b)
pconstantToRepr (a
x, b
y) = (forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr a
x, forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr b
y)
  pconstantFromRepr :: PConstantRepr (a, b) -> Maybe (a, b)
pconstantFromRepr (PConstantRepr a
x, PConstantRepr b
y) = do
    a
x' <- forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr @a PConstantRepr a
x
    b
y' <- forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr @b PConstantRepr b
y
    forall a. a -> Maybe a
Just (a
x', b
y')

pfstBuiltin :: Term s (PBuiltinPair a b :--> a)
pfstBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin 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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin 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 = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkPairData

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

instance (PShow a, PLift 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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ 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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ 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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> 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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ 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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkCons

instance PConstant a => PConstantDecl [a] where
  type PConstantRepr [a] = [PConstantRepr a]
  type PConstanted [a] = PBuiltinList (PConstanted a)
  pconstantToRepr :: [a] -> PConstantRepr [a]
pconstantToRepr [a]
x = forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
x
  pconstantFromRepr :: PConstantRepr [a] -> Maybe [a]
pconstantFromRepr = forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr @a)

instance PUnsafeLiftDecl a => PUnsafeLiftDecl (PBuiltinList a) where
  type PLifted (PBuiltinList a) = [PLifted a]

instance PLift 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) = forall (s :: S) (a :: PType).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs
  pcon' PBuiltinList a s
PNil = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant []
  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 = 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' forall a b. (a -> b) -> a -> b
$ \Term s (PInner (PBuiltinList a))
xs ->
    forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> 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)))

instance PListLike PBuiltinList where
  type PElemConstraint PBuiltinList a = PLift 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 = 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 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 = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PBuiltinList a)
xs -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (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 = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PBuiltinList a s
PNil
  phead :: forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
phead = 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 = 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 = forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> PBool)
pnullBuiltin

type family F (a :: PType) :: Bool where
  F PData = 'True
  F (PAsData _) = 'True
  F _ = 'False

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

instance (PLift a, PEq 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 = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList a)
xs forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== 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
(#==) = forall (x :: Bool) (a :: PType) (s :: S).
Fc x a =>
Proxy @Bool x
-> Term s (PBuiltinList a)
-> Term s (PBuiltinList a)
-> Term s PBool
fc (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 (forall (s :: S). Term s (PData :--> PString)
go0 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
b) (Term s PString
"(" forall a. Semigroup a => a -> a -> a
<> Term s PString
s 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 (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam 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 = 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 forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp ->
                Term s PString
"Constr "
                  forall a. Semigroup a => a -> a -> a
<> forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
False (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
pp)
                  forall a. Semigroup a => a -> a -> a
<> Term s PString
" "
                  forall a. Semigroup a => a -> a -> a
<> forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PString)
go forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 " forall a. Semigroup a => a -> a -> a
<> forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData :--> PString)
pshowPair forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PData PData)
pp0 -> 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 forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PData PData)
pp ->
                Term s PString
"("
                  forall a. Semigroup a => a -> a -> a
<> (Term s (PData :--> PString)
go forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pp))
                  forall a. Semigroup a => a -> a -> a
<> Term s PString
", "
                  forall a. Semigroup a => a -> a -> a
<> (Term s (PData :--> PString)
go forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pp))
                  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 " forall a. Semigroup a => a -> a -> a
<> forall {list :: PType -> PType} {s :: S}.
(PElemConstraint list PString, PListLike list) =>
Term s (list PString :--> PString)
pshowListPString forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PString)
go forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
xs)
              pshowListPString :: Term s (list PString :--> PString)
pshowListPString = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
                forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list PString)
plist ->
                  Term s PString
"["
                    forall a. Semigroup a => a -> a -> a
<> 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 forall a. Semigroup a => a -> a -> a
<> (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
", " forall a. Semigroup a => a -> a -> a
<> Term s1 PString
x forall a. Semigroup a => a -> a -> a
<> Term s1 PString
r) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PString
"" :: Term s PString) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list PString)
xs0)
                      )
                      Term s PString
""
                      Term s (list PString)
plist
                    forall a. Semigroup a => a -> a -> a
<> Term s PString
"]"
           in forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$
                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 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 (forall (s :: S). Term s PData -> PData s
PData Term s (PInner PData)
t)

instance PUnsafeLiftDecl PData where type PLifted PData = Data
deriving via (DerivePConstantDirect Data PData) instance PConstantDecl Data

instance PEq PData where
  Term s PData
x #== :: forall (s :: S). Term s PData -> Term s PData -> Term s PBool
#== Term s PData
y = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$ 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant

newtype PAsData (a :: PType) (s :: S) = PAsData (Term s a)

type family IfSameThenData (a :: PType) (b :: PType) :: PType where
  IfSameThenData a a = PData
  IfSameThenData _ b = PAsData b

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) = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ 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 (forall (a :: PType) (s :: S). Term s a -> PAsData a s
PAsData forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PAsData a))
t)

type role PAsDataLifted nominal
data PAsDataLifted (a :: PType)

instance PConstantDecl (PAsDataLifted a) where
  type PConstantRepr (PAsDataLifted a) = Data
  type PConstanted (PAsDataLifted a) = PAsData a
  pconstantToRepr :: PAsDataLifted a -> PConstantRepr (PAsDataLifted a)
pconstantToRepr = \case {}
  pconstantFromRepr :: PConstantRepr (PAsDataLifted a) -> Maybe (PAsDataLifted a)
pconstantFromRepr PConstantRepr (PAsDataLifted a)
_ = forall a. Maybe a
Nothing

instance PUnsafeLiftDecl (PAsData a) where type PLifted (PAsData a) = PAsDataLifted a

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 = 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 :: PType -> PType) 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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PCovariant p)) in forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | Inverse of 'pforgetData''.
prememberData :: forall (p :: PType -> PType) 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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PVariant p)) in forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | Like 'prememberData' but generalised.
prememberData' :: forall a (p :: PType -> PType) 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 ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PSubtype PData a, PVariant p)) in 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 = forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromDataImpl (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 = forall (a :: PType) (s :: S). PIsData a => Term s a -> Term s PData
pdataImpl forall a b. (a -> b) -> a -> b
$ 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 = 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 = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 = forall a. a -> a
id

instance forall (a :: PType). 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 = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 = forall (s :: S). Term s (PBuiltinList PData :--> PData)
plistData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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
Proxy @PBuiltinList) Term s (PBuiltinList a)
x

newtype Helper2 f a s = Helper2 (Term s (PAsData (f a)))
  deriving stock (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
$cto :: forall k (f :: k -> PType) (a :: k) (s :: S) x.
Rep (Helper2 @k f a s) x -> Helper2 @k f a s
$cfrom :: forall k (f :: k -> PType) (a :: k) (s :: S) x.
Helper2 @k f a s -> Rep (Helper2 @k f a s) x
Generic)
  deriving anyclass (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 (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
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (Helper2 @k f a))
-> (Helper2 @k f a s -> Term s b) -> Term s b
$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
pcon' :: forall (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
$cpcon' :: forall k (f :: k -> PType) (a :: k) (s :: S).
Helper2 @k f a s -> Term s (PInner (Helper2 @k f a))
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 = forall (s :: S). Term s (PData :--> PInteger)
pasInt forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (s :: S). Term s (PData :--> PByteString)
pasByteStr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.BData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 =
    forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall (s :: S). Term s PData -> Term s PBool
toBool) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 = forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
d) 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 =
    forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall (s :: S). Term s PBool -> Term s PData
toData) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 =
        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 = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | NB: `PAsData (PBuiltinPair (PAsData a) (PAsData b))` and `PAsData (PTuple a b)` have the same representation.
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 = forall {s :: S} {a :: PType} {a :: PType} {b :: PType}.
Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PAsData a)
pairDat -> forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData a)
pairDat) forall a b. (a -> b) -> a -> b
$
          \Term s (PBuiltinList PData)
pd -> forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
pd) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = 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 = forall {s :: S}.
Term
  s
  (PBuiltinPair PData PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
        forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
          \Term s (PBuiltinPair PData PData)
pair -> forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pair) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PData PData)
pair) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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 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
$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
$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
Generic)
  deriving anyclass (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 (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
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
$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
pcon' :: forall (s :: S).
Helper3 @k @k f b a s -> Term s (PInner (Helper3 @k @k f b 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))
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 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
$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
$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
Generic)
  deriving anyclass (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 (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
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
$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
pcon' :: forall (s :: S).
Helper4 @k @k f b a s -> Term s (PInner (Helper4 @k @k f b 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))
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 = forall (s :: S).
Term s (PBuiltinPair (PAsData PData) (PAsData PData))
-> Term s (PBuiltinPair PData PData)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall a b. (a -> b) -> a -> b
$ 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
Proxy @(Helper3 PBuiltinPair (PAsData PData))) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall a b. (a -> b) -> a -> b
$ 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
Proxy @(Helper2 (PBuiltinPair PData))) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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 = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto 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' (forall {k} (t :: k). Proxy @k t
Proxy @(Helper4 PBuiltinPair PData)) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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 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
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 = forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S).
Term s (PAsData (PBuiltinPair (PAsData PData) (PAsData PData)))
-> Term s (PAsData (PBuiltinPair PData PData))
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall a b. (a -> b) -> a -> b
$ 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
Proxy @(Helper4 PBuiltinPair (PAsData PData))) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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
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 = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto 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
Proxy @(Helper3 PBuiltinPair PData)) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto 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
Proxy @(Helper2 (PBuiltinPair (PAsData PData)))) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ 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
"(" forall a. Semigroup a => a -> a -> a
<> forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
pair) forall a. Semigroup a => a -> a -> a
<> Term s PString
"," forall a. Semigroup a => a -> a -> a
<> forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
pair) 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 = forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p2 forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair a b)
p1 forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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))
_ = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ()
  pdataImpl :: forall (s :: S). Term s (PUnit @S) -> Term s PData
pdataImpl Term s (PUnit @S)
_ = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
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 = forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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' = forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast forall a b. (a -> b) -> a -> 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))
x' forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
x -> forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x

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 = forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsData forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
w (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData a)
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 = 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 h s. (ToData h, PLifted p ~ h, PConstanted h ~ p) => h -> Term s (PAsData p)
pconstantData :: forall (p :: PType) h (s :: S).
(ToData h, (PLifted p :: Type) ~ (h :: Type),
 (PConstanted h :: PType) ~ (p :: PType)) =>
h -> Term s (PAsData p)
pconstantData h
x = let ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(PLifted p ~ h, PConstanted h ~ p)) in forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant forall a b. (a -> b) -> a -> b
$ forall a. ToData a => a -> Data
PlutusTx.toData h
x

newtype Flip f a b = Flip (f b a) deriving stock (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
$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
$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
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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s PInteger
ver <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S). Term s (PData :--> PInteger)
pasInt forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s PByteString
ver <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S). Term s (PData :--> PByteString)
pasByteStr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList PData)
ver <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    let lst :: Term _ (PBuiltinList PData)
        lst :: Term s (PBuiltinList PData)
lst = forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PData
e ->
          forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont 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))
_) <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont 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) forall a b. (a -> b) -> a -> b
$ Term s PData
e
            forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s (PAsData a)
wrapped
    Term s (PBuiltinList (PAsData a))
ver <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ 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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall {s :: S}. Term s (PData :--> PAsData a)
verify forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
lst
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData forall a b. (a -> b) -> a -> b
$ 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' = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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' = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
fst' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
snd'
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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 = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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, ())