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

module Plutarch.Internal.PlutusType (
  PlutusType,
  PInnermost,
  PCon,
  PMatch,
  pcon',
  pmatch',
  pmatch,
  pcon,
  PInner,
  PVariant,
  PCovariant,
  PContravariant,
  PVariant',
  PCovariant',
  PContravariant',
  PVariant'',
  PCovariant'',
  PContravariant'',
  DeriveNewtypePlutusType (DeriveNewtypePlutusType, unDeriveNewtypePlutusType),
  DeriveFakePlutusType (DeriveFakePlutusType),
) where

import Plutarch.Builtin.BLS (
  PBuiltinBLS12_381_G1_Element,
  PBuiltinBLS12_381_G2_Element,
  PBuiltinBLS12_381_MlResult,
 )
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pfalse, pif', ptrue)
import Plutarch.Builtin.ByteString (
  PByte,
  PByteString,
  PEndianness,
  PLogicOpSemantics,
 )
import Plutarch.Builtin.Data (
  PAsData (PAsData),
  PBuiltinList (PCons, PNil),
  PBuiltinPair (PBuiltinPair),
  PData (PData),
  pchooseListBuiltin,
  pconsBuiltin,
  pheadBuiltin,
  ptailBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Builtin.Opaque (POpaque (POpaque))
import Plutarch.Builtin.String (PString)
import Plutarch.Builtin.Unit (PUnit (PUnit), punit)

import Data.Kind (Constraint, Type)
import GHC.Exts (Any)
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
import Generics.SOP (
  All2,
  Code,
  I (I),
  NP (Nil, (:*)),
  NS (Z),
  SOP (SOP),
 )
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (Head)
import Plutarch.Internal.Generic (PCode, PGeneric)
import {-# SOURCE #-} Plutarch.Internal.IsData (
  PIsData,
  pdata,
  pfromData,
 )
import {-# SOURCE #-} Plutarch.Internal.Lift (
  PlutusRepr,
  getPLifted,
  unsafeHaskToUni,
 )
import Plutarch.Internal.Quantification (PForall (PForall))
import Plutarch.Internal.Term (PType, S, Term, pdelay, pforce, plam', plet, punsafeCoerce, (#), (:-->) (PLam))
import PlutusCore qualified as PLC

type family PInnermost' (a :: S -> Type) (b :: S -> Type) :: S -> Type where
  PInnermost' a a = a
  PInnermost' a _b = PInnermost' (PInner a) a

type PInnermost a = PInnermost' (PInner a) a

class PlutusType (a :: PType) where
  type PInner a :: PType
  type PCovariant' a :: Constraint
  type PCovariant' a = All2 PCovariant'' (PCode a)
  type PContravariant' a :: Constraint
  type PContravariant' a = All2 PContravariant'' (PCode a)
  type PVariant' a :: Constraint
  type PVariant' a = All2 PVariant'' (PCode a)
  pcon' :: forall s. a s -> Term s (PInner a)
  pmatch' :: forall s b. Term s (PInner a) -> (a s -> Term s b) -> Term s b

{-# DEPRECATED PCon "Use PlutusType" #-}
type PCon = PlutusType
{-# DEPRECATED PMatch "Use PlutusType" #-}
type PMatch = PlutusType

-- | Construct a Plutarch Term via a Haskell datatype
pcon :: PlutusType a => a s -> Term s a
pcon :: forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon a s
x = Term s (PInner a) -> Term s a
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (a s -> Term s (PInner a)
forall (s :: S). a s -> Term s (PInner a)
forall (a :: PType) (s :: S).
PlutusType a =>
a s -> Term s (PInner a)
pcon' a s
x)

-- | Pattern match over Plutarch Terms via a Haskell datatype
pmatch :: PlutusType a => Term s a -> (a s -> Term s b) -> Term s b
pmatch :: forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s a
x = Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (s :: S) (b :: PType).
Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s (PInner a) -> (a s -> Term s b) -> Term s b
pmatch' (Term s a -> Term s (PInner a)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s a
x)

class PCovariant' a => PCovariant'' a
instance PCovariant' a => PCovariant'' a

class PContravariant' a => PContravariant'' a
instance PContravariant' a => PContravariant'' a

class PVariant' a => PVariant'' a
instance PVariant' a => PVariant'' a

class (forall t. PCovariant'' t => PCovariant'' (a t)) => PCovariant a
instance (forall t. PCovariant'' t => PCovariant'' (a t)) => PCovariant a

class (forall t. PCovariant'' t => PContravariant'' (a t)) => PContravariant a
instance (forall t. PCovariant'' t => PContravariant'' (a t)) => PContravariant a

class (forall t. PVariant'' t => PVariant'' (a t)) => PVariant a
instance (forall t. PVariant'' t => PVariant'' (a t)) => PVariant a

instance PlutusType (a :--> b) where
  type PInner (a :--> b) = a :--> b
  type PCovariant' (a :--> b) = (PContravariant' a, PCovariant' b)
  type PContravariant' (a :--> b) = (PCovariant' a, PContravariant' b)
  type PVariant' (a :--> b) = (PVariant' a, PVariant' b)
  pcon' :: forall (s :: S). (:-->) a b s -> Term s (PInner (a :--> b))
pcon' (PLam Term s a -> Term s b
f) = (Term s a -> Term s b) -> Term s (a :--> b)
forall (s :: S) (a :: PType) (b :: PType).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' Term s a -> Term s b
f
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (a :--> b))
-> ((:-->) a b s -> Term s b) -> Term s b
pmatch' Term s (PInner (a :--> b))
f (:-->) a b s -> Term s b
g = Term s (PInner (a :--> b))
-> (Term s (PInner (a :--> b)) -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PInner (a :--> b))
f \Term s (PInner (a :--> b))
f' -> (:-->) a b s -> Term s b
g ((Term s a -> Term s b) -> (:-->) a b s
forall (a :: PType) (b :: PType) (s :: S).
(Term s a -> Term s b) -> (:-->) a b s
PLam (Term s (a :--> b)
Term s (PInner (a :--> b))
f' #))

instance PlutusType (PForall f) where
  type PInner (PForall f) = PForall f
  pcon' :: forall (s :: S). PForall @a f s -> Term s (PInner (PForall @a f))
pcon' (PForall forall (x :: a). Term s (f x)
x) = Term s (f (Any @a)) -> Term s (PInner (PForall @a f))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (f (Any @a))
forall (x :: a). Term s (f x)
x
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PForall @a f))
-> (PForall @a f s -> Term s b) -> Term s b
pmatch' Term s (PInner (PForall @a f))
x PForall @a f s -> Term s b
f = PForall @a f s -> Term s b
f ((forall (x :: a). Term s (f x)) -> PForall @a f s
forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall ((forall (x :: a). Term s (f x)) -> PForall @a f s)
-> (forall (x :: a). Term s (f x)) -> PForall @a f s
forall a b. (a -> b) -> a -> b
$ Term s (PInner (PForall @a f)) -> Term s (f x)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PInner (PForall @a f))
x)

--------------------------------------------------------------------------------

class (PGeneric a, PCode a ~ '[ '[GetPNewtype a]]) => Helper (a :: PType)
instance (PGeneric a, PCode a ~ '[ '[GetPNewtype a]]) => Helper (a :: PType)

type family GetPNewtype' (a :: [[PType]]) :: PType where
  GetPNewtype' '[ '[a]] = a

type family GetPNewtype (a :: PType) :: PType where
  GetPNewtype a = GetPNewtype' (PCode a)

--------------------------------------------------------------------------------

-- | @since 1.10.0
newtype DeriveNewtypePlutusType (a :: S -> Type) s = DeriveNewtypePlutusType
  { forall (a :: PType) (s :: S). DeriveNewtypePlutusType a s -> a s
unDeriveNewtypePlutusType :: a s
  -- ^ @since 1.10.0
  }

-- Helpers

type family UnTermSingle (x :: Type) :: S -> Type where
  UnTermSingle (Term _ a) = a

class (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt
instance (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt

instance
  forall (a :: S -> Type) (pt :: S -> Type).
  ( pt ~ UnTermSingle (Head (Head (Code (a Any))))
  , forall s. H s a pt
  ) =>
  PlutusType (DeriveNewtypePlutusType a)
  where
  -- Note:
  -- This is not @PInner (DeriveNewtypePlutusType a) = PInner a@ because
  -- We want the PInner of wrapper type to be the type it wraps not the PInner of that.
  type PInner (DeriveNewtypePlutusType a) = UnTermSingle (Head (Head (Code (a Any))))
  type PCovariant' (DeriveNewtypePlutusType a) = PCovariant' a
  type PContravariant' (DeriveNewtypePlutusType a) = PContravariant' a
  type PVariant' (DeriveNewtypePlutusType a) = PVariant' a

  -- This breaks without type signature because of (s :: S) needs to be bind.
  pcon' :: forall s. DeriveNewtypePlutusType a s -> Term s (PInner (DeriveNewtypePlutusType a))
  pcon' :: forall (s :: S).
DeriveNewtypePlutusType a s
-> Term s (PInner (DeriveNewtypePlutusType a))
pcon' (DeriveNewtypePlutusType a s
x) =
    case NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall {k} (f :: k -> Type) (x :: k).
NS @k f ((':) @k x ('[] @k)) -> f x
SOP.unZ (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
 -> NP @Type I ((':) @Type (Term s pt) ('[] @Type)))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall a b. (a -> b) -> a -> b
$ SOP
  @Type
  I
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
SOP.unSOP (a s -> Rep (a s)
forall a. Generic a => a -> Rep a
SOP.from a s
x :: SOP I '[ '[Term s pt]]) of
      (I x
x) :* NP @Type I xs
Nil -> x
Term s pt
x :: Term s pt

  pmatch' :: forall s b. Term s (PInner (DeriveNewtypePlutusType a)) -> (DeriveNewtypePlutusType a s -> Term s b) -> Term s b
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (DeriveNewtypePlutusType a))
-> (DeriveNewtypePlutusType a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveNewtypePlutusType a))
x DeriveNewtypePlutusType a s -> Term s b
f =
    DeriveNewtypePlutusType a s -> Term s b
f (a s -> DeriveNewtypePlutusType a s
forall (a :: PType) (s :: S). a s -> DeriveNewtypePlutusType a s
DeriveNewtypePlutusType (a s -> DeriveNewtypePlutusType a s)
-> a s -> DeriveNewtypePlutusType a s
forall a b. (a -> b) -> a -> b
$ Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to ((NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
     @Type
     I
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
 -> SOP
      @Type
      I
      ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
     @Type
     I
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (NP @Type I ((':) @Type (Term s pt) ('[] @Type))
 -> NS
      @[Type]
      (NP @Type I)
      ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ Term s (PInner (DeriveNewtypePlutusType a))
-> I (Term s (PInner (DeriveNewtypePlutusType a)))
forall a. a -> I a
I Term s (PInner (DeriveNewtypePlutusType a))
x I (Term s (PInner (DeriveNewtypePlutusType a)))
-> NP @Type I ('[] @Type)
-> NP
     @Type
     I
     ((':)
        @Type (Term s (PInner (DeriveNewtypePlutusType a))) ('[] @Type))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) :: SOP I '[ '[Term s pt]]))

--------------------------------------------------------------------------------

class Bottom

{- |
This is a cursed derivation strategy that will give you @PlutusType@ with no questions asked. This is occasionally helpful
for deriving @PlutusType@ for another derivation strategy wrapper whose target instance requires @PlutusType@ as superclass.

See @PLiftable@
-}
newtype DeriveFakePlutusType (a :: S -> Type) (s :: S) = DeriveFakePlutusType (a s)

instance PlutusType (DeriveFakePlutusType a) where
  type PInner (DeriveFakePlutusType a) = TypeError ('ShowType a ':<>: 'Text " derived PlutusType with DeriveFakePlutusType. This type is not meant to be used as PlutusType.")
  type PCovariant' (DeriveFakePlutusType a) = Bottom
  type PContravariant' (DeriveFakePlutusType a) = Bottom
  type PVariant' (DeriveFakePlutusType a) = Bottom

  -- This breaks without type signature because of (s :: S) needs to be bind.
  pcon' :: forall s. DeriveFakePlutusType a s -> Term s (PInner (DeriveFakePlutusType a))
  pcon' :: forall (s :: S).
DeriveFakePlutusType a s
-> Term s (PInner (DeriveFakePlutusType a))
pcon' DeriveFakePlutusType a s
_ = [Char] -> Term s (PInner (DeriveFakePlutusType a))
forall a. HasCallStack => [Char] -> a
error [Char]
"Attepted to use a type derived with DeriveFakePlutusType"

  pmatch' :: forall s b. Term s (PInner (DeriveFakePlutusType a)) -> (DeriveFakePlutusType a s -> Term s b) -> Term s b
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (DeriveFakePlutusType a))
-> (DeriveFakePlutusType a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveFakePlutusType a))
_ DeriveFakePlutusType a s -> Term s b
_ = [Char] -> Term s b
forall a. HasCallStack => [Char] -> a
error [Char]
"Attepted to use a type derived with DeriveFakePlutusType"

--------------------------------------------------------------------------------

deriving via (DeriveNewtypePlutusType PInteger) instance PlutusType PInteger

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

-- | @since 1.10.0
instance PlutusType PBool where
  type PInner PBool = PBool
  {-# INLINEABLE pcon' #-}
  pcon' :: forall (s :: S). PBool s -> Term s (PInner PBool)
pcon' PBool s
PTrue = Term s PBool
Term s (PInner PBool)
forall (s :: S). Term s PBool
ptrue
  pcon' PBool s
PFalse = Term s PBool
Term s (PInner PBool)
forall (s :: S). Term s PBool
pfalse
  {-# INLINEABLE pmatch' #-}
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PBool) -> (PBool s -> Term s b) -> Term s b
pmatch' Term s (PInner PBool)
b PBool s -> Term s b
f = Term s (PDelayed b) -> Term s b
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed b) -> Term s b)
-> Term s (PDelayed b) -> Term s b
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> (PDelayed b :--> (PDelayed b :--> PDelayed b)))
forall (a :: PType) (s :: S).
Term s (PBool :--> (a :--> (a :--> a)))
pif' Term s (PBool :--> (PDelayed b :--> (PDelayed b :--> PDelayed b)))
-> Term s PBool
-> Term s (PDelayed b :--> (PDelayed b :--> PDelayed b))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
Term s (PInner PBool)
b Term s (PDelayed b :--> (PDelayed b :--> PDelayed b))
-> Term s (PDelayed b) -> Term s (PDelayed b :--> PDelayed b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PBool s -> Term s b
f PBool s
forall (s :: S). PBool s
PTrue) Term s (PDelayed b :--> PDelayed b)
-> Term s (PDelayed b) -> Term s (PDelayed b)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PBool s -> Term s b
f PBool s
forall (s :: S). PBool s
PFalse)

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

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

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

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

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PByteString) instance PlutusType PByteString

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PByte) instance PlutusType PByte

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PLogicOpSemantics) instance PlutusType PLogicOpSemantics

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PString) instance PlutusType PString

instance PlutusType PUnit where
  type PInner PUnit = PUnit
  pcon' :: forall (s :: S). PUnit s -> Term s (PInner PUnit)
pcon' PUnit s
PUnit = Term s PUnit
Term s (PInner PUnit)
forall (s :: S). Term s PUnit
punit
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PUnit) -> (PUnit s -> Term s b) -> Term s b
pmatch' Term s (PInner PUnit)
x PUnit s -> Term s b
f = Term s (PInner PUnit)
-> (Term s (PInner PUnit) -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PInner PUnit)
x \Term s (PInner PUnit)
_ -> PUnit s -> Term s b
f PUnit s
forall (s :: S). PUnit s
PUnit

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PBuiltinBLS12_381_G1_Element) instance PlutusType PBuiltinBLS12_381_G1_Element

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PBuiltinBLS12_381_G2_Element) instance PlutusType PBuiltinBLS12_381_G2_Element

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PBuiltinBLS12_381_MlResult) instance PlutusType PBuiltinBLS12_381_MlResult

-- | @since 1.10.0
deriving via (DeriveNewtypePlutusType PEndianness) instance PlutusType PEndianness