{-# LANGUAGE UndecidableInstances #-}

module Plutarch.FFI (
  type (>~<),
  PTxList (PTxCons, PTxNil),
  PTxMaybe (PTxJust, PTxNothing),
  foreignExport,
  foreignImport,
  opaqueExport,
  opaqueImport,
  plistFromTx,
  plistToTx,
  pmaybeFromTx,
  pmaybeToTx,
  unsafeForeignExport,
  unsafeForeignImport,
) where

import Control.Lens (over)
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import Data.Text qualified as T
import Data.Void (Void)
import GHC.Generics (Generic)
import GHC.TypeLits qualified as TypeLits
import Generics.SOP qualified as SOP
import Generics.SOP.GGP (GCode, GDatatypeInfoOf)
import Generics.SOP.Type.Metadata (
  ConstructorInfo (Constructor, Infix, Record),
  ConstructorName,
  DatatypeInfo (ADT, Newtype),
 )
import Plutarch (
  ClosedTerm,
  Config,
  DPTStrat,
  DerivePlutusType,
  PDelayed,
  PForall (PForall),
  POpaque,
  PType,
  PlutusTypeNewtype,
  PlutusTypeScott,
  S,
  compile,
  pcon,
  pdelay,
  pforce,
  phoistAcyclic,
  plam,
  pmatch,
  pto,
  (#),
  (:-->),
 )
import Plutarch.Bool (PBool, PEq, (#==))
import Plutarch.Builtin (PData)
import Plutarch.ByteString (PByteString)
import Plutarch.Integer (PInteger)
import Plutarch.Internal (
  RawTerm (RCompiled),
  Term (Term),
  TermResult (TermResult),
 )
import Plutarch.Internal.Generic (PCode)
import Plutarch.Internal.PlutusType (PlutusType (PInner, pcon', pmatch'))
import Plutarch.Internal.Witness (witness)
import Plutarch.List (PList, PListLike (PElemConstraint, pcons, pelimList, pnil), pconvertLists, plistEquals)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Script (Script (Script))
import Plutarch.Show (PShow)
import Plutarch.String (PString)
import Plutarch.Unit (PUnit)
import PlutusTx.Builtins.Internal (BuiltinBool, BuiltinByteString, BuiltinData, BuiltinUnit)
import PlutusTx.Code (CompiledCode, CompiledCodeIn (DeserializedCode), getPlc)
import PlutusTx.Prelude (BuiltinString)
import UntypedPlutusCore (fakeNameDeBruijn)
import UntypedPlutusCore qualified as UPLC

{- | Plutarch type of lists compatible with the PlutusTx encoding of Haskell
 lists and convertible with the regular 'PList' using 'plistToTx' and
 'plistFromTx'.
-}
data PTxList (a :: PType) (s :: S)
  = PTxCons (Term s a) (Term s (PTxList a))
  | PTxNil
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x. Rep (PTxList a s) x -> PTxList a s
forall (a :: PType) (s :: S) x. PTxList a s -> Rep (PTxList a s) x
$cto :: forall (a :: PType) (s :: S) x. Rep (PTxList a s) x -> PTxList a s
$cfrom :: forall (a :: PType) (s :: S) x. PTxList a s -> Rep (PTxList a s) x
Generic)
  deriving anyclass (forall a.
All @[Type] (SListI @Type) (Code a)
-> (a -> Rep a) -> (Rep a -> a) -> Generic a
forall {a :: PType} {s :: S}.
All @[Type] (SListI @Type) (Code (PTxList a s))
forall (a :: PType) (s :: S). Rep (PTxList a s) -> PTxList a s
forall (a :: PType) (s :: S). PTxList a s -> Rep (PTxList a s)
to :: Rep (PTxList a s) -> PTxList a s
$cto :: forall (a :: PType) (s :: S). Rep (PTxList a s) -> PTxList a s
from :: PTxList a s -> Rep (PTxList a s)
$cfrom :: forall (a :: PType) (s :: S). PTxList a s -> Rep (PTxList a s)
SOP.Generic, forall a.
Generic a
-> (forall (proxy :: Type -> Type).
    proxy a -> DatatypeInfo (Code a))
-> HasDatatypeInfo a
forall (a :: PType) (s :: S). Generic (PTxList a s)
forall (a :: PType) (s :: S) (proxy :: Type -> Type).
proxy (PTxList a s) -> DatatypeInfo (Code (PTxList a s))
datatypeInfo :: forall (proxy :: Type -> Type).
proxy (PTxList a s) -> DatatypeInfo (Code (PTxList a s))
$cdatatypeInfo :: forall (a :: PType) (s :: S) (proxy :: Type -> Type).
proxy (PTxList a s) -> DatatypeInfo (Code (PTxList a s))
SOP.HasDatatypeInfo, forall (a :: PType) (s :: S).
PShow a =>
Bool -> Term s (PTxList a) -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s (PTxList a) -> Term s PString
$cpshow' :: forall (a :: PType) (s :: S).
PShow a =>
Bool -> Term s (PTxList a) -> Term s PString
PShow)

{- | Plutarch type compatible with the PlutusTx encoding of Haskell 'Maybe' and
 convertible with the regular 'PMaybe' using 'pmaybeToTx' and 'pmaybeFromTx'.
-}
data PTxMaybe (a :: PType) (s :: S)
  = PTxJust (Term s a)
  | PTxNothing
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x.
Rep (PTxMaybe a s) x -> PTxMaybe a s
forall (a :: PType) (s :: S) x.
PTxMaybe a s -> Rep (PTxMaybe a s) x
$cto :: forall (a :: PType) (s :: S) x.
Rep (PTxMaybe a s) x -> PTxMaybe a s
$cfrom :: forall (a :: PType) (s :: S) x.
PTxMaybe a s -> Rep (PTxMaybe a s) x
Generic)
  deriving anyclass (forall a.
All @[Type] (SListI @Type) (Code a)
-> (a -> Rep a) -> (Rep a -> a) -> Generic a
forall {a :: PType} {s :: S}.
All @[Type] (SListI @Type) (Code (PTxMaybe a s))
forall (a :: PType) (s :: S). Rep (PTxMaybe a s) -> PTxMaybe a s
forall (a :: PType) (s :: S). PTxMaybe a s -> Rep (PTxMaybe a s)
to :: Rep (PTxMaybe a s) -> PTxMaybe a s
$cto :: forall (a :: PType) (s :: S). Rep (PTxMaybe a s) -> PTxMaybe a s
from :: PTxMaybe a s -> Rep (PTxMaybe a s)
$cfrom :: forall (a :: PType) (s :: S). PTxMaybe a s -> Rep (PTxMaybe a s)
SOP.Generic, forall a.
Generic a
-> (forall (proxy :: Type -> Type).
    proxy a -> DatatypeInfo (Code a))
-> HasDatatypeInfo a
forall (a :: PType) (s :: S). Generic (PTxMaybe a s)
forall (a :: PType) (s :: S) (proxy :: Type -> Type).
proxy (PTxMaybe a s) -> DatatypeInfo (Code (PTxMaybe a s))
datatypeInfo :: forall (proxy :: Type -> Type).
proxy (PTxMaybe a s) -> DatatypeInfo (Code (PTxMaybe a s))
$cdatatypeInfo :: forall (a :: PType) (s :: S) (proxy :: Type -> Type).
proxy (PTxMaybe a s) -> DatatypeInfo (Code (PTxMaybe a s))
SOP.HasDatatypeInfo, forall (a :: PType) (s :: S).
PEq a =>
Term s (PTxMaybe a) -> Term s (PTxMaybe a) -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
#== :: forall (s :: S).
Term s (PTxMaybe a) -> Term s (PTxMaybe a) -> Term s PBool
$c#== :: forall (a :: PType) (s :: S).
PEq a =>
Term s (PTxMaybe a) -> Term s (PTxMaybe a) -> Term s PBool
PEq, forall (a :: PType) (s :: S).
PShow a =>
Bool -> Term s (PTxMaybe a) -> Term s PString
forall (t :: PType).
(forall (s :: S). Bool -> Term s t -> Term s PString) -> PShow t
pshow' :: forall (s :: S). Bool -> Term s (PTxMaybe a) -> Term s PString
$cpshow' :: forall (a :: PType) (s :: S).
PShow a =>
Bool -> Term s (PTxMaybe a) -> Term s PString
PShow)

instance PEq a => PEq (PTxList a) where
  #== :: forall (s :: S).
Term s (PTxList a) -> Term s (PTxList a) -> Term s PBool
(#==) Term s (PTxList a)
xs Term s (PTxList a)
ys = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PTxList a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PTxList a)
ys

-- | Compile and export a Plutarch term so it can be used by `PlutusTx.applyCode`.
foreignExport :: forall p t. p >~< t => Config -> ClosedTerm p -> CompiledCode t
foreignExport :: forall (p :: PType) t.
(p >~< t) =>
Config -> ClosedTerm p -> CompiledCode t
foreignExport = let ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(p >~< t)) in forall (p :: PType) t. Config -> ClosedTerm p -> CompiledCode t
unsafeForeignExport

-- | Import compiled UPLC code (such as a spliced `PlutusTx.compile` result) as a Plutarch term.
foreignImport :: forall p t. p >~< t => CompiledCode t -> ClosedTerm p
foreignImport :: forall (p :: PType) t. (p >~< t) => CompiledCode t -> ClosedTerm p
foreignImport = let ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(p >~< t)) in forall t (p :: PType). CompiledCode t -> ClosedTerm p
unsafeForeignImport

-- | Export Plutarch term of any type as @CompiledCode Void@.
opaqueExport :: Config -> ClosedTerm p -> CompiledCode Void
opaqueExport :: forall (p :: PType). Config -> ClosedTerm p -> CompiledCode Void
opaqueExport = forall (p :: PType) t. Config -> ClosedTerm p -> CompiledCode t
unsafeForeignExport

-- | Import compiled UPLC code of any type as a Plutarch opaque term.
opaqueImport :: CompiledCode t -> ClosedTerm POpaque
opaqueImport :: forall t. CompiledCode t -> ClosedTerm POpaque
opaqueImport = forall t (p :: PType). CompiledCode t -> ClosedTerm p
unsafeForeignImport

-- | Seriously unsafe, may fail at run time or result in unexpected behaviour in your on-chain validator.
unsafeForeignExport :: Config -> ClosedTerm p -> CompiledCode t
unsafeForeignExport :: forall (p :: PType) t. Config -> ClosedTerm p -> CompiledCode t
unsafeForeignExport Config
config ClosedTerm p
t = forall (uni :: Type -> Type) fun a.
Program NamedDeBruijn uni fun ()
-> Maybe (Program TyName Name uni fun ())
-> CoverageIndex
-> CompiledCodeIn uni fun a
DeserializedCode Program NamedDeBruijn DefaultUni DefaultFun ()
program forall a. Maybe a
Nothing forall a. Monoid a => a
mempty
  where
    (Script (UPLC.Program ()
_ Version ()
version Term DeBruijn DefaultUni DefaultFun ()
term)) = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. HasCallStack => [Char] -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall (a :: PType). Config -> ClosedTerm a -> Either Text Script
compile Config
config ClosedTerm p
t
    program :: Program NamedDeBruijn DefaultUni DefaultFun ()
program =
      forall name (uni :: Type -> Type) fun ann.
ann
-> Version ann -> Term name uni fun ann -> Program name uni fun ann
UPLC.Program () Version ()
version forall a b. (a -> b) -> a -> b
$
        forall name name' (uni :: Type -> Type) fun ann.
(name -> name') -> Term name uni fun ann -> Term name' uni fun ann
UPLC.termMapNames DeBruijn -> NamedDeBruijn
fakeNameDeBruijn Term DeBruijn DefaultUni DefaultFun ()
term

-- | Seriously unsafe, may fail at run time or result in unexpected behaviour in your on-chain validator.
unsafeForeignImport :: CompiledCode t -> ClosedTerm p
unsafeForeignImport :: forall t (p :: PType). CompiledCode t -> ClosedTerm p
unsafeForeignImport CompiledCode t
c = forall (s :: S) (a :: PType).
(Word64 -> TermMonad TermResult) -> Term s a
Term forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult (Term DeBruijn DefaultUni DefaultFun () -> RawTerm
RCompiled forall a b. (a -> b) -> a -> b
$ forall name (uni :: Type -> Type) fun ann.
Program name uni fun ann -> Term name uni fun ann
UPLC._progTerm forall a b. (a -> b) -> a -> b
$ Program NamedDeBruijn DefaultUni DefaultFun ()
-> Program DeBruijn DefaultUni DefaultFun ()
toNameless forall a b. (a -> b) -> a -> b
$ forall (uni :: Type -> Type) fun a.
(Closed uni, Everywhere uni Flat, Flat fun) =>
CompiledCodeIn uni fun a -> Program NamedDeBruijn uni fun ()
getPlc CompiledCode t
c) []
  where
    toNameless ::
      UPLC.Program UPLC.NamedDeBruijn UPLC.DefaultUni UPLC.DefaultFun () ->
      UPLC.Program UPLC.DeBruijn UPLC.DefaultUni UPLC.DefaultFun ()
    toNameless :: Program NamedDeBruijn DefaultUni DefaultFun ()
-> Program DeBruijn DefaultUni DefaultFun ()
toNameless = forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall name1 (uni1 :: Type -> Type) fun1 ann name2
       (uni2 :: Type -> Type) fun2.
Lens
  (Program name1 uni1 fun1 ann)
  (Program name2 uni2 fun2 ann)
  (Term name1 uni1 fun1 ann)
  (Term name2 uni2 fun2 ann)
UPLC.progTerm forall a b. (a -> b) -> a -> b
$ forall name name' (uni :: Type -> Type) fun ann.
(name -> name') -> Term name uni fun ann -> Term name' uni fun ann
UPLC.termMapNames NamedDeBruijn -> DeBruijn
UPLC.unNameDeBruijn

-- | Convert a 'PList' to a 'PTxList', perhaps before exporting it with 'foreignExport'.
plistToTx :: Term s (PList a :--> PTxList a)
plistToTx :: forall (s :: S) (a :: PType). Term s (PList a :--> PTxList a)
plistToTx = forall (f :: PType -> PType) (g :: PType -> PType) (a :: PType)
       (s :: S).
(PIsListLike f a, PIsListLike g a) =>
Term s (f a :--> g a)
pconvertLists

-- | Convert a 'PTxList' to a 'PList', probably after importing it with 'foreignImport'.
plistFromTx :: Term s (PTxList a :--> PList a)
plistFromTx :: forall (s :: S) (a :: PType). Term s (PTxList a :--> PList a)
plistFromTx = forall (f :: PType -> PType) (g :: PType -> PType) (a :: PType)
       (s :: S).
(PIsListLike f a, PIsListLike g a) =>
Term s (f a :--> g a)
pconvertLists

-- | Convert a 'PMaybe' to a 'PTxMaybe', perhaps before exporting it with 'foreignExport'.
pmaybeToTx :: Term s (PMaybe a :--> PTxMaybe a)
pmaybeToTx :: forall (s :: S) (a :: PType). Term s (PMaybe a :--> PTxMaybe a)
pmaybeToTx =
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch forall a b. (a -> b) -> a -> b
$
      forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
        PMaybe a s
PNothing -> forall (a :: PType) (s :: S). PTxMaybe a s
PTxNothing
        PJust Term s a
x -> forall (a :: PType) (s :: S). Term s a -> PTxMaybe a s
PTxJust Term s a
x

-- | Convert a 'PTxMaybe' to a 'PMaybe', probably after importing it with 'foreignImport'.
pmaybeFromTx :: Term s (PTxMaybe a :--> PMaybe a)
pmaybeFromTx :: forall (s :: S) (a :: PType). Term s (PTxMaybe a :--> PMaybe a)
pmaybeFromTx =
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch forall a b. (a -> b) -> a -> b
$
      forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
        PTxMaybe a s
PTxNothing -> forall (a :: PType) (s :: S). PMaybe a s
PNothing
        PTxJust Term s a
x -> forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust Term s a
x

newtype PTxList' a r s = PTxList' (Term s (PDelayed (r :--> (a :--> PTxList a :--> r) :--> r)))
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (r :: PType) (s :: S) x.
Rep (PTxList' a r s) x -> PTxList' a r s
forall (a :: PType) (r :: PType) (s :: S) x.
PTxList' a r s -> Rep (PTxList' a r s) x
$cto :: forall (a :: PType) (r :: PType) (s :: S) x.
Rep (PTxList' a r s) x -> PTxList' a r s
$cfrom :: forall (a :: PType) (r :: PType) (s :: S) x.
PTxList' a r s -> Rep (PTxList' a r s) x
Generic)
  deriving anyclass (forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: PType) (r :: PType) (s :: S).
PTxList' a r s -> Term s (PInner (PTxList' a r))
forall (a :: PType) (r :: PType) (s :: S) (b :: PType).
Term s (PInner (PTxList' a r))
-> (PTxList' a r s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PTxList' a r))
-> (PTxList' a r s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (r :: PType) (s :: S) (b :: PType).
Term s (PInner (PTxList' a r))
-> (PTxList' a r s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PTxList' a r s -> Term s (PInner (PTxList' a r))
$cpcon' :: forall (a :: PType) (r :: PType) (s :: S).
PTxList' a r s -> Term s (PInner (PTxList' a r))
PlutusType)
instance DerivePlutusType (PTxList' a r) where type DPTStrat _ = PlutusTypeNewtype

instance PlutusType (PTxList a) where
  type PInner (PTxList a) = PForall (PTxList' a)
  pcon' :: forall (s :: S). PTxList a s -> Term s (PInner (PTxList a))
pcon' (PTxCons Term s a
x Term s (PTxList a)
xs) = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (r :: PType) (s :: S).
Term s (PDelayed (r :--> ((a :--> (PTxList a :--> r)) :--> r)))
-> PTxList' a r s
PTxList' forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s x
_nil Term s (a :--> (PTxList a :--> x))
cons -> Term s (a :--> (PTxList a :--> x))
cons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PTxList a)
xs
  pcon' PTxList a s
PTxNil = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (r :: PType) (s :: S).
Term s (PDelayed (r :--> ((a :--> (PTxList a :--> r)) :--> r)))
-> PTxList' a r s
PTxList' forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. a -> b -> a
const
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PTxList a))
-> (PTxList a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PTxList a))
elim PTxList a s -> Term s b
f = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInner (PTxList a))
elim \(PForall forall (x :: PType). Term s (PTxList' a x)
elim) -> forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (x :: PType). Term s (PTxList' a x)
elim) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# PTxList a s -> Term s b
f forall (a :: PType) (s :: S). PTxList a s
PTxNil forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term s a
x Term s (PTxList a)
xs -> PTxList a s -> Term s b
f forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
Term s a -> Term s (PTxList a) -> PTxList a s
PTxCons Term s a
x Term s (PTxList a)
xs)

instance PListLike PTxList where
  type PElemConstraint PTxList _ = ()
  pelimList :: forall (a :: PType) (s :: S) (r :: PType).
PElemConstraint PTxList a =>
(Term s a -> Term s (PTxList a) -> Term s r)
-> Term s r -> Term s (PTxList a) -> Term s r
pelimList Term s a -> Term s (PTxList a) -> Term s r
cons Term s r
nil Term s (PTxList a)
list = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PTxList a)
list) \(PForall forall (x :: PType). Term s (PTxList' a x)
list) -> forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (x :: PType). Term s (PTxList' a x)
list) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s r
nil forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam Term s a -> Term s (PTxList a) -> Term s r
cons
  pcons :: forall (a :: PType) (s :: S).
PElemConstraint PTxList a =>
Term s (a :--> (PTxList a :--> PTxList a))
pcons = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PTxList a)
xs -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (forall (a :: PType) (s :: S).
Term s a -> Term s (PTxList a) -> PTxList a s
PTxCons Term s a
x Term s (PTxList a)
xs)
  pnil :: forall (a :: PType) (s :: S).
PElemConstraint PTxList a =>
Term s (PTxList a)
pnil = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PTxList a s
PTxNil

newtype PTxMaybe' a r s = PTxMaybe' (Term s (PDelayed ((a :--> r) :--> r :--> r)))
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (r :: PType) (s :: S) x.
Rep (PTxMaybe' a r s) x -> PTxMaybe' a r s
forall (a :: PType) (r :: PType) (s :: S) x.
PTxMaybe' a r s -> Rep (PTxMaybe' a r s) x
$cto :: forall (a :: PType) (r :: PType) (s :: S) x.
Rep (PTxMaybe' a r s) x -> PTxMaybe' a r s
$cfrom :: forall (a :: PType) (r :: PType) (s :: S) x.
PTxMaybe' a r s -> Rep (PTxMaybe' a r s) x
Generic)
  deriving anyclass (forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: PType) (r :: PType) (s :: S).
PTxMaybe' a r s -> Term s (PInner (PTxMaybe' a r))
forall (a :: PType) (r :: PType) (s :: S) (b :: PType).
Term s (PInner (PTxMaybe' a r))
-> (PTxMaybe' a r s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PTxMaybe' a r))
-> (PTxMaybe' a r s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (r :: PType) (s :: S) (b :: PType).
Term s (PInner (PTxMaybe' a r))
-> (PTxMaybe' a r s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PTxMaybe' a r s -> Term s (PInner (PTxMaybe' a r))
$cpcon' :: forall (a :: PType) (r :: PType) (s :: S).
PTxMaybe' a r s -> Term s (PInner (PTxMaybe' a r))
PlutusType)
instance DerivePlutusType (PTxMaybe' a r) where type DPTStrat _ = PlutusTypeNewtype

instance PlutusType (PTxMaybe a) where
  type PInner (PTxMaybe a) = PForall (PTxMaybe' a)
  pcon' :: forall (s :: S). PTxMaybe a s -> Term s (PInner (PTxMaybe a))
pcon' (PTxJust Term s a
x) = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (r :: PType) (s :: S).
Term s (PDelayed ((a :--> r) :--> (r :--> r))) -> PTxMaybe' a r s
PTxMaybe' forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> x)
just Term s x
_nothing -> Term s (a :--> x)
just forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x
  pcon' PTxMaybe a s
PTxNothing = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (r :: PType) (s :: S).
Term s (PDelayed ((a :--> r) :--> (r :--> r))) -> PTxMaybe' a r s
PTxMaybe' forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> x)
_just Term s x
nothing -> Term s x
nothing
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PTxMaybe a))
-> (PTxMaybe a s -> Term s b) -> Term s b
pmatch' Term s (PInner (PTxMaybe a))
elim PTxMaybe a s -> Term s b
f = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInner (PTxMaybe a))
elim \(PForall forall (x :: PType). Term s (PTxMaybe' a x)
elim) -> forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall (x :: PType). Term s (PTxMaybe' a x)
elim) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (PTxMaybe a s -> Term s b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PTxMaybe a s
PTxJust) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# PTxMaybe a s -> Term s b
f forall (a :: PType) (s :: S). PTxMaybe a s
PTxNothing

type family F (p :: [PType]) (t :: [Type]) :: Constraint where
  F '[] '[] = ()
  F (x : xs) (y : ys) = (x >~< y, F xs ys)

type family G (p :: [[PType]]) (t :: [[Type]]) :: Constraint where
  G '[] '[] = ()
  G (x : xs) (y : ys) = (F x y, G xs ys)

-- | Equality of inner types - Plutarch on the left and Haskell on the right.
type family (p :: PType) >~< (t :: Type) :: Constraint where
  PBool >~< BuiltinBool = ()
  PInteger >~< Integer = ()
  PString >~< BuiltinString = ()
  PByteString >~< BuiltinByteString = ()
  PData >~< BuiltinData = ()
  PUnit >~< BuiltinUnit = ()
  (a :--> b) >~< (a' -> b') = (a >~< a', b >~< b')
  (PTxList a) >~< [a'] = a >~< a'
  (PTxMaybe a) >~< Maybe a' = a >~< a'
  (PDelayed p) >~< t = (DPTStrat p ~ PlutusTypeScott, G (PCode p) (TypeEncoding t))

type TypeEncoding a = (TypeEncoding' (GCode a) (GDatatypeInfoOf a))

type TypeEncoding' :: [[Type]] -> DatatypeInfo -> [[Type]]
type family TypeEncoding' a rep where
  TypeEncoding' '[ '[b]] ( 'Newtype _ _ _) = TypeEncoding b
  -- Matching the behaviour of PlutusTx.Lift.Class.sortedCons
  TypeEncoding' sop ( 'ADT _ "Bool" _ _) = sop
  TypeEncoding' sop ( 'ADT _ _ cons _) = Fst (SortedBy '(sop, NamesOf cons))

type Fst :: (a, b) -> a
type family Fst x where
  Fst '(a, _) = a

type SortedBy :: ([[Type]], [ConstructorName]) -> ([[Type]], [ConstructorName])
type family SortedBy xs where
  SortedBy '(ts ': tss, name ': names) = Insert ts name (SortedBy '(tss, names))
  SortedBy '( '[], '[]) = '( '[], '[])

type Insert :: [Type] -> ConstructorName -> ([[Type]], [ConstructorName]) -> ([[Type]], [ConstructorName])
type family Insert ts name xs where
  Insert ts1 name1 '(ts2 ': tss, name2 : names) = Insert' (TypeLits.CmpSymbol name1 name2) ts1 name1 '(ts2 ': tss, name2 : names)
  Insert ts name '( '[], '[]) = '( '[ts], '[name])

type Insert' :: Ordering -> [Type] -> ConstructorName -> ([[Type]], [ConstructorName]) -> ([[Type]], [ConstructorName])
type family Insert' o ts name xs where
  Insert' 'GT ts1 name1 '(ts2 ': tss, name2 ': names) = Cons ts2 name2 (Insert ts1 name1 '(tss, names))
  Insert' _ ts name '(tss, names) = '(ts ': tss, name ': names)

type Cons :: a -> b -> ([a], [b]) -> ([a], [b])
type family Cons ts name xs where
  Cons ts name '(tss, names) = '(ts ': tss, name ': names)

type NamesOf :: [ConstructorInfo] -> [ConstructorName]
type family NamesOf cs where
  NamesOf ( 'Constructor name ': cs) = name ': NamesOf cs
  NamesOf ( 'Infix name _ _ ': cs) = name ': NamesOf cs
  NamesOf ( 'Record name _ ': cs) = name ': NamesOf cs
  NamesOf '[] = '[]