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

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

import Data.Kind (Constraint, Type)
import GHC.TypeError (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), TypeError)
import GHC.TypeLits (Symbol)
import Plutarch.Builtin.Bool (PBool, pif)
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PBuiltinPair (PBuiltinPair),
  PData,
  pasConstr,
  pasList,
  pconstrBuiltin,
  plistData,
  ppairDataBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger, pconstantInteger)
import Plutarch.Builtin.Unit (PUnit, punit)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.ListLike (
  PListLike (pcons, phead, pnil, ptail),
 )
import Plutarch.Internal.PLam (PLamN (plam))
import Plutarch.Internal.PlutusType (
  PInnermost,
  PlutusType (PInner),
  pmatch,
 )
import Plutarch.Internal.Subtype (
  PSubtype,
  pto,
  punsafeDowncast,
  pupcast,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plet,
  punsafeBuiltin,
  punsafeCoerce,
  punsafeConstantInternal,
  (#),
  (#$),
 )
import PlutusCore qualified as PLC
import PlutusTx qualified as PTx

type family PInnermostIsData' (msg :: Maybe Symbol) (a :: k) (b :: S -> Type) :: Constraint where
  PInnermostIsData' _ _ PData = ()
  PInnermostIsData' ('Just msg) a b =
    TypeError
      ( 'Text msg
          ':$$: 'Text "Inner most representation of \""
            ':<>: 'ShowType a
            ':<>: 'Text "\" is \""
            ':<>: 'ShowType b
            ':<>: 'Text "\""
      )
      ~ ()
  PInnermostIsData' 'Nothing a b =
    TypeError
      ( 'Text "Inner most representation of \""
          ':<>: 'ShowType a
          ':<>: 'Text "\" is \""
          ':<>: 'ShowType b
          ':<>: 'Text "\""
      )
      ~ ()

class (PInnermostIsData' msg a (PInnermost a), PInnermost a ~ PData) => PInnermostIsData msg a
instance (PInnermostIsData' msg a (PInnermost a), PInnermost a ~ PData) => PInnermostIsData msg a

{- | 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 :: S -> Type). 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 :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromDataImpl (Term s (PAsData a) -> Term s (PAsData (PInner a))
forall (b :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (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 (a :: S -> Type) (s :: S). 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 :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata = Term s PData -> Term s (PAsData a)
forall (b :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (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 :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData = Term s (PAsData a) -> Term s PData
forall (b :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (b :: S -> Type) (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 =
    (forall (s' :: S). Term s' (PData :--> PBool))
-> Term s (PData :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((Term s' PData -> Term s' PBool) -> Term s' (PData :--> PBool)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' PBool) -> Term s' (c :--> PBool)
plam Term s' 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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PBool) -> Term s PData
forall (s :: S) (a :: S -> Type).
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))
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s PBool)
-> Term s PBool
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
d) ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s PBool)
 -> Term s PBool)
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
x Term s (PBuiltinList PData)
_) ->
        Term s PInteger
x Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== 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 =
    (forall (s' :: S). Term s' (PBool :--> PData))
-> Term s (PBool :--> PData)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((Term s' PBool -> Term s' PData) -> Term s' (PBool :--> PData)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). 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 :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

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 :: S -> Type} {a :: S -> Type} {b :: S -> Type}.
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 :: S -> Type) (b :: S -> Type).
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 (s' :: S).
 Term s' (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b)))
-> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term s' (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b)))
 -> Term s (PAsData a :--> PBuiltinPair (PAsData a) (PAsData b)))
-> (forall (s' :: S).
    Term s' (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 :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' (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' (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s'
    -> Term s' (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s' (PBuiltinPair (PAsData a) (PAsData b))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s' (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s' (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s' PData
-> Term s' (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PAsData a) -> Term s' PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData Term s' (PAsData a)
pairDat) ((PBuiltinPair PInteger (PBuiltinList PData) s'
  -> Term s' (PBuiltinPair (PAsData a) (PAsData b)))
 -> Term s' (PBuiltinPair (PAsData a) (PAsData b)))
-> (PBuiltinPair PInteger (PBuiltinList PData) s'
    -> Term s' (PBuiltinPair (PAsData a) (PAsData b)))
-> Term s' (PBuiltinPair (PAsData a) (PAsData b))
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s' PInteger
_ Term s' (PBuiltinList PData)
y) ->
          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 :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s' (PBuiltinList PData)
y ((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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PData -> Term s' (PAsData a)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s' (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s' (PBuiltinList PData :--> PData)
-> Term s' (PBuiltinList PData) -> Term s' PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinList PData)
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s' PData -> Term s' (PAsData b)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s' (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s' (PBuiltinList PData :--> PData)
-> Term s' (PBuiltinList PData) -> Term s' PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s' (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s' (PBuiltinList PData :--> PBuiltinList PData)
-> Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinList PData)
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 :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData a) (PAsData b))
-> Term s (PBuiltinPair PData PData)
forall (b :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' 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 :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c
 -> Term s' (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' (PBuiltinPair PData PData)
-> (PBuiltinPair PData PData s'
    -> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s' (PBuiltinPair PData PData)
pair ((PBuiltinPair PData PData s'
  -> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
 -> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> (PBuiltinPair PData PData s'
    -> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s' (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s' PData
x Term s' PData
y) ->
          Term
  s'
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s'
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s' PInteger
-> Term
     s'
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# 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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s' (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s' (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s' PData
-> Term s' (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PData
x Term s' (PBuiltinList PData :--> PBuiltinList PData)
-> Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s' (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s' (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s' PData
-> Term s' (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' PData
y Term s' (PBuiltinList PData :--> PBuiltinList PData)
-> Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

instance PIsData (PBuiltinPair PData PData) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PBuiltinPair PData PData))
-> Term s (PBuiltinPair PData PData)
pfromDataImpl = forall (a :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (a :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
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 (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s
    -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinPair PInteger (PBuiltinList PData))
x ((PBuiltinPair PInteger (PBuiltinList PData) s
  -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
 -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> (PBuiltinPair PInteger (PBuiltinList PData) s
    -> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
x1 Term s (PBuiltinList PData)
x2) ->
      Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s PInteger
-> Term
     s
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x1 Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
x2

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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnIData Term s (PData :--> PInteger) -> Term s PData -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PInteger) -> Term s PData
forall (s :: S) (a :: S -> Type).
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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.IData Term s (PInteger :--> PData) -> Term s PInteger -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnBData Term s (PData :--> PByteString)
-> Term s PData -> Term s PByteString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PByteString) -> Term s PData
forall (s :: S) (a :: S -> Type).
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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.BData Term s (PByteString :--> PData)
-> Term s PByteString -> Term s PData
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type).
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).
  ( PInnermostIsData ('Just "PBuiltinList only implements PIsData when inner most type of its elements are PData") a
  , 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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinList a)) -> Term s PData
forall (s :: S) (a :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a) -> Term s (PBuiltinList PData)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList a)
x