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

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

import Data.Coerce (coerce)
import Data.Functor.Compose qualified as F
import Data.Functor.Const (Const (Const))
import Data.Kind (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.Builtin.Bool (PBool, pif)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PData,
  pasConstr,
  pchooseListBuiltin,
  pconstrBuiltin,
  pfstBuiltin,
  psndBuiltin,
 )
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Builtin.Opaque (POpaque, popaque)
import Plutarch.Builtin.String (PString)
import Plutarch.Builtin.Unit (PUnit (PUnit))
import Plutarch.DataRepr.Internal.HList (
  HRec (HCons, HNil),
  HRecGeneric (HRecGeneric),
  Labeled (Labeled),
  type Drop,
  type IndexList,
 )
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom, gpto)
import Plutarch.Internal.IsData (PIsData, pdata, pdataImpl, pforgetData, pfromData, pfromDataImpl)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.ListLike (PListLike (pnil), pcons, pdrop, phead, ptail, ptryIndex)
import Plutarch.Internal.Newtype (PlutusTypeNewtype)
import Plutarch.Internal.Ord (POrd (pmax, pmin, (#<), (#<=)))
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  DerivedPInner,
  PlutusType (PInner, pcon', pmatch'),
  PlutusTypeStrat,
  PlutusTypeStratConstraint,
  derivedPCon,
  derivedPMatch,
  pcon,
  pmatch,
 )
import Plutarch.Internal.Show (PShow (pshow'))
import Plutarch.Internal.Term (
  Dig,
  Term,
  pdelay,
  perror,
  pforce,
  phoistAcyclic,
  plet,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.Term qualified as P
import Plutarch.Internal.TermCont (
  TermCont,
  hashOpenTerm,
  runTermCont,
  tcont,
  unTermCont,
 )
import Plutarch.Internal.TryFrom (
  PSubtype',
  PSubtypeRelation (PNoSubtypeRelation, PSubtypeRelation),
  PTryFrom,
  PTryFromExcess,
  ptryFrom,
  ptryFrom',
  pupcast,
 )
import Plutarch.Reducible (NoReduce, Reduce)
import Plutarch.Trace (ptraceInfoError)
import Plutarch.Unsafe (punsafeCoerce)

{- | A "record" of `exists a. PAsData a`. The underlying representation is
 `PBuiltinList PData`.
-}
data PDataRecord (as :: [PLabeledType]) (s :: P.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) = Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData x) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData x)
x Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord xs) -> Term s (PInner (PDataRecord xs))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataRecord xs)
xs
  pcon' PDataRecord l s
PDNil = PDataRecord ('[] @PLabeledType) s
-> Term s (PInner (PDataRecord ('[] @PLabeledType)))
forall (s :: S).
PDataRecord ('[] @PLabeledType) s
-> Term s (PInner (PDataRecord ('[] @PLabeledType)))
forall (a :: PType) (s :: S).
PlutusType a =>
a s -> Term s (PInner a)
pcon' PDataRecord ('[] @PLabeledType) s
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' = H s l
-> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r
forall (s :: S) (l :: [PLabeledType]).
H s l
-> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r
unH
    (H s l
 -> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r)
-> H s l
-> forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ H s ('[] @PLabeledType)
-> (forall {y :: PLabeledType} {ys :: [PLabeledType]}.
    All @PLabeledType (Top @PLabeledType) ys =>
    H s ((':) @PLabeledType y ys))
-> H s l
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 (r :: PType).
 (PDataRecord ('[] @PLabeledType) s -> Term s r) -> Term s r)
-> H s ('[] @PLabeledType)
forall (s :: S) (l :: [PLabeledType]).
(forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r)
-> H s l
H ((forall (r :: PType).
  (PDataRecord ('[] @PLabeledType) s -> Term s r) -> Term s r)
 -> H s ('[] @PLabeledType))
-> (forall (r :: PType).
    (PDataRecord ('[] @PLabeledType) s -> Term s r) -> Term s r)
-> H s ('[] @PLabeledType)
forall a b. (a -> b) -> a -> b
$ \PDataRecord ('[] @PLabeledType) s -> Term s r
f -> PDataRecord ('[] @PLabeledType) s -> Term s r
f PDataRecord ('[] @PLabeledType) s
forall (s :: S). PDataRecord ('[] @PLabeledType) s
PDNil)
    ((forall {y :: PLabeledType} {ys :: [PLabeledType]}.
  All @PLabeledType (Top @PLabeledType) ys =>
  H s ((':) @PLabeledType y ys))
 -> H s l)
-> (forall {y :: PLabeledType} {ys :: [PLabeledType]}.
    All @PLabeledType (Top @PLabeledType) ys =>
    H s ((':) @PLabeledType y ys))
-> H s l
forall a b. (a -> b) -> a -> b
$ (forall (r :: PType).
 (PDataRecord ((':) @PLabeledType y ys) s -> Term s r) -> Term s r)
-> H s ((':) @PLabeledType y ys)
forall (s :: S) (l :: [PLabeledType]).
(forall (r :: PType). (PDataRecord l s -> Term s r) -> Term s r)
-> H s l
H
    ((forall (r :: PType).
  (PDataRecord ((':) @PLabeledType y ys) s -> Term s r) -> Term s r)
 -> H s ((':) @PLabeledType y ys))
-> (forall (r :: PType).
    (PDataRecord ((':) @PLabeledType y ys) s -> Term s r) -> Term s r)
-> H s ((':) @PLabeledType y ys)
forall a b. (a -> b) -> a -> b
$ \PDataRecord ((':) @PLabeledType y ys) s -> Term s r
f ->
      Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
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 = Term s PData -> Term s (PAsData x)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s (PAsData x))
-> Term s PData -> Term s (PAsData x)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
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 = Term s (PBuiltinList PData) -> Term s (PDataRecord xs)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData) -> Term s (PDataRecord xs))
-> Term s (PBuiltinList PData) -> Term s (PDataRecord xs)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
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 (PDataRecord ((':) @PLabeledType y ys) s -> Term s r)
-> PDataRecord ((':) @PLabeledType y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PUnLabel y))
-> Term s (PDataRecord ys)
-> PDataRecord ((':) @PLabeledType y ys) s
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 Term s (PAsData (PUnLabel y))
forall (x :: PType). Term s (PAsData x)
x Term s (PDataRecord ys)
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 = Term s (PDataRecord xs) -> Term s (PInner (PDataRecord xs))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s (PDataRecord xs)
x Term s (PInner (PDataRecord xs))
-> Term s (PInner (PDataRecord xs)) -> Term s PBool
forall (s :: S).
Term s (PInner (PDataRecord xs))
-> Term s (PInner (PDataRecord xs)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PDataRecord xs) -> Term s (PInner (PDataRecord xs))
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 POrd (PDataRecord '[]) where
  {-# INLINEABLE (#<=) #-}
  Term s (PDataRecord ('[] @PLabeledType))
_ #<= :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PBool
#<= Term s (PDataRecord ('[] @PLabeledType))
_ = AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  {-# INLINEABLE (#<) #-}
  Term s (PDataRecord ('[] @PLabeledType))
_ #< :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PBool
#< Term s (PDataRecord ('[] @PLabeledType))
_ = AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
  {-# INLINEABLE pmin #-}
  pmin :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
pmin Term s (PDataRecord ('[] @PLabeledType))
t Term s (PDataRecord ('[] @PLabeledType))
_ = Term s (PDataRecord ('[] @PLabeledType))
t
  {-# INLINEABLE pmax #-}
  pmax :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
pmax = Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType))
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s t
pmin

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
"[" Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
-> (PDataRecord ((':) @PLabeledType (label ':= x) xs) s
    -> Term s PString)
-> Term s PString
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 PDataRecord ((':) @PLabeledType (label ':= x) xs) s
-> Term s PString
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) =
        Proxy @Symbol label -> Bool -> Term s (PAsData x) -> Term s PString
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
forall (t :: Symbol). Proxy @Symbol t
Proxy @label) Bool
b Term s (PAsData x)
y
          Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Bool -> Term s (PDataRecordShowHelper xs) -> Term s PString
forall (s :: S).
Bool -> Term s (PDataRecordShowHelper xs) -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs))
-> PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs)
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord xs) -> PDataRecordShowHelper xs s
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 x.
 PDataRecordShowHelper as s -> Rep (PDataRecordShowHelper as s) x)
-> (forall x.
    Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s)
-> Generic (PDataRecordShowHelper as s)
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 x.
Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s
forall 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
$cfrom :: forall (as :: [PLabeledType]) (s :: S) x.
PDataRecordShowHelper as s -> Rep (PDataRecordShowHelper as s) x
from :: forall x.
PDataRecordShowHelper as s -> Rep (PDataRecordShowHelper as s) x
$cto :: forall (as :: [PLabeledType]) (s :: S) x.
Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s
to :: forall x.
Rep (PDataRecordShowHelper as s) x -> PDataRecordShowHelper as s
Generic)
  deriving anyclass ((forall (s :: S).
 PDataRecordShowHelper as s
 -> Term s (PInner (PDataRecordShowHelper as)))
-> (forall (s :: S) (b :: PType).
    Term s (PInner (PDataRecordShowHelper as))
    -> (PDataRecordShowHelper as s -> Term s b) -> Term s b)
-> PlutusType (PDataRecordShowHelper as)
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 (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
forall (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
$cpcon' :: forall (as :: [PLabeledType]) (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
pcon' :: forall (s :: S).
PDataRecordShowHelper as s
-> Term s (PInner (PDataRecordShowHelper as))
$cpmatch' :: forall (as :: [PLabeledType]) (s :: S) (b :: PType).
Term s (PInner (PDataRecordShowHelper as))
-> (PDataRecordShowHelper as s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PDataRecordShowHelper as))
-> (PDataRecordShowHelper as s -> Term s b) -> Term s b
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
", " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term
  s
  (PInner
     (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs)))
-> (PInner
      (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs)) s
    -> Term s PString)
-> Term s PString
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term
  s (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs))
-> Term
     s
     (PInner
        (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs)))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term
  s (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs))
xs) PInner
  (PDataRecordShowHelper ((':) @PLabeledType (label ':= x) xs)) s
-> Term s PString
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) =
        Proxy @Symbol label -> Bool -> Term s (PAsData x) -> Term s PString
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
forall (t :: Symbol). Proxy @Symbol t
Proxy @label) Bool
b Term s (PAsData x)
y
          Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Bool -> Term s (PDataRecordShowHelper xs) -> Term s PString
forall (s :: S).
Bool -> Term s (PDataRecordShowHelper xs) -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs))
-> PDataRecordShowHelper xs s -> Term s (PDataRecordShowHelper xs)
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord xs) -> PDataRecordShowHelper xs s
forall (as :: [PLabeledType]) (s :: S).
Term s (PDataRecord as) -> PDataRecordShowHelper as s
PDataRecordShowHelper Term s (PDataRecord xs)
ys)

instance (POrd x, PIsData x) => POrd (PDataRecord '[label ':= x]) where
  {-# INLINEABLE (#<) #-}
  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 = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
_ <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
    -> Term s PBool)
-> Term s PBool
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)
_ <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
    -> Term s PBool)
-> Term s PBool
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
    Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y
  {-# INLINEABLE (#<=) #-}
  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 = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
_ <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
    -> Term s PBool)
-> Term s PBool
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)
_ <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)) s
    -> Term s PBool)
-> Term s PBool
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
    Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y

instance
  (SListI xs, POrd x, PIsData x, POrd (PDataRecord (x' ': xs))) =>
  POrd (PDataRecord ((label ':= x) ': x' ': xs))
  where
  {-# INLINEABLE (#<) #-}
  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 = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
xs <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
    -> Term s PBool)
-> Term s PBool
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 <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
    -> Term s PBool)
-> Term s PBool
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 <- ((Term s x -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s x)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s x -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s x))
-> (Term s x -> (Term s x -> Term s PBool) -> Term s PBool)
-> Term s x
-> TermCont @PBool s (Term s x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s x -> (Term s x -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s x -> TermCont @PBool s (Term s x))
-> Term s x -> TermCont @PBool s (Term s x)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x
    Term s x
b <- ((Term s x -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s x)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s x -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s x))
-> (Term s x -> (Term s x -> Term s PBool) -> Term s PBool)
-> Term s x
-> TermCont @PBool s (Term s x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s x -> (Term s x -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s x -> TermCont @PBool s (Term s x))
-> Term s x -> TermCont @PBool s (Term s x)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y
    Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s x
Term s x
b) (AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True) (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s x
Term s x
b) (Term s (PDataRecord xs)
xs Term s (PDataRecord xs) -> Term s (PDataRecord xs) -> Term s PBool
forall (s :: S).
Term s (PDataRecord xs) -> Term s (PDataRecord xs) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PDataRecord xs)
Term s (PDataRecord xs)
ys) (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
  {-# INLINEABLE (#<=) #-}
  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 = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    PDCons Term s (PAsData x)
x Term s (PDataRecord xs)
xs <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
    -> Term s PBool)
-> Term s PBool
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 <- ((PDataRecord
    ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (PDataRecord
         ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s))
-> ((PDataRecord
       ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> (PDataRecord
      ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)) s
    -> Term s PBool)
-> Term s PBool
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 <- ((Term s x -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s x)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s x -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s x))
-> (Term s x -> (Term s x -> Term s PBool) -> Term s PBool)
-> Term s x
-> TermCont @PBool s (Term s x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s x -> (Term s x -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s x -> TermCont @PBool s (Term s x))
-> Term s x -> TermCont @PBool s (Term s x)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
x
    Term s x
b <- ((Term s x -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s x)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s x -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s x))
-> (Term s x -> (Term s x -> Term s PBool) -> Term s PBool)
-> Term s x
-> TermCont @PBool s (Term s x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s x -> (Term s x -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s x -> TermCont @PBool s (Term s x))
-> Term s x -> TermCont @PBool s (Term s x)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData x) -> Term s x
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData x)
y
    Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s x
Term s x
b) (AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True) (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s x
a Term s x -> Term s x -> Term s PBool
forall (s :: S). Term s x -> Term s x -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s x
Term s x
b) (Term s (PDataRecord xs)
xs Term s (PDataRecord xs) -> Term s (PDataRecord xs) -> Term s PBool
forall (s :: S).
Term s (PDataRecord xs) -> Term s (PDataRecord xs) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PDataRecord xs)
Term s (PDataRecord xs)
ys) (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False

{- | 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 = Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term
     s
     (PAsData a
      :--> (PDataRecord l
            :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
 -> Term
      s
      (PAsData a
       :--> (PDataRecord l
             :--> PDataRecord ((':) @PLabeledType (label ':= a) l))))
-> Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term
     s
     (PAsData a
      :--> (PDataRecord l
            :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
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 = Term s (PBuiltinList PData)
-> Term s (PDataRecord ('[] @PLabeledType))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData)
 -> Term s (PDataRecord ('[] @PLabeledType)))
-> Term s (PBuiltinList PData)
-> Term s (PDataRecord ('[] @PLabeledType))
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 := (P.S -> Type)

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

type PLookupLabel :: Symbol -> [PLabeledType] -> P.S -> Type
type family PLookupLabel name as where
  PLookupLabel name ((name ':= a) ': _) = a
  PLookupLabel name (_ ': as) = PLookupLabel name as

type family PUnLabel (a :: PLabeledType) :: P.S -> Type 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 = Term s (PBuiltinList PData) -> Term s (PDataRecord xs)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PAsData (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PDataRecord xs))
-> Term s (PAsData (PBuiltinList PData))
forall (b :: PType) (a :: PType) (s :: S). 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 = Term s (PAsData (PBuiltinList PData)) -> Term s PData
forall (a :: PType) (b :: PType) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast (Term s (PAsData (PBuiltinList PData)) -> Term s PData)
-> Term s (PAsData (PBuiltinList PData)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinList PData))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s (PDataRecord xs) -> Term s (PBuiltinList 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]] -> P.S -> Type
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 = Term s (PDataSum defs)
-> (PDataSum defs s -> Term s PString) -> Term s PString
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 PDataSum defs s -> Term s PString
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)) = Bool -> Term s (PDataRecord x) -> Term s PString
forall (s :: S). Bool -> Term s (PDataRecord x) -> Term s PString
forall (t :: PType) (s :: S).
PShow t =>
Bool -> Term s t -> Term s PString
pshow' Bool
b (Compose @PType @[PLabeledType] (Term s) PDataRecord x
-> Term s (PDataRecord x)
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)) = PDataSum xs s -> Term s PString
forall (xs :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] PShow PDataRecord)
  xs =>
PDataSum xs s -> Term s PString
showSum (NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
-> PDataSum xs s
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 :: [[P.S -> Type]]) 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))) = NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> PDataSum
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
     s
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)
   (IsPDataSumDefs
      ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
 -> PDataSum
      (IsPDataSumDefs
         ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
      s)
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> PDataSum
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
     s
forall a b. (a -> b) -> a -> b
$ Compose @PType @[PLabeledType] (Term s) PDataRecord l
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] l (IsPDataSumDefs xs))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (Compose @PType @[PLabeledType] (Term s) PDataRecord l
 -> NS
      @[PLabeledType]
      (Compose @PType @[PLabeledType] (Term s) PDataRecord)
      ((':) @[PLabeledType] l (IsPDataSumDefs xs)))
-> Compose @PType @[PLabeledType] (Term s) PDataRecord l
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] l (IsPDataSumDefs xs))
forall a b. (a -> b) -> a -> b
$ Term s x -> Compose @PType @[PLabeledType] (Term s) PDataRecord l
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 SOP @PType (Term s) xs -> PDataSum (IsPDataSumDefs xs) s
forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
SOP @PType (Term s) a -> PDataSum (IsPDataSumDefs a) s
forall (s :: S).
SOP @PType (Term s) xs -> PDataSum (IsPDataSumDefs xs) s
toSum (NS @[PType] (NP @PType (Term s)) xs -> SOP @PType (Term s) xs
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 -> NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> PDataSum
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
     s
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)
   (IsPDataSumDefs
      ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
 -> PDataSum
      (IsPDataSumDefs
         ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
      s)
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> PDataSum
     (IsPDataSumDefs
        ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
     s
forall a b. (a -> b) -> a -> b
$ NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  (IsPDataSumDefs xs)
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] l (IsPDataSumDefs xs))
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)) = NS
  @[PType]
  (NP @PType (Term s))
  ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
-> SOP
     @PType
     (Term s)
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[PType]
   (NP @PType (Term s))
   ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
 -> SOP
      @PType
      (Term s)
      ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
-> SOP
     @PType
     (Term s)
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall a b. (a -> b) -> a -> b
$ NP @PType (Term s) ((':) @PType (PDataRecord l) ('[] @PType))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (NP @PType (Term s) ((':) @PType (PDataRecord l) ('[] @PType))
 -> NS
      @[PType]
      (NP @PType (Term s))
      ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> NP @PType (Term s) ((':) @PType (PDataRecord l) ('[] @PType))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall a b. (a -> b) -> a -> b
$ Compose @PType @[PLabeledType] (Term s) PDataRecord x
-> Term s (PDataRecord l)
forall a b. Coercible @Type a b => a -> b
coerce Compose @PType @[PLabeledType] (Term s) PDataRecord x
x Term s (PDataRecord l)
-> NP @PType (Term s) ('[] @PType)
-> NP @PType (Term s) ((':) @PType (PDataRecord l) ('[] @PType))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @PType (Term s) ('[] @PType)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil
  fromSum (PDataSum (S NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
x)) = case PDataSum (IsPDataSumDefs xs) s -> SOP @PType (Term s) xs
forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
PDataSum (IsPDataSumDefs a) s -> SOP @PType (Term s) a
forall (s :: S).
PDataSum (IsPDataSumDefs xs) s -> SOP @PType (Term s) xs
fromSum (NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  xs
-> PDataSum xs s
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 -> NS
  @[PType]
  (NP @PType (Term s))
  ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
-> SOP
     @PType
     (Term s)
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[PType]
   (NP @PType (Term s))
   ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
 -> SOP
      @PType
      (Term s)
      ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs))
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
-> SOP
     @PType
     (Term s)
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
forall a b. (a -> b) -> a -> b
$ NS @[PType] (NP @PType (Term s)) xs
-> NS
     @[PType]
     (NP @PType (Term s))
     ((':) @[PType] ((':) @PType (PDataRecord l) ('[] @PType)) xs)
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 :: P.S -> Type) (defs :: [[PLabeledType]]) (s :: P.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 = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> Int
forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
forall (f :: [PLabeledType] -> Type) (xs :: [[PLabeledType]]).
NS @[PLabeledType] 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 = NS
  @[PLabeledType]
  (K @[PLabeledType] (Term s (PBuiltinList PData)))
  defs
-> CollapseTo
     @[PLabeledType]
     @[[PLabeledType]]
     (NS @[PLabeledType])
     (Term s (PBuiltinList PData))
forall (xs :: [[PLabeledType]]) a.
SListIN
  @[PLabeledType] @[[PLabeledType]] (NS @[PLabeledType]) xs =>
NS @[PLabeledType] (K @[PLabeledType] a) xs
-> CollapseTo
     @[PLabeledType] @[[PLabeledType]] (NS @[PLabeledType]) a
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 (NS
   @[PLabeledType]
   (K @[PLabeledType] (Term s (PBuiltinList PData)))
   defs
 -> CollapseTo
      @[PLabeledType]
      @[[PLabeledType]]
      (NS @[PLabeledType])
      (Term s (PBuiltinList PData)))
-> NS
     @[PLabeledType]
     (K @[PLabeledType] (Term s (PBuiltinList PData)))
     defs
-> CollapseTo
     @[PLabeledType]
     @[[PLabeledType]]
     (NS @[PLabeledType])
     (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ (forall (a :: [PLabeledType]).
 Compose @PType @[PLabeledType] (Term s) PDataRecord a
 -> K @[PLabeledType] (Term s (PBuiltinList PData)) a)
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     defs
-> NS
     @[PLabeledType]
     (K @[PLabeledType] (Term s (PBuiltinList PData)))
     defs
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 (Term s (PInner (PDataRecord a))
-> K @[PLabeledType] (Term s (PInner (PDataRecord a))) a
forall k a (b :: k). a -> K @k a b
K (Term s (PInner (PDataRecord a))
 -> K @[PLabeledType] (Term s (PInner (PDataRecord a))) a)
-> (Compose @PType @[PLabeledType] (Term s) PDataRecord a
    -> Term s (PInner (PDataRecord a)))
-> Compose @PType @[PLabeledType] (Term s) PDataRecord a
-> K @[PLabeledType] (Term s (PInner (PDataRecord a))) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDataRecord a) -> Term s (PInner (PDataRecord a))
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s (PDataRecord a) -> Term s (PInner (PDataRecord a)))
-> (Compose @PType @[PLabeledType] (Term s) PDataRecord a
    -> Term s (PDataRecord a))
-> Compose @PType @[PLabeledType] (Term s) PDataRecord a
-> Term s (PInner (PDataRecord a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose @PType @[PLabeledType] (Term s) PDataRecord a
-> Term s (PDataRecord a)
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 Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
 -> Term s PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s PInteger
-> Term
     s
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Integer
AsHaskell PInteger
constrIx Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
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 = (PDataSum defs s -> Term s b) -> DataReprHandlers b defs s
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 (Term s (PDataRecord def) -> Term s b)
-> Term s (PDataRecord def) -> Term s b
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
-> Term
     s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
-> Term s (PDataRecord def)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PInner (PDataSum defs)) -> Term s (PDataSum defs)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataSum defs))
d :: Term _ (PDataSum defs))
          DataReprHandlers b defs s
_ -> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s b)
-> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s PData
Term s (PInner (PDataSum defs))
d) ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s b)
 -> Term s b)
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s b)
-> Term s b
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
d' ->
            Term s PInteger -> (Term s PInteger -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d') ((Term s PInteger -> Term s b) -> Term s b)
-> (Term s PInteger -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
constr ->
              Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d') ((Term s (PBuiltinList PData) -> Term s b) -> Term s b)
-> (Term s (PBuiltinList PData) -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList PData)
args ->
                let handlers' :: [Term s b]
handlers' = Term s (PBuiltinList PData)
-> DataReprHandlers b defs s -> [Term s b]
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 TermCont @b s (Dig, Term s b)
-> ((Dig, Term s b) -> Term s b) -> Term s b
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont ([Term s b] -> TermCont @b s (Dig, Term s b)
forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s (Dig, Term s out)
findCommon [Term s b]
handlers') (((Dig, Term s b) -> Term s b) -> Term s b)
-> ((Dig, Term s b) -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(Dig, Term s b)
common ->
                      (Dig, Term s b)
-> Integer -> [Term s b] -> Term s PInteger -> Term s b
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 (Term s (PBuiltinList PData) -> Term s (PDataRecord def)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args) Term s out -> [Term s out] -> [Term s out]
forall a. a -> [a] -> [a]
: Term s (PBuiltinList PData)
-> DataReprHandlers out defs s -> [Term s out]
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 =
        A s out defs
-> (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
A s out defs
-> (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s
unA (A s out defs
 -> (PDataSum defs s -> Term s out) -> DataReprHandlers out defs s)
-> A s out defs
-> (PDataSum defs s -> Term s out)
-> DataReprHandlers out defs s
forall a b. (a -> b) -> a -> b
$
          A s out ('[] @[PLabeledType])
-> (forall (y :: [PLabeledType]) (ys :: [[PLabeledType]]).
    SListI @[PLabeledType] ys =>
    A s out ys -> A s out ((':) @[PLabeledType] y ys))
-> A s out defs
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
            (((PDataSum ('[] @[PLabeledType]) s -> Term s out)
 -> DataReprHandlers out ('[] @[PLabeledType]) s)
-> A s out ('[] @[PLabeledType])
forall (s :: S) (out :: PType) (defs :: [[PLabeledType]]).
((PDataSum defs s -> Term s out) -> DataReprHandlers out defs s)
-> A s out defs
A (((PDataSum ('[] @[PLabeledType]) s -> Term s out)
  -> DataReprHandlers out ('[] @[PLabeledType]) s)
 -> A s out ('[] @[PLabeledType]))
-> ((PDataSum ('[] @[PLabeledType]) s -> Term s out)
    -> DataReprHandlers out ('[] @[PLabeledType]) s)
-> A s out ('[] @[PLabeledType])
forall a b. (a -> b) -> a -> b
$ DataReprHandlers out ('[] @[PLabeledType]) s
-> (PDataSum ('[] @[PLabeledType]) s -> Term s out)
-> DataReprHandlers out ('[] @[PLabeledType]) s
forall a b. a -> b -> a
const DataReprHandlers out ('[] @[PLabeledType]) s
forall (out :: PType) (s :: S).
DataReprHandlers out ('[] @[PLabeledType]) s
DRHNil)
            ( \(A (PDataSum ys s -> Term s out) -> DataReprHandlers out ys s
prev) -> ((PDataSum ((':) @[PLabeledType] y ys) s -> Term s out)
 -> DataReprHandlers out ((':) @[PLabeledType] y ys) s)
-> A s out ((':) @[PLabeledType] y ys)
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 ->
                (Term s (PDataRecord y) -> Term s out)
-> DataReprHandlers out ys s
-> DataReprHandlers out ((':) @[PLabeledType] y ys) s
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 (NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  ((':) @[PLabeledType] y ys)
-> PDataSum ((':) @[PLabeledType] y ys) s
forall (defs :: [[PLabeledType]]) (s :: S).
NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  defs
-> PDataSum defs s
PDataSum (Compose @PType @[PLabeledType] (Term s) PDataRecord y
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (Compose @PType @[PLabeledType] (Term s) PDataRecord y
 -> NS
      @[PLabeledType]
      (Compose @PType @[PLabeledType] (Term s) PDataRecord)
      ((':) @[PLabeledType] y ys))
-> Compose @PType @[PLabeledType] (Term s) PDataRecord y
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] y ys)
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord y)
-> Compose @PType @[PLabeledType] (Term s) PDataRecord y
forall a b. Coercible @Type a b => a -> b
coerce Term s (PDataRecord y)
x)))
                  (DataReprHandlers out ys s
 -> DataReprHandlers out ((':) @[PLabeledType] y ys) s)
-> DataReprHandlers out ys s
-> DataReprHandlers out ((':) @[PLabeledType] y ys) s
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 (NS
  @[PLabeledType]
  (Compose @PType @[PLabeledType] (Term s) PDataRecord)
  ((':) @[PLabeledType] y ys)
-> PDataSum ((':) @[PLabeledType] y ys) s
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)
  ys
-> NS
     @[PLabeledType]
     (Compose @PType @[PLabeledType] (Term s) PDataRecord)
     ((':) @[PLabeledType] y ys)
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 = Term s (PAsData (PDataSum defs)) -> Term s (PDataSum defs)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce
  pdataImpl :: forall (s :: S). Term s (PDataSum defs) -> Term s PData
pdataImpl = Term s (PDataSum defs) -> Term s PData
forall (b :: PType) (a :: PType) (s :: S). 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 = Term s (PDataSum defs) -> Term s (PAsData (PDataSum defs))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
x Term s (PAsData (PDataSum defs))
-> Term s (PAsData (PDataSum defs)) -> Term s PBool
forall (s :: S).
Term s (PAsData (PDataSum defs))
-> Term s (PAsData (PDataSum defs)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PDataSum defs) -> Term s (PAsData (PDataSum defs))
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 => POrd (PDataSum defs) where
  {-# INLINEABLE (#<) #-}
  Term s (PDataSum defs)
x' #< :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#< Term s (PDataSum defs)
y' = Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
-> Term s (PDataSum defs) -> Term s (PDataSum defs :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
x' Term s (PDataSum defs :--> PBool)
-> Term s (PDataSum defs) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
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 (s :: S).
 Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
 -> Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> (forall (s :: S).
    Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (c :--> (PDataSum defs :--> PBool))
plam ((Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool)
 -> Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> (Term s (PDataSum defs)
    -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PDataSum defs)
x Term s (PDataSum defs)
y -> Term s (PDataSum defs)
-> Term s (PDataSum defs)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> Term s PBool
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 NP @[PLabeledType] (DualReprHandler s PBool) defs
forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTHandler
  {-# INLINEABLE (#<=) #-}
  Term s (PDataSum defs)
x' #<= :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#<= Term s (PDataSum defs)
y' = Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall (s :: S).
Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
f Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
-> Term s (PDataSum defs) -> Term s (PDataSum defs :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
x' Term s (PDataSum defs :--> PBool)
-> Term s (PDataSum defs) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
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 (s :: S).
 Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
 -> Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> (forall (s :: S).
    Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (c :--> (PDataSum defs :--> PBool))
plam ((Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool)
 -> Term s (PDataSum defs :--> (PDataSum defs :--> PBool)))
-> (Term s (PDataSum defs)
    -> Term s (PDataSum defs) -> Term s PBool)
-> Term s (PDataSum defs :--> (PDataSum defs :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PDataSum defs)
x Term s (PDataSum defs)
y -> Term s (PDataSum defs)
-> Term s (PDataSum defs)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> Term s PBool
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 NP @[PLabeledType] (DualReprHandler s PBool) defs
forall (def :: [[PLabeledType]]) (s :: S).
All
  @[PLabeledType]
  (Compose @PType @[PLabeledType] POrd PDataRecord)
  def =>
NP @[PLabeledType] (DualReprHandler s PBool) def
mkLTEHandler

-- | 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 = ClosedTerm
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
      :--> PDataRecord def)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
    :--> PDataRecord def)
 -> Term
      s
      (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
       :--> PDataRecord def))
-> ClosedTerm
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
      :--> PDataRecord def)
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
      :--> PDataRecord def)
forall a b. (a -> b) -> a -> b
$
  (Term s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
 -> Term s (PDataRecord def))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
      :--> PDataRecord def)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PDataRecord def))
-> Term s (c :--> PDataRecord def)
plam ((Term
    s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
  -> Term s (PDataRecord def))
 -> Term
      s
      (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
       :--> PDataRecord def))
-> (Term
      s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
    -> Term s (PDataRecord def))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
      :--> PDataRecord def)
forall a b. (a -> b) -> a -> b
$ \Term s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
t ->
    (Term s (PBuiltinList PData) -> Term s (PDataRecord def)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData) -> Term s (PDataRecord def))
-> Term s (PBuiltinList PData) -> Term s (PDataRecord def)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PAsData
     (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))))
-> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term
   s
   (PAsData
      (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))))
 -> Term s PData)
-> Term
     s
     (PAsData
        (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType])))
-> Term
     s
     (PAsData
        (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))))
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 = ClosedTerm
  (PDataSum ((':) @[PLabeledType] def defs)
   :--> PDataRecord
          (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PDataSum ((':) @[PLabeledType] def defs)
    :--> PDataRecord
           (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
 -> Term
      s
      (PDataSum ((':) @[PLabeledType] def defs)
       :--> PDataRecord
              (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> ClosedTerm
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall a b. (a -> b) -> a -> b
$
  (Term s (PDataSum ((':) @[PLabeledType] def defs))
 -> Term
      s
      (PDataRecord
         (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c
 -> Term
      s
      (PDataRecord
         (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> Term
     s
     (c
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
plam ((Term s (PDataSum ((':) @[PLabeledType] def defs))
  -> Term
       s
       (PDataRecord
          (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
 -> Term
      s
      (PDataSum ((':) @[PLabeledType] def defs)
       :--> PDataRecord
              (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> (Term s (PDataSum ((':) @[PLabeledType] def defs))
    -> Term
         s
         (PDataRecord
            (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> Term
     s
     (PDataSum ((':) @[PLabeledType] def defs)
      :--> PDataRecord
             (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall a b. (a -> b) -> a -> b
$ \Term s (PDataSum ((':) @[PLabeledType] def defs))
t ->
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term
         s
         (PDataRecord
            (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> Term
     s
     (PDataRecord
        (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PAsData (PDataSum ((':) @[PLabeledType] def defs)))
-> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PDataSum ((':) @[PLabeledType] def defs)))
 -> Term s PData)
-> Term s (PAsData (PDataSum ((':) @[PLabeledType] def defs)))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s (PDataSum ((':) @[PLabeledType] def defs))
-> Term s (PAsData (PDataSum ((':) @[PLabeledType] def defs)))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum ((':) @[PLabeledType] def defs))
t) ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
  -> Term
       s
       (PDataRecord
          (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
 -> Term
      s
      (PDataRecord
         (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term
         s
         (PDataRecord
            (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs))))
-> Term
     s
     (PDataRecord
        (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinPair PInteger (PBuiltinList PData))
d ->
      let Term s PInteger
i :: Term _ PInteger = Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d
       in Term s PBool
-> Term
     s
     (PDataRecord
        (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
-> Term
     s
     (PDataRecord
        (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
-> Term
     s
     (PDataRecord
        (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Integer -> Term s PInteger
forall a. Num a => Integer -> a
fromInteger (Proxy @Nat n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n))
            (Term s (PBuiltinList PData) -> Term s (PDataRecord w)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData) -> Term s (PDataRecord w))
-> Term s (PBuiltinList PData) -> Term s (PDataRecord w)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
d :: Term _ (PDataRecord _))
            Term
  s
  (PDataRecord
     (IndexList @[PLabeledType] n ((':) @[PLabeledType] def defs)))
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 =
  Term s PData
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PData
 -> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as))))
-> Term s PData
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
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 (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ Proxy @Nat n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n) (Term s (PDataRecord as) -> Term s (PBuiltinList PData)
forall (b :: PType) (a :: PType) (s :: S). 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 =
  Term s (PBuiltinList PData)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData)
 -> Term s (PDataRecord (Drop @PLabeledType n xs)))
-> Term s (PBuiltinList PData)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
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 (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ Proxy @Nat n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy @Nat n
n) (Term s (PDataRecord xs) -> Term s (PBuiltinList PData)
forall (b :: PType) (a :: PType) (s :: S). 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 = DerivedPInner PlutusTypeData a s
-> Term s (DerivedPInner PlutusTypeData a)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (DerivedPInner PlutusTypeData a s
 -> Term s (DerivedPInner PlutusTypeData a))
-> DerivedPInner PlutusTypeData a s
-> Term s (DerivedPInner PlutusTypeData a)
forall a b. (a -> b) -> a -> b
$ SOP
  @PType
  (Term s)
  (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> PDataSum
     (IsPDataSumDefs
        (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
     s
forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
SOP @PType (Term s) a -> PDataSum (IsPDataSumDefs a) s
forall (s :: S).
SOP
  @PType
  (Term s)
  (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> PDataSum
     (IsPDataSumDefs
        (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
     s
toSum (SOP
   @PType
   (Term s)
   (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
 -> PDataSum
      (IsPDataSumDefs
         (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
      s)
-> SOP
     @PType
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> PDataSum
     (IsPDataSumDefs
        (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
     s
forall a b. (a -> b) -> a -> b
$ a s
-> SOP
     @PType
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
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 = Term s (DerivedPInner PlutusTypeData a)
-> (DerivedPInner PlutusTypeData a s -> Term s b) -> Term s b
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 (a s -> Term s b)
-> (PDataSum
      (IsPDataSumDefs
         (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
      s
    -> a s)
-> PDataSum
     (IsPDataSumDefs
        (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
     s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP
  @PType
  (Term s)
  (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> a s
forall (a :: PType) (s :: S).
PGeneric a =>
SOP @PType (Term s) (PCode a) -> a s
gpto (SOP
   @PType
   (Term s)
   (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
 -> a s)
-> (PDataSum
      (IsPDataSumDefs
         (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
      s
    -> SOP
         @PType
         (Term s)
         (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
-> PDataSum
     (IsPDataSumDefs
        (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
     s
-> a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDataSum
  (IsPDataSumDefs
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
  s
-> SOP
     @PType
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
forall (a :: [[PType]]) (s :: S).
IsPDataSum a =>
PDataSum (IsPDataSumDefs a) s -> SOP @PType (Term s) a
forall (s :: S).
PDataSum
  (IsPDataSumDefs
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))))
  s
-> SOP
     @PType
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
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 (Term
  s
  (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType]))
   :--> PDataRecord x)
forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum Term
  s
  (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType]))
   :--> PDataRecord x)
-> Term s (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType])))
-> Term s (PDataRecord x)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
Term s (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType])))
d1) (Term
  s
  (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType]))
   :--> PDataRecord x)
forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum Term
  s
  (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType]))
   :--> PDataRecord x)
-> Term s (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType])))
-> Term s (PDataRecord x)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataSum defs)
Term s (PDataSum ((':) @[PLabeledType] x ('[] @[PLabeledType])))
d2)
pmatchLT Term s (PDataSum defs)
d1 Term s (PDataSum defs)
d2 NP @[PLabeledType] (DualReprHandler s PBool) defs
handlers = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
  Term s (PBuiltinPair PInteger (PBuiltinList PData))
a <- ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair PInteger (PBuiltinList PData))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
        -> Term s PBool)
    -> Term s PBool)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s PBool)
-> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PAsData (PDataSum defs)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PDataSum defs)) -> Term s PData)
-> Term s (PAsData (PDataSum defs)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s (PDataSum defs) -> Term s (PAsData (PDataSum defs))
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 <- ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair PInteger (PBuiltinList PData))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
        -> Term s PBool)
    -> Term s PBool)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s PBool)
-> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @PBool s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PAsData (PDataSum defs)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PDataSum defs)) -> Term s PData)
-> Term s (PAsData (PDataSum defs)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term s (PDataSum defs) -> Term s (PAsData (PDataSum defs))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDataSum defs)
d2

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

  Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
    (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
cid1 Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd 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.
      (AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True)
    (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
cid1 Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
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.
      ( TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
          Term s (PBuiltinList PData)
flds1 <- ((Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s (PBuiltinList PData)))
-> (Term s (PBuiltinList PData)
    -> (Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
-> Term s (PBuiltinList PData)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinList PData)
 -> TermCont @PBool s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
a
          Term s (PBuiltinList PData)
flds2 <- ((Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
 -> TermCont @PBool s (Term s (PBuiltinList PData)))
-> (Term s (PBuiltinList PData)
    -> (Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool)
-> Term s (PBuiltinList PData)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s PBool) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinList PData)
 -> TermCont @PBool s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont @PBool s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
b
          let handlers' :: [Term s PBool]
handlers' = Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
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 <- [Term s PBool] -> TermCont @PBool s (Dig, Term s PBool)
forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s (Dig, Term s out)
findCommon [Term s PBool]
handlers'
          Term s PBool -> TermCont @PBool s (Term s PBool)
forall a. a -> TermCont @PBool s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ (Dig, Term s PBool)
-> Integer -> [Term s PBool] -> Term s PInteger -> Term s PBool
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 (Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) defs
-> [Term s PBool]
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.
    (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
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 (Term s (PBuiltinList PData) -> Term s (PDataRecord x)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args1) (Term s (PBuiltinList PData) -> Term s (PDataRecord x)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args2)
        Term s PBool -> [Term s PBool] -> [Term s PBool]
forall a. a -> [a] -> [a]
: Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData)
-> NP @[PLabeledType] (DualReprHandler s PBool) xs
-> [Term s PBool]
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
_ = (Dig, Term s out) -> Term s out
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 =
  TermCont @out s Dig -> (Dig -> Term s out) -> Term s out
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (Term s out -> TermCont @out s Dig
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s Dig
hashOpenTerm Term s out
handler) ((Dig -> Term s out) -> Term s out)
-> (Dig -> Term s out) -> Term s out
forall a b. (a -> b) -> a -> b
$ \Dig
hhash ->
    if Dig
hhash Dig -> Dig -> Bool
forall a. Eq a => a -> a -> Bool
== (Dig, Term s out) -> Dig
forall a b. (a, b) -> a
fst (Dig, Term s out)
common
      then (Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) [Term s out]
rest Term s PInteger
c
      else
        Term s PBool -> Term s out -> Term s out -> Term s out
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Integer -> Term s PInteger
forall a. Num a => Integer -> a
fromInteger Integer
idx Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
c)
          Term s out
handler
          (Term s out -> Term s out) -> Term s out -> Term s out
forall a b. (a -> b) -> a -> b
$ (Dig, Term s out)
-> Integer -> [Term s out] -> Term s PInteger -> Term s out
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 Integer -> Integer -> Integer
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 [] = [(Dig, Term s out)] -> TermCont @r s [(Dig, Term s out)]
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
hashHandlers (Term s out
handler : [Term s out]
rest) = do
  Dig
hash <- Term s out -> TermCont @r s Dig
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s Dig
hashOpenTerm Term s out
handler
  [(Dig, Term s out)]
hashes <- [Term s out] -> TermCont @r s [(Dig, Term s out)]
forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s [(Dig, Term s out)]
hashHandlers [Term s out]
rest
  [(Dig, Term s out)] -> TermCont @r s [(Dig, Term s out)]
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([(Dig, Term s out)] -> TermCont @r s [(Dig, Term s out)])
-> [(Dig, Term s out)] -> TermCont @r s [(Dig, Term s out)]
forall a b. (a -> b) -> a -> b
$ (Dig
hash, Term s out
handler) (Dig, Term s out) -> [(Dig, Term s out)] -> [(Dig, Term s out)]
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 <- [Term s out] -> TermCont @r s [(Dig, Term s out)]
forall {r :: PType} (s :: S) (out :: PType).
[Term s out] -> TermCont @r s [(Dig, Term s out)]
hashHandlers [Term s out]
handlers
  (Dig, Term s out) -> TermCont @r s (Dig, Term s out)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Dig, Term s out) -> TermCont @r s (Dig, Term s out))
-> (Dig, Term s out) -> TermCont @r s (Dig, Term s out)
forall a b. (a -> b) -> a -> b
$ [(Dig, Term s out)] -> (Dig, Term s out)
forall a. HasCallStack => [a] -> a
head ([(Dig, Term s out)] -> (Dig, Term s out))
-> ([(Dig, Term s out)] -> [(Dig, Term s out)])
-> [(Dig, Term s out)]
-> (Dig, Term s out)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Dig, Term s out)] -> [(Dig, Term s out)] -> Ordering)
-> [[(Dig, Term s out)]] -> [(Dig, Term s out)]
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (\[(Dig, Term s out)]
x [(Dig, Term s out)]
y -> [(Dig, Term s out)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Dig, Term s out)]
x Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [(Dig, Term s out)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Dig, Term s out)]
y) ([[(Dig, Term s out)]] -> [(Dig, Term s out)])
-> ([(Dig, Term s out)] -> [[(Dig, Term s out)]])
-> [(Dig, Term s out)]
-> [(Dig, Term s out)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dig, Term s out) -> (Dig, Term s out) -> Bool)
-> [(Dig, Term s out)] -> [[(Dig, Term s out)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Dig, Term s out)
x (Dig, Term s out)
y -> (Dig, Term s out) -> Dig
forall a b. (a, b) -> a
fst (Dig, Term s out)
x Dig -> Dig -> Bool
forall a. Eq a => a -> a -> Bool
== (Dig, Term s out) -> Dig
forall a b. (a, b) -> a
fst (Dig, Term s out)
y) ([(Dig, Term s out)] -> [[(Dig, Term s out)]])
-> ([(Dig, Term s out)] -> [(Dig, Term s out)])
-> [(Dig, Term s out)]
-> [[(Dig, Term s out)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Dig, Term s out) -> Dig)
-> [(Dig, Term s out)] -> [(Dig, Term s out)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Dig, Term s out) -> Dig
forall a b. (a, b) -> a
fst ([(Dig, Term s out)] -> (Dig, Term s out))
-> [(Dig, Term s out)] -> (Dig, Term s out)
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 = Proxy
  @([PLabeledType] -> Constraint)
  (Compose @PType @[PLabeledType] 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))
-> Const @[[PLabeledType]] () def
-> NP @[PLabeledType] (DualReprHandler s PBool) def
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
forall (t :: [PLabeledType] -> Constraint).
Proxy @([PLabeledType] -> Constraint) t
Proxy @(Compose POrd PDataRecord)) Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
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]] () def
 -> NP @[PLabeledType] (DualReprHandler s PBool) def)
-> Const @[[PLabeledType]] () def
-> NP @[PLabeledType] (DualReprHandler s PBool) def
forall a b. (a -> b) -> a -> b
$ () -> Const @[[PLabeledType]] () def
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)
_ = ((Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool)
-> DualReprHandler s PBool y
forall (s :: S) (out :: PType) (def :: [PLabeledType]).
(Term s (PDataRecord def)
 -> Term s (PDataRecord def) -> Term s out)
-> DualReprHandler s out def
DualRepr Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool
forall (s :: S).
Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
(#<), () -> Const @[[PLabeledType]] () ys
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 = Proxy
  @([PLabeledType] -> Constraint)
  (Compose @PType @[PLabeledType] 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))
-> Const @[[PLabeledType]] () def
-> NP @[PLabeledType] (DualReprHandler s PBool) def
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
forall (t :: [PLabeledType] -> Constraint).
Proxy @([PLabeledType] -> Constraint) t
Proxy @(Compose POrd PDataRecord)) Const @[[PLabeledType]] () ((':) @[PLabeledType] y ys)
-> (DualReprHandler s PBool y, Const @[[PLabeledType]] () ys)
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]] () def
 -> NP @[PLabeledType] (DualReprHandler s PBool) def)
-> Const @[[PLabeledType]] () def
-> NP @[PLabeledType] (DualReprHandler s PBool) def
forall a b. (a -> b) -> a -> b
$ () -> Const @[[PLabeledType]] () def
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)
_ = ((Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool)
-> DualReprHandler s PBool y
forall (s :: S) (out :: PType) (def :: [PLabeledType]).
(Term s (PDataRecord def)
 -> Term s (PDataRecord def) -> Term s out)
-> DualReprHandler s out def
DualRepr Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool
forall (s :: S).
Term s (PDataRecord y) -> Term s (PDataRecord y) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
(#<=), () -> Const @[[PLabeledType]] () ys
forall {k} a (b :: k). a -> Const @k a b
Const ())

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

type HRecPApply :: [(Symbol, P.S -> Type)] -> P.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, P.S -> Type)]) (s :: P.S)
  = HRecP (NoReduce (HRecGeneric (HRecPApply as s)))
  deriving stock ((forall x. HRecP as s -> Rep (HRecP as s) x)
-> (forall x. Rep (HRecP as s) x -> HRecP as s)
-> Generic (HRecP as s)
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 x. Rep (HRecP as s) x -> HRecP as s
forall 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
$cfrom :: forall (as :: [(Symbol, PType)]) (s :: S) x.
HRecP as s -> Rep (HRecP as s) x
from :: forall x. HRecP as s -> Rep (HRecP as s) x
$cto :: forall (as :: [(Symbol, PType)]) (s :: S) x.
Rep (HRecP as s) x -> HRecP as s
to :: forall x. Rep (HRecP as s) x -> HRecP as s
Generic)

newtype Flip f a b = Flip (f b a)
  deriving stock ((forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x)
-> (forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b)
-> Generic (Flip @k @k f a b)
forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
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
$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
from :: forall 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
to :: forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
Generic)

class Helper2 (b :: PSubtypeRelation) a where
  type Helper2Excess b a :: P.S -> Type
  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
_ = Term s PData
-> ((Term s (PAsData a),
     Reduce (PTryFromExcess PData (PAsData a) s))
    -> Term s r)
-> Term s r
Term s PData
-> ((Term s (PAsData a),
     Reduce (Helper2Excess 'PNoSubtypeRelation a s))
    -> Term s r)
-> Term s r
forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData a),
     Reduce (PTryFromExcess PData (PAsData a) s))
    -> Term s r)
-> Term s r
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 = TermCont
  @r
  s
  (Term s (PAsData a), Reduce (Helper2Excess 'PSubtypeRelation a s))
-> ((Term s (PAsData a),
     Reduce (Helper2Excess 'PSubtypeRelation a s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData a), Reduce (Helper2Excess 'PSubtypeRelation a s))
 -> ((Term s (PAsData a),
      Reduce (Helper2Excess 'PSubtypeRelation a s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData a), Reduce (Helper2Excess 'PSubtypeRelation a s))
-> ((Term s (PAsData a),
     Reduce (Helper2Excess 'PSubtypeRelation a s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s a
y, GReduce (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s))
exc) <- (((Term s a,
   GReduce
     (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s a,
      GReduce
        (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s a,
    GReduce
      (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term s a,
       GReduce
         (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s))))
-> (((Term s a,
      GReduce
        (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term s a,
      GReduce
        (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
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
    (Term s (PAsData a),
 GReduce
   (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
-> TermCont
     @r
     s
     (Term s (PAsData a),
      GReduce
        (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s a -> Term s (PAsData a)
forall (b :: PType) (a :: PType) (s :: S). 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 :: P.S -> Type) (s :: P.S)
  = ExcessForField (Term s (PAsData a), Reduce (Helper2Excess b a s))
  deriving stock ((forall x. ExcessForField b a s -> Rep (ExcessForField b a s) x)
-> (forall x. Rep (ExcessForField b a s) x -> ExcessForField b a s)
-> Generic (ExcessForField b a s)
forall x. Rep (ExcessForField b a s) x -> ExcessForField b a s
forall x. ExcessForField b a s -> Rep (ExcessForField b a s) x
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
$cfrom :: forall (b :: PSubtypeRelation) (a :: PType) (s :: S) x.
ExcessForField b a s -> Rep (ExcessForField b a s) x
from :: forall 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
to :: forall x. Rep (ExcessForField b a s) x -> ExcessForField b a s
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 = TermCont
  @r
  s
  (Term s (PDataRecord ('[] @PLabeledType)),
   Reduce
     (PTryFromExcess
        (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
-> ((Term s (PDataRecord ('[] @PLabeledType)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PDataRecord ('[] @PLabeledType)),
    Reduce
      (PTryFromExcess
         (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
 -> ((Term s (PDataRecord ('[] @PLabeledType)),
      Reduce
        (PTryFromExcess
           (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PDataRecord ('[] @PLabeledType)),
      Reduce
        (PTryFromExcess
           (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
-> ((Term s (PDataRecord ('[] @PLabeledType)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData) (PDataRecord ('[] @PLabeledType)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PUnit
_ <-
      ((Term s PUnit -> Term s r) -> Term s r)
-> TermCont @r s (Term s PUnit)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PUnit -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PUnit))
-> (Term s (PDelayed PUnit)
    -> (Term s PUnit -> Term s r) -> Term s r)
-> Term s (PDelayed PUnit)
-> TermCont @r s (Term s PUnit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PUnit -> (Term s PUnit -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PUnit -> (Term s PUnit -> Term s r) -> Term s r)
-> (Term s (PDelayed PUnit) -> Term s PUnit)
-> Term s (PDelayed PUnit)
-> (Term s PUnit -> Term s r)
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed PUnit) -> Term s PUnit
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed PUnit) -> TermCont @r s (Term s PUnit))
-> Term s (PDelayed PUnit) -> TermCont @r s (Term s PUnit)
forall a b. (a -> b) -> a -> b
$
        Term
  s
  (PBuiltinList PData
   :--> (PDelayed PUnit :--> (PDelayed PUnit :--> PDelayed PUnit)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin Term
  s
  (PBuiltinList PData
   :--> (PDelayed PUnit :--> (PDelayed PUnit :--> PDelayed PUnit)))
-> Term s (PBuiltinList PData)
-> Term
     s (PDelayed PUnit :--> (PDelayed PUnit :--> PDelayed PUnit))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
opq Term s (PDelayed PUnit :--> (PDelayed PUnit :--> PDelayed PUnit))
-> Term s (PDelayed PUnit)
-> Term s (PDelayed PUnit :--> PDelayed PUnit)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PUnit -> Term s (PDelayed PUnit)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PUnit s -> Term s PUnit
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PUnit s
forall (s :: S). PUnit s
PUnit) Term s (PDelayed PUnit :--> PDelayed PUnit)
-> Term s (PDelayed PUnit) -> Term s (PDelayed PUnit)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PUnit -> Term s (PDelayed PUnit)
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (Term s PString -> Term s PUnit
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"ptryFrom(PDataRecord[]): list is longer than zero")
    (Term s (PDataRecord ('[] @PLabeledType)),
 HRecGeneric ('[] @(Symbol, Type)))
-> TermCont
     @r
     s
     (Term s (PDataRecord ('[] @PLabeledType)),
      HRecGeneric ('[] @(Symbol, Type)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PDataRecord ('[] @PLabeledType))
forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil, HRec ('[] @(Symbol, Type)) -> HRecGeneric ('[] @(Symbol, Type))
forall (as :: [(Symbol, Type)]). HRec as -> HRecGeneric as
HRecGeneric HRec ('[] @(Symbol, Type))
HNil)

type family UnHRecP (x :: P.S -> Type) :: [(Symbol, P.S -> Type)] 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 = TermCont
  @r
  s
  (Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
   Reduce
     (PTryFromExcess
        (PBuiltinList PData)
        (PDataRecord ((':) @PLabeledType (name ':= pty) as))
        s))
-> ((Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData)
          (PDataRecord ((':) @PLabeledType (name ':= pty) as))
          s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
    Reduce
      (PTryFromExcess
         (PBuiltinList PData)
         (PDataRecord ((':) @PLabeledType (name ':= pty) as))
         s))
 -> ((Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
      Reduce
        (PTryFromExcess
           (PBuiltinList PData)
           (PDataRecord ((':) @PLabeledType (name ':= pty) as))
           s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
      Reduce
        (PTryFromExcess
           (PBuiltinList PData)
           (PDataRecord ((':) @PLabeledType (name ':= pty) as))
           s))
-> ((Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
     Reduce
       (PTryFromExcess
          (PBuiltinList PData)
          (PDataRecord ((':) @PLabeledType (name ':= pty) as))
          s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PData
h <- ((Term s PData -> Term s r) -> Term s r)
-> TermCont @r s (Term s PData)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PData -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PData))
-> ((Term s PData -> Term s r) -> Term s r)
-> TermCont @r s (Term s PData)
forall a b. (a -> b) -> a -> b
$ Term s PData -> (Term s PData -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PData -> (Term s PData -> Term s r) -> Term s r)
-> Term s PData -> (Term s PData -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
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 <- (((Term s (PAsData pty),
   GReduce
     (Helper2Excess (PSubtype' PData pty) pty s)
     (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData pty),
      GReduce
        (Helper2Excess (PSubtype' PData pty) pty s)
        (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData pty),
    GReduce
      (Helper2Excess (PSubtype' PData pty) pty s)
      (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term s (PAsData pty),
       GReduce
         (Helper2Excess (PSubtype' PData pty) pty s)
         (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
-> (((Term s (PAsData pty),
      GReduce
        (Helper2Excess (PSubtype' PData pty) pty s)
        (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData pty),
      GReduce
        (Helper2Excess (PSubtype' PData pty) pty s)
        (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
forall a b. (a -> b) -> a -> b
$ Proxy @PSubtypeRelation (PSubtype' PData pty)
-> Term s PData
-> ((Term s (PAsData pty),
     Reduce (Helper2Excess (PSubtype' PData pty) pty s))
    -> Term s r)
-> Term s r
forall (s :: S) (r :: PType).
Proxy @PSubtypeRelation (PSubtype' PData pty)
-> Term s PData
-> ((Term s (PAsData pty),
     Reduce (Helper2Excess (PSubtype' PData pty) pty s))
    -> Term s r)
-> Term s r
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
forall (t :: PSubtypeRelation). Proxy @PSubtypeRelation t
Proxy @(PSubtype' PData pty)) Term s PData
h
    Term s (PBuiltinList PData)
t <- ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList PData)))
-> ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinList PData)
 -> (Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
opq
    (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
tv <- (((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s)))
-> (((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
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
    (Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
 HRecGeneric
   ((':)
      @(Symbol, Type)
      '(name,
        (Term s (PAsData pty),
         GReduce
           (Helper2Excess (PSubtype' PData pty) pty s)
           (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
      (HRecPApply ase s)))
-> TermCont
     @r
     s
     (Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as)),
      HRecGeneric
        ((':)
           @(Symbol, Type)
           '(name,
             (Term s (PAsData pty),
              GReduce
                (Helper2Excess (PSubtype' PData pty) pty s)
                (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
           (HRecPApply ase s)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PBuiltinList PData)
-> Term s (PDataRecord ((':) @PLabeledType (name ':= pty) as))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
opq, HRec
  ((':)
     @(Symbol, Type)
     '(name,
       (Term s (PAsData pty),
        GReduce
          (Helper2Excess (PSubtype' PData pty) pty s)
          (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
     (HRecPApply ase s))
-> HRecGeneric
     ((':)
        @(Symbol, Type)
        '(name,
          (Term s (PAsData pty),
           GReduce
             (Helper2Excess (PSubtype' PData pty) pty s)
             (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
        (HRecPApply ase s))
forall (as :: [(Symbol, Type)]). HRec as -> HRecGeneric as
HRecGeneric (Labeled
  @Symbol
  name
  (Term s (PAsData pty),
   GReduce
     (Helper2Excess (PSubtype' PData pty) pty s)
     (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
-> HRec (HRecPApply ase s)
-> HRec
     ((':)
        @(Symbol, Type)
        '(name,
          (Term s (PAsData pty),
           GReduce
             (Helper2Excess (PSubtype' PData pty) pty s)
             (Rep (Helper2Excess (PSubtype' PData pty) pty s))))
        (HRecPApply ase s))
forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons ((Term s (PAsData pty),
 GReduce
   (Helper2Excess (PSubtype' PData pty) pty s)
   (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
-> Labeled
     @Symbol
     name
     (Term s (PAsData pty),
      GReduce
        (Helper2Excess (PSubtype' PData pty) pty s)
        (Rep (Helper2Excess (PSubtype' PData pty) pty s)))
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) (HRecGeneric (HRecPApply ase s) -> HRec (HRecPApply ase s)
forall a b. Coercible @Type a b => a -> b
coerce (HRecGeneric (HRecPApply ase s) -> HRec (HRecPApply ase s))
-> HRecGeneric (HRecPApply ase s) -> HRec (HRecPApply ase s)
forall a b. (a -> b) -> a -> b
$ (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
-> HRecGeneric (HRecPApply ase s)
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 x. Helper @k a b s -> Rep (Helper @k a b s) x)
-> (forall x. Rep (Helper @k a b s) x -> Helper @k a b s)
-> Generic (Helper @k a b s)
forall x. Rep (Helper @k a b s) x -> Helper @k a b s
forall x. Helper @k a b s -> Rep (Helper @k a b s) x
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
$cfrom :: forall k (a :: k -> Type) (b :: k -> Type) (s :: k) x.
Helper @k a b s -> Rep (Helper @k a b s) x
from :: forall 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
to :: forall x. Rep (Helper @k a b s) x -> Helper @k a b s
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 = TermCont
  @r
  s
  (Term s (PAsData (PDataRecord as)),
   Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
-> ((Term s (PAsData (PDataRecord as)),
     Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PDataRecord as)),
    Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
 -> ((Term s (PAsData (PDataRecord as)),
      Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PDataRecord as)),
      Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
-> ((Term s (PAsData (PDataRecord as)),
     Reduce (PTryFromExcess PData (PAsData (PDataRecord as)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList PData)
l <- (Term s (PAsData (PBuiltinList PData)),
 Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s)
forall a b. (a, b) -> b
snd ((Term s (PAsData (PBuiltinList PData)),
  Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
 -> Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> TermCont
     @r
     s
     (Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s (PAsData (PBuiltinList PData)),
   Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
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 <- (((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s)))
-> (((Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
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
    (Term s (PAsData (PDataRecord as)),
 (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s)))
-> TermCont
     @r
     s
     (Term s (PAsData (PDataRecord as)),
      (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PDataRecord as))
forall (b :: PType) (a :: PType) (s :: S). 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 =
    Term s PBool -> Term s POpaque -> Term s POpaque -> Term s POpaque
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Integer -> Term s PInteger
forall a. Num a => Integer -> a
fromInteger (Proxy @Nat n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy @Nat n -> Integer) -> Proxy @Nat n -> Integer
forall a b. (a -> b) -> a -> b
$ forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @n) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
constr)
      ( TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
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)))
_ <- (((Term s (PDataRecord x),
   GReduce
     (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
     (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (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 ((((Term s (PDataRecord x),
    GReduce
      (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
      (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (Term s (PDataRecord x),
       GReduce
         (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
         (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s))))
-> (((Term s (PDataRecord x),
      GReduce
        (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
        (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (Term s (PDataRecord x),
      GReduce
        (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)
        (Rep (PTryFromExcess (PBuiltinList PData) (PDataRecord x) s)))
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
          Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a. a -> TermCont @POpaque s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s PUnit -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s PUnit -> Term s POpaque) -> Term s PUnit -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PUnit s -> Term s PUnit
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PUnit s
forall (s :: S). PUnit s
PUnit
      )
      (Proxy @Nat (n + 1)
-> Proxy @[[PLabeledType]] xs
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
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
forall (s :: S).
Proxy @Nat (n + 1)
-> Proxy @[[PLabeledType]] xs
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @(n + 1)) (forall (t :: [[PLabeledType]]). Proxy @[[PLabeledType]] t
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)
_ = Term s PString -> Term s POpaque
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError 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 = TermCont
  @r
  s
  (Term s (PDataSum ys),
   Reduce (PTryFromExcess PData (PDataSum ys) s))
-> ((Term s (PDataSum ys),
     Reduce (PTryFromExcess PData (PDataSum ys) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PDataSum ys),
    Reduce (PTryFromExcess PData (PDataSum ys) s))
 -> ((Term s (PDataSum ys),
      Reduce (PTryFromExcess PData (PDataSum ys) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PDataSum ys),
      Reduce (PTryFromExcess PData (PDataSum ys) s))
-> ((Term s (PDataSum ys),
     Reduce (PTryFromExcess PData (PDataSum ys) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
x <- ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> ((Term s (PBuiltinPair PInteger (PBuiltinList PData))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
     -> Term s r)
 -> Term s r)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    Term s PInteger
constr <- ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PInteger -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PInteger))
-> ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r)
-> Term s PInteger -> (Term s PInteger -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x
    Term s (PBuiltinList PData)
fields <- ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList PData)))
-> ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PBuiltinList PData)
 -> (Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x
    Term s POpaque
_ <- ((Term s POpaque -> Term s r) -> Term s r)
-> TermCont @r s (Term s POpaque)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s POpaque -> Term s r) -> Term s r)
 -> TermCont @r s (Term s POpaque))
-> ((Term s POpaque -> Term s r) -> Term s r)
-> TermCont @r s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s POpaque -> (Term s POpaque -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s POpaque -> (Term s POpaque -> Term s r) -> Term s r)
-> Term s POpaque -> (Term s POpaque -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 0
-> Proxy @[[PLabeledType]] ys
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
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
forall (s :: S).
Proxy @Nat 0
-> Proxy @[[PLabeledType]] ys
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @0) (forall (t :: [[PLabeledType]]). Proxy @[[PLabeledType]] t
forall {k} (t :: k). Proxy @k t
Proxy @ys) Term s PInteger
constr Term s (PBuiltinList PData)
fields
    (Term s (PDataSum ys), ())
-> TermCont @r s (Term s (PDataSum ys), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PDataSum ys)
forall (b :: PType) (a :: PType) (s :: S). 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 = TermCont
  @r
  s
  (Term s (PAsData (PDataSum ys)),
   Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
-> ((Term s (PAsData (PDataSum ys)),
     Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
    -> Term s r)
-> Term s r
forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PDataSum ys)),
    Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
 -> ((Term s (PAsData (PDataSum ys)),
      Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PDataSum ys)),
      Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
-> ((Term s (PAsData (PDataSum ys)),
     Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PDataSum ys)
y, ()
exc) <- (((Term s (PDataSum ys), ()) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PDataSum ys), ())
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PDataSum ys), ()) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PDataSum ys), ()))
-> (((Term s (PDataSum ys), ()) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PDataSum ys), ())
forall a b. (a -> b) -> a -> b
$ Term s PData
-> ((Term s (PDataSum ys),
     Reduce (PTryFromExcess PData (PDataSum ys) s))
    -> Term s r)
-> Term s r
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
    (Term s (PAsData (PDataSum ys)), ())
-> TermCont @r s (Term s (PAsData (PDataSum ys)), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PDataSum ys) -> Term s (PAsData (PDataSum ys))
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 Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
" = " Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Bool -> Term s t -> Term s PString
forall (s :: S). Bool -> Term s t -> Term s PString
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 = String -> Term s PString
forall a. IsString a => String -> a
fromString (String -> Term s PString) -> String -> Term s PString
forall a b. (a -> b) -> a -> b
$ Proxy @Symbol label -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy @Symbol label
proxy