{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Internal.IsData (PIsData, pfromDataImpl, pdataImpl, pdata, pfromData, pforgetData, prememberData, pforgetData', prememberData') where

import Plutarch.Builtin.Bool (PBool, pif')
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PBuiltinPair,
  PData,
  pasConstr,
  pasList,
  pconstrBuiltin,
  pfstBuiltin,
  plistData,
  ppairDataBuiltin,
  psndBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger, pconstantInteger)
import Plutarch.Builtin.Unit (PUnit, punit)

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))

import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.ListLike (
  PListLike (pcons, phead, pnil, ptail),
 )

import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (PLamN (plam))
import Plutarch.Internal.PlutusType (
  PCovariant,
  PVariant,
  PlutusType (PInner),
 )
import Plutarch.Internal.Subtype (PSubtype, pupcast, pupcastF)
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plet,
  punsafeBuiltin,
  punsafeCoerce,
  punsafeConstantInternal,
  (#),
  (#$),
 )
import Plutarch.Internal.Witness (witness)
import Plutarch.Unsafe (punsafeDowncast)

import PlutusCore qualified as PLC
import PlutusTx qualified as PTx

{- | 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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). 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

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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce

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 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
#== Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
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 # pconstantInteger 1 # (pconstantInteger 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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). 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 (b :: PType) (a :: PType) (s :: S). 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
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
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

instance PIsData (PBuiltinPair PData PData) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PBuiltinPair PData PData)
pfromDataImpl = forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromDataImpl @(PBuiltinPair PData PData) (Term s (PAsData (PBuiltinPair PData PData))
 -> Term s (PBuiltinPair PData PData))
-> (Term s (PAsData (PBuiltinPair PData PData))
    -> Term s (PAsData (PBuiltinPair PData 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 PData PData))
-> Term s (PAsData (PBuiltinPair PData PData))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce
  pdataImpl :: forall (s :: S). Term s (PBuiltinPair PData PData) -> Term s PData
pdataImpl = Term s PData -> Term s PData
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s PData)
-> (Term s (PBuiltinPair PData PData) -> Term s PData)
-> Term s (PBuiltinPair PData PData)
-> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PIsData a => Term s a -> Term s PData
pdataImpl @(PBuiltinPair PData PData)

-- 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

instance PIsData PInteger where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PInteger) -> Term s PInteger
pfromDataImpl Term s (PAsData PInteger)
x = DefaultFun -> Term s (PData :--> PInteger)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnIData 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 = DefaultFun -> Term s (PData :--> PByteString)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnBData 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 PIsData PUnit where
  pfromDataImpl :: forall (s :: S). Term s (PAsData PUnit) -> Term s PUnit
pfromDataImpl Term s (PAsData PUnit)
_ = Term s PUnit
forall (s :: S). Term s PUnit
punit
  pdataImpl :: forall (s :: S). Term s PUnit -> Term s PData
pdataImpl Term s PUnit
_ = Some @Type (ValueOf DefaultUni) -> Term s PData
forall (s :: S) (a :: PType).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal (Some @Type (ValueOf DefaultUni) -> Term s PData)
-> Some @Type (ValueOf DefaultUni) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Data -> Some @Type (ValueOf DefaultUni)
forall a (uni :: Type -> Type).
Contains @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue (Integer -> [Data] -> Data
PTx.Constr Integer
0 [])

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 (b :: PType) (a :: PType) (s :: S). 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