{-# 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 (
  PAsData,
  PBuiltinList,
  PData,
  PIsData,
  pasConstr,
  pchooseListBuiltin,
  pconstrBuiltin,
  pdata,
  pdataImpl,
  pforgetData,
  pfromData,
  pfromDataImpl,
  pfstBuiltin,
  psndBuiltin,
 )
import Plutarch.Builtin.Bool (PBool, pif)
import Plutarch.DataRepr.Internal.HList (
  HRec (HCons, HNil),
  HRecGeneric (HRecGeneric),
  Labeled (Labeled),
  type Drop,
  type IndexList,
 )
import Plutarch.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom, gpto)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.Newtype (PlutusTypeNewtype)
import Plutarch.Internal.Ord (POrd, PPartialOrd ((#<), (#<=)))
import Plutarch.Internal.Other (POpaque, popaque, 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.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.List (PListLike (pnil), pcons, pdrop, phead, ptail, ptryIndex)
import Plutarch.Reducible (NoReduce, Reduce)
import Plutarch.Show (PShow (pshow'))
import Plutarch.String (PString)
import Plutarch.Trace (ptraceInfoError)
import Plutarch.TryFrom (
  PSubtype',
  PSubtypeRelation (PNoSubtypeRelation, PSubtypeRelation),
  PTryFrom,
  PTryFromExcess,
  ptryFrom,
  ptryFrom',
  pupcast,
 )
import Plutarch.Unit (PUnit (PUnit))
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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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 PPartialOrd (PDataRecord '[]) where
  Term s (PDataRecord ('[] @PLabeledType))
_ #<= :: forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType))
-> Term s (PDataRecord ('[] @PLabeledType)) -> Term s PBool
#<= Term s (PDataRecord ('[] @PLabeledType))
_ = AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True
  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

instance POrd (PDataRecord '[])

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

instance
  (All Top xs, KnownSymbol label, PIsData x, PShow x, PShow (PDataRecordShowHelper xs)) =>
  PShow (PDataRecord ((label ':= x) ': xs))
  where
  pshow' :: forall (s :: S).
Bool
-> Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
-> Term s PString
pshow' Bool
b Term s (PDataRecord ((':) @PLabeledType (label ':= x) xs))
xs = Term s PString
"[" 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) => PPartialOrd (PDataRecord '[label ':= x]) where
  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l1 #< :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
-> Term s PBool
#< Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ('[] @PLabeledType)))
l2 = 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).
PPartialOrd 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

  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).
PPartialOrd 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 (POrd x, PIsData x) => POrd (PDataRecord '[label ':= x])

instance
  (SListI xs, POrd x, PIsData x, POrd (PDataRecord (x' ': xs))) =>
  PPartialOrd (PDataRecord ((label ':= x) ': x' ': xs))
  where
  Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l1 #< :: forall (s :: S).
Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
-> Term s PBool
#< Term
  s
  (PDataRecord
     ((':) @PLabeledType (label ':= x) ((':) @PLabeledType x' xs)))
l2 = 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).
PPartialOrd 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).
PPartialOrd 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

  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).
PPartialOrd 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).
PPartialOrd 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

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

{- | Cons a field to a data record.

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

@

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

@
-}
pdcons :: forall label a l s. Term s (PAsData a :--> PDataRecord l :--> PDataRecord ((label ':= a) ': l))
pdcons :: forall (label :: Symbol) (a :: PType) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l
         :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
pdcons = Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term
     s
     (PAsData a
      :--> (PDataRecord l
            :--> PDataRecord ((':) @PLabeledType (label ':= a) l)))
forall (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PAsData (PDataRecord xs))
x) :: Term _ (PBuiltinList PData))
  pdataImpl :: forall (s :: S). Term s (PDataRecord xs) -> Term s PData
pdataImpl Term s (PDataRecord xs)
x = 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataSum defs))
d :: Term _ (PDataSum defs))
          DataReprHandlers b defs s
_ -> 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 (PInner (PDataSum defs))
Term s PData
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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce
  pdataImpl :: forall (s :: S). Term s (PDataSum defs) -> Term s PData
pdataImpl = Term s (PDataSum defs) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

instance PEq (PDataSum defs) where
  Term s (PDataSum defs)
x #== :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#== Term s (PDataSum defs)
y = 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 => PPartialOrd (PDataSum defs) where
  Term s (PDataSum defs)
x' #< :: forall (s :: S).
Term s (PDataSum defs) -> Term s (PDataSum defs) -> Term s PBool
#< Term s (PDataSum defs)
y' = 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
  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

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

-- | If there is only a single variant, then we can safely extract it.
punDataSum :: Term s (PDataSum '[def] :--> PDataRecord def)
punDataSum :: forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum = 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PDataRecord as)
xs)

-- | Safely drop the first n items of a 'PDataRecord'.
pdropDataRecord :: KnownNat n => Proxy n -> Term s (PDataRecord xs) -> Term s (PDataRecord (Drop n xs))
pdropDataRecord :: forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord Proxy @Nat n
n Term s (PDataRecord xs)
xs =
  Term s (PBuiltinList PData)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
forall (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PDataRecord xs)
xs)

data PlutusTypeData

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

instance PlutusTypeStrat PlutusTypeData where
  type PlutusTypeStratConstraint PlutusTypeData = PlutusTypeDataConstraint
  type DerivedPInner PlutusTypeData a = PDataSum (IsPDataSumDefs (PCode a))
  derivedPCon :: forall (a :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeData :: Type)) =>
a s -> Term s (DerivedPInner PlutusTypeData a)
derivedPCon a s
x = 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).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
cid2)
      -- Left arg's constructor id is less, no need to continue.
      (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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
args1) (Term s (PBuiltinList PData) -> Term s (PDataRecord x)
forall (s :: S) (a :: PType) (b :: PType). 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).
PPartialOrd 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).
PPartialOrd 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s a
y, GReduce (PTryFromExcess PData a s) (Rep (PTryFromExcess PData a s))
exc)

-- We could have a more advanced instance but it's not needed really.
newtype ExcessForField (b :: PSubtypeRelation) (a :: 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 @S)
_ <-
      ((Term s (PUnit @S) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PUnit @S))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PUnit @S) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PUnit @S)))
-> (Term s (PDelayed (PUnit @S))
    -> (Term s (PUnit @S) -> Term s r) -> Term s r)
-> Term s (PDelayed (PUnit @S))
-> TermCont @r s (Term s (PUnit @S))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PUnit @S) -> (Term s (PUnit @S) -> 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 @S) -> (Term s (PUnit @S) -> Term s r) -> Term s r)
-> (Term s (PDelayed (PUnit @S)) -> Term s (PUnit @S))
-> Term s (PDelayed (PUnit @S))
-> (Term s (PUnit @S) -> Term s r)
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed (PUnit @S)) -> Term s (PUnit @S)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PUnit @S)) -> TermCont @r s (Term s (PUnit @S)))
-> Term s (PDelayed (PUnit @S))
-> TermCont @r s (Term s (PUnit @S))
forall a b. (a -> b) -> a -> b
$
        Term
  s
  (PBuiltinList PData
   :--> (PDelayed (PUnit @S)
         :--> (PDelayed (PUnit @S) :--> PDelayed (PUnit @S))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin Term
  s
  (PBuiltinList PData
   :--> (PDelayed (PUnit @S)
         :--> (PDelayed (PUnit @S) :--> PDelayed (PUnit @S))))
-> Term s (PBuiltinList PData)
-> Term
     s
     (PDelayed (PUnit @S)
      :--> (PDelayed (PUnit @S) :--> PDelayed (PUnit @S)))
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 @S)
   :--> (PDelayed (PUnit @S) :--> PDelayed (PUnit @S)))
-> Term s (PDelayed (PUnit @S))
-> Term s (PDelayed (PUnit @S) :--> PDelayed (PUnit @S))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUnit @S) -> Term s (PDelayed (PUnit @S))
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (PUnit @S s -> Term s (PUnit @S)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PUnit @S s
forall {k} (s :: k). PUnit @k s
PUnit) Term s (PDelayed (PUnit @S) :--> PDelayed (PUnit @S))
-> Term s (PDelayed (PUnit @S)) -> Term s (PDelayed (PUnit @S))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PUnit @S) -> Term s (PDelayed (PUnit @S))
forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (Term s PString -> Term s (PUnit @S)
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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, (Term s (PDataRecord as), HRecGeneric (HRecPApply ase s))
r)

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

instance
  forall (n :: Nat) (x :: [PLabeledType]) (xs :: [[PLabeledType]]).
  ( PTryFrom (PBuiltinList PData) (PDataRecord x)
  , SumValidation (n + 1) xs
  , KnownNat n
  ) =>
  SumValidation n (x ': xs)
  where
  validateSum :: forall (s :: S).
Proxy @Nat n
-> Proxy @[[PLabeledType]] ((':) @[PLabeledType] x xs)
-> Term s PInteger
-> Term s (PBuiltinList PData)
-> Term s POpaque
validateSum Proxy @Nat n
_ Proxy @[[PLabeledType]] ((':) @[PLabeledType] x xs)
_ Term s PInteger
constr Term s (PBuiltinList PData)
fields =
    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 @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s (PUnit @S) -> Term s POpaque)
-> Term s (PUnit @S) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PUnit @S s -> Term s (PUnit @S)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PUnit @S s
forall {k} (s :: k). PUnit @k 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 (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
opq, ())

instance PTryFrom PData (PDataSum ys) => PTryFrom PData (PAsData (PDataSum ys)) where
  type PTryFromExcess _ _ = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData (PDataSum ys)),
     Reduce (PTryFromExcess PData (PAsData (PDataSum ys)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
x = 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