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

module Plutarch.Internal.PlutusType (
  PlutusType,
  PlutusTypeStratConstraint,
  PCon,
  PMatch,
  pcon',
  pmatch',
  pmatch,
  pcon,
  PInner,
  PlutusTypeStrat,
  DerivePlutusType,
  DPTStrat,
  DerivedPInner,
  derivedPCon,
  derivedPMatch,
  PVariant,
  PCovariant,
  PContravariant,
  PVariant',
  PCovariant',
  PContravariant',
  PVariant'',
  PCovariant'',
  PContravariant'',
) 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 Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
import Generics.SOP (All2)
import Generics.SOP qualified as SOP
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom, gpto)
import {-# SOURCE #-} Plutarch.Internal.IsData (
  PIsData,
  pdata,
  pfromData,
 )
import {-# SOURCE #-} Plutarch.Internal.Lift (
  PlutusRepr,
  getPLifted,
  unsafeToUni,
 )
import Plutarch.Internal.Quantification (PFix (PFix), PForall (PForall), PSome (PSome))
import Plutarch.Internal.Term (PType, S, Term, pdelay, pforce, plam', plet, punsafeCoerce, (#), (:-->) (PLam))
import Plutarch.Internal.Witness (witness)
import PlutusCore qualified as PLC

class PlutusTypeStrat (strategy :: Type) where
  type PlutusTypeStratConstraint strategy :: PType -> Constraint
  type DerivedPInner strategy (a :: PType) :: PType
  derivedPCon :: forall a s. (DerivePlutusType a, DPTStrat a ~ strategy) => a s -> Term s (DerivedPInner strategy a)
  derivedPMatch :: forall a s b. (DerivePlutusType a, DPTStrat a ~ strategy) => Term s (DerivedPInner strategy a) -> (a s -> Term s b) -> Term s b

class
  ( PInner a ~ DerivedPInner (DPTStrat a) a
  , PlutusTypeStrat (DPTStrat a)
  , PlutusTypeStratConstraint (DPTStrat a) a
  , PlutusType a
  ) =>
  DerivePlutusType (a :: PType)
  where
  type DPTStrat a :: Type
  type DPTStrat a = TypeError ('Text "Please specify a strategy for deriving PlutusType for type " ':<>: 'ShowType a)

class PlutusType (a :: PType) where
  type PInner a :: PType
  type PInner a = DerivedPInner (DPTStrat a) a
  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)
  default pcon' :: DerivePlutusType a => forall s. a s -> Term s (PInner a)
  pcon' = let ()
_ = Proxy @Constraint (PlutusType a) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PlutusType a)) in a s -> Term s (PInner a)
a s -> Term s (DerivedPInner (DPTStrat a) a)
forall strategy (a :: PType) (s :: S).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
a s -> Term s (DerivedPInner strategy a)
forall (a :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (DPTStrat a :: Type)) =>
a s -> Term s (DerivedPInner (DPTStrat a) a)
derivedPCon

  pmatch' :: forall s b. Term s (PInner a) -> (a s -> Term s b) -> Term s b
  -- FIXME buggy GHC, needs AllowAmbiguousTypes
  default pmatch' :: DerivePlutusType a => forall s b. Term s (PInner a) -> (a s -> Term s b) -> Term s b
  pmatch' = Term s (PInner a) -> (a s -> Term s b) -> Term s b
Term s (DerivedPInner (DPTStrat a) a)
-> (a s -> Term s b) -> Term s b
forall strategy (a :: PType) (s :: S) (b :: PType).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
Term s (DerivedPInner strategy a) -> (a s -> Term s b) -> Term s b
forall (a :: PType) (s :: S) (b :: PType).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (DPTStrat a :: Type)) =>
Term s (DerivedPInner (DPTStrat a) a)
-> (a s -> Term s b) -> Term s b
derivedPMatch

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

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

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

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

data PlutusTypeNewtype

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

instance PlutusTypeStrat PlutusTypeNewtype where
  type PlutusTypeStratConstraint PlutusTypeNewtype = Helper
  type DerivedPInner PlutusTypeNewtype a = GetPNewtype a
  derivedPCon :: forall (a :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeNewtype :: Type)) =>
a s -> Term s (DerivedPInner PlutusTypeNewtype a)
derivedPCon a s
x = case a s -> SOP @PType (Term s) (PCode a)
forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom a s
x of
    SOP.SOP (SOP.Z (Term s x
x SOP.:* NP @PType (Term s) xs
SOP.Nil)) -> Term s x
Term s (DerivedPInner PlutusTypeNewtype a)
x
    SOP.SOP (SOP.S NS @[PType] (NP @PType (Term s)) xs
x) -> case NS @[PType] (NP @PType (Term s)) xs
x of {}
  derivedPMatch :: forall (a :: PType) (s :: S) (b :: PType).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeNewtype :: Type)) =>
Term s (DerivedPInner PlutusTypeNewtype a)
-> (a s -> Term s b) -> Term s b
derivedPMatch Term s (DerivedPInner PlutusTypeNewtype a)
x a s -> Term s b
f = a s -> Term s b
f (SOP @PType (Term s) (PCode a) -> a s
forall (a :: PType) (s :: S).
PGeneric a =>
SOP @PType (Term s) (PCode a) -> a s
gpto (SOP @PType (Term s) (PCode a) -> a s)
-> SOP @PType (Term s) (PCode a) -> a s
forall a b. (a -> b) -> a -> b
$ NS @[PType] (NP @PType (Term s)) (PCode a)
-> SOP @PType (Term s) (PCode a)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP.SOP (NS @[PType] (NP @PType (Term s)) (PCode a)
 -> SOP @PType (Term s) (PCode a))
-> NS @[PType] (NP @PType (Term s)) (PCode a)
-> SOP @PType (Term s) (PCode a)
forall a b. (a -> b) -> a -> b
$ NP
  @PType (Term s) ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':)
        @[PType]
        ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
        ('[] @[PType]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
SOP.Z (NP
   @PType (Term s) ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
 -> NS
      @[PType]
      (NP @PType (Term s))
      ((':)
         @[PType]
         ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
         ('[] @[PType])))
-> NP
     @PType (Term s) ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':)
        @[PType]
        ((':) @PType (GetPNewtype' (PCode a)) ('[] @PType))
        ('[] @[PType]))
forall a b. (a -> b) -> a -> b
$ Term s (DerivedPInner PlutusTypeNewtype a)
x Term s (DerivedPInner PlutusTypeNewtype a)
-> NP @PType (Term s) ('[] @PType)
-> NP
     @PType
     (Term s)
     ((':) @PType (DerivedPInner PlutusTypeNewtype a) ('[] @PType))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
SOP.:* NP @PType (Term s) ('[] @PType)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
SOP.Nil)

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

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

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

instance DerivePlutusType PInteger where type DPTStrat _ = PlutusTypeNewtype
deriving anyclass 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 WIP
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
unsafeToUni @[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)))

type family IfSameThenData (a :: S -> Type) (b :: S -> Type) :: S -> Type where
  IfSameThenData a a = PData
  IfSameThenData _ POpaque = PData
  IfSameThenData _ b = PAsData b

instance PIsData a => PlutusType (PAsData a) where
  type PInner (PAsData a) = IfSameThenData a (PInner a)
  type PCovariant' (PAsData a) = PCovariant' a
  type PContravariant' (PAsData a) = PContravariant' a
  type PVariant' (PAsData a) = PVariant' a
  pcon' :: forall (s :: S). PAsData a s -> Term s (PInner (PAsData a))
pcon' (PAsData Term s a
t) = 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)

instance DerivePlutusType PByteString where type DPTStrat _ = PlutusTypeNewtype
deriving anyclass instance PlutusType PByteString

instance DerivePlutusType PByte where type DPTStrat _ = PlutusTypeNewtype
deriving anyclass instance PlutusType PByte

instance DerivePlutusType PLogicOpSemantics where type DPTStrat _ = PlutusTypeNewtype
deriving anyclass instance PlutusType PLogicOpSemantics

instance DerivePlutusType PString where type DPTStrat _ = PlutusTypeNewtype
deriving anyclass 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 WIP
instance DerivePlutusType PBuiltinBLS12_381_G1_Element where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since WIP
deriving anyclass instance PlutusType PBuiltinBLS12_381_G1_Element

-- | @since WIP
instance DerivePlutusType PBuiltinBLS12_381_G2_Element where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since WIP
deriving anyclass instance PlutusType PBuiltinBLS12_381_G2_Element

-- | @since WIP
instance DerivePlutusType PBuiltinBLS12_381_MlResult where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since WIP
deriving anyclass instance PlutusType PBuiltinBLS12_381_MlResult

-- | @since WIP
instance DerivePlutusType PEndianness where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since WIP
deriving anyclass instance PlutusType PEndianness