{-# 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.Proxy (Proxy (Proxy))
import GHC.TypeLits (
  KnownNat,
  Symbol,
 )

import Data.Kind (Constraint, Type)
import Plutarch (
  PInner,
  PType,
  S,
  Term,
  plam,
  plet,
  pto,
  (#),
  type (:-->),
 )

import Plutarch.Builtin (
  PAsData,
  PIsData,
  pfromData,
 )
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.Witness (witness)
import Plutarch.TermCont (TermCont (TermCont), runTermCont)

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

type family Helper (x :: PType) :: [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 :: PType) 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 = forall (a :: PType) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType). 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 = 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 = (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 = forall (a :: PType) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (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 :: PType -> [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 :: PType -> 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 :: PType) (s :: S) (b :: PType)
       (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 =
  forall (r :: PType) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont forall a b. (a -> b) -> a -> b
$
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$
      forall (a :: PType) (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 :: PType} (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 =
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons (forall {k} (sym :: k) a. a -> Labeled @k sym a
Labeled forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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' <- forall (r :: PType) (a :: S) b.
((b -> Term a r) -> Term a r) -> TermCont @r a b
TermCont forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t
    HRec (BoundTerms ps bs s)
xs <- forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) (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 {k} (t :: k). Proxy @k t
Proxy @1) Term s (PDataRecord ((':) @PLabeledType (l ':= p) ps))
t')
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) a (as1 :: [(Symbol, Type)]).
Labeled @Symbol name a
-> HRec as1 -> HRec ((':) @(Symbol, Type) '(name, a) as1)
HCons (forall {k} (sym :: k) a. a -> Labeled @k sym a
Labeled forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType} (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
    forall (ps :: [PLabeledType]) (bs :: [ToBind]) {r :: PType}
       (s :: S).
BindFields ps bs =>
Proxy @[ToBind] bs
-> Term s (PDataRecord ps)
-> TermCont @r s (HRec (BoundTerms ps bs s))
bindFields (forall {k} (t :: k). Proxy @k t
Proxy @bs) forall a b. (a -> b) -> a -> b
$ 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 {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 :: PType) (p :: PType) (s :: S)
       (a :: PType) (as :: [PLabeledType]) (n :: Nat).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield =
  let ()
_ = forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
Proxy @(n ~ PLabelIndex name as))
   in forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s p
i ->
        forall (a :: PType) (b :: PType) (s :: S).
PFromDataable a b =>
Term s (PAsData a) -> Term s b
pmaybeFromAsData forall a b. (a -> b) -> a -> b
$ 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 {k} (t :: k). Proxy @k t
Proxy @n) forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PDataFields a =>
Term s a -> Term s (PDataRecord (PFields a))
ptoFields @p Term s p
i