{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoPartialTypeSignatures #-}
-- Note (Koz, 25/08/2025): Needed to ensure that `pparseData` doesn't get used
-- on a type that doesn't have a sensible `PAsData`.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Plutarch.Internal.Parse (
  -- * Type class
  PValidateData (..),

  -- * Function
  pparseData,

  -- * Helper deriving newtype
  Don'tValidate (..),
  DeriveNewtypePValidateData (..),
) where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Exts (Any)
import Generics.SOP qualified as SOP
import Plutarch.Builtin.Bool (PBool, pif)
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList (PCons, PNil),
  PBuiltinPair (PBuiltinPair),
  PData,
  pasByteStr,
  pasConstr,
  pasInt,
  pasList,
  pasMap,
  pheadBuiltin,
  pheadTailBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Builtin.Opaque (POpaque, popaque)
import Plutarch.Internal.Case (punsafeCase)
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.IsData (PIsData, pfromData)
import Plutarch.Internal.Numeric (PPositive)
import Plutarch.Internal.Ord ((#<=))
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  PlutusType (PInner, pcon', pmatch'),
  pmatch,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  perror,
  phoistAcyclic,
  plet,
  punsafeCoerce,
  (#),
  (:-->),
 )
import Plutarch.Repr.Data (
  DeriveAsDataRec,
  DeriveAsDataStruct,
  PInnermostIsDataDataRepr,
 )
import Plutarch.Repr.Internal (UnTermRec, UnTermStruct)
import Plutarch.Repr.Tag (DeriveAsTag)

{- | Describes a @Data@ encoded Plutarch type that requires some additional
validation to ensure its structure is indeed what we expect. This is
especially useful for datums or other user-supplied arguments, since these
can be malformed.

= Why the CPS

'pwithValidated' is written in continuation-passing style (or CPS) for
reasons of efficiency. As 'pwithValidated' is meant to check structure (and
nothing more), our first instinct would be to write something like

@pwithValidated :: Term s PData -> Term s PBool@

or

@pwithValidated :: Term s PData -> Term s PUnit@

and rely on 'perror' to sort things out. However, constructing either 'PUnit'
or 'PBool' isn't free, and ultimately, this value ends up unused. At the same
time, we want to ensure that the validation specified in 'pwithValidated' is
actually performed, which neither of the above signatures can promise
anything about.

CPS solves both of these problems. Since the result of 'pwithValidated' is
technically a function that /must/ behave the same no matter what type of @r@
it operates over, we can't do anything except potentially mess with the
argument 'PData' or error out, which means we don't need to allocate any
\'result value\'. Furthermore, by working in CPS, we ensure that any
validation defined in 'pwithValidated' must happen, even if the 'PData' (or
whatever it's supposed to be) is never handled or forced.

= Important note

It is essential practice to document what /exactly/ any given instance of
'PValidateData' checks. Each instance should specify this: all the instances
provided by Plutarch and its related libraries follow this rule.

@since 1.12.0
-}
class PValidateData (a :: S -> Type) where
  pwithValidated ::
    forall (s :: S).
    Term s PData ->
    (forall (r :: S -> Type). Term s r -> Term s r)

{- | Given a 'PData', check that it is, indeed, structured as @a@ expects. If it
is, return that same 'PData' \'rewrapped\' into 'PAsData' @a@.

This helper exists to avoid having to work in CPS when writing regular code.
It is kept out of 'PValidateData' for efficiency and safety reasons.

@since 1.12.0
-}
pparseData ::
  forall (a :: S -> Type) (s :: S).
  (PIsData a, PValidateData a) =>
  Term s PData ->
  Term s (PAsData a)
pparseData :: forall (a :: S -> Type) (s :: S).
(PIsData a, PValidateData a) =>
Term s PData -> Term s (PAsData a)
pparseData Term s PData
opq = forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @a Term s PData
opq (Term s (PAsData a) -> Term s (PAsData a))
-> (Term s PData -> Term s (PAsData a))
-> Term s PData
-> Term s (PAsData a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 PData -> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ Term s PData
opq

{- | Checks (and does) nothing.

@since 1.12.0
-}
deriving via (Don'tValidate PData) instance PValidateData PData

{- | Checks that we have an @I@.

@since 1.12.0
-}
instance PValidateData PInteger where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq = Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PInteger)
forall (s :: S). Term s (PData :--> PInteger)
pasInt 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 PData
opq) ((Term s PInteger -> Term s r) -> Term s r)
-> (Term s r -> Term s PInteger -> Term s r)
-> Term s r
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s r -> Term s PInteger -> Term s r
forall a b. a -> b -> a
const

{- | Checks that we have a positive @I@.

@since 1.13.0
-}
instance PValidateData PPositive where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x =
    Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PAsData PInteger) -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PInteger) -> Term s PInteger)
-> Term s (PAsData PInteger) -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S).
(PIsData a, PValidateData a) =>
Term s PData -> Term s (PAsData a)
pparseData @PInteger Term s PData
opq) ((Term s PInteger -> Term s r) -> Term s r)
-> (Term s PInteger -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n ->
      Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PInteger
n 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).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0) Term s r
forall (s :: S) (a :: S -> Type). Term s a
perror Term s r
x

{- | Checks that we have a @B@.

@since 1.12.0
-}
instance PValidateData PByteString where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq = Term s PByteString -> (Term s PByteString -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PByteString)
forall (s :: S). Term s (PData :--> PByteString)
pasByteStr 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 PData
opq) ((Term s PByteString -> Term s r) -> Term s r)
-> (Term s r -> Term s PByteString -> Term s r)
-> Term s r
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s r -> Term s PByteString -> Term s r
forall a b. a -> b -> a
const

{- | Checks that we have a @Constr@ with either @0@ or @1@ as its tag. The
second field of @Constr@ is not checked at all.

@since 1.12.0
-}
instance PValidateData PBool where
  -- Note (Koz, 24/11/2025): This slightly weird implementation relies on `Case`
  -- over `Integer` treating the first 'arm' of the match as `0`, the second as
  -- `1`, and so on. Since we error on anything other than those two, we can use
  -- this for speed.
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x =
    Term s PInteger -> [Term s POpaque] -> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase
      (Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s
    -> Term s PInteger)
-> Term s PInteger
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
opq) ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s PInteger)
 -> Term s PInteger)
-> (PBuiltinPair PInteger (PBuiltinList PData) s
    -> Term s PInteger)
-> Term s PInteger
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
i Term s (PBuiltinList PData)
_) -> Term s PInteger
i)
      [ Term s r -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque Term s r
x
      , Term s r -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque Term s r
x
      ]

{- | Checks that we have a @Constr@ with a second field of at least length 2.
Furthermore, checks that the first element validates as per @a@, while the
second element validates as per @b@. The @Constr@ tag is not checked at all.

@since 1.12.0
-}
instance (PValidateData a, PValidateData b) => PValidateData (PBuiltinPair (PAsData a) (PAsData b)) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq) ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
 -> Term s r)
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
_ Term s (PBuiltinList PData)
p) ->
    Term s (PBuiltinList PData)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PBuiltinList a)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b) -> Term s b
pheadTailBuiltin Term s (PBuiltinList PData)
p ((Term s PData -> Term s (PBuiltinList PData) -> Term s r)
 -> Term s r)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PData
fstOne Term s (PBuiltinList PData)
rest ->
      Term s PData -> (Term s PData -> Term s r) -> Term s r
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 :--> PData)
forall (s :: S) (a :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin 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)
rest) ((Term s PData -> Term s r) -> Term s r)
-> (Term s PData -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PData
sndOne ->
        forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @a Term s PData
fstOne (Term s r -> Term s r)
-> (Term s r -> Term s r) -> Term s r -> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @b Term s PData
sndOne (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s r
x

{- | Checks that we have a @Constr@ with a second field of at least length 2.
The @Constr@ tag, or the elements, are not checked at all.

@since 1.12.0
-}
instance PValidateData (PBuiltinPair PData PData) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq) ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
 -> Term s r)
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
_ Term s (PBuiltinList PData)
p) ->
    Term s (PBuiltinList PData)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PBuiltinList a)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b) -> Term s b
pheadTailBuiltin Term s (PBuiltinList PData)
p ((Term s PData -> Term s (PBuiltinList PData) -> Term s r)
 -> Term s r)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PData
_ Term s (PBuiltinList PData)
rest ->
      Term s PData -> (Term s PData -> Term s r) -> Term s r
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 :--> PData)
forall (s :: S) (a :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin 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)
rest) ((Term s PData -> Term s r) -> Term s r)
-> (Term s PData -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s r -> Term s PData -> Term s r
forall a b. a -> b -> a
const Term s r
x

{- | Checks that we have a @List@. Furthermore, checks that every element
validates as per @a@.

@since 1.12.0
-}
instance {-# OVERLAPPABLE #-} PValidateData a => PValidateData (PBuiltinList a) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> 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 PData
opq) ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList PData)
ell ->
    (forall (s' :: S). Term s' (PBuiltinList PData :--> (r :--> r)))
-> Term s (PBuiltinList PData :--> (r :--> r))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((Term s' (PBuiltinList PData :--> (r :--> r))
 -> Term s' (PBuiltinList PData :--> (r :--> r)))
-> Term s' (PBuiltinList PData :--> (r :--> r))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s' (PBuiltinList PData :--> (r :--> r))
  -> Term s' (PBuiltinList PData :--> (r :--> r)))
 -> Term s' (PBuiltinList PData :--> (r :--> r)))
-> (Term s' (PBuiltinList PData :--> (r :--> r))
    -> Term s' (PBuiltinList PData :--> (r :--> r)))
-> Term s' (PBuiltinList PData :--> (r :--> r))
forall a b. (a -> b) -> a -> b
$ (Term s' (PBuiltinList PData) -> Term s' r -> Term s' r)
-> Term s' (PBuiltinList PData :--> (r :--> r))
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' r -> Term s' r)
-> Term s' (c :--> (r :--> r))
plam ((Term s' (PBuiltinList PData) -> Term s' r -> Term s' r)
 -> Term s' (PBuiltinList PData :--> (r :--> r)))
-> (Term s' (PBuiltinList PData :--> (r :--> r))
    -> Term s' (PBuiltinList PData) -> Term s' r -> Term s' r)
-> Term s' (PBuiltinList PData :--> (r :--> r))
-> Term s' (PBuiltinList PData :--> (r :--> r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s' (PBuiltinList PData :--> (r :--> r))
-> Term s' (PBuiltinList PData) -> Term s' r -> Term s' r
forall (r :: S -> Type) (s :: S).
Term s (PBuiltinList PData :--> (r :--> r))
-> Term s (PBuiltinList PData) -> Term s r -> Term s r
go) Term s (PBuiltinList PData :--> (r :--> r))
-> Term s (PBuiltinList PData) -> Term s (r :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ell Term s (r :--> r) -> Term s r -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s r
x
    where
      go ::
        forall (r :: S -> Type) (s :: S).
        Term s (PBuiltinList PData :--> r :--> r) ->
        Term s (PBuiltinList PData) ->
        Term s r ->
        Term s r
      go :: forall (r :: S -> Type) (s :: S).
Term s (PBuiltinList PData :--> (r :--> r))
-> Term s (PBuiltinList PData) -> Term s r -> Term s r
go Term s (PBuiltinList PData :--> (r :--> r))
self Term s (PBuiltinList PData)
ell Term s r
done = Term s (PBuiltinList PData)
-> (PBuiltinList PData s -> Term s r) -> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinList PData)
ell ((PBuiltinList PData s -> Term s r) -> Term s r)
-> (PBuiltinList PData s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
        PBuiltinList PData s
PNil -> Term s r
done
        PCons Term s PData
h Term s (PBuiltinList PData)
t -> Term s (PBuiltinList PData :--> (r :--> r))
self Term s (PBuiltinList PData :--> (r :--> r))
-> Term s (PBuiltinList PData) -> Term s (r :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
t Term s (r :--> r) -> Term s r -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @a Term s PData
h Term s r
done

{- | Checks that we have a @Map@. Furthermore, checks that every key-value pair
validates as per @a@ and @b@. Takes precedence over the overlapping
@PValidateData (PBuiltinList a)@ instance.

@since 1.13.0
-}
instance
  {-# OVERLAPPING #-}
  (PValidateData a, PValidateData b) =>
  PValidateData (PBuiltinList (PBuiltinPair (PAsData a) (PAsData b)))
  where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinList (PBuiltinPair PData PData))
-> (Term s (PBuiltinList (PBuiltinPair PData PData)) -> Term s r)
-> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
forall (s :: S).
Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
-> Term s PData -> Term s (PBuiltinList (PBuiltinPair PData PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq) ((Term s (PBuiltinList (PBuiltinPair PData PData)) -> Term s r)
 -> Term s r)
-> (Term s (PBuiltinList (PBuiltinPair PData PData)) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList (PBuiltinPair PData PData))
mp ->
    (forall (s' :: S).
 Term s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
-> Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((Term s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
 -> Term
      s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
-> Term
     s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
  -> Term
       s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
 -> Term
      s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
-> (Term
      s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
    -> Term
         s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
-> Term
     s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
forall a b. (a -> b) -> a -> b
$ (Term s' (PBuiltinList (PBuiltinPair PData PData))
 -> Term s' r -> Term s' r)
-> Term
     s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
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' r -> Term s' r)
-> Term s' (c :--> (r :--> r))
plam ((Term s' (PBuiltinList (PBuiltinPair PData PData))
  -> Term s' r -> Term s' r)
 -> Term
      s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r)))
-> (Term
      s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
    -> Term s' (PBuiltinList (PBuiltinPair PData PData))
    -> Term s' r
    -> Term s' r)
-> Term
     s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term
     s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s' (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term s' (PBuiltinList (PBuiltinPair PData PData))
-> Term s' r
-> Term s' r
forall (r :: S -> Type) (s :: S).
Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term s (PBuiltinList (PBuiltinPair PData PData))
-> Term s r
-> Term s r
go) Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term s (PBuiltinList (PBuiltinPair PData PData))
-> Term s (r :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair PData PData))
mp Term s (r :--> r) -> Term s r -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s r
x
    where
      go ::
        forall (r :: S -> Type) (s :: S).
        Term s (PBuiltinList (PBuiltinPair PData PData) :--> r :--> r) ->
        Term s (PBuiltinList (PBuiltinPair PData PData)) ->
        Term s r ->
        Term s r
      go :: forall (r :: S -> Type) (s :: S).
Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term s (PBuiltinList (PBuiltinPair PData PData))
-> Term s r
-> Term s r
go Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
self Term s (PBuiltinList (PBuiltinPair PData PData))
mp Term s r
done = Term s (PBuiltinList (PBuiltinPair PData PData))
-> (PBuiltinList (PBuiltinPair PData PData) s -> Term s r)
-> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinList (PBuiltinPair PData PData))
mp ((PBuiltinList (PBuiltinPair PData PData) s -> Term s r)
 -> Term s r)
-> (PBuiltinList (PBuiltinPair PData PData) s -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \case
        PBuiltinList (PBuiltinPair PData PData) s
PNil -> Term s r
done
        PCons Term s (PBuiltinPair PData PData)
h Term s (PBuiltinList (PBuiltinPair PData PData))
t ->
          Term s (PBuiltinPair PData PData)
-> (PBuiltinPair PData PData s -> Term s r) -> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinPair PData PData)
h ((PBuiltinPair PData PData s -> Term s r) -> Term s r)
-> (PBuiltinPair PData PData s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PData
fst Term s PData
snd) ->
            Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
self Term s (PBuiltinList (PBuiltinPair PData PData) :--> (r :--> r))
-> Term s (PBuiltinList (PBuiltinPair PData PData))
-> Term s (r :--> r)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PBuiltinPair PData PData))
t Term s (r :--> r) -> Term s r -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @a Term s PData
fst (Term s r -> Term s r)
-> (Term s r -> Term s r) -> Term s r -> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @b Term s PData
snd (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s r
done)

{- | Checks that we have a @List@.

@since 1.12.0
-}
instance PValidateData (PBuiltinList PData) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> 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 PData
opq) ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s r -> Term s (PBuiltinList PData) -> Term s r
forall a b. a -> b -> a
const Term s r
x

-- | @since 1.12.0
instance PValidateData a => PValidateData (PAsData a) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated = forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @a

{- | Checks that we have an @I@, and that it is in the range @[0, n - 1]@, where
@n@ is the number of \'arms\' in the encoded sum type.

@since 1.12.0
-}
instance SOP.Generic (a Any) => PValidateData (DeriveAsTag a) where
  {-# INLINEABLE pwithValidated #-}
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x =
    let len :: Int
len = forall k (xs :: [k]) (proxy :: [k] -> Type).
SListI @k xs =>
proxy xs -> Int
SOP.lengthSList @_ @(SOP.Code (a Any)) Proxy @[[Type]] (Code (a (Any @S)))
forall {k} (t :: k). Proxy @k t
Proxy
     in Term s PInteger -> [Term s POpaque] -> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase (Term s (PData :--> PInteger)
forall (s :: S). Term s (PData :--> PInteger)
pasInt Term s (PData :--> PInteger) -> Term s PData -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq) ([Term s POpaque] -> Term s r)
-> (Term s r -> [Term s POpaque]) -> Term s r -> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term s POpaque -> [Term s POpaque]
forall a. Int -> a -> [a]
replicate Int
len (Term s POpaque -> [Term s POpaque])
-> (Term s r -> Term s POpaque) -> Term s r -> [Term s POpaque]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s r -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s r
x

{- | Checks that we have a @List@, that it has (at least) enough elements for
each field of @a@, and that each of those elements, in order, validates as
per its respective 'PValidateData' instance.

@since 1.12.0
-}
instance
  forall (a :: S -> Type) (struct' :: [Type]) (struct :: [S -> Type]).
  ( SOP.Generic (a Any)
  , SOP.All PInnermostIsDataDataRepr struct
  , struct ~ UnTermRec struct'
  , SOP.Generic (a Any)
  , '[struct'] ~ SOP.Code (a Any)
  , SOP.All PValidateData struct
  , SOP.SListI struct
  ) =>
  PValidateData (DeriveAsDataRec a)
  where
  {-# INLINEABLE pwithValidated #-}
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> 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 PData
opq) ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList PData)
ell ->
    Term s (PBuiltinList PData)
-> Shape @(S -> Type) struct -> Term s r -> Term s r
forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
go Term s (PBuiltinList PData)
ell (forall k (xs :: [k]). SListI @k xs => Shape @k xs
SOP.shape @(S -> Type) @struct) Term s r
x
    where
      go ::
        forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
        SOP.All PValidateData w =>
        Term s (PBuiltinList PData) ->
        SOP.Shape w ->
        Term s r ->
        Term s r
      go :: forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
go Term s (PBuiltinList PData)
ell Shape @(S -> Type) w
aShape Term s r
x = case Shape @(S -> Type) w
aShape of
        Shape @(S -> Type) w
SOP.ShapeNil -> Term s r
x
        SOP.ShapeCons @_ @y Shape @(S -> Type) xs
SOP.ShapeNil -> forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @y (Term s (PBuiltinList PData :--> PData)
forall (s :: S) (a :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin 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)
ell) Term s r
x
        SOP.ShapeCons @_ @y Shape @(S -> Type) xs
restShape -> Term s (PBuiltinList PData)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PBuiltinList a)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b) -> Term s b
pheadTailBuiltin Term s (PBuiltinList PData)
ell ((Term s PData -> Term s (PBuiltinList PData) -> Term s r)
 -> Term s r)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PData
h Term s (PBuiltinList PData)
t ->
          forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @y Term s PData
h (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> Shape @(S -> Type) xs -> Term s r -> Term s r
forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
go Term s (PBuiltinList PData)
t Shape @(S -> Type) xs
restShape Term s r
x

{- | Checks that we have a @Constr@, that its tag is in the range @[0, n - 1]@
(where @n@ is the number of \'arms\' in the encoded sum type), and that there
are at least enough fields in the second @Constr@ argument, each of which
decodes as per that field's 'PValidateData' instance.

@since 1.12.0
-}
instance
  forall (a :: S -> Type) (struct :: [[S -> Type]]).
  ( SOP.Generic (a Any)
  , struct ~ UnTermStruct (a Any)
  , SOP.All2 PInnermostIsDataDataRepr struct
  , SOP.All2 PValidateData struct
  , SOP.SListI2 struct
  ) =>
  PValidateData (DeriveAsDataStruct a)
  where
  {-# INLINEABLE pwithValidated #-}
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
opq Term s r
x = Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq) ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
 -> Term s r)
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
p ->
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PBuiltinPair PInteger (PBuiltinList PData))
p ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
 -> Term s r)
-> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \(PBuiltinPair Term s PInteger
ix Term s (PBuiltinList PData)
fields) ->
      Term s PInteger -> [Term s POpaque] -> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase Term s PInteger
ix ([Term s POpaque] -> Term s r) -> [Term s POpaque] -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> Shape @[S -> Type] struct -> Term s r -> [Term s POpaque]
forall (wOuter :: [[S -> Type]]) (s :: S) (r :: S -> Type).
(SListI2 @(S -> Type) wOuter,
 All2 @(S -> Type) PValidateData wOuter) =>
Term s (PBuiltinList PData)
-> Shape @[S -> Type] wOuter -> Term s r -> [Term s POpaque]
goOuter Term s (PBuiltinList PData)
fields (forall k (xs :: [k]). SListI @k xs => Shape @k xs
SOP.shape @[S -> Type] @struct) Term s r
x
    where
      goOuter ::
        forall (wOuter :: [[S -> Type]]) (s :: S) (r :: S -> Type).
        (SOP.SListI2 wOuter, SOP.All2 PValidateData wOuter) =>
        Term s (PBuiltinList PData) ->
        SOP.Shape wOuter ->
        Term s r ->
        [Term s POpaque]
      goOuter :: forall (wOuter :: [[S -> Type]]) (s :: S) (r :: S -> Type).
(SListI2 @(S -> Type) wOuter,
 All2 @(S -> Type) PValidateData wOuter) =>
Term s (PBuiltinList PData)
-> Shape @[S -> Type] wOuter -> Term s r -> [Term s POpaque]
goOuter Term s (PBuiltinList PData)
ell Shape @[S -> Type] wOuter
outerShape Term s r
x = case Shape @[S -> Type] wOuter
outerShape of
        Shape @[S -> Type] wOuter
SOP.ShapeNil -> []
        SOP.ShapeCons @_ @y Shape @[S -> Type] xs
restShape -> Term s r -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s (PBuiltinList PData)
-> Shape @(S -> Type) x -> Term s r -> Term s r
forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
goInner Term s (PBuiltinList PData)
ell (forall k (xs :: [k]). SListI @k xs => Shape @k xs
SOP.shape @_ @y) Term s r
x) Term s POpaque -> [Term s POpaque] -> [Term s POpaque]
forall a. a -> [a] -> [a]
: Term s (PBuiltinList PData)
-> Shape @[S -> Type] xs -> Term s r -> [Term s POpaque]
forall (wOuter :: [[S -> Type]]) (s :: S) (r :: S -> Type).
(SListI2 @(S -> Type) wOuter,
 All2 @(S -> Type) PValidateData wOuter) =>
Term s (PBuiltinList PData)
-> Shape @[S -> Type] wOuter -> Term s r -> [Term s POpaque]
goOuter Term s (PBuiltinList PData)
ell Shape @[S -> Type] xs
restShape Term s r
x
      goInner ::
        forall (wInner :: [S -> Type]) (s :: S) (r :: S -> Type).
        SOP.All PValidateData wInner =>
        Term s (PBuiltinList PData) ->
        SOP.Shape wInner ->
        Term s r ->
        Term s r
      goInner :: forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
goInner Term s (PBuiltinList PData)
ell Shape @(S -> Type) wInner
aShape Term s r
x = case Shape @(S -> Type) wInner
aShape of
        Shape @(S -> Type) wInner
SOP.ShapeNil -> Term s r
x
        SOP.ShapeCons @_ @y Shape @(S -> Type) xs
SOP.ShapeNil -> forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @y (Term s (PBuiltinList PData :--> PData)
forall (s :: S) (a :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin 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)
ell) Term s r
x
        SOP.ShapeCons @_ @y Shape @(S -> Type) xs
restShape -> Term s (PBuiltinList PData)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PBuiltinList a)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b) -> Term s b
pheadTailBuiltin Term s (PBuiltinList PData)
ell ((Term s PData -> Term s (PBuiltinList PData) -> Term s r)
 -> Term s r)
-> (Term s PData -> Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s PData
h Term s (PBuiltinList PData)
t ->
          forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @y Term s PData
h (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> Shape @(S -> Type) xs -> Term s r -> Term s r
forall (w :: [S -> Type]) (s :: S) (r :: S -> Type).
All @(S -> Type) PValidateData w =>
Term s (PBuiltinList PData)
-> Shape @(S -> Type) w -> Term s r -> Term s r
goInner Term s (PBuiltinList PData)
t Shape @(S -> Type) xs
restShape Term s r
x

{- | Helper to define a do-nothing instance of 'PValidateData'. Useful when
defining an instance for a complex type where we want to validate some parts,
but not others.

@since 1.12.0
-}
newtype Don'tValidate (a :: S -> Type) (s :: S) = Don'tValidate {forall (a :: S -> Type) (s :: S). Don'tValidate a s -> a s
unDon'tValidate :: a s}

-- | @since 1.12.0
instance PlutusType a => PlutusType (Don'tValidate a) where
  type PInner (Don'tValidate a) = PInner a
  pcon' :: forall (s :: S).
Don'tValidate a s -> Term s (PInner (Don'tValidate a))
pcon' (Don'tValidate a s
x) = a s -> Term s (PInner a)
forall (s :: S). a s -> Term s (PInner a)
forall (a :: S -> Type) (s :: S).
PlutusType a =>
a s -> Term s (PInner a)
pcon' a s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (Don'tValidate a))
-> (Don'tValidate a s -> Term s b) -> Term s b
pmatch' Term s (PInner (Don'tValidate a))
x Don'tValidate a s -> Term s b
f = Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (s :: S) (b :: S -> Type).
Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s (PInner a) -> (a s -> Term s b) -> Term s b
pmatch' Term s (PInner a)
Term s (PInner (Don'tValidate a))
x (Don'tValidate a s -> Term s b
f (Don'tValidate a s -> Term s b)
-> (a s -> Don'tValidate a s) -> a s -> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> Don'tValidate a s
forall (a :: S -> Type) (s :: S). a s -> Don'tValidate a s
Don'tValidate)

-- | @since 1.12.0
instance PValidateData (Don'tValidate a) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated Term s PData
_ = Term s r -> Term s r
forall a. a -> a
id

{- | Helper to define an instance of 'PValidateData' for @newtype@s over
'Term's, which \'borrows\' the 'PValidateData' instance for whatever the
@newtype@ is wrapping.

@since 1.12.0
-}
newtype DeriveNewtypePValidateData (a :: S -> Type) (b :: S -> Type) (s :: S)
  = DeriveNewtypePValidateData (a s)

-- | @since 1.12.0
instance PValidateData b => PValidateData (DeriveNewtypePValidateData a b) where
  pwithValidated :: forall (s :: S).
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated = forall (a :: S -> Type) (s :: S).
PValidateData a =>
Term s PData -> forall (r :: S -> Type). Term s r -> Term s r
pwithValidated @b