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

module Plutarch.Internal.PlutusType (
  PlutusType,
  PInnermost,
  PlutusTypeStratConstraint,
  pcon',
  pmatch',
  pmatch,
  pcon,
  PInner,
  PlutusTypeStrat,
  DerivePlutusType,
  DPTStrat,
  DerivedPInner,
  derivedPCon,
  derivedPMatch,
  DeriveNewtypePlutusType (DeriveNewtypePlutusType, unDeriveNewtypePlutusType),
  DeriveFakePlutusType (DeriveFakePlutusType),
) where

import Plutarch.Builtin.Array (PArray (PArray))
import Plutarch.Builtin.BLS (
  PBuiltinBLS12_381_G1_Element,
  PBuiltinBLS12_381_G2_Element,
  PBuiltinBLS12_381_MlResult,
 )
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pfalse, ptrue)
import Plutarch.Builtin.ByteString (
  PByte,
  PByteString,
  PEndianness,
  PLogicOpSemantics,
 )
import Plutarch.Builtin.Data (
  PAsData (PAsData),
  PBuiltinList (PCons, PNil),
  PBuiltinPair (PBuiltinPair),
  PData (PData),
  pconsBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Builtin.Opaque (POpaque (POpaque), popaque)
import Plutarch.Builtin.String (PString, ptraceInfo)
import Plutarch.Builtin.Unit (PUnit (PUnit), punit)
import Plutarch.Internal.Case (punsafeCase)
import Plutarch.Internal.PLam (plam)

import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Exts (Any)
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
import Generics.SOP (
  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, gpfrom, gpto)
import {-# SOURCE #-} Plutarch.Internal.IsData (
  PIsData,
  pdata,
  pfromData,
 )
import {-# SOURCE #-} Plutarch.Internal.Lift (
  PlutusRepr,
  getPLifted,
  unsafeHaskToUni,
 )
import Plutarch.Internal.Quantification (PFix (PFix), PForall (PForall), PSome (PSome))
import Plutarch.Internal.Term (
  S,
  Term,
  perror,
  plam',
  plet,
  punsafeCoerce,
  (#),
  (:-->) (PLam),
 )
import Plutarch.Internal.Witness (witness)
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

{-# DEPRECATED PlutusTypeStrat "Use the new mechanisms instead" #-}
class PlutusTypeStrat (strategy :: Type) where
  type PlutusTypeStratConstraint strategy :: (S -> Type) -> Constraint
  type DerivedPInner strategy (a :: S -> Type) :: S -> Type
  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

{-# DEPRECATED DerivePlutusType "Use the new mechanisms instead" #-}
class
  ( PInner a ~ DerivedPInner (DPTStrat a) a
  , PlutusTypeStrat (DPTStrat a)
  , PlutusTypeStratConstraint (DPTStrat a) a
  , PlutusType a
  ) =>
  DerivePlutusType (a :: S -> Type)
  where
  type DPTStrat a :: Type
  type DPTStrat a = TypeError ('Text "Please specify a strategy for deriving PlutusType for type " ':<>: 'ShowType a)

class PlutusType (a :: S -> Type) where
  type PInner a :: S -> Type
  type PInner a = DerivedPInner (DPTStrat a) 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 :: S -> Type) (s :: S).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
a s -> Term s (DerivedPInner strategy a)
forall (a :: S -> Type) (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 :: S -> Type) (s :: S) (b :: S -> Type).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
Term s (DerivedPInner strategy a) -> (a s -> Term s b) -> Term s b
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (DPTStrat a :: Type)) =>
Term s (DerivedPInner (DPTStrat a) a)
-> (a s -> Term s b) -> Term s b
derivedPMatch

-- | Construct a Plutarch Term via a Haskell datatype
pcon :: PlutusType a => a s -> Term s a
pcon :: forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon a s
x = Term s (PInner a) -> Term s a
forall (b :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (s :: S) (b :: S -> Type).
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 :: 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 a -> Term s (PInner a)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s a
x)

instance PlutusType (a :--> b) where
  type PInner (a :--> b) = a :--> 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 :: S -> Type) (b :: S -> Type).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' Term s a -> Term s b
f
  pmatch' :: forall (s :: S) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type).
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 -> S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (f x)
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
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 -> S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type).
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 :: (S -> Type) -> S -> Type) (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 :: S -> Type)
instance (PGeneric a, PCode a ~ '[ '[GetPNewtype a]]) => Helper (a :: S -> Type)

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

type family GetPNewtype' (a :: [[S -> Type]]) :: S -> Type where
  GetPNewtype' '[ '[a]] = a

type family GetPNewtype (a :: S -> Type) :: S -> Type where
  GetPNewtype a = GetPNewtype' (PCode a)

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

-- | @since 1.10.0
newtype DeriveNewtypePlutusType (a :: S -> Type) s = DeriveNewtypePlutusType
  { forall (a :: S -> Type) (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))))

  -- 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 :: S -> Type).
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 :: S -> Type) (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]]))

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

{- |
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.")

  -- 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]
"Attempted 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 :: S -> Type).
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]
"Attempted to use a type derived with DeriveFakePlutusType"

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

deriving via (DeriveNewtypePlutusType PInteger) instance PlutusType PInteger

instance PlutusType POpaque where
  type PInner POpaque = 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 :: S -> Type).
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' = \case
    PBool s
PTrue -> Term s PBool
Term s (PInner PBool)
forall (s :: S). Term s PBool
ptrue
    PBool s
PFalse -> Term s PBool
Term s (PInner PBool)
forall (s :: S). Term s PBool
pfalse
  {-# INLINEABLE pmatch' #-}
  pmatch' :: forall (s :: S) (b :: S -> Type).
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 (PInner PBool) -> [Term s POpaque] -> Term s b
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase Term s (PInner PBool)
b [Term s b -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s b -> Term s POpaque)
-> (PBool s -> Term s b) -> PBool s -> Term s POpaque
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBool s -> Term s b
f (PBool s -> Term s POpaque) -> PBool s -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PBool s
forall (s :: S). PBool s
PFalse, Term s b -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s b -> Term s POpaque)
-> (PBool s -> Term s b) -> PBool s -> Term s POpaque
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBool s -> Term s b
f (PBool s -> Term s POpaque) -> PBool s -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PBool s
forall (s :: S). PBool s
PTrue]

instance PlutusType PData where
  type PInner PData = 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 :: S -> Type).
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)

{- | = Important note

Due to some weirdnesses regarding builtins, 'PBuiltinPair's cannot be
constructed from anything that's not already @Data@-encoded, but as builtin
pairs are, well, /built-in/, we can lift, and 'pmatch', them just fine. Thus,
you should /not/ use 'pcon' for 'PBuiltinPair'.

@since 1.12.0
-}
instance PlutusType (PBuiltinPair a b) where
  type PInner (PBuiltinPair a b) = PBuiltinPair a b
  pcon' :: forall (s :: S).
PBuiltinPair a b s -> Term s (PInner (PBuiltinPair a b))
pcon' PBuiltinPair a b s
_ = Term s PString
-> Term s (PInner (PBuiltinPair a b))
-> Term s (PInner (PBuiltinPair a b))
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"Do not use pcon for PBuiltinPair; instead, use ppairDataBuiltin or pconstant" Term s (PInner (PBuiltinPair a b))
forall (s :: S) (a :: S -> Type). Term s a
perror
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PBuiltinPair a b))
-> (PBuiltinPair a b s -> Term s b) -> Term s b
pmatch' Term s (PInner (PBuiltinPair a b))
t PBuiltinPair a b s -> Term s b
f = Term s (PInner (PBuiltinPair a b)) -> [Term s POpaque] -> Term s b
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase Term s (PInner (PBuiltinPair a b))
t [Term s (a :--> (b :--> b)) -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s (a :--> (b :--> b)) -> Term s POpaque)
-> ((Term s a -> Term s b -> Term s b)
    -> Term s (a :--> (b :--> b)))
-> (Term s a -> Term s b -> Term s b)
-> Term s POpaque
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term s a -> Term s b -> Term s b) -> Term s (a :--> (b :--> 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 b -> Term s b) -> Term s (c :--> (b :--> b))
plam ((Term s a -> Term s b -> Term s b) -> Term s POpaque)
-> (Term s a -> Term s b -> Term s b) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> PBuiltinPair a b s -> Term s b
f (Term s a -> Term s b -> PBuiltinPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PBuiltinPair a b s
PBuiltinPair Term s a
x Term s b
y)]

instance PLC.Contains PLC.DefaultUni (PlutusRepr a) => PlutusType (PBuiltinList a) where
  type PInner (PBuiltinList a) = PBuiltinList a
  pcon' :: forall (s :: S).
PBuiltinList a s -> Term s (PInner (PBuiltinList a))
pcon' = \case
    PCons Term s a
x Term s (PBuiltinList a)
xs -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList a)
xs
    PBuiltinList a s
PNil -> PLifted s (PInner (PBuiltinList a))
-> Term s (PInner (PBuiltinList a))
forall (s :: S) (a :: S -> Type). 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 :: S -> Type) (s :: S).
Includes @Type DefaultUni h =>
h -> PLifted s a
unsafeHaskToUni @[PlutusRepr a] []
  pmatch' :: forall (s :: S) (b :: S -> Type).
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 POpaque] -> Term s b
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> [Term s POpaque] -> Term s b
punsafeCase Term s (PInner (PBuiltinList a))
xs [Term s (a :--> (PBuiltinList a :--> b)) -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s (a :--> (PBuiltinList a :--> b)) -> Term s POpaque)
-> ((Term s a -> Term s (PBuiltinList a) -> Term s b)
    -> Term s (a :--> (PBuiltinList a :--> b)))
-> (Term s a -> Term s (PBuiltinList a) -> Term s b)
-> Term s POpaque
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term s a -> Term s (PBuiltinList a) -> Term s b)
-> Term s (a :--> (PBuiltinList a :--> 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 (PBuiltinList a) -> Term s b)
-> Term s (c :--> (PBuiltinList a :--> b))
plam ((Term s a -> Term s (PBuiltinList a) -> Term s b)
 -> Term s POpaque)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \Term s a
y Term s (PBuiltinList a)
ys -> PBuiltinList a s -> Term s b
f (Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PBuiltinList a) -> PBuiltinList a s
PCons Term s a
y Term s (PBuiltinList a)
ys), Term s b -> Term s POpaque
forall (s :: S) (a :: S -> Type). Term s a -> Term s POpaque
popaque (Term s b -> Term s POpaque)
-> (PBuiltinList a s -> Term s b)
-> PBuiltinList a s
-> Term s POpaque
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PBuiltinList a s -> Term s b
f (PBuiltinList a s -> Term s POpaque)
-> PBuiltinList a s -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PBuiltinList a s
forall (a :: S -> Type) (s :: S). PBuiltinList a s
PNil]

instance PIsData a => PlutusType (PAsData a) where
  type PInner (PAsData a) = PData
  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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s a
t
  pmatch' :: forall (s :: S) (b :: S -> Type).
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 :: S -> Type) (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 :: S -> Type) (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 :: S -> Type) (a :: S -> Type) (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 :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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

-- | @since 1.11.0
instance PlutusType (PArray a) where
  type PInner (PArray a) = PArray a
  pcon' :: forall (s :: S). PArray a s -> Term s (PInner (PArray a))
pcon' (PArray Term s (PArray a)
t) = Term s (PArray a)
Term s (PInner (PArray a))
t
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PArray a)) -> (PArray a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PArray a))
x PArray a s -> Term s b
f = PArray a s -> Term s b
f (Term s (PArray a) -> PArray a s
forall (a :: S -> Type) (s :: S). Term s (PArray a) -> PArray a s
PArray Term s (PArray a)
Term s (PInner (PArray a))
x)