{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}

module Plutarch.Extra.Field (pletAll, pletAllC) where

import GHC.TypeLits (Symbol)
import Plutarch.DataRepr.Internal.Field (
  BindFields,
  Bindings,
  BoundTerms,
  HRec,
  HRecOf,
  PDataFields (PFields),
 )

type family BindAll (ps :: [PLabeledType]) :: [Symbol] where
  BindAll '[] = '[]
  BindAll ((name ':= _) ': xs) = name : BindAll xs

{- | Same as `pletFields` but instead of specifiying fields, it will take all fields.

 @since 1.3.0
-}
pletAll ::
  forall (a :: S -> Type) (s :: S) (b :: S -> Type) (ps :: [PLabeledType]) bs.
  ( PDataFields a
  , ps ~ PFields a
  , bs ~ Bindings ps (BindAll ps)
  , BindFields ps bs
  ) =>
  Term s a ->
  (HRecOf a (BindAll ps) s -> Term s b) ->
  Term s b
pletAll :: forall (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps (BindAll ps),
 BindFields ps bs) =>
Term s a -> (HRecOf a (BindAll ps) s -> Term s b) -> Term s b
pletAll = forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(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 @(BindAll ps)

{- | TermCont version of `pletAll`

 @since 1.3.0
-}
pletAllC ::
  forall (a :: S -> Type) (s :: S) (b :: S -> Type) (ps :: [PLabeledType]) bs.
  ( PDataFields a
  , ps ~ PFields a
  , bs ~ Bindings ps (BindAll ps)
  , BindFields ps bs
  ) =>
  Term s a ->
  TermCont @b s (HRec (BoundTerms ps bs s))
pletAllC :: forall (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a, ps ~ PFields a, bs ~ Bindings ps (BindAll ps),
 BindFields ps bs) =>
Term s a -> TermCont s (HRec (BoundTerms ps bs s))
pletAllC = forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont s a
tcont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [Symbol]) (a :: S -> Type) (s :: S) (b :: S -> Type)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(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 @(BindAll ps)