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

module Plutarch.DataRepr.Internal.Field (
  -- * PDataField class & deriving utils
  PDataFields (..),
  pletFields,
  pfield,

  -- * BindFields class mechanism
  BindFields (..),
  type Bindings,
  type BoundTerms,
  type Drop,
  type HRecOf,
  type PMemberFields,
  type PMemberField,

  -- * Re-exports
  HRec (..),
  Labeled (Labeled, unLabeled),
  hrecField,
) where

import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (
  KnownNat,
  Symbol,
 )
import Plutarch.Builtin.Data (PAsData)
import Plutarch.DataRepr.Internal (
  PDataRecord,
  PDataSum,
  PLabeledType ((:=)),
  pdropDataRecord,
  pindexDataRecord,
  punDataSum,
  type PLabelIndex,
  type PLookupLabel,
  type PUnLabel,
 )
import Plutarch.DataRepr.Internal.FromData (PFromDataable, pmaybeFromAsData)
import Plutarch.DataRepr.Internal.HList (
  HRec (HCons, HNil),
  Labeled (Labeled, unLabeled),
  hrecField,
  type Drop,
  type ElemOf,
  type IndexLabel,
  type IndexList,
 )
import Plutarch.Internal.IsData (PIsData, pfromData)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (PInner)
import Plutarch.Internal.Term (S, Term, plet, (#), (:-->))
import Plutarch.Internal.TermCont (TermCont (TermCont), runTermCont)
import Plutarch.Internal.Witness (witness)

--------------------------------------------------------------------------------
---------- PDataField class & deriving utils

type family Helper (x :: S -> Type) :: [PLabeledType] where
  Helper (PDataSum '[y]) = y
  Helper (PDataRecord y) = y

{- |
  Class allowing 'letFields' to work for a PType, usually via
  `PIsDataRepr`, but is derived for some other types for convenience.
-}
class PDataFields (a :: S -> Type) where
  -- | Fields in HRec bound by 'letFields'
  type PFields a :: [PLabeledType]

  type PFields a = Helper (PInner a)

  -- | Convert a Term to a 'PDataList'
  ptoFields :: Term s a -> Term s (PDataRecord (PFields a))
  default ptoFields :: (PDataFields (PInner a), PFields (PInner a) ~ PFields a) => Term s a -> Term s (PDataRecord (PFields a))
  ptoFields Term s a
x = Term s (PInner a) -> Term s (PDataRecord (PFields (PInner a)))
forall (s :: S).
Term s (PInner a) -> Term s (PDataRecord (PFields (PInner a)))
forall (a :: S -> Type) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields (Term s (PInner a) -> Term s (PDataRecord (PFields (PInner a))))
-> Term s (PInner a) -> Term s (PDataRecord (PFields (PInner a)))
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s (PInner a)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s a
x

instance PDataFields (PDataRecord as) where
  type PFields (PDataRecord as) = as
  ptoFields :: forall (s :: S).
Term s (PDataRecord as)
-> Term s (PDataRecord (PFields (PDataRecord as)))
ptoFields = Term s (PDataRecord as) -> Term s (PDataRecord as)
Term s (PDataRecord as)
-> Term s (PDataRecord (PFields (PDataRecord as)))
forall a. a -> a
id

instance PDataFields (PDataSum '[as]) where
  type PFields (PDataSum '[as]) = as
  ptoFields :: forall (s :: S).
Term s (PDataSum ((':) @[PLabeledType] as ('[] @[PLabeledType])))
-> Term
     s
     (PDataRecord
        (PFields
           (PDataSum ((':) @[PLabeledType] as ('[] @[PLabeledType])))))
ptoFields = (Term
  s
  (PDataSum ((':) @[PLabeledType] as ('[] @[PLabeledType]))
   :--> PDataRecord as)
forall (s :: S) (def :: [PLabeledType]).
Term
  s
  (PDataSum ((':) @[PLabeledType] def ('[] @[PLabeledType]))
   :--> PDataRecord def)
punDataSum #)

instance
  forall a.
  ( PIsData a
  , PDataFields a
  ) =>
  PDataFields (PAsData a)
  where
  type PFields (PAsData a) = PFields a
  ptoFields :: forall (s :: S).
Term s (PAsData a) -> Term s (PDataRecord (PFields (PAsData a)))
ptoFields = Term s a -> Term s (PDataRecord (PFields a))
forall (s :: S). Term s a -> Term s (PDataRecord (PFields a))
forall (a :: S -> Type) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields (Term s a -> Term s (PDataRecord (PFields a)))
-> (Term s (PAsData a) -> Term s a)
-> Term s (PAsData a)
-> Term s (PDataRecord (PFields a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData a) -> Term s a
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData

-- | The 'HRec' yielded by 'pletFields @fs t'.
type HRecOf t fs s =
  HRec
    ( BoundTerms
        (PFields t)
        (Bindings (PFields t) fs)
        s
    )

{- | Constrain an 'HRec' to contain the specified fields from the given Plutarch type.

=== Example ===

@
import qualified GHC.Generics as GHC
import Generics.SOP

import Plutarch.Prelude
import Plutarch.DataRepr

newtype PFooType s = PFooType (Term s (PDataRecord '["frst" ':= PInteger, "scnd" ':= PBool, "thrd" ':= PString]))
  deriving stock (GHC.Generic)
  deriving anyclass (Generic)
  deriving anyclass (PIsDataRepr)
  deriving
    (PlutusType, PIsData, PDataFields, PEq)
    via PIsDataReprInstances PFooType

foo :: PMemberFields PFooType '["scnd", "frst"] s as => HRec as -> Term s PInteger
foo h = pif (getField @"scnd" h) (getField @"frst" h) 0
@
-}
type PMemberFields :: (S -> Type) -> [Symbol] -> S -> [(Symbol, Type)] -> Constraint
type family PMemberFields t fs s as where
  PMemberFields _ '[] _ _ = ()
  PMemberFields t (name ': rest) s as = (PMemberField t name s as, PMemberFields t rest s as)

-- | Single field version of 'PMemberFields'.
type PMemberField :: (S -> Type) -> Symbol -> S -> [(Symbol, Type)] -> Constraint
type family PMemberField t name s as where
  PMemberField t name s as =
    ( IndexLabel name as ~ Term s (PAsData (PLookupLabel name (PFields t)))
    , ElemOf name (Term s (PAsData (PLookupLabel name (PFields t)))) as
    )

{- |
  Bind a HRec of named fields containing all the specified
  fields.
-}
pletFields ::
  forall fs a s b ps bs.
  ( PDataFields a
  , ps ~ PFields a
  , bs ~ Bindings ps fs
  , BindFields ps bs
  ) =>
  Term s a ->
  (HRecOf a fs s -> Term s b) ->
  Term s b
pletFields :: forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields Term s a
t =
  TermCont @b s (HRecOf a fs s)
-> (HRecOf a fs s -> Term s b) -> Term s b
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont @b s (HRecOf a fs s)
 -> (HRecOf a fs s -> Term s b) -> Term s b)
-> TermCont @b s (HRecOf a fs s)
-> (HRecOf a fs s -> Term s b)
-> Term s b
forall a b. (a -> b) -> a -> b
$
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @b s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @b s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @b s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$
      forall (a :: S -> Type) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields @a Term s a
t

data ToBind = Bind | Skip

{- | Get whether a field should be bound based on its inclusion in a
     list of fields.
-}
type family BindField (p :: Symbol) (fs :: [Symbol]) :: ToBind where
  BindField _ '[] = 'Skip
  BindField name (name ': _) = 'Bind
  BindField name (_ ': as) = BindField name as

-- | Map 'BindField' over @[PLabeledType]@, with 'Skips' removed at tail
type family Bindings (ps :: [PLabeledType]) (fs :: [Symbol]) :: [ToBind] where
  Bindings '[] _ = '[]
  Bindings ((name ':= _) ': ps) fs = BindField name fs ': CutSkip (Bindings ps fs)

-- | Remove 'Skip's at tail
type family CutSkip (bs :: [ToBind]) :: [ToBind] where
  CutSkip '[ 'Skip] = '[]
  CutSkip bs = bs

{- |
  Get the 'Term' representations to be bound based on the
  result of 'Bindings'.
-}
type BoundTerms :: [PLabeledType] -> [ToBind] -> S -> [(Symbol, Type)]
type family BoundTerms ps bs s where
  BoundTerms '[] _ _ = '[]
  BoundTerms _ '[] _ = '[]
  BoundTerms (_ ': ps) ('Skip ': bs) s = BoundTerms ps bs s
  BoundTerms ((name ':= p) ': ps) ('Bind ': bs) s = '(name, Term s (PAsData p)) ': BoundTerms ps bs s

class BindFields (ps :: [PLabeledType]) (bs :: [ToBind]) where
  -- |
  --    Bind all the fields in a 'PDataList' term to a corresponding
  --    HList of Terms.
  --
  --    A continuation is returned to enable sharing of
  --    the generated bound-variables.
  bindFields :: Proxy bs -> Term s (PDataRecord ps) -> TermCont s (HRec (BoundTerms ps bs s))

instance {-# OVERLAPPABLE #-} BindFields ((l ':= p) ': ps) ('Bind ': '[]) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] ((':) @ToBind 'Bind ('[] @ToBind))
-> Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':) @PLabeledType (l ':= p) ps)
           ((':) @ToBind 'Bind ('[] @ToBind))
           s))
bindFields Proxy @[ToBind] ((':) @ToBind 'Bind ('[] @ToBind))
_ Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t =
    HRec
  (BoundTerms
     ((':) @PLabeledType (l ':= p) ps)
     ((':) @ToBind 'Bind ('[] @ToBind))
     s)
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':) @PLabeledType (l ':= p) ps)
           ((':) @ToBind 'Bind ('[] @ToBind))
           s))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (HRec
   (BoundTerms
      ((':) @PLabeledType (l ':= p) ps)
      ((':) @ToBind 'Bind ('[] @ToBind))
      s)
 -> TermCont
      @r
      s
      (HRec
         (BoundTerms
            ((':) @PLabeledType (l ':= p) ps)
            ((':) @ToBind 'Bind ('[] @ToBind))
            s)))
-> HRec
     (BoundTerms
        ((':) @PLabeledType (l ':= p) ps)
        ((':) @ToBind 'Bind ('[] @ToBind))
        s)
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':) @PLabeledType (l ':= p) ps)
           ((':) @ToBind 'Bind ('[] @ToBind))
           s))
forall a b. (a -> b) -> a -> b
$ Labeled @Symbol l (Term s (PAsData p))
-> HRec ('[] @(Symbol, Type))
-> HRec
     ((':)
        @(Symbol, Type) '(l, Term s (PAsData p)) ('[] @(Symbol, Type)))
forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons (Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p))
forall {k} (sym :: k) a. a -> Labeled @k sym a
Labeled (Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p)))
-> Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 0
-> Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList @PLabeledType 0 ((':) @PLabeledType (l ':= p) ps))))
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 (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @0) Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t) HRec ('[] @(Symbol, Type))
HNil

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields ((l ':= p) ': ps) ('Bind ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] ((':) @ToBind 'Bind bs)
-> Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':) @PLabeledType (l ':= p) ps) ((':) @ToBind 'Bind bs) s))
bindFields Proxy @[ToBind] ((':) @ToBind 'Bind bs)
_ Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t = do
    Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t' <- ((Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps)))
forall (r :: S -> Type) (a :: S) b.
((b -> Term a r) -> Term a r) -> TermCont @r a b
TermCont (((Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))))
-> ((Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r s (Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps)))
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> (Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t
    HRec (BoundTerms ps bs s)
xs <- Proxy @[ToBind] bs
-> Term
     s
     (PDataRecord
        (Drop @PLabeledType 1 ((':) @PLabeledType (l ':= p) ps)))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           (Drop @PLabeledType 1 ((':) @PLabeledType (l ':= p) ps)) bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term
     s
     (PDataRecord
        (Drop @PLabeledType 1 ((':) @PLabeledType (l ':= p) ps)))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           (Drop @PLabeledType 1 ((':) @PLabeledType (l ':= p) ps)) bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Proxy @Nat 1
-> Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> Term
     s
     (PDataRecord
        (Drop @PLabeledType 1 ((':) @PLabeledType (l ':= p) ps)))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @1) Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t')
    HRec
  ((':)
     @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s))
-> TermCont
     @r
     s
     (HRec
        ((':)
           @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (HRec
   ((':)
      @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s))
 -> TermCont
      @r
      s
      (HRec
         ((':)
            @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s))))
-> HRec
     ((':)
        @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s))
-> TermCont
     @r
     s
     (HRec
        ((':)
           @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s)))
forall a b. (a -> b) -> a -> b
$ Labeled @Symbol l (Term s (PAsData p))
-> HRec (BoundTerms ps bs s)
-> HRec
     ((':)
        @(Symbol, Type) '(l, Term s (PAsData p)) (BoundTerms ps bs s))
forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons (Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p))
forall {k} (sym :: k) a. a -> Labeled @k sym a
Labeled (Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p)))
-> Term s (PAsData p) -> Labeled @Symbol l (Term s (PAsData p))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 0
-> Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList @PLabeledType 0 ((':) @PLabeledType (l ':= p) ps))))
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 (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @0) Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t') HRec (BoundTerms ps bs s)
xs

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': ps) ('Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] ((':) @ToBind 'Skip bs)
-> Term s (PDataRecord ((':) @PLabeledType p1 ps))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms ((':) @PLabeledType p1 ps) ((':) @ToBind 'Skip bs) s))
bindFields Proxy @[ToBind] ((':) @ToBind 'Skip bs)
_ Term s (PDataRecord ((':) @PLabeledType p1 ps))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 1
-> Term s (PDataRecord ((':) @PLabeledType p1 ps))
-> Term
     s (PDataRecord (Drop @PLabeledType 1 ((':) @PLabeledType p1 ps)))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @1) Term s (PDataRecord ((':) @PLabeledType p1 ps))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': ps) ('Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))
-> Term
     s (PDataRecord ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps)))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps))
           ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))
           s))
bindFields Proxy @[ToBind] ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))
_ Term
  s (PDataRecord ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps)))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 2
-> Term
     s (PDataRecord ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps)))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           2
           ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @2) Term
  s (PDataRecord ((':) @PLabeledType p1 ((':) @PLabeledType p2 ps)))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': p3 ': ps) ('Skip ': 'Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy
  @[ToBind]
  ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps))))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':)
              @PLabeledType
              p1
              ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps)))
           ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))
           s))
bindFields Proxy
  @[ToBind]
  ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))
_ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps))))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 3
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps))))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           3
           ((':)
              @PLabeledType
              p1
              ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps)))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @3) Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':) @PLabeledType p2 ((':) @PLabeledType p3 ps))))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': p3 ': p4 ': ps) ('Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps)))))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps))))
           ((':)
              @ToBind
              'Skip
              ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))
           s))
bindFields Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))
_ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps)))))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 4
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps)))))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           4
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps))))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @4) Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':) @PLabeledType p3 ((':) @PLabeledType p4 ps)))))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': ps) ('Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps))))))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps)))))
           ((':)
              @ToBind
              'Skip
              ((':)
                 @ToBind
                 'Skip
                 ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))
           s))
bindFields Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':) @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))
_ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps))))))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 5
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps))))))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           5
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps)))))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @5) Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':) @PLabeledType p4 ((':) @PLabeledType p5 ps))))))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': ps) ('Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':)
           @ToBind
           'Skip
           ((':)
              @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':)
                    @PLabeledType
                    p4
                    ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps)))))))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':)
                       @PLabeledType
                       p4
                       ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps))))))
           ((':)
              @ToBind
              'Skip
              ((':)
                 @ToBind
                 'Skip
                 ((':)
                    @ToBind
                    'Skip
                    ((':)
                       @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))))
           s))
bindFields Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':)
           @ToBind
           'Skip
           ((':)
              @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs))))))
_ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':)
                 @PLabeledType
                 p4
                 ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps)))))))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 6
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':)
                    @PLabeledType
                    p4
                    ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps)))))))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           6
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':)
                       @PLabeledType
                       p4
                       ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps))))))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @6) Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':)
                 @PLabeledType
                 p4
                 ((':) @PLabeledType p5 ((':) @PLabeledType p6 ps)))))))
t

instance {-# OVERLAPPABLE #-} BindFields ps bs => BindFields (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': p7 ': ps) ('Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': 'Skip ': bs) where
  bindFields :: forall {r :: S -> Type} (s :: S).
Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':)
           @ToBind
           'Skip
           ((':)
              @ToBind
              'Skip
              ((':)
                 @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':)
                    @PLabeledType
                    p4
                    ((':)
                       @PLabeledType
                       p5
                       ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps))))))))
-> TermCont
     @r
     s
     (HRec
        (BoundTerms
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':)
                       @PLabeledType
                       p4
                       ((':)
                          @PLabeledType
                          p5
                          ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps)))))))
           ((':)
              @ToBind
              'Skip
              ((':)
                 @ToBind
                 'Skip
                 ((':)
                    @ToBind
                    'Skip
                    ((':)
                       @ToBind
                       'Skip
                       ((':)
                          @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))))
           s))
bindFields Proxy
  @[ToBind]
  ((':)
     @ToBind
     'Skip
     ((':)
        @ToBind
        'Skip
        ((':)
           @ToBind
           'Skip
           ((':)
              @ToBind
              'Skip
              ((':)
                 @ToBind 'Skip ((':) @ToBind 'Skip ((':) @ToBind 'Skip bs)))))))
_ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':)
                 @PLabeledType
                 p4
                 ((':)
                    @PLabeledType
                    p5
                    ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps))))))))
t = do
    Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: S -> Type}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall {r :: S -> Type} (s :: S).
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall (t :: [ToBind]). Proxy @[ToBind] t
forall {k} (t :: k). Proxy @k t
Proxy @bs) (Term s (PDataRecord ps)
 -> TermCont @r s (HRec (BoundTerms ps bs s)))
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
forall a b. (a -> b) -> a -> b
$ Proxy @Nat 7
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           p1
           ((':)
              @PLabeledType
              p2
              ((':)
                 @PLabeledType
                 p3
                 ((':)
                    @PLabeledType
                    p4
                    ((':)
                       @PLabeledType
                       p5
                       ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps))))))))
-> Term
     s
     (PDataRecord
        (Drop
           @PLabeledType
           7
           ((':)
              @PLabeledType
              p1
              ((':)
                 @PLabeledType
                 p2
                 ((':)
                    @PLabeledType
                    p3
                    ((':)
                       @PLabeledType
                       p4
                       ((':)
                          @PLabeledType
                          p5
                          ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps)))))))))
forall (n :: Nat) (s :: S) (xs :: [PLabeledType]).
KnownNat n =>
Proxy @Nat n
-> Term s (PDataRecord xs)
-> Term s (PDataRecord (Drop @PLabeledType n xs))
pdropDataRecord (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @7) Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        p1
        ((':)
           @PLabeledType
           p2
           ((':)
              @PLabeledType
              p3
              ((':)
                 @PLabeledType
                 p4
                 ((':)
                    @PLabeledType
                    p5
                    ((':) @PLabeledType p6 ((':) @PLabeledType p7 ps))))))))
t

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

{- |
  Get a single field from a Term.

  *NB*: If you access more than one field from
  the same value you should use 'pletFields' instead,
  which will generate the bindings more efficiently.
-}
pfield ::
  forall name b p s a as n.
  ( PDataFields p
  , as ~ PFields p
  , n ~ PLabelIndex name as
  , KnownNat n
  , a ~ PUnLabel (IndexList n as)
  , PFromDataable a b
  ) =>
  Term s (p :--> b)
pfield :: forall (name :: Symbol) (b :: S -> Type) (p :: S -> Type) (s :: S)
       (a :: S -> Type) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: (S -> Type))
 ~ (PUnLabel (IndexList @PLabeledType n as) :: (S -> Type)),
 PFromDataable a b) =>
Term s (p :--> b)
pfield =
  let ()
_ = Proxy @Constraint ((n :: Nat) ~ (PLabelIndex name as :: Nat)) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(n ~ PLabelIndex name as))
   in (Term s p -> Term s b) -> Term s (p :--> b)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s b) -> Term s (c :--> b)
plam ((Term s p -> Term s b) -> Term s (p :--> b))
-> (Term s p -> Term s b) -> Term s (p :--> b)
forall a b. (a -> b) -> a -> b
$ \Term s p
i ->
        Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
-> Term s b
forall (s :: S).
Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
-> Term s b
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PFromDataable a b =>
Term s (PAsData a) -> Term s b
pmaybeFromAsData (Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
 -> Term s b)
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
-> Term s b
forall a b. (a -> b) -> a -> b
$ Proxy @Nat n
-> Term s (PDataRecord as)
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
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 (forall (t :: Nat). Proxy @Nat t
forall {k} (t :: k). Proxy @k t
Proxy @n) (Term s (PDataRecord as)
 -> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as))))
-> Term s (PDataRecord as)
-> Term s (PAsData (PUnLabel (IndexList @PLabeledType n as)))
forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields @p Term s p
i