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

module Plutarch.DataRepr.Internal (
  PDataSum (..),
  punDataSum,
  ptryIndexDataSum,
  pdcons,
  pdnil,
  DataReprHandlers (..),
  PConstantData,
  PDataRecord (..),
  PLiftData,
  PLabeledType (..),
  type PLabelIndex,
  type PUnLabel,
  type PLookupLabel,
  pindexDataRecord,
  pdropDataRecord,
  DerivePConstantViaData (..),
  DualReprHandler (..),
  PlutusTypeData,
) where

import Data.Coerce (coerce)
import Data.Functor.Compose qualified as F
import Data.Functor.Const (Const (Const))
import Data.Kind (Constraint, Type)
import Data.List (groupBy, maximumBy, sortOn)
import Data.Proxy (Proxy (Proxy))
import Data.SOP.NP (cana_NP)
import Data.String (fromString)
import GHC.Generics (Generic)
import GHC.TypeLits (
  KnownNat,
  KnownSymbol,
  Nat,
  Symbol,
  natVal,
  symbolVal,
  type (+),
 )
import Generics.SOP (
  All,
  Compose,
  K (K),
  NP (Nil, (:*)),
  NS (S, Z),
  SListI,
  SOP (SOP),
  Top,
  case_SList,
  hcollapse,
  hindex,
  hmap,
  para_SList,
 )
import Plutarch (
  Dig,
  PInner,
  POpaque,
  PType,
  PlutusType,
  PlutusTypeNewtype,
  S,
  Term,
  pcon,
  pdelay,
  perror,
  pforce,
  phoistAcyclic,
  plam,
  plet,
  pmatch,
  popaque,
  pto,
  (#),
  (#$),
  type (:-->),
 )
import Plutarch.Bool (PBool, PEq, POrd, PPartialOrd, pif, (#<), (#<=), (#==))
import Plutarch.Builtin (
  PAsData,
  PBuiltinList,
  PData,
  PIsData,
  pasConstr,
  pchooseListBuiltin,
  pconstrBuiltin,
  pdata,
  pdataImpl,
  pforgetData,
  pfromData,
  pfromDataImpl,
  pfstBuiltin,
  psndBuiltin,
 )
import Plutarch.DataRepr.Internal.HList (
  HRec (HCons, HNil),
  HRecGeneric (HRecGeneric),
  Labeled (Labeled),
  type Drop,
  type IndexList,
 )
import Plutarch.Integer (PInteger)
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom, gpto)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  DerivedPInner,
  PlutusTypeStrat,
  PlutusTypeStratConstraint,
  derivedPCon,
  derivedPMatch,
  pcon',
  pmatch',
 )
import Plutarch.Lift (
  PConstant,
  PConstantDecl,
  PConstantRepr,
  PConstanted,
  PLift,
  PLifted,
  pconstant,
  pconstantFromRepr,
  pconstantToRepr,
 )
import Plutarch.List (PListLike (pnil), pcons, pdrop, phead, ptail, ptryIndex)
import Plutarch.TermCont (TermCont, hashOpenTerm, runTermCont, tcont, unTermCont)
import Plutarch.Trace (ptraceError)
import Plutarch.TryFrom (PSubtype, PSubtype', PSubtypeRelation (PNoSubtypeRelation, PSubtypeRelation), PTryFrom, PTryFromExcess, ptryFrom, ptryFrom', pupcast)
import Plutarch.Unit (PUnit (PUnit))
import Plutarch.Unsafe (punsafeCoerce)
import PlutusLedgerApi.V1 qualified as Ledger

import Plutarch.Reducible (NoReduce, Reduce)
import Plutarch.Show (PShow (pshow'))
import Plutarch.String (PString)

{- | A "record" of `exists a. PAsData a`. The underlying representation is
 `PBuiltinList PData`.
-}
data PDataRecord (as :: [PLabeledType]) (s :: S) where
  PDCons ::
    forall name_x x xs s.
    PUnLabel name_x ~ x =>
    Term s (PAsData x) ->
    (Term s (PDataRecord xs)) ->
    -- GHC bug prevents `name ':= x` from working well
    PDataRecord (name_x ': xs) s
  PDNil :: PDataRecord '[] s

newtype H s (l :: [PLabeledType]) = H {forall (s :: S) (l :: [PLabeledType]).
H s l
-> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r
unH :: forall r. (PDataRecord l s -> Term s r) -> Term s r}

instance SListI l => PlutusType (PDataRecord l) where
  type PInner (PDataRecord l) = PBuiltinList PData
  pcon' :: PDataRecord l s -> Term s (PBuiltinList PData)
  pcon' :: forall (s :: S). PDataRecord l s -> Term s (PBuiltinList PData)
pcon' (PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
xs) = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData x)
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataRecord xs)
xs
  pcon' PDataRecord l s
PDNil = forall (a :: PType) (s :: S).
PlutusType a =>
a s -> Term s (PInner a)
pcon' forall (s :: S). PDataRecord ('[] @PLabeledType) s
PDNil
  pmatch' :: Term s (PBuiltinList PData) -> (PDataRecord l s -> Term s b) -> Term s b
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PBuiltinList PData)
-> (PDataRecord l s -> Term s b) -> Term s b
pmatch' Term s (PBuiltinList PData)
l' = forall (s :: S) (l :: [PLabeledType]).
H s l
-> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r
unH
    forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (r :: [k] -> Type).
SListI @k xs =>
r ('[] @k)
-> (forall (y :: k) (ys :: [k]). SListI @k ys => r ((':) @k y ys))
-> r xs
case_SList
      (forall (s :: S) (l :: [PLabeledType]).
(forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r)
-> H s l
H forall a b. (a -> b) -> a -> b
$ \PDataRecord ('[] @PLabeledType) s -> Term s r
f -> PDataRecord ('[] @PLabeledType) s -> Term s r
f forall (s :: S). PDataRecord ('[] @PLabeledType) s
PDNil)
    forall a b. (a -> b) -> a -> b
$ forall (s :: S) (l :: [PLabeledType]).
(forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r)
-> H s l
H
    forall a b. (a -> b) -> a -> b
$ \PDataRecord ((':) @PLabeledType y ys) s -> Term s r
f ->
      forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PBuiltinList PData)
l' \Term s (PBuiltinList PData)
l ->
        let x :: Term _ (PAsData x)
            x :: Term s (PAsData x)
x = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
l
            xs :: Term _ (PDataRecord xs)
            xs :: Term s (PDataRecord xs)
xs = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
l
         in PDataRecord ((':) @PLabeledType y ys) s -> Term s r
f forall a b. (a -> b) -> a -> b
$ forall (def :: PLabeledType) (defs :: PType) (xs :: [PLabeledType])
       (s :: S).
((PUnLabel def :: PType) ~ (defs :: PType)) =>
Term s (PAsData defs)
-> Term s (PDataRecord xs)
-> PDataRecord ((':) @PLabeledType def xs) s
PDCons forall (x :: PType). Term s (PAsData x)
x forall (xs :: [PLabeledType]). Term s (PDataRecord xs)
xs

-- | This uses data equality. 'PEq' instances of elements don't make any difference.
instance PEq (PDataRecord xs) where
  Term s (PDataRecord xs)
x #== :: forall (s :: S).
Term s (PDataRecord xs) -> Term s (PDataRecord xs) -> Term s PBool
#== Term s (PDataRecord xs)
y = forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataRecord xs)
x forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataRecord xs)
y

-- Lexicographic ordering based 'Ord' instances for 'PDataRecord'.

instance PPartialOrd (PDataRecord '[]) where
  Term s (PDataRecord ('[] @PLabeledType))
_ #<= :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PBool
#<= Term s (PDataRecord ('[] @PLabeledType))
_ = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True
  Term s (PDataRecord ('[] @PLabeledType))
_ #< :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PBool
#< Term s (PDataRecord ('[] @PLabeledType))
_ = forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

instance POrd (PDataRecord '[])

instance PShow (PDataRecord '[]) where
  pshow' :: forall (s :: S).
Bool -> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PString
pshow' Bool
_ Term s (PDataRecord ('[] @PLabeledType))
_ = Term s PString
"[]"

instance
  (All Top xs, KnownSymbol label, PIsData x, PShow x, PShow (PDataRecordShowHelper xs)) =>
  PShow (PDataRecord ((label ':= x) ': xs))
  where
  pshow' :: forall (s :: S).
Bool
-> Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
-> Term s PString
pshow' Bool
b Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
xs = Term s PString
"[" forall a. Semigroup a => a -> a -> a
<> forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
xs forall (s :: S).
PDataRecord ((':) @PLabeledType (label ':= x) xs) s
-> Term s PString
go
    where
      go :: PDataRecord ((label ':= x) : xs) s -> Term s PString
      go :: forall (s :: S).
PDataRecord ((':) @PLabeledType (label ':= x) xs) s
-> Term s PString
go (PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
ys) =
        forall (label :: Symbol) (t :: PType) (s :: S).
(KnownSymbol label, PShow t) =>
Proxy @Symbol label -> Bool -> Term s t -> Term s PString
showWithLabel (forall {k} (t :: k). Proxy @k t
Proxy @label) Bool
b Term s (PAsData x)
y
          forall a. Semigroup a => a -> a -> a
<> forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (as :: [PLabeledType]) (s :: S).
Term s (PDataRecord as) -> PDataRecordShowHelper as s
PDataRecordShowHelper Term s (PDataRecord xs)
ys)

{- | This type exists because we need different show strategies depending
 on if the original list was non-empty. The idea is to implement the
 following at the type-level:

 @
 showList' :: Show a => [a] -> String
 showList' [] = "[]"
 showList' (x:xs) = '[' : show x ++ go xs
 where
   go [] = "]"
   go (y:ys) = ',' : show y ++ go ys
 @
-}
newtype PDataRecordShowHelper as s = PDataRecordShowHelper (Term s (PDataRecord as))
  deriving stock (forall (as :: [PLabeledType]) (s :: S) x.
Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s
forall (as :: [PLabeledType]) (s :: S) x.
PDataRecordShowHelper as s -> Rep (PDataRecordShowHelper as s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (as :: [PLabeledType]) (s :: S) x.
Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s
$cfrom :: forall (as :: [PLabeledType]) (s :: S) x.
PDataRecordShowHelper as s -> Rep (PDataRecordShowHelper as s) x
Generic)
  deriving anyclass (forall (as :: [PLabeledType]) (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
forall (as :: [PLabeledType]) (s :: S) (b :: PType).
Term s (PInner (PDataRecordShowHelper as))
-> (PDataRecordShowHelper as s -> Term s b) -> Term s b
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
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PDataRecordShowHelper as))
-> (PDataRecordShowHelper as s -> Term s b) -> Term s b
$cpmatch' :: forall (as :: [PLabeledType]) (s :: S) (b :: PType).
Term s (PInner (PDataRecordShowHelper as))
-> (PDataRecordShowHelper as s -> Term s b) -> Term s b
pcon' :: forall (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
$cpcon' :: forall (as :: [PLabeledType]) (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
PlutusType)

instance DerivePlutusType (PDataRecordShowHelper as) where type DPTStrat _ = PlutusTypeNewtype

instance PShow (PDataRecordShowHelper '[]) where
  pshow' :: forall (s :: S).
Bool
-> Term s (PDataRecordShowHelper ('[] @PLabeledType))
-> Term s PString
pshow' Bool
_ Term s (PDataRecordShowHelper ('[] @PLabeledType))
_ = Term s PString
"]"

instance
  (All Top xs, KnownSymbol label, PIsData x, PShow x, PShow (PDataRecordShowHelper xs)) =>
  PShow (PDataRecordShowHelper ((label ':= x) ': xs))
  where
  pshow' :: forall (s :: S).
Bool
-> Term
     s (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs))
-> Term s PString
pshow' Bool
b Term
  s (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs))
xs = Term s PString
", " forall a. Semigroup a => a -> a -> a
<> 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 (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs))
xs) PDataRecord ((':) @PLabeledType (label ':= x) xs) s
-> Term s PString
go
    where
      go :: PDataRecord ((':) @PLabeledType (label ':= x) xs) s
-> Term s PString
go (PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
ys) =
        forall (label :: Symbol) (t :: PType) (s :: S).
(KnownSymbol label, PShow t) =>
Proxy @Symbol label -> Bool -> Term s t -> Term s PString
showWithLabel (forall {k} (t :: k). Proxy @k t
Proxy @label) Bool
b Term s (PAsData x)
y
          forall a. Semigroup a => a -> a -> a
<> forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (as :: [PLabeledType]) (s :: S).
Term s (PDataRecord as) -> PDataRecordShowHelper as s
PDataRecordShowHelper Term s (PDataRecord xs)
ys)

instance (POrd x, PIsData x) => PPartialOrd (PDataRecord '[label ':= x]) where
  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l1 #< :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term s PBool
#< Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l2 = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l1
    PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l2

    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y

  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l1 #<= :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term s PBool
#<= Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l2 = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l1
    PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l2

    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y

instance (POrd x, PIsData x) => POrd (PDataRecord '[label ':= x])

instance
  (SListI xs, POrd x, PIsData x, POrd (PDataRecord (x' ': xs))) =>
  PPartialOrd (PDataRecord ((label ':= x) ': x' ': xs))
  where
  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l1 #< :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term s PBool
#< Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l2 = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
xs <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l1
    PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
ys <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l2

    Term s x
a <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x
    Term s x
b <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y

    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s x
b) (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True) forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s x
b) (Term s (PDataRecord xs)
xs forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PDataRecord xs)
ys) forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l1 #<= :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term s PBool
#<= Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l2 = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
xs <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l1
    PDCons Term s (PAsData x)
y Term s (PDataRecord xs)
ys <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l2

    Term s x
a <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x
    Term s x
b <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y

    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s x
b) (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True) forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s x
b) (Term s (PDataRecord xs)
xs forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PDataRecord xs)
ys) forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False

instance
  (SListI xs, POrd x, PIsData x, POrd (PDataRecord (x' ': xs))) =>
  POrd (PDataRecord ((label ':= x) ': x' ': xs))

{- | Cons a field to a data record.

You can specify the label to associate with the field using type applications-

@

foo :: Term s (PDataRecord '[ "fooField" ':= PByteString ])
foo = pdcons @"fooField" # pdata (phexByteStr "ab") # pdnil

@
-}
pdcons :: forall label a l s. Term s (PAsData a :--> PDataRecord l :--> PDataRecord ((label ':= a) ': l))
pdcons :: forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons @PBuiltinList @PData

-- | An empty 'PDataRecord'.
pdnil :: Term s (PDataRecord '[])
pdnil :: forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil @PBuiltinList @PData

data PLabeledType = Symbol := PType

type family PLabelIndex (name :: Symbol) (as :: [PLabeledType]) :: Nat where
  PLabelIndex name ((name ':= _) ': _) = 0
  PLabelIndex name (_ ': as) = PLabelIndex name as + 1

type PLookupLabel :: Symbol -> [PLabeledType] -> PType
type family PLookupLabel name as where
  PLookupLabel name ((name ':= a) ': _) = a
  PLookupLabel name (_ ': as) = PLookupLabel name as

type family PUnLabel (a :: PLabeledType) :: PType where
  PUnLabel (_ ':= a) = a

instance PIsData (PDataRecord xs) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PDataRecord xs)) -> Term s (PDataRecord xs)
pfromDataImpl Term s (PAsData (PDataRecord xs))
x = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PAsData (PDataRecord xs))
x) :: Term _ (PBuiltinList PData))
  pdataImpl :: forall (s :: S). Term s (PDataRecord xs) -> Term s PData
pdataImpl Term s (PDataRecord xs)
x = forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s (PDataRecord xs)
x :: Term _ (PBuiltinList PData))

{- | A sum of 'PDataRecord's. The underlying representation is the `Constr` constructor,
where the integer is the index of the variant and the list is the record.
-}
type PDataSum :: [[PLabeledType]] -> PType
newtype PDataSum defs s = PDataSum (NS (F.Compose (Term s) PDataRecord) defs)

instance (All Top defs, All (Compose PShow PDataRecord) defs) => PShow (PDataSum defs) where
  pshow' :: forall (s :: S). Bool -> Term s (PDataSum defs) -> Term s PString
pshow' Bool
b Term s (PDataSum defs)
dsum = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PDataSum defs)
dsum forall (xs :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] PShow PDataRecord)
  xs =>
PDataSum xs s -> Term s PString
showSum
    where
      showSum :: (All (Compose PShow PDataRecord) xs) => PDataSum xs s -> Term s PString
      showSum :: forall (xs :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] PShow PDataRecord)
  xs =>
PDataSum xs s -> Term s PString
showSum (PDataSum (Z Compose @PType @[PLabeledType] (Term s) PDataRecord x
x)) = forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose @k1 @k2 f g a -> f (g a)
F.getCompose Compose @PType @[PLabeledType] (Term s) PDataRecord x
x)
      showSum (PDataSum (S NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
x)) = forall (xs :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] PShow PDataRecord)
  xs =>
PDataSum xs s -> Term s PString
showSum (forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
x)

class IsPDataSum (a :: [[PType]]) where
  type IsPDataSumDefs a :: [[PLabeledType]]
  toSum :: SOP (Term s) a -> PDataSum (IsPDataSumDefs a) s
  fromSum :: PDataSum (IsPDataSumDefs a) s -> SOP (Term s) a

instance IsPDataSum '[] where
  type IsPDataSumDefs '[] = '[]
  toSum :: forall (s :: S).
SOP @PType (Term s) ('[] @[PType])
-> PDataSum (IsPDataSumDefs ('[] @[PType])) s
toSum (SOP NS @[PType] (NP @PType (Term s)) ('[] @[PType])
x) = case NS @[PType] (NP @PType (Term s)) ('[] @[PType])
x of {}
  fromSum :: forall (s :: S).
PDataSum (IsPDataSumDefs ('[] @[PType])) s
-> SOP @PType (Term s) ('[] @[PType])
fromSum (PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs ('[] @[PType]))
x) = case NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs ('[] @[PType]))
x of {}

instance IsPDataSum xs => IsPDataSum ('[PDataRecord l] : xs) where
  type IsPDataSumDefs ('[PDataRecord l] : xs) = (l : IsPDataSumDefs xs)
  toSum :: forall (s :: S).
SOP
  @PType
  (Term s)
  ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
-> PDataSum
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
     s
toSum (SOP (Z (Term s x
x :* NP @PType (Term s) xs
Nil))) = forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible @Type a b => a -> b
coerce Term s x
x
  toSum (SOP (S NS @[PType] (NP @PType (Term s)) xs
x)) = case forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
SOP @PType (Term s) a -> PDataSum (IsPDataSumDefs a) s
toSum (forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP NS @[PType] (NP @PType (Term s)) xs
x) of
    PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs xs)
y -> forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs xs)
y
  fromSum :: forall (s :: S).
PDataSum
  (IsPDataSumDefs
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
  s
-> SOP
     @PType
     (Term s)
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
fromSum (PDataSum (Z Compose @PType @[PLabeledType] (Term s) PDataRecord x
x)) = forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible @Type a b => a -> b
coerce Compose @PType @[PLabeledType] (Term s) PDataRecord x
x forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil
  fromSum (PDataSum (S NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
x)) = case forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
PDataSum (IsPDataSumDefs a) s -> SOP @PType (Term s) a
fromSum (forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
x) of
    SOP NS @[PType] (NP @PType (Term s)) xs
y -> forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[PType] (NP @PType (Term s)) xs
y

data DataReprHandlers (out :: PType) (defs :: [[PLabeledType]]) (s :: S) where
  DRHNil :: DataReprHandlers out '[] s
  DRHCons :: (Term s (PDataRecord def) -> Term s out) -> DataReprHandlers out defs s -> DataReprHandlers out (def : defs) s

newtype A s out defs = A {forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
A s out defs
-> (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
unA :: (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s}

instance
  ( SListI defs
  ) =>
  PlutusType (PDataSum defs)
  where
  type PInner (PDataSum defs) = PData
  pcon' :: forall (s :: S). PDataSum defs s -> Term s (PInner (PDataSum defs))
pcon' (PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
xss) =
    let constrIx :: Integer
constrIx = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
hindex NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
xss
        datRec :: CollapseTo
  @[PLabeledType]
  @[[PLabeledType]]
  (NS @[PLabeledType])
  (Term s (PBuiltinList PData))
datRec = forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
hcollapse forall a b. (a -> b) -> a -> b
$ forall {k} {l} (h :: (k -> Type) -> l -> Type) (xs :: l)
       (f :: k -> Type) (f' :: k -> Type).
(SListIN @k @l (Prod @k @l h) xs, HAp @k @l h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap (forall k a (b :: k). a -> K @k a b
K forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose @k1 @k2 f g a -> f (g a)
F.getCompose) NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
xss
     in forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Integer
constrIx forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# CollapseTo
  @[PLabeledType]
  @[[PLabeledType]]
  (NS @[PLabeledType])
  (Term s (PBuiltinList PData))
datRec
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PDataSum defs))
-> (PDataSum defs s -> Term s b) -> Term s b
pmatch' Term s (PInner (PDataSum defs))
d PDataSum defs s -> Term s b
f =
    let handlers :: DataReprHandlers b defs s
handlers = forall (out :: PType) (s :: S) (defs :: [[PLabeledType]]).
SListI @[PLabeledType] defs =>
(PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
conv PDataSum defs s -> Term s b
f
     in case DataReprHandlers b defs s
handlers of
          DRHCons Term s (PDataRecord def) -> Term s b
handler DataReprHandlers b defs s
DRHNil -> Term s (PDataRecord def) -> Term s b
handler forall a b. (a -> b) -> a -> b
$ forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataSum defs))
d :: Term _ (PDataSum defs))
          DataReprHandlers b defs s
_ -> forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PInner (PDataSum defs))
d) forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
d' ->
            forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d') forall a b. (a -> b) -> a -> b
$ \Term s PInteger
constr ->
              forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d') forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList PData)
args ->
                let handlers' :: [Term s b]
handlers' = forall (out :: PType) (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> DataReprHandlers out defs s -> [Term s out]
applyHandlers Term s (PBuiltinList PData)
args DataReprHandlers b defs s
handlers
                 in forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s (Dig, Term s out)
findCommon [Term s b]
handlers') forall a b. (a -> b) -> a -> b
$ \(Dig, Term s b)
common ->
                      forall (s :: S) (out :: PType).
(Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
reprHandlersGo
                        (Dig, Term s b)
common
                        Integer
0
                        [Term s b]
handlers'
                        Term s PInteger
constr
    where
      applyHandlers :: forall out s defs. Term s (PBuiltinList PData) -> DataReprHandlers out defs s -> [Term s out]
      applyHandlers :: forall (out :: PType) (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> DataReprHandlers out defs s -> [Term s out]
applyHandlers Term s (PBuiltinList PData)
_ DataReprHandlers out defs s
DRHNil = []
      applyHandlers Term s (PBuiltinList PData)
args (DRHCons Term s (PDataRecord def) -> Term s out
handler DataReprHandlers out defs s
rest) = Term s (PDataRecord def) -> Term s out
handler (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args) forall a. a -> [a] -> [a]
: forall (out :: PType) (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> DataReprHandlers out defs s -> [Term s out]
applyHandlers Term s (PBuiltinList PData)
args DataReprHandlers out defs s
rest

      conv :: forall out s defs. SListI defs => (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
      conv :: forall (out :: PType) (s :: S) (defs :: [[PLabeledType]]).
SListI @[PLabeledType] defs =>
(PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
conv =
        forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
A s out defs
-> (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
unA forall a b. (a -> b) -> a -> b
$
          forall {k} (xs :: [k]) (r :: [k] -> Type).
SListI @k xs =>
r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    SListI @k ys =>
    r ys -> r ((':) @k y ys))
-> r xs
para_SList
            (forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
((PDataSum defs s -> Term s out) -> DataReprHandlers out defs s)
-> A s out defs
A forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (out :: PType) (s :: S).
DataReprHandlers out ('[] @[PLabeledType]) s
DRHNil)
            ( \(A (PDataSum ys s -> Term s out) -> DataReprHandlers out ys s
prev) -> forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
((PDataSum defs s -> Term s out) -> DataReprHandlers out defs s)
-> A s out defs
A \PDataSum ((':) @[PLabeledType] y ys) s -> Term s out
f ->
                forall (s :: S) (def :: [PLabeledType]) (out :: PType)
       (defs :: [[PLabeledType]]).
(Term s (PDataRecord def) -> Term s out)
-> DataReprHandlers out defs s
-> DataReprHandlers out ((':) @[PLabeledType] def defs) s
DRHCons
                  (\Term s (PDataRecord y)
x -> PDataSum ((':) @[PLabeledType] y ys) s -> Term s out
f (forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum (forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible @Type a b => a -> b
coerce Term s (PDataRecord y)
x)))
                  forall a b. (a -> b) -> a -> b
$ (PDataSum ys s -> Term s out) -> DataReprHandlers out ys s
prev (\(PDataSum NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  ys
x) -> PDataSum ((':) @[PLabeledType] y ys) s -> Term s out
f (forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum (forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  ys
x)))
            )

instance PIsData (PDataSum defs) where
  pfromDataImpl :: forall (s :: S).
Term s (PAsData (PDataSum defs)) -> Term s (PDataSum defs)
pfromDataImpl = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce
  pdataImpl :: forall (s :: S). Term s (PDataSum defs) -> Term s PData
pdataImpl = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

instance PEq (PDataSum defs) where
  Term s (PDataSum defs)
x #== :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#== Term s (PDataSum defs)
y = forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
x forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
y

instance All (Compose POrd PDataRecord) defs => PPartialOrd (PDataSum defs) where
  Term s (PDataSum defs)
x' #< :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#< Term s (PDataSum defs)
y' = forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
x' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
y'
    where
      f :: Term s (PDataSum defs :--> PDataSum defs :--> PBool)
      f :: forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f = 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 (PDataSum defs)
x Term s (PDataSum defs)
y -> forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PDataSum defs)
-> Term s (PDataSum defs)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> Term s PBool
pmatchLT Term s (PDataSum defs)
x Term s (PDataSum defs)
y forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTHandler
  Term s (PDataSum defs)
x' #<= :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#<= Term s (PDataSum defs)
y' = forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
x' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
y'
    where
      f :: Term s (PDataSum defs :--> PDataSum defs :--> PBool)
      f :: forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f = 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 (PDataSum defs)
x Term s (PDataSum defs)
y -> forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PDataSum defs)
-> Term s (PDataSum defs)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> Term s PBool
pmatchLT Term s (PDataSum defs)
x Term s (PDataSum defs)
y forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTEHandler

instance All (Compose POrd PDataRecord) defs => POrd (PDataSum defs)

-- | If there is only a single variant, then we can safely extract it.
punDataSum :: Term s (PDataSum '[def] :--> PDataRecord def)
punDataSum :: forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum = 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 (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
t ->
    (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
t) :: Term _ (PDataRecord def))

-- | Try getting the nth variant. Errs if it's another variant.
ptryIndexDataSum :: (KnownNat n) => Proxy n -> Term s (PDataSum (def : defs) :--> PDataRecord (IndexList n (def : defs)))
ptryIndexDataSum :: forall (n :: Nat) (s :: S) (def :: [PLabeledType])
       (defs :: [[PLabeledType]]).
KnownNat n =>
Proxy @Nat n
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
ptryIndexDataSum Proxy @Nat n
n = 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 (PDataSum ((':) @[PLabeledType] def defs))
t ->
    forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum ((':) @[PLabeledType] def defs))
t) forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
d ->
      let Term s PInteger
i :: Term _ PInteger = forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d
       in forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s PInteger
i forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n))
            (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d :: Term _ (PDataRecord _))
            forall (s :: S) (a :: PType). Term s a
perror

-- | Safely index a 'PDataRecord'.
pindexDataRecord :: (KnownNat n) => Proxy n -> Term s (PDataRecord as) -> Term s (PAsData (PUnLabel (IndexList n as)))
pindexDataRecord :: forall (n :: Nat) (s :: S) (as :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord as)
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
pindexDataRecord Proxy @Nat n
n Term s (PDataRecord as)
xs =
  forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$
    forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Nat -> Term s (list a) -> Term s a
ptryIndex @PBuiltinList @PData (forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n) (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PDataRecord as)
xs)

-- | Safely drop the first n items of a 'PDataRecord'.
pdropDataRecord :: (KnownNat n) => Proxy n -> Term s (PDataRecord xs) -> Term s (PDataRecord (Drop n xs))
pdropDataRecord :: forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord Proxy @Nat n
n Term s (PDataRecord xs)
xs =
  forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$
    forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Nat -> Term s (list a) -> Term s (list a)
pdrop @PBuiltinList @PData (forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n) (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PDataRecord xs)
xs)

data PlutusTypeData

class
  ( IsPDataSum (PCode a)
  , SListI (IsPDataSumDefs (PCode a))
  , PGeneric a
  ) =>
  PlutusTypeDataConstraint a
instance
  ( IsPDataSum (PCode a)
  , SListI (IsPDataSumDefs (PCode a))
  , PGeneric a
  ) =>
  PlutusTypeDataConstraint a

instance PlutusTypeStrat PlutusTypeData where
  type PlutusTypeStratConstraint PlutusTypeData = PlutusTypeDataConstraint
  type DerivedPInner PlutusTypeData a = PDataSum (IsPDataSumDefs (PCode a))
  derivedPCon :: forall (a :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeData :: Type)) =>
a s -> Term s (DerivedPInner PlutusTypeData a)
derivedPCon a s
x = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
SOP @PType (Term s) a -> PDataSum (IsPDataSumDefs a) s
toSum forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom a s
x
  derivedPMatch :: forall (a :: PType) (s :: S) (b :: PType).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeData :: Type)) =>
Term s (DerivedPInner PlutusTypeData a)
-> (a s -> Term s b) -> Term s b
derivedPMatch Term s (DerivedPInner PlutusTypeData a)
x 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 (DerivedPInner PlutusTypeData a)
x (a s -> Term s b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PGeneric a =>
SOP @PType (Term s) (PCode a) -> a s
gpto forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
PDataSum (IsPDataSumDefs a) s -> SOP @PType (Term s) a
fromSum)

newtype DualReprHandler s out def = DualRepr (Term s (PDataRecord def) -> Term s (PDataRecord def) -> Term s out)

-- | Optimized dual pmatch specialized for lexicographic '#<' and '#<=' implementations.
pmatchLT :: Term s (PDataSum defs) -> Term s (PDataSum defs) -> NP (DualReprHandler s PBool) defs -> Term s PBool
pmatchLT :: forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PDataSum defs)
-> Term s (PDataSum defs)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> Term s PBool
pmatchLT Term s (PDataSum defs)
d1 Term s (PDataSum defs)
d2 (DualRepr Term s (PDataRecord x) -> Term s (PDataRecord x) -> Term s PBool
handler :* NP @[PLabeledType] (DualReprHandler s PBool) xs
Nil) = Term s (PDataRecord x) -> Term s (PDataRecord x) -> Term s PBool
handler (forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
d1) (forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
d2)
pmatchLT Term s (PDataSum defs)
d1 Term s (PDataSum defs)
d2 NP @[PLabeledType] (DualReprHandler s PBool) defs
handlers = forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
  Term s (PBuiltinPair PInteger (PBuiltinList PData))
a <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
d1
  Term s (PBuiltinPair PInteger (PBuiltinList PData))
b <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
d2

  Term s PInteger
cid1 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
a
  Term s PInteger
cid2 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
b

  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
    forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
cid1 forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
cid2)
      -- Left arg's constructor id is less, no need to continue.
      (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True)
    forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
cid1 forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
cid2)
      -- Matching constructors, compare fields now.
      ( forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
          Term s (PBuiltinList PData)
flds1 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
a
          Term s (PBuiltinList PData)
flds2 <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
b
          let handlers' :: [Term s PBool]
handlers' = forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
applyHandlers Term s (PBuiltinList PData)
flds1 Term s (PBuiltinList PData)
flds2 NP @[PLabeledType] (DualReprHandler s PBool) defs
handlers
          (Dig, Term s PBool)
common <- forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s (Dig, Term s out)
findCommon [Term s PBool]
handlers'
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s :: S) (out :: PType).
(Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
reprHandlersGo (Dig, Term s PBool)
common Integer
0 (forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
applyHandlers Term s (PBuiltinList PData)
flds1 Term s (PBuiltinList PData)
flds2 NP @[PLabeledType] (DualReprHandler s PBool) defs
handlers) Term s PInteger
cid1
      )
    -- Left arg's constructor id is greater, no need to continue.
    forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False
  where
    applyHandlers ::
      Term s (PBuiltinList PData) ->
      Term s (PBuiltinList PData) ->
      NP (DualReprHandler s PBool) defs ->
      [Term s PBool]
    applyHandlers :: forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
applyHandlers Term s (PBuiltinList PData)
_ Term s (PBuiltinList PData)
_ NP @[PLabeledType] (DualReprHandler s PBool) defs
Nil = []
    applyHandlers Term s (PBuiltinList PData)
args1 Term s (PBuiltinList PData)
args2 (DualRepr Term s (PDataRecord x) -> Term s (PDataRecord x) -> Term s PBool
handler :* NP @[PLabeledType] (DualReprHandler s PBool) xs
rest) =
      Term s (PDataRecord x) -> Term s (PDataRecord x) -> Term s PBool
handler (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args1) (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args2)
        forall a. a -> [a] -> [a]
: forall (s :: S) (defs :: [[PLabeledType]]).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
applyHandlers Term s (PBuiltinList PData)
args1 Term s (PBuiltinList PData)
args2 NP @[PLabeledType] (DualReprHandler s PBool) xs
rest

reprHandlersGo ::
  (Dig, Term s out) ->
  Integer ->
  [Term s out] ->
  Term s PInteger ->
  Term s out
reprHandlersGo :: forall (s :: S) (out :: PType).
(Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
reprHandlersGo (Dig, Term s out)
common Integer
_ [] Term s PInteger
_ = forall a b. (a, b) -> b
snd (Dig, Term s out)
common
reprHandlersGo (Dig, Term s out)
common Integer
idx (Term s out
handler : [Term s out]
rest) Term s PInteger
c =
  forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s Dig
hashOpenTerm Term s out
handler) forall a b. (a -> b) -> a -> b
$ \Dig
hhash ->
    if Dig
hhash forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (Dig, Term s out)
common
      then forall (s :: S) (out :: PType).
(Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
reprHandlersGo (Dig, Term s out)
common (Integer
idx forall a. Num a => a -> a -> a
+ Integer
1) [Term s out]
rest Term s PInteger
c
      else
        forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (forall a. Num a => Integer -> a
fromInteger Integer
idx forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
c)
          Term s out
handler
          forall a b. (a -> b) -> a -> b
$ forall (s :: S) (out :: PType).
(Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
reprHandlersGo (Dig, Term s out)
common (Integer
idx forall a. Num a => a -> a -> a
+ Integer
1) [Term s out]
rest Term s PInteger
c

hashHandlers :: [Term s out] -> TermCont s [(Dig, Term s out)]
hashHandlers :: forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s [(Dig, Term s out)]
hashHandlers [] = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
hashHandlers (Term s out
handler : [Term s out]
rest) = do
  Dig
hash <- forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s Dig
hashOpenTerm Term s out
handler
  [(Dig, Term s out)]
hashes <- forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s [(Dig, Term s out)]
hashHandlers [Term s out]
rest
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Dig
hash, Term s out
handler) forall a. a -> [a] -> [a]
: [(Dig, Term s out)]
hashes

findCommon :: [Term s out] -> TermCont s (Dig, Term s out)
findCommon :: forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s (Dig, Term s out)
findCommon [Term s out]
handlers = do
  [(Dig, Term s out)]
l <- forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s [(Dig, Term s out)]
hashHandlers [Term s out]
handlers
  forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (\[(Dig, Term s out)]
x [(Dig, Term s out)]
y -> forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Dig, Term s out)]
x forall a. Ord a => a -> a -> Ordering
`compare` forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Dig, Term s out)]
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Dig, Term s out)
x (Dig, Term s out)
y -> forall a b. (a, b) -> a
fst (Dig, Term s out)
x forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (Dig, Term s out)
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(Dig, Term s out)]
l

mkLTHandler :: forall def s. All (Compose POrd PDataRecord) def => NP (DualReprHandler s PBool) def
mkLTHandler :: forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTHandler = forall {k} (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> Type) (s :: [k] -> Type)
       (f :: k -> Type) (xs :: [k]).
All @k c xs =>
proxy c
-> (forall (y :: k) (ys :: [k]).
    c y =>
    s ((':) @k y ys) -> (f y, s ys))
-> s xs
-> NP @k f xs
cana_NP (forall {k} (t :: k). Proxy @k t
Proxy @(Compose POrd PDataRecord)) forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
Compose @PType @[PLabeledType] POrd PDataRecord y =>
Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
rer forall a b. (a -> b) -> a -> b
$ forall {k} a (b :: k). a -> Const @k a b
Const ()
  where
    rer ::
      forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
      Compose POrd PDataRecord y =>
      Const () (y : ys) ->
      (DualReprHandler s PBool y, Const () ys)
    rer :: forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
Compose @PType @[PLabeledType] POrd PDataRecord y =>
Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
rer Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
_ = (forall (s :: S) (out :: PType) (def :: [PLabeledType]).
(Term s (PDataRecord def)
 -> Term s (PDataRecord def) -> Term s out)
-> DualReprHandler s out def
DualRepr forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
(#<), forall {k} a (b :: k). a -> Const @k a b
Const ())

mkLTEHandler :: forall def s. All (Compose POrd PDataRecord) def => NP (DualReprHandler s PBool) def
mkLTEHandler :: forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTEHandler = forall {k} (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> Type) (s :: [k] -> Type)
       (f :: k -> Type) (xs :: [k]).
All @k c xs =>
proxy c
-> (forall (y :: k) (ys :: [k]).
    c y =>
    s ((':) @k y ys) -> (f y, s ys))
-> s xs
-> NP @k f xs
cana_NP (forall {k} (t :: k). Proxy @k t
Proxy @(Compose POrd PDataRecord)) forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
Compose @PType @[PLabeledType] POrd PDataRecord y =>
Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
rer forall a b. (a -> b) -> a -> b
$ forall {k} a (b :: k). a -> Const @k a b
Const ()
  where
    rer ::
      forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
      Compose POrd PDataRecord y =>
      Const () (y : ys) ->
      (DualReprHandler s PBool y, Const () ys)
    rer :: forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
Compose @PType @[PLabeledType] POrd PDataRecord y =>
Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
rer Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
_ = (forall (s :: S) (out :: PType) (def :: [PLabeledType]).
(Term s (PDataRecord def)
 -> Term s (PDataRecord def) -> Term s out)
-> DualReprHandler s out def
DualRepr forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
(#<=), forall {k} a (b :: k). a -> Const @k a b
Const ())

{- | Type synonym to simplify deriving of @PConstant@ via @DerivePConstantViaData@.

A type @Foo a@ is considered "ConstantableData" if:

- The wrapped type @a@ has a @PConstant@ instance.
- The lifted type of @a@ has a @PUnsafeLiftDecl@ instance.
- There is type equality between @a@ and @PLifted (PConstanted a)@.
- The newtype has @FromData@ and @ToData@ instances

These constraints are sufficient to derive a @PConstant@ instance for the newtype.

For deriving @PConstant@ for a wrapped type represented in UPLC as @Data@, see
@DerivePConstantViaData@.

Polymorphic types can be derived as follows:

>data Bar a = Bar a deriving stock (GHC.Generic)
>
>PlutusTx.makeLift ''Bar
>PlutusTx.makeIsDataIndexed ''Bar [('Bar, 0)]
>
>data PBar (a :: PType) (s :: S)
>  = PBar (Term s (PDataRecord '["_0" ':= a]))
>  deriving stock (GHC.Generic)
>  deriving anyclass (SOP.Generic, PIsDataRepr)
>  deriving (PlutusType, PIsData, PDataFields) via PIsDataReprInstances (PBar a)
>
>instance
>  forall a.
>  PLiftData a =>
>  PUnsafeLiftDecl (PBar a)
>  where
>  type PLifted (PBar a) = Bar (PLifted a)
>
>deriving via
>  ( DerivePConstantViaData
>      (Bar a)
>      (PBar (PConstanted a))
>  )
>  instance
>    PConstantData a =>
>    PConstantDecl (Bar a)
-}
type PConstantData :: Type -> Constraint
type PConstantData h =
  ( PConstant h
  , Ledger.FromData h
  , Ledger.ToData h
  , PIsData (PConstanted h)
  )

type PLiftData :: PType -> Constraint
type PLiftData p =
  ( PLift p
  , Ledger.FromData (PLifted p)
  , Ledger.ToData (PLifted p)
  , PIsData p
  )

{- |

For deriving @PConstant@ for a wrapped type represented by a builtin type, see
@DerivePConstantViaNewtype@.
-}
newtype
  DerivePConstantViaData
    (h :: Type)
    (p :: PType) -- The Plutarch synonym to the Haskell type
  = -- | The Haskell type for which @PConstant is being derived.
    DerivePConstantViaData h

instance
  ( PSubtype PData p
  , PLift p
  , Ledger.FromData h
  , Ledger.ToData h
  ) =>
  PConstantDecl (DerivePConstantViaData h p)
  where
  type PConstantRepr (DerivePConstantViaData h p) = Ledger.Data
  type PConstanted (DerivePConstantViaData h p) = p
  pconstantToRepr :: DerivePConstantViaData h p
-> PConstantRepr (DerivePConstantViaData h p)
pconstantToRepr (DerivePConstantViaData h
x) = forall a. ToData a => a -> Data
Ledger.toData h
x
  pconstantFromRepr :: PConstantRepr (DerivePConstantViaData h p)
-> Maybe (DerivePConstantViaData h p)
pconstantFromRepr PConstantRepr (DerivePConstantViaData h p)
x = forall h (p :: PType). h -> DerivePConstantViaData h p
DerivePConstantViaData forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. FromData a => Data -> Maybe a
Ledger.fromData PConstantRepr (DerivePConstantViaData h p)
x

----------------------- HRecP and friends -----------------------------------------------

type HRecPApply :: [(Symbol, PType)] -> S -> [(Symbol, Type)]
type family HRecPApply as s where
  HRecPApply ('(name, ty) ': rest) s = '(name, Reduce (ty s)) ': HRecPApply rest s
  HRecPApply '[] _ = '[]

newtype HRecP (as :: [(Symbol, PType)]) (s :: S) = HRecP (NoReduce (HRecGeneric (HRecPApply as s)))
  deriving stock (forall (as :: [(Symbol, PType)]) (s :: S) x.
Rep (HRecP as s) x -> HRecP as s
forall (as :: [(Symbol, PType)]) (s :: S) x.
HRecP as s -> Rep (HRecP as s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (as :: [(Symbol, PType)]) (s :: S) x.
Rep (HRecP as s) x -> HRecP as s
$cfrom :: forall (as :: [(Symbol, PType)]) (s :: S) x.
HRecP as s -> Rep (HRecP as s) x
Generic)

newtype Flip f a b = Flip (f b a)
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
Generic)

class Helper2 (b :: PSubtypeRelation) a where
  type Helper2Excess b a :: PType
  ptryFromData' :: forall s r. Proxy b -> Term s PData -> ((Term s (PAsData a), Reduce (Helper2Excess b a s)) -> Term s r) -> Term s r

instance PTryFrom PData (PAsData a) => Helper2 'PNoSubtypeRelation a where
  type Helper2Excess 'PNoSubtypeRelation a = PTryFromExcess PData (PAsData a)
  ptryFromData' :: forall (s :: S) (r :: PType).
Proxy @PSubtypeRelation 'PNoSubtypeRelation
-> Term s PData
-> ((Term s (PAsData a),
     Reduce (Helper2Excess 'PNoSubtypeRelation a s))
    -> Term s r)
-> Term s r
ptryFromData' Proxy @PSubtypeRelation 'PNoSubtypeRelation
_ = forall (a :: PType) (b :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom'

instance PTryFrom PData a => Helper2 'PSubtypeRelation a where
  type Helper2Excess 'PSubtypeRelation a = PTryFromExcess PData a
  ptryFromData' :: forall (s :: S) (r :: PType).
Proxy @PSubtypeRelation 'PSubtypeRelation
-> Term s PData
-> ((Term s (PAsData a),
     Reduce (Helper2Excess 'PSubtypeRelation a s))
    -> Term s r)
-> Term s r
ptryFromData' Proxy @PSubtypeRelation 'PSubtypeRelation
_ Term s PData
x = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    (Term s a
y, GReduce (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s))
exc) <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @a @PData Term s PData
x
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s a
y, GReduce (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s))
exc)

-- We could have a more advanced instance but it's not needed really.
newtype ExcessForField (b :: PSubtypeRelation) (a :: PType) (s :: S) = ExcessForField (Term s (PAsData a), Reduce (Helper2Excess b a s))
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (b :: PSubtypeRelation) (a :: PType) (s :: S) x.
Rep (ExcessForField b a s) x -> ExcessForField b a s
forall (b :: PSubtypeRelation) (a :: PType) (s :: S) x.
ExcessForField b a s -> Rep (ExcessForField b a s) x
$cto :: forall (b :: PSubtypeRelation) (a :: PType) (s :: S) x.
Rep (ExcessForField b a s) x -> ExcessForField b a s
$cfrom :: forall (b :: PSubtypeRelation) (a :: PType) (s :: S) x.
ExcessForField b a s -> Rep (ExcessForField b a s) x
Generic)

instance PTryFrom (PBuiltinList PData) (PDataRecord '[]) where
  type PTryFromExcess (PBuiltinList PData) (PDataRecord '[]) = HRecP '[]
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s (PBuiltinList PData)
-> ((Term s (PDataRecord ('[] @PLabeledType)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s (PBuiltinList PData)
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PUnit @S)
_ <-
      forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce forall a b. (a -> b) -> a -> b
$
        forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
opq forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall {k} (s :: k). PUnit @k s
PUnit) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (forall (s :: S) (a :: PType). Term s PString -> Term s a
ptraceError Term s PString
"ptryFrom(PDataRecord[]): list is longer than zero")
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil, forall (as :: [(Symbol, Type)]). HRec as -> HRecGeneric as
HRecGeneric HRec ('[] @(Symbol, Type))
HNil)

type family UnHRecP (x :: PType) :: [(Symbol, PType)] where
  UnHRecP (HRecP as) = as

instance
  ( Helper2 (PSubtype' PData pty) pty
  , PTryFrom (PBuiltinList PData) (PDataRecord as)
  , PTryFromExcess (PBuiltinList PData) (PDataRecord as) ~ HRecP ase
  ) =>
  PTryFrom (PBuiltinList PData) (PDataRecord ((name ':= pty) ': as))
  where
  type
    PTryFromExcess (PBuiltinList PData) (PDataRecord ((name ':= pty) ': as)) =
      HRecP
        ( '(name, ExcessForField (PSubtype' PData pty) pty)
            ': UnHRecP (PTryFromExcess (PBuiltinList PData) (PDataRecord as))
        )
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s (PBuiltinList PData)
-> ((Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData)
          (PDataRecord ((':) @PLabeledType (name ':= pty) as))
          s))
    -> Term s r)
-> Term s r
ptryFrom' Term s (PBuiltinList PData)
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s PData
h <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
opq
    (Term s (PAsData pty),
 GReduce
   (Helper2Excess (PSubtype' PData pty) pty s)
   (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
hv <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PSubtypeRelation) (a :: PType) (s :: S) (r :: PType).
Helper2 b a =>
Proxy @PSubtypeRelation b
-> Term s PData
-> ((Term s (PAsData a), Reduce (Helper2Excess b a s)) -> Term s r)
-> Term s r
ptryFromData' (forall {k} (t :: k). Proxy @k t
Proxy @(PSubtype' PData pty)) Term s PData
h
    Term s (PBuiltinList PData)
t <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
opq
    (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
tv <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PDataRecord as) @(PBuiltinList PData) Term s (PBuiltinList PData)
t
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
opq, forall (as :: [(Symbol, Type)]). HRec as -> HRecGeneric as
HRecGeneric (forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons (forall {k} (sym :: k) a. a -> Labeled @k sym a
Labeled (Term s (PAsData pty),
 GReduce
   (Helper2Excess (PSubtype' PData pty) pty s)
   (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
hv) (coerce :: forall a b. Coercible @Type a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
tv)))

newtype Helper a b s = Helper (Reduce (a s), Reduce (b s)) deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (a :: k -> Type) (b :: k -> Type) (s :: k) x.
Rep (Helper @k a b s) x -> Helper @k a b s
forall k (a :: k -> Type) (b :: k -> Type) (s :: k) x.
Helper @k a b s -> Rep (Helper @k a b s) x
$cto :: forall k (a :: k -> Type) (b :: k -> Type) (s :: k) x.
Rep (Helper @k a b s) x -> Helper @k a b s
$cfrom :: forall k (a :: k -> Type) (b :: k -> Type) (s :: k) x.
Helper @k a b s -> Rep (Helper @k a b s) x
Generic)

instance
  ( PTryFrom (PBuiltinList PData) (PDataRecord as)
  , PTryFromExcess (PBuiltinList PData) (PDataRecord as) ~ HRecP ase
  ) =>
  PTryFrom PData (PAsData (PDataRecord as))
  where
  type
    PTryFromExcess PData (PAsData (PDataRecord as)) =
      Helper (Flip Term (PDataRecord as)) (PTryFromExcess (PBuiltinList PData) (PDataRecord as))
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PDataRecord as)),
     Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList PData)
l <- forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData (PBuiltinList PData)) Term s PData
opq)
    (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
r <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PDataRecord as) Term s (PBuiltinList PData)
l
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
r)

class SumValidation (n :: Nat) (sum :: [[PLabeledType]]) where
  validateSum :: Proxy n -> Proxy sum -> Term s PInteger -> Term s (PBuiltinList PData) -> Term s POpaque

instance
  forall (n :: Nat) (x :: [PLabeledType]) (xs :: [[PLabeledType]]).
  ( PTryFrom (PBuiltinList PData) (PDataRecord x)
  , SumValidation (n + 1) xs
  , KnownNat n
  ) =>
  SumValidation n (x ': xs)
  where
  validateSum :: forall (s :: S).
Proxy @Nat n
-> Proxy @[[PLabeledType]] ((':) @[PLabeledType] x xs)
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum Proxy @Nat n
_ Proxy @[[PLabeledType]] ((':) @[PLabeledType] x xs)
_ Term s PInteger
constr Term s (PBuiltinList PData)
fields =
    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy @k t
Proxy @n) forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
constr)
      ( forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
          (Term s (PDataRecord x),
 GReduce
   (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
   (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)))
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PDataRecord x) Term s (PBuiltinList PData)
fields
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall {k} (s :: k). PUnit @k s
PUnit
      )
      (forall (n :: Nat) (sum :: [[PLabeledType]]) (s :: S).
SumValidation n sum =>
Proxy @Nat n
-> Proxy @[[PLabeledType]] sum
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum (forall {k} (t :: k). Proxy @k t
Proxy @(n + 1)) (forall {k} (t :: k). Proxy @k t
Proxy @xs) Term s PInteger
constr Term s (PBuiltinList PData)
fields)

instance SumValidation n '[] where
  validateSum :: forall (s :: S).
Proxy @Nat n
-> Proxy @[[PLabeledType]] ('[] @[PLabeledType])
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum Proxy @Nat n
_ Proxy @[[PLabeledType]] ('[] @[PLabeledType])
_ Term s PInteger
_ Term s (PBuiltinList PData)
_ = forall (s :: S) (a :: PType). Term s PString -> Term s a
ptraceError Term s PString
"reached end of sum while still not having found the constructor"

instance SumValidation 0 ys => PTryFrom PData (PDataSum ys) where
  type PTryFromExcess _ _ = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PDataSum ys),
     Reduce (PTryFromExcess PData (PDataSum ys) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
x <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    Term s PInteger
constr <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x
    Term s (PBuiltinList PData)
fields <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x
    Term s POpaque
_ <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (sum :: [[PLabeledType]]) (s :: S).
SumValidation n sum =>
Proxy @Nat n
-> Proxy @[[PLabeledType]] sum
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum (forall {k} (t :: k). Proxy @k t
Proxy @0) (forall {k} (t :: k). Proxy @k t
Proxy @ys) Term s PInteger
constr Term s (PBuiltinList PData)
fields
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, ())

instance PTryFrom PData (PDataSum ys) => PTryFrom PData (PAsData (PDataSum ys)) where
  type PTryFromExcess _ _ = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PDataSum ys)),
     Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
x = forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$ do
    (Term s (PDataSum ys)
y, ()
exc) <- forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont forall a b. (a -> b) -> a -> b
$ forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom Term s PData
x
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum ys)
y, ()
exc)

-- | Annotates a shown field with a label.
showWithLabel ::
  forall label t s.
  (KnownSymbol label, PShow t) =>
  Proxy label ->
  Bool ->
  Term s t ->
  Term s PString
showWithLabel :: forall (label :: Symbol) (t :: PType) (s :: S).
(KnownSymbol label, PShow t) =>
Proxy @Symbol label -> Bool -> Term s t -> Term s PString
showWithLabel Proxy @Symbol label
proxy Bool
b Term s t
x = Term s PString
lblStr forall a. Semigroup a => a -> a -> a
<> Term s PString
" = " forall a. Semigroup a => a -> a -> a
<> forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b Term s t
x
  where
    lblStr :: Term s PString
lblStr = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy @Symbol label
proxy