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

module Plutarch.Repr.Data (
  PDataStruct (PDataStruct, unPDataStruct),
  PDataRec (PDataRec, unPDataRec),
  DeriveAsDataRec (DeriveAsDataRec, unDeriveAsDataRec),
  DeriveAsDataStruct (DeriveAsDataStruct, unDeriveAsDataStruct),
) where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Exts (Any)
import Generics.SOP (
  All,
  All2,
  Code,
  K (K),
  NP (Nil, (:*)),
  NS (Z),
  SListI,
  SListI2,
  SOP (SOP),
 )
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (Head)
import Plutarch.Builtin.Data (
  PBuiltinList,
  PData,
  pasConstr,
  pconsBuiltin,
  pconstrBuiltin,
  pfstBuiltin,
  psndBuiltin,
 )
import Plutarch.Internal.Eq (PEq, (#==))
import Plutarch.Internal.IsData (PInnermostIsData, PIsData)
import Plutarch.Internal.Lift
import Plutarch.Internal.ListLike (phead, ptail)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  PContravariant',
  PContravariant'',
  PCovariant',
  PCovariant'',
  PInner,
  PVariant',
  PVariant'',
  PlutusType,
  pcon,
  pcon',
  pmatch,
  pmatch',
 )
import Plutarch.Internal.Term (
  InternalConfig (..),
  S,
  Term,
  pgetInternalConfig,
  phoistAcyclic,
  plet,
  pplaceholder,
  punsafeCoerce,
  pwithInternalConfig,
  (#),
  (#$),
 )
import Plutarch.Repr.Internal (
  PRec (PRec, unPRec),
  PStruct (PStruct, unPStruct),
  RecAsHaskell,
  RecTypePrettyError,
  StructSameRepr,
  UnTermRec,
  UnTermStruct,
  groupHandlers,
 )
import Plutarch.TermCont (pfindAllPlaceholders, pletC, unTermCont)
import PlutusLedgerApi.V3 qualified as PLA

type PInnermostIsDataDataRepr =
  PInnermostIsData
    ('Just "Data representation can only hold types whose inner most representation is PData")

-- | @since 1.10.0
newtype PDataStruct (struct :: [[S -> Type]]) (s :: S) = PDataStruct {forall (struct :: [[S -> Type]]) (s :: S).
PDataStruct struct s -> PStruct struct s
unPDataStruct :: PStruct struct s}

-- | @since 1.10.0
newtype PDataRec (struct :: [S -> Type]) (s :: S) = PDataRec {forall (struct :: [S -> Type]) (s :: S).
PDataRec struct s -> PRec struct s
unPDataRec :: PRec struct s}

-- | @since 1.10.0
instance (SListI2 struct, All2 PInnermostIsDataDataRepr struct) => PlutusType (PDataStruct struct) where
  type PInner (PDataStruct struct) = PData
  type PCovariant' (PDataStruct struct) = All2 PCovariant'' struct
  type PContravariant' (PDataStruct struct) = All2 PContravariant'' struct
  type PVariant' (PDataStruct struct) = All2 PVariant'' struct
  pcon' :: forall (s :: S).
PDataStruct struct s -> Term s (PInner (PDataStruct struct))
pcon' (PDataStruct PStruct struct s
x) = Term s (PDataStruct struct) -> Term s (PInner (PDataStruct struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PDataStruct struct)
 -> Term s (PInner (PDataStruct struct)))
-> Term s (PDataStruct struct)
-> Term s (PInner (PDataStruct struct))
forall a b. (a -> b) -> a -> b
$ PStruct struct s -> Term s (PDataStruct struct)
forall (struct :: [[S -> Type]]) (s :: S).
(SListI2 @(S -> Type) struct,
 All2 @(S -> Type) PInnermostIsDataDataRepr struct) =>
PStruct struct s -> Term s (PDataStruct struct)
pconDataStruct PStruct struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PDataStruct struct))
-> (PDataStruct struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PDataStruct struct))
x PDataStruct struct s -> Term s b
f = Term s (PDataStruct struct)
-> (PStruct struct s -> Term s b) -> Term s b
forall (struct :: [[S -> Type]]) (b :: S -> Type) (s :: S).
All2 @(S -> Type) PInnermostIsDataDataRepr struct =>
Term s (PDataStruct struct)
-> (PStruct struct s -> Term s b) -> Term s b
pmatchDataStruct (Term s (PInner (PDataStruct struct)) -> Term s (PDataStruct struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataStruct struct))
x) (PDataStruct struct s -> Term s b
f (PDataStruct struct s -> Term s b)
-> (PStruct struct s -> PDataStruct struct s)
-> PStruct struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct struct s -> PDataStruct struct s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PDataStruct struct s
PDataStruct)

-- | @since 1.10.0
instance (SListI struct, All PInnermostIsDataDataRepr struct) => PlutusType (PDataRec struct) where
  type PInner (PDataRec struct) = PBuiltinList PData
  type PCovariant' (PDataRec struct) = All PCovariant'' struct
  type PContravariant' (PDataRec struct) = All PContravariant'' struct
  type PVariant' (PDataRec struct) = All PVariant'' struct
  pcon' :: forall (s :: S).
PDataRec struct s -> Term s (PInner (PDataRec struct))
pcon' (PDataRec PRec struct s
x) = Term s (PDataRec struct) -> Term s (PInner (PDataRec struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PDataRec struct) -> Term s (PInner (PDataRec struct)))
-> Term s (PDataRec struct) -> Term s (PInner (PDataRec struct))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> Term s (PDataRec struct)
forall (struct :: [S -> Type]) (s :: S).
All @(S -> Type) PInnermostIsDataDataRepr struct =>
PRec struct s -> Term s (PDataRec struct)
pconDataRec PRec struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PDataRec struct))
-> (PDataRec struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PDataRec struct))
x PDataRec struct s -> Term s b
f = Term s (PDataRec struct) -> (PRec struct s -> Term s b) -> Term s b
forall (struct :: [S -> Type]) (b :: S -> Type) (s :: S).
All @(S -> Type) PInnermostIsDataDataRepr struct =>
Term s (PDataRec struct) -> (PRec struct s -> Term s b) -> Term s b
pmatchDataRec (Term s (PInner (PDataRec struct)) -> Term s (PDataRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PDataRec struct))
x) (PDataRec struct s -> Term s b
f (PDataRec struct s -> Term s b)
-> (PRec struct s -> PDataRec struct s)
-> PRec struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRec struct s -> PDataRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PDataRec struct s
PDataRec)

-- | @since 1.10.0
instance PEq (PDataStruct struct) where
  Term s (PDataStruct struct)
a #== :: forall (s :: S).
Term s (PDataStruct struct)
-> Term s (PDataStruct struct) -> Term s PBool
#== Term s (PDataStruct struct)
b = Term s (PDataStruct struct) -> Term s (PInner (PDataStruct struct))
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s (PDataStruct struct)
a Term s (PInner (PDataStruct struct))
-> Term s (PInner (PDataStruct struct)) -> Term s PBool
forall (s :: S).
Term s (PInner (PDataStruct struct))
-> Term s (PInner (PDataStruct struct)) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PDataStruct struct) -> Term s (PInner (PDataStruct struct))
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s (PDataStruct struct)
b

-- | @since 1.10.0
instance PEq (PDataRec struct) where
  Term s (PDataRec struct)
a #== :: forall (s :: S).
Term s (PDataRec struct)
-> Term s (PDataRec struct) -> Term s PBool
#== Term s (PDataRec struct)
b = Term s (PDataRec struct) -> Term s (PInner (PDataRec struct))
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s (PDataRec struct)
a Term s (PInner (PDataRec struct))
-> Term s (PInner (PDataRec struct)) -> Term s PBool
forall (s :: S).
Term s (PInner (PDataRec struct))
-> Term s (PInner (PDataRec struct)) -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PDataRec struct) -> Term s (PInner (PDataRec struct))
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s (PDataRec struct)
b

-- | @since 1.10.0
instance PIsData (PDataRec struct)

-- | @since 1.10.0
instance PIsData (PDataStruct struct)

{- |
@DeriveAsDataRec@ derives @PlutusType@ instances for given type as builtin list of Data. Unlike @PDataAsDataStruct@ above, this will
encode data as @List@. Similarly, only types with its innermost representation @PData@ is allowed for its fields.

One major difference is that @DeriveAsDataRec@ only allows single constructor as it does not encode the constructor index. When
attempted to use this strategy to a type with more than one constructor will result in type error with detailed explanation of the issue.

@PInner@ of defined type will be @PDataRec (struct :: [S -> Type])@ where @struct@ is product type of its structure. @PInner@ of @PDataRec struct@
is @PBuiltinList PData@.

It is almost always better to use @DeriveAsDataRec@ over @DeriveAsDataStruct@ when data type only have one constructor as it is more efficient
to work with on-chain. However, Plith(previously PlutusTx), by default, derives every datatype to use @Constr@. So, if a Plutarch type needs to remain
compatible with type defined in Plith, one needs to use @DeriveAsDataStruct@. This is why many single-constructor types are derived using
@DeriveAsDataStruct@ on plutarch-ledger-api.

Consult example below for defining custom data-encoded datatype:
@@
data PBobData (a :: S -> Type) (s :: S)
  = PBobData (Term s (PAsData a)) (Term s (PAsData PBool))
  deriving stock (Generic)
  deriving anyclass (SOP.Generic)
  deriving PlutusType via (DeriveAsDataRec (PBobData a))

pcon $ PBobData (pdata 10) (pdata pfalse) -- [#10, #false]
@@

 @since 1.10.0
-}
newtype DeriveAsDataRec (a :: S -> Type) s = DeriveAsDataRec {forall (a :: S -> Type) (s :: S). DeriveAsDataRec a s -> a s
unDeriveAsDataRec :: a s}

-- | @since 1.10.0
instance
  forall (a :: S -> Type) (struct' :: [Type]) (struct :: [S -> Type]).
  ( SOP.Generic (a Any)
  , '[struct'] ~ Code (a Any)
  , struct ~ UnTermRec struct'
  , All PInnermostIsDataDataRepr struct
  , SListI struct
  , forall s. StructSameRepr s a '[struct]
  , RecTypePrettyError (Code (a Any))
  ) =>
  PlutusType (DeriveAsDataRec a)
  where
  type PInner (DeriveAsDataRec a) = PDataRec (UnTermRec (Head (Code (a Any))))
  type PCovariant' (DeriveAsDataRec a) = PCovariant' a
  type PContravariant' (DeriveAsDataRec a) = PContravariant' a
  type PVariant' (DeriveAsDataRec a) = PVariant' a
  pcon' :: forall (s :: S).
DeriveAsDataRec a s -> Term s (PInner (DeriveAsDataRec a))
pcon' (DeriveAsDataRec a s
x) =
    PInner (DeriveAsDataRec a) s -> Term s (PInner (DeriveAsDataRec a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInner (DeriveAsDataRec a) s
 -> Term s (PInner (DeriveAsDataRec a)))
-> PInner (DeriveAsDataRec a) s
-> Term s (PInner (DeriveAsDataRec a))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> PDataRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PDataRec struct s
PDataRec (PRec struct s -> PDataRec struct s)
-> PRec struct s -> PDataRec struct s
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) struct -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (NP @(S -> Type) (Term s) struct -> PRec struct s)
-> NP @(S -> Type) (Term s) struct -> PRec struct s
forall a b. (a -> b) -> a -> b
$ NS
  @[S -> Type]
  (NP @(S -> Type) (Term s))
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NP @(S -> Type) (Term s) struct
forall {k} (f :: k -> Type) (x :: k).
NS @k f ((':) @k x ('[] @k)) -> f x
SOP.unZ (NS
   @[S -> Type]
   (NP @(S -> Type) (Term s))
   ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> NP @(S -> Type) (Term s) struct)
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NP @(S -> Type) (Term s) struct
forall a b. (a -> b) -> a -> b
$ SOP
  @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
SOP.unSOP (SOP
   @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> NS
      @[S -> Type]
      (NP @(S -> Type) (Term s))
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall a b. (a -> b) -> a -> b
$ SOP @Type I (Code (a s))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: Type -> Type) (g :: (S -> Type) -> Type)
       (xs :: [[Type]]) (ys :: [[S -> Type]]).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  (LiftedCoercible @Type @Type @(S -> Type) f g)
  xs
  ys =>
SOP @Type f xs -> SOP @(S -> Type) g ys
SOP.hcoerce (SOP @Type I (Code (a s))
 -> SOP
      @(S -> Type)
      (Term s)
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> SOP @Type I (Code (a s))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall a b. (a -> b) -> a -> b
$ a s -> SOP @Type I (Code (a s))
forall a. Generic a => a -> Rep a
SOP.from a s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsDataRec a))
-> (DeriveAsDataRec a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsDataRec a))
x DeriveAsDataRec a s -> Term s b
f =
    Term s (PInner (DeriveAsDataRec a))
-> (PInner (DeriveAsDataRec a) s -> Term s b) -> Term s b
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInner (DeriveAsDataRec a))
x (DeriveAsDataRec a s -> Term s b
f (DeriveAsDataRec a s -> Term s b)
-> (PDataRec struct s -> DeriveAsDataRec a s)
-> PDataRec struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsDataRec a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsDataRec a s
DeriveAsDataRec (a s -> DeriveAsDataRec a s)
-> (PDataRec struct s -> a s)
-> PDataRec struct s
-> DeriveAsDataRec a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to (Rep (a s) -> a s)
-> (PDataRec struct s -> Rep (a s)) -> PDataRec struct s -> a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP
  @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> Rep (a s)
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: (S -> Type) -> Type) (g :: Type -> Type)
       (xs :: [[S -> Type]]) (ys :: [[Type]]).
AllZipN
  @(S -> Type)
  @[[S -> Type]]
  @(S -> Type)
  @Type
  @[[S -> Type]]
  @[[Type]]
  (Prod @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)))
  (LiftedCoercible @(S -> Type) @Type @Type f g)
  xs
  ys =>
SOP @(S -> Type) f xs -> SOP @Type g ys
SOP.hcoerce (SOP
   @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> Rep (a s))
-> (PDataRec struct s
    -> SOP
         @(S -> Type)
         (Term s)
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PDataRec struct s
-> Rep (a s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS
  @[S -> Type]
  (NP @(S -> Type) (Term s))
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[S -> Type]
   (NP @(S -> Type) (Term s))
   ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> SOP
      @(S -> Type)
      (Term s)
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> (PDataRec struct s
    -> NS
         @[S -> Type]
         (NP @(S -> Type) (Term s))
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PDataRec struct s
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
forall (a :: [S -> Type] -> Type) (x :: [S -> Type])
       (xs :: [[S -> Type]]).
a x -> NS @[S -> Type] a ((':) @[S -> Type] x xs)
Z @_ @_ @'[]) (NP @(S -> Type) (Term s) struct
 -> NS
      @[S -> Type]
      (NP @(S -> Type) (Term s))
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> (PDataRec struct s -> NP @(S -> Type) (Term s) struct)
-> PDataRec struct s
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRec struct s -> NP @(S -> Type) (Term s) struct
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> NP @(S -> Type) (Term s) struct
unPRec (PRec struct s -> NP @(S -> Type) (Term s) struct)
-> (PDataRec struct s -> PRec struct s)
-> PDataRec struct s
-> NP @(S -> Type) (Term s) struct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDataRec struct s -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
PDataRec struct s -> PRec struct s
unPDataRec)

{- |
@DeriveAsDataStruct@ derives @PlutusType@ instances for the given type as Data structure, namely, using @Constr@ constructor
of the @Data@ type. Each constructor of the given type will have matching constructor index in the order of its definition.

Also, it is important to note that each fields can only contain term that has innermost representation of Data. Hence,
@PInteger@ is not allowed but @PAsData PInteger@ is allowed. Failure to follow this requirement will result in type error
with detailed explanation of the issue.

@PInner@ of defined type will be @PDataStruct (struct :: [[S -> Type]])@ where @struct@ is SOP type of its structure. Since @PInner@ of
@PDataStruct@ is @PData@, multiple data encoded structure can be nested without being wrapped in @PAsData@.

Consult example below for defining custom data-encoded datatype:
@@
data PBobData (a :: S -> Type) (s :: S)
  = PBobData (Term s (PAsData a)) (Term s (PAsData PBool))
  | PRobData (Term s (PAsData PByteString))
  deriving stock (Generic)
  deriving anyclass (SOP.Generic)
  deriving PlutusType via (DeriveAsDataStruct (PBobData a))

pcon $ PBobData (pdata 10) (pdata pfalse) -- Constr 0 [#10, #false]
pcon $ PRobData "hello" -- Constr 1 [#"hello"]
@@

 @since 1.10.0
-}
newtype DeriveAsDataStruct (a :: S -> Type) s = DeriveAsDataStruct {forall (a :: S -> Type) (s :: S). DeriveAsDataStruct a s -> a s
unDeriveAsDataStruct :: a s}

-- | @since 1.10.0
instance
  forall (a :: S -> Type) (struct :: [[S -> Type]]).
  ( SOP.Generic (a Any)
  , struct ~ UnTermStruct (a Any)
  , All2 PInnermostIsDataDataRepr struct
  , SListI2 struct
  , forall s. StructSameRepr s a struct
  ) =>
  PlutusType (DeriveAsDataStruct a)
  where
  type PInner (DeriveAsDataStruct a) = PDataStruct (UnTermStruct (a Any))
  type PCovariant' (DeriveAsDataStruct a) = PCovariant' a
  type PContravariant' (DeriveAsDataStruct a) = PContravariant' a
  type PVariant' (DeriveAsDataStruct a) = PVariant' a
  pcon' :: forall (s :: S).
DeriveAsDataStruct a s -> Term s (PInner (DeriveAsDataStruct a))
pcon' (DeriveAsDataStruct a s
x) =
    forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon @(PDataStruct (UnTermStruct (a Any))) (PDataStruct (UnTermStruct (a (Any @S))) s
 -> Term s (PDataStruct (UnTermStruct (a (Any @S)))))
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> Term s (PDataStruct (UnTermStruct (a (Any @S))))
forall a b. (a -> b) -> a -> b
$ PStruct (UnTermStruct (a (Any @S))) s
-> PDataStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PDataStruct struct s
PDataStruct (PStruct (UnTermStruct (a (Any @S))) s
 -> PDataStruct (UnTermStruct (a (Any @S))) s)
-> PStruct (UnTermStruct (a (Any @S))) s
-> PDataStruct (UnTermStruct (a (Any @S))) s
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
-> PStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
 -> PStruct (UnTermStruct (a (Any @S))) s)
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
-> PStruct (UnTermStruct (a (Any @S))) s
forall a b. (a -> b) -> a -> b
$ SOP @Type I (Code (a s))
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: Type -> Type) (g :: (S -> Type) -> Type)
       (xs :: [[Type]]) (ys :: [[S -> Type]]).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  (LiftedCoercible @Type @Type @(S -> Type) f g)
  xs
  ys =>
SOP @Type f xs -> SOP @(S -> Type) g ys
SOP.hcoerce (SOP @Type I (Code (a s))
 -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> SOP @Type I (Code (a s))
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall a b. (a -> b) -> a -> b
$ a s -> SOP @Type I (Code (a s))
forall a. Generic a => a -> Rep a
SOP.from a s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsDataStruct a))
-> (DeriveAsDataStruct a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsDataStruct a))
x DeriveAsDataStruct a s -> Term s b
f =
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch @(PDataStruct (UnTermStruct (a Any))) Term s (PInner (DeriveAsDataStruct a))
Term s (PDataStruct (UnTermStruct (a (Any @S))))
x (DeriveAsDataStruct a s -> Term s b
f (DeriveAsDataStruct a s -> Term s b)
-> (PDataStruct (UnTermStruct (a (Any @S))) s
    -> DeriveAsDataStruct a s)
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsDataStruct a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsDataStruct a s
DeriveAsDataStruct (a s -> DeriveAsDataStruct a s)
-> (PDataStruct (UnTermStruct (a (Any @S))) s -> a s)
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> DeriveAsDataStruct a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to (Rep (a s) -> a s)
-> (PDataStruct (UnTermStruct (a (Any @S))) s -> Rep (a s))
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))) -> Rep (a s)
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: (S -> Type) -> Type) (g :: Type -> Type)
       (xs :: [[S -> Type]]) (ys :: [[Type]]).
AllZipN
  @(S -> Type)
  @[[S -> Type]]
  @(S -> Type)
  @Type
  @[[S -> Type]]
  @[[Type]]
  (Prod @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)))
  (LiftedCoercible @(S -> Type) @Type @Type f g)
  xs
  ys =>
SOP @(S -> Type) f xs -> SOP @Type g ys
SOP.hcoerce (SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
 -> Rep (a s))
-> (PDataStruct (UnTermStruct (a (Any @S))) s
    -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> Rep (a s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct (UnTermStruct (a (Any @S))) s
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> SOP @(S -> Type) (Term s) struct
unPStruct (PStruct (UnTermStruct (a (Any @S))) s
 -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> (PDataStruct (UnTermStruct (a (Any @S))) s
    -> PStruct (UnTermStruct (a (Any @S))) s)
-> PDataStruct (UnTermStruct (a (Any @S))) s
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PDataStruct (UnTermStruct (a (Any @S))) s
-> PStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PDataStruct struct s -> PStruct struct s
unPDataStruct)

-- Helpers

-- NOTE: I'm intentionally not providing default ordering instance here because ordering of
-- product and sum types can be handled in various ways:
-- https://en.wikipedia.org/wiki/Total_order#Orders_on_the_Cartesian_product_of_totally_ordered_sets
-- If anyone can make convincing argument to support one over another, it can be done easily
-- instance (PlutusType (PDataRec struct), All PPartialOrd struct) => PPartialOrd (PDataRec struct) where
--   x #<= y = undefined
--   a #< b = undefined

pconDataRec ::
  forall (struct :: [S -> Type]) (s :: S).
  All PInnermostIsDataDataRepr struct =>
  PRec struct s ->
  Term s (PDataRec struct)
pconDataRec :: forall (struct :: [S -> Type]) (s :: S).
All @(S -> Type) PInnermostIsDataDataRepr struct =>
PRec struct s -> Term s (PDataRec struct)
pconDataRec (PRec NP @(S -> Type) (Term s) struct
xs) =
  let
    collapesdData :: [Term s PData]
    collapesdData :: [Term s PData]
collapesdData = NP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PData)
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> Type)) 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
SOP.hcollapse (NP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
 -> CollapseTo
      @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PData))
-> NP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
-> CollapseTo
     @(S -> Type) @[S -> Type] (NP @(S -> Type)) (Term s PData)
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PInnermostIsDataDataRepr
-> (forall (a :: S -> Type).
    PInnermostIsDataDataRepr a =>
    Term s a -> K @(S -> Type) (Term s PData) a)
-> NP @(S -> Type) (Term s) struct
-> NP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
forall {k} {l} (h :: (k -> Type) -> l -> Type)
       (c :: k -> Constraint) (xs :: l)
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
       (f' :: k -> Type).
(AllN @k @l (Prod @k @l h) c xs, HAp @k @l h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
SOP.hcmap (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PInnermostIsDataDataRepr) (Term s PData -> K @(S -> Type) (Term s PData) a
forall k a (b :: k). a -> K @k a b
K (Term s PData -> K @(S -> Type) (Term s PData) a)
-> (Term s a -> Term s PData)
-> Term s a
-> K @(S -> Type) (Term s PData) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s PData
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce) NP @(S -> Type) (Term s) struct
xs
    builtinList :: Term s (PBuiltinList PData)
builtinList = (Term s PData
 -> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData))
-> Term s (PBuiltinList PData)
-> [Term s PData]
-> Term s (PBuiltinList PData)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term s PData
x Term s (PBuiltinList PData)
xs -> Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (s :: S) (a :: S -> Type).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
xs) (AsHaskell (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant []) [Term s PData]
collapesdData
   in
    Term s (PBuiltinList PData) -> Term s (PDataRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PBuiltinList PData)
builtinList

pconDataStruct ::
  forall (struct :: [[S -> Type]]) (s :: S).
  (SListI2 struct, All2 PInnermostIsDataDataRepr struct) =>
  PStruct struct s ->
  Term s (PDataStruct struct)
pconDataStruct :: forall (struct :: [[S -> Type]]) (s :: S).
(SListI2 @(S -> Type) struct,
 All2 @(S -> Type) PInnermostIsDataDataRepr struct) =>
PStruct struct s -> Term s (PDataStruct struct)
pconDataStruct (PStruct SOP @(S -> Type) (Term s) struct
xs) =
  let
    collapesdData :: CollapseTo
  @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) (Term s PData)
collapesdData = SOP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
-> CollapseTo
     @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) (Term s PData)
forall (xs :: [[S -> Type]]) a.
SListIN @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) xs =>
SOP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) 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
SOP.hcollapse (SOP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
 -> CollapseTo
      @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) (Term s PData))
-> SOP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
-> CollapseTo
     @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) (Term s PData)
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PInnermostIsDataDataRepr
-> (forall (a :: S -> Type).
    PInnermostIsDataDataRepr a =>
    Term s a -> K @(S -> Type) (Term s PData) a)
-> SOP @(S -> Type) (Term s) struct
-> SOP @(S -> Type) (K @(S -> Type) (Term s PData)) struct
forall {k} {l} (h :: (k -> Type) -> l -> Type)
       (c :: k -> Constraint) (xs :: l)
       (proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
       (f' :: k -> Type).
(AllN @k @l (Prod @k @l h) c xs, HAp @k @l h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
SOP.hcmap (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PInnermostIsDataDataRepr) (Term s PData -> K @(S -> Type) (Term s PData) a
forall k a (b :: k). a -> K @k a b
K (Term s PData -> K @(S -> Type) (Term s PData) a)
-> (Term s a -> Term s PData)
-> Term s a
-> K @(S -> Type) (Term s PData) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s PData
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce) SOP @(S -> Type) (Term s) struct
xs
    builtinList :: Term s (PBuiltinList PData)
builtinList = (Term s PData
 -> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData))
-> Term s (PBuiltinList PData)
-> [Term s PData]
-> Term s (PBuiltinList PData)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term s PData
x Term s (PBuiltinList PData)
xs -> Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
forall (s :: S) (a :: S -> Type).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin Term s (PData :--> (PBuiltinList PData :--> PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
xs) (AsHaskell (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant []) [Term s PData]
CollapseTo
  @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) (Term s PData)
collapesdData
    idx :: Term s PInteger
idx = AsHaskell PInteger -> Term s PInteger
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (AsHaskell PInteger -> Term s PInteger)
-> AsHaskell PInteger -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) struct -> Int
forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
forall (f :: (S -> Type) -> Type) (xs :: [[S -> Type]]).
SOP @(S -> Type) f xs -> Int
SOP.hindex SOP @(S -> Type) (Term s) struct
xs
   in
    Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PDataStruct struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
 -> Term s (PDataStruct struct))
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PDataStruct struct)
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
idx Term
  s
  (PBuiltinList PData
   :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PBuiltinList PData)
builtinList

newtype PHB s struct struct' = PHB
  { forall (s :: S) (struct :: [S -> Type]) (struct' :: [S -> Type]).
PHB s struct struct'
-> Integer
-> (PRec struct' s -> PRec struct s)
-> (PRec struct s, Integer)
unPHB ::
      Integer ->
      (PRec struct' s -> PRec struct s) ->
      (PRec struct s, Integer)
  }

newtype H s struct = H
  { forall (s :: S) (struct :: [S -> Type]).
H s struct
-> forall (r :: S -> Type).
   Integer
   -> Term s (PBuiltinList PData)
   -> (Integer, Term s (PBuiltinList PData))
   -> (PRec struct s -> Term s r)
   -> Term s r
unH ::
      forall r.
      Integer ->
      Term s (PBuiltinList PData) ->
      (Integer, Term s (PBuiltinList PData)) ->
      (PRec struct s -> Term s r) ->
      Term s r
  }

pmatchDataRec ::
  forall (struct :: [S -> Type]) b s.
  All PInnermostIsDataDataRepr struct =>
  Term s (PDataRec struct) ->
  (PRec struct s -> Term s b) ->
  Term s b
pmatchDataRec :: forall (struct :: [S -> Type]) (b :: S -> Type) (s :: S).
All @(S -> Type) PInnermostIsDataDataRepr struct =>
Term s (PDataRec struct) -> (PRec struct s -> Term s b) -> Term s b
pmatchDataRec (Term s (PDataRec struct) -> Term s (PBuiltinList PData)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce -> Term s (PBuiltinList PData)
x) PRec struct s -> Term s b
f = (InternalConfig -> Term s b) -> Term s b
forall (s :: S) (a :: S -> Type).
(InternalConfig -> Term s a) -> Term s a
pgetInternalConfig ((InternalConfig -> Term s b) -> Term s b)
-> (InternalConfig -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \InternalConfig
cfg -> TermCont @b s (Term s b) -> Term s b
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ do
  let
    placeholderBuilder :: forall y ys. PHB s struct ys -> PHB s struct (y ': ys)
    placeholderBuilder :: forall (y :: S -> Type) (ys :: [S -> Type]).
PHB s struct ys -> PHB s struct ((':) @(S -> Type) y ys)
placeholderBuilder (PHB Integer -> (PRec ys s -> PRec struct s) -> (PRec struct s, Integer)
rest) = (Integer
 -> (PRec ((':) @(S -> Type) y ys) s -> PRec struct s)
 -> (PRec struct s, Integer))
-> PHB s struct ((':) @(S -> Type) y ys)
forall (s :: S) (struct :: [S -> Type]) (struct' :: [S -> Type]).
(Integer
 -> (PRec struct' s -> PRec struct s) -> (PRec struct s, Integer))
-> PHB s struct struct'
PHB ((Integer
  -> (PRec ((':) @(S -> Type) y ys) s -> PRec struct s)
  -> (PRec struct s, Integer))
 -> PHB s struct ((':) @(S -> Type) y ys))
-> (Integer
    -> (PRec ((':) @(S -> Type) y ys) s -> PRec struct s)
    -> (PRec struct s, Integer))
-> PHB s struct ((':) @(S -> Type) y ys)
forall a b. (a -> b) -> a -> b
$ \Integer
idx PRec ((':) @(S -> Type) y ys) s -> PRec struct s
g ->
      Integer -> (PRec ys s -> PRec struct s) -> (PRec struct s, Integer)
rest (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (\(PRec NP @(S -> Type) (Term s) ys
prev) -> PRec ((':) @(S -> Type) y ys) s -> PRec struct s
g (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
 -> PRec ((':) @(S -> Type) y ys) s)
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall a b. (a -> b) -> a -> b
$ Integer -> Term s y
forall (s :: S) (a :: S -> Type). Integer -> Term s a
pplaceholder Integer
idx Term s y
-> NP @(S -> Type) (Term s) ys
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @(S -> Type) (Term s) ys
prev))

    placeholder :: (PRec struct s, Integer)
    placeholder :: (PRec struct s, Integer)
placeholder = (PHB s struct struct
-> Integer
-> (PRec struct s -> PRec struct s)
-> (PRec struct s, Integer)
forall (s :: S) (struct :: [S -> Type]) (struct' :: [S -> Type]).
PHB s struct struct'
-> Integer
-> (PRec struct' s -> PRec struct s)
-> (PRec struct s, Integer)
unPHB (PHB s struct struct
 -> Integer
 -> (PRec struct s -> PRec struct s)
 -> (PRec struct s, Integer))
-> PHB s struct struct
-> Integer
-> (PRec struct s -> PRec struct s)
-> (PRec struct s, Integer)
forall a b. (a -> b) -> a -> b
$ PHB s struct ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PHB s struct ys -> PHB s struct ((':) @(S -> Type) y ys))
-> PHB s struct struct
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
SOP.para_SList ((Integer
 -> (PRec ('[] @(S -> Type)) s -> PRec struct s)
 -> (PRec struct s, Integer))
-> PHB s struct ('[] @(S -> Type))
forall (s :: S) (struct :: [S -> Type]) (struct' :: [S -> Type]).
(Integer
 -> (PRec struct' s -> PRec struct s) -> (PRec struct s, Integer))
-> PHB s struct struct'
PHB ((Integer
  -> (PRec ('[] @(S -> Type)) s -> PRec struct s)
  -> (PRec struct s, Integer))
 -> PHB s struct ('[] @(S -> Type)))
-> (Integer
    -> (PRec ('[] @(S -> Type)) s -> PRec struct s)
    -> (PRec struct s, Integer))
-> PHB s struct ('[] @(S -> Type))
forall a b. (a -> b) -> a -> b
$ \Integer
idx PRec ('[] @(S -> Type)) s -> PRec struct s
g -> (PRec ('[] @(S -> Type)) s -> PRec struct s
g (NP @(S -> Type) (Term s) ('[] @(S -> Type))
-> PRec ('[] @(S -> Type)) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil), Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) PHB s struct ys -> PHB s struct ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
SListI @(S -> Type) ys =>
PHB s struct ys -> PHB s struct ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
PHB s struct ys -> PHB s struct ((':) @(S -> Type) y ys)
placeholderBuilder) Integer
0 PRec struct s -> PRec struct s
forall a. a -> a
id

    placeholderApplied :: Term s b
placeholderApplied = InternalConfig -> Term s b -> Term s b
forall (s :: S) (a :: S -> Type).
InternalConfig -> Term s a -> Term s a
pwithInternalConfig (Bool -> InternalConfig
InternalConfig Bool
False) (Term s b -> Term s b) -> Term s b -> Term s b
forall a b. (a -> b) -> a -> b
$ PRec struct s -> Term s b
f ((PRec struct s, Integer) -> PRec struct s
forall a b. (a, b) -> a
fst (PRec struct s, Integer)
placeholder)

  [Integer]
usedFields <-
    if InternalConfig -> Bool
internalConfig'dataRecPMatchOptimization InternalConfig
cfg
      then Term s b -> TermCont @b s [Integer]
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s [Integer]
pfindAllPlaceholders Term s b
placeholderApplied
      else [Integer] -> TermCont @b s [Integer]
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [Integer
Item [Integer]
0 .. ((PRec struct s, Integer) -> Integer
forall a b. (a, b) -> b
snd (PRec struct s, Integer)
placeholder)]

  let
    -- Technically, we don't need @running@ here since we are pretty sure there's nothing using field
    -- that is not found in @usedFields@--because one can only @evalTerm@ closed terms and using bound field
    -- means free variable. I added it regardlessly.
    --
    -- Also, this can be easily tweaked to have different performance characteristics
    -- (i.e. CPU/MEM optimized or Size optimized).
    -- Currently, to balance off both, we hoist "dropToCurrent" function. However, it could be made to
    -- cost even less on CPU/MEM by not hoisting it. It is likely not a good trade off if there's a
    -- whole bunch of record deconstruction.
    go :: forall y ys. H s ys -> H s (y ': ys)
    go :: forall (y :: S -> Type) (ys :: [S -> Type]).
H s ys -> H s ((':) @(S -> Type) y ys)
go (H forall (r :: S -> Type).
Integer
-> Term s (PBuiltinList PData)
-> (Integer, Term s (PBuiltinList PData))
-> (PRec ys s -> Term s r)
-> Term s r
rest) =
      (forall (r :: S -> Type).
 Integer
 -> Term s (PBuiltinList PData)
 -> (Integer, Term s (PBuiltinList PData))
 -> (PRec ((':) @(S -> Type) y ys) s -> Term s r)
 -> Term s r)
-> H s ((':) @(S -> Type) y ys)
forall (s :: S) (struct :: [S -> Type]).
(forall (r :: S -> Type).
 Integer
 -> Term s (PBuiltinList PData)
 -> (Integer, Term s (PBuiltinList PData))
 -> (PRec struct s -> Term s r)
 -> Term s r)
-> H s struct
H ((forall (r :: S -> Type).
  Integer
  -> Term s (PBuiltinList PData)
  -> (Integer, Term s (PBuiltinList PData))
  -> (PRec ((':) @(S -> Type) y ys) s -> Term s r)
  -> Term s r)
 -> H s ((':) @(S -> Type) y ys))
-> (forall (r :: S -> Type).
    Integer
    -> Term s (PBuiltinList PData)
    -> (Integer, Term s (PBuiltinList PData))
    -> (PRec ((':) @(S -> Type) y ys) s -> Term s r)
    -> Term s r)
-> H s ((':) @(S -> Type) y ys)
forall a b. (a -> b) -> a -> b
$ \Integer
idx Term s (PBuiltinList PData)
running lastBind :: (Integer, Term s (PBuiltinList PData))
lastBind@(Integer
lastBindIdx, Term s (PBuiltinList PData)
lastBindT) PRec ((':) @(S -> Type) y ys) s -> Term s r
g ->
        if Integer
idx Integer -> [Integer] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Integer]
usedFields
          then
            let
              -- See if this is last field being used.
              lastBind :: Bool
lastBind = (Integer -> Bool) -> [Integer] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx) [Integer]
usedFields
              dropAmount :: Int
dropAmount = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lastBindIdx
              dropToCurrent' :: forall s'. Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
              dropToCurrent' :: forall (s' :: S).
Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
dropToCurrent' = ((Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
 -> (Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
 -> Term s' (PBuiltinList PData)
 -> Term s' (PBuiltinList PData))
-> (Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
-> [Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)]
-> Term s' (PBuiltinList PData)
-> Term s' (PBuiltinList PData)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
-> (Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
-> Term s' (PBuiltinList PData)
-> Term s' (PBuiltinList PData)
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
forall a. a -> a
id ([Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)]
 -> Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
-> [Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)]
-> Term s' (PBuiltinList PData)
-> Term s' (PBuiltinList PData)
forall a b. (a -> b) -> a -> b
$ Int
-> (Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData))
-> [Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)]
forall a. Int -> a -> [a]
replicate Int
dropAmount (Term s' (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail #)

              -- If this is last term, or amount of @ptail@ we need is less than 3, we don't hoist.
              currentTerm :: Term s (PBuiltinList PData)
currentTerm
                | Bool
lastBind Bool -> Bool -> Bool
|| Int
dropAmount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
3 = Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s' :: S).
Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
dropToCurrent' Term s (PBuiltinList PData)
lastBindT
                | Bool
otherwise = ClosedTerm (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((Term s (PBuiltinList PData) -> Term s (PBuiltinList PData))
-> Term s (PBuiltinList PData :--> PBuiltinList PData)
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 (PBuiltinList PData))
-> Term s (c :--> PBuiltinList PData)
plam Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s' :: S).
Term s' (PBuiltinList PData) -> Term s' (PBuiltinList PData)
dropToCurrent') Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
lastBindT
             in
              -- If this is the last field, we don't need to plet.
              (if Bool
lastBind then (\Term s (PBuiltinList PData)
a Term s (PBuiltinList PData) -> Term s r
h -> Term s (PBuiltinList PData) -> Term s r
h Term s (PBuiltinList PData)
a) else Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> 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 (PBuiltinList PData)
currentTerm ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> (Term s (PBuiltinList PData) -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (PBuiltinList PData)
newBind ->
                Integer
-> Term s (PBuiltinList PData)
-> (Integer, Term s (PBuiltinList PData))
-> (PRec ys s -> Term s r)
-> Term s r
forall (r :: S -> Type).
Integer
-> Term s (PBuiltinList PData)
-> (Integer, Term s (PBuiltinList PData))
-> (PRec ys s -> Term s r)
-> Term s r
rest
                  (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
                  (Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
running)
                  (Integer
idx, Term s (PBuiltinList PData)
newBind)
                  ((PRec ys s -> Term s r) -> Term s r)
-> (PRec ys s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \(PRec NP @(S -> Type) (Term s) ys
rest') -> PRec ((':) @(S -> Type) y ys) s -> Term s r
g (PRec ((':) @(S -> Type) y ys) s -> Term s r)
-> PRec ((':) @(S -> Type) y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
 -> PRec ((':) @(S -> Type) y ys) s)
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall a b. (a -> b) -> a -> b
$ Term s PData -> Term s y
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
newBind) Term s y
-> NP @(S -> Type) (Term s) ys
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @(S -> Type) (Term s) ys
rest'
          else Integer
-> Term s (PBuiltinList PData)
-> (Integer, Term s (PBuiltinList PData))
-> (PRec ys s -> Term s r)
-> Term s r
forall (r :: S -> Type).
Integer
-> Term s (PBuiltinList PData)
-> (Integer, Term s (PBuiltinList PData))
-> (PRec ys s -> Term s r)
-> Term s r
rest
            (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
            (Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
running)
            (Integer, Term s (PBuiltinList PData))
lastBind
            ((PRec ys s -> Term s r) -> Term s r)
-> (PRec ys s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \(PRec NP @(S -> Type) (Term s) ys
rest') -> PRec ((':) @(S -> Type) y ys) s -> Term s r
g (PRec ((':) @(S -> Type) y ys) s -> Term s r)
-> PRec ((':) @(S -> Type) y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
 -> PRec ((':) @(S -> Type) y ys) s)
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall a b. (a -> b) -> a -> b
$ Term s PData -> Term s y
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData :--> PData)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
running) Term s y
-> NP @(S -> Type) (Term s) ys
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @(S -> Type) (Term s) ys
rest'

    record :: Term s (PBuiltinList PData) -> (PRec struct s -> Term s r) -> Term s r
    record :: forall (r :: S -> Type).
Term s (PBuiltinList PData)
-> (PRec struct s -> Term s r) -> Term s r
record Term s (PBuiltinList PData)
ds = (H s struct
-> forall (r :: S -> Type).
   Integer
   -> Term s (PBuiltinList PData)
   -> (Integer, Term s (PBuiltinList PData))
   -> (PRec struct s -> Term s r)
   -> Term s r
forall (s :: S) (struct :: [S -> Type]).
H s struct
-> forall (r :: S -> Type).
   Integer
   -> Term s (PBuiltinList PData)
   -> (Integer, Term s (PBuiltinList PData))
   -> (PRec struct s -> Term s r)
   -> Term s r
unH (H s struct
 -> forall (r :: S -> Type).
    Integer
    -> Term s (PBuiltinList PData)
    -> (Integer, Term s (PBuiltinList PData))
    -> (PRec struct s -> Term s r)
    -> Term s r)
-> H s struct
-> forall (r :: S -> Type).
   Integer
   -> Term s (PBuiltinList PData)
   -> (Integer, Term s (PBuiltinList PData))
   -> (PRec struct s -> Term s r)
   -> Term s r
forall a b. (a -> b) -> a -> b
$ H s ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    H s ys -> H s ((':) @(S -> Type) y ys))
-> H s struct
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
SOP.para_SList ((forall (r :: S -> Type).
 Integer
 -> Term s (PBuiltinList PData)
 -> (Integer, Term s (PBuiltinList PData))
 -> (PRec ('[] @(S -> Type)) s -> Term s r)
 -> Term s r)
-> H s ('[] @(S -> Type))
forall (s :: S) (struct :: [S -> Type]).
(forall (r :: S -> Type).
 Integer
 -> Term s (PBuiltinList PData)
 -> (Integer, Term s (PBuiltinList PData))
 -> (PRec struct s -> Term s r)
 -> Term s r)
-> H s struct
H ((forall (r :: S -> Type).
  Integer
  -> Term s (PBuiltinList PData)
  -> (Integer, Term s (PBuiltinList PData))
  -> (PRec ('[] @(S -> Type)) s -> Term s r)
  -> Term s r)
 -> H s ('[] @(S -> Type)))
-> (forall (r :: S -> Type).
    Integer
    -> Term s (PBuiltinList PData)
    -> (Integer, Term s (PBuiltinList PData))
    -> (PRec ('[] @(S -> Type)) s -> Term s r)
    -> Term s r)
-> H s ('[] @(S -> Type))
forall a b. (a -> b) -> a -> b
$ \Integer
_ Term s (PBuiltinList PData)
_ (Integer, Term s (PBuiltinList PData))
_ PRec ('[] @(S -> Type)) s -> Term s r
g -> PRec ('[] @(S -> Type)) s -> Term s r
g (PRec ('[] @(S -> Type)) s -> Term s r)
-> PRec ('[] @(S -> Type)) s -> Term s r
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ('[] @(S -> Type))
-> PRec ('[] @(S -> Type)) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) H s ys -> H s ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
SListI @(S -> Type) ys =>
H s ys -> H s ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
H s ys -> H s ((':) @(S -> Type) y ys)
go) Integer
0 Term s (PBuiltinList PData)
ds (Integer
0, Term s (PBuiltinList PData)
ds)

  Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s b -> TermCont @b s (Term s b))
-> Term s b -> TermCont @b s (Term s b)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> (PRec struct s -> Term s b) -> Term s b
forall (r :: S -> Type).
Term s (PBuiltinList PData)
-> (PRec struct s -> Term s r) -> Term s r
record Term s (PBuiltinList PData)
x PRec struct s -> Term s b
f

newtype StructureHandler s r struct = StructureHandler
  { forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
StructureHandler s r struct
-> Integer
-> Term s (PBuiltinList PData)
-> (PStruct struct s -> Term s r)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct
unSBR ::
      Integer ->
      Term s (PBuiltinList PData) ->
      (PStruct struct s -> Term s r) ->
      NP (K (Integer, Term s r)) struct
  }

-- This is probably general enough to be used for non-Data encoded types
pmatchDataStruct ::
  forall (struct :: [[S -> Type]]) b s.
  All2 PInnermostIsDataDataRepr struct =>
  Term s (PDataStruct struct) ->
  (PStruct struct s -> Term s b) ->
  Term s b
pmatchDataStruct :: forall (struct :: [[S -> Type]]) (b :: S -> Type) (s :: S).
All2 @(S -> Type) PInnermostIsDataDataRepr struct =>
Term s (PDataStruct struct)
-> (PStruct struct s -> Term s b) -> Term s b
pmatchDataStruct (Term s (PDataStruct struct) -> Term s PData
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce -> Term s PData
x) PStruct struct s -> Term s b
f = TermCont @b s (Term s b) -> Term s b
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ do
  let
    go :: forall y ys. All PInnermostIsDataDataRepr y => StructureHandler s b ys -> StructureHandler s b (y ': ys)
    go :: forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
All @(S -> Type) PInnermostIsDataDataRepr y =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
go (StructureHandler Integer
-> Term s (PBuiltinList PData)
-> (PStruct ys s -> Term s b)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
rest) = (Integer
 -> Term s (PBuiltinList PData)
 -> (PStruct ((':) @[S -> Type] y ys) s -> Term s b)
 -> NP
      @[S -> Type]
      (K @[S -> Type] (Integer, Term s b))
      ((':) @[S -> Type] y ys))
-> StructureHandler s b ((':) @[S -> Type] y ys)
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
(Integer
 -> Term s (PBuiltinList PData)
 -> (PStruct struct s -> Term s r)
 -> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct)
-> StructureHandler s r struct
StructureHandler ((Integer
  -> Term s (PBuiltinList PData)
  -> (PStruct ((':) @[S -> Type] y ys) s -> Term s b)
  -> NP
       @[S -> Type]
       (K @[S -> Type] (Integer, Term s b))
       ((':) @[S -> Type] y ys))
 -> StructureHandler s b ((':) @[S -> Type] y ys))
-> (Integer
    -> Term s (PBuiltinList PData)
    -> (PStruct ((':) @[S -> Type] y ys) s -> Term s b)
    -> NP
         @[S -> Type]
         (K @[S -> Type] (Integer, Term s b))
         ((':) @[S -> Type] y ys))
-> StructureHandler s b ((':) @[S -> Type] y ys)
forall a b. (a -> b) -> a -> b
$ \Integer
i Term s (PBuiltinList PData)
ds PStruct ((':) @[S -> Type] y ys) s -> Term s b
cps ->
      let
        dataRecAsBuiltinList :: Term s (PBuiltinList PData) -> Term s (PDataRec y)
        dataRecAsBuiltinList :: Term s (PBuiltinList PData) -> Term s (PDataRec y)
dataRecAsBuiltinList = Term s (PBuiltinList PData) -> Term s (PDataRec y)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce

        handler :: Term s b
handler = forall (struct :: [S -> Type]) (b :: S -> Type) (s :: S).
All @(S -> Type) PInnermostIsDataDataRepr struct =>
Term s (PDataRec struct) -> (PRec struct s -> Term s b) -> Term s b
pmatchDataRec @y (Term s (PBuiltinList PData) -> Term s (PDataRec y)
dataRecAsBuiltinList Term s (PBuiltinList PData)
ds) ((PRec y s -> Term s b) -> Term s b)
-> (PRec y s -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \(PRec NP @(S -> Type) (Term s) y
r) -> PStruct ((':) @[S -> Type] y ys) s -> Term s b
cps (PStruct ((':) @[S -> Type] y ys) s -> Term s b)
-> PStruct ((':) @[S -> Type] y ys) s -> Term s b
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
-> PStruct ((':) @[S -> Type] y ys) s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
 -> PStruct ((':) @[S -> Type] y ys) s)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
-> PStruct ((':) @[S -> Type] y ys) s
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
 -> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys))
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) y
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @(S -> Type) (Term s) y
r
        restHandlers :: NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
restHandlers = Integer
-> Term s (PBuiltinList PData)
-> (PStruct ys s -> Term s b)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
rest (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Term s (PBuiltinList PData)
ds (\(PStruct (SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
sop)) -> PStruct ((':) @[S -> Type] y ys) s -> Term s b
cps (PStruct ((':) @[S -> Type] y ys) s -> Term s b)
-> PStruct ((':) @[S -> Type] y ys) s -> Term s b
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
-> PStruct ((':) @[S -> Type] y ys) s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
 -> PStruct ((':) @[S -> Type] y ys) s)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
-> PStruct ((':) @[S -> Type] y ys) s
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
 -> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys))
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
-> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys)
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
SOP.S NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
sop)
       in
        (Integer, Term s b) -> K @[S -> Type] (Integer, Term s b) y
forall k a (b :: k). a -> K @k a b
K (Integer
i, Term s b
handler) K @[S -> Type] (Integer, Term s b) y
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
-> NP
     @[S -> Type]
     (K @[S -> Type] (Integer, Term s b))
     ((':) @[S -> Type] y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
restHandlers

    -- This builds "handlers"--that is each cases of SOP data
    -- By building this we can figure out which cases share same computation, hence which branches to group
    handlers' :: StructureHandler s b struct
    handlers' :: StructureHandler s b struct
handlers' = Proxy
  @([S -> Type] -> Constraint)
  (All @(S -> Type) PInnermostIsDataDataRepr)
-> StructureHandler s b ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (All @(S -> Type) PInnermostIsDataDataRepr y,
     All @[S -> Type] (All @(S -> Type) PInnermostIsDataDataRepr) ys) =>
    StructureHandler s b ys
    -> StructureHandler s b ((':) @[S -> Type] y ys))
-> StructureHandler s b struct
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (r :: [k] -> Type).
All @k c xs =>
proxy c
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, All @k c ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (proxy :: ([S -> Type] -> Constraint) -> Type)
       (r :: [[S -> Type]] -> Type).
proxy (All @(S -> Type) PInnermostIsDataDataRepr)
-> r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (All @(S -> Type) PInnermostIsDataDataRepr y,
     All @[S -> Type] (All @(S -> Type) PInnermostIsDataDataRepr) ys) =>
    r ys -> r ((':) @[S -> Type] y ys))
-> r struct
SOP.cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [S -> Type] -> Constraint).
Proxy @([S -> Type] -> Constraint) t
Proxy @(All PInnermostIsDataDataRepr)) ((Integer
 -> Term s (PBuiltinList PData)
 -> (PStruct ('[] @[S -> Type]) s -> Term s b)
 -> NP
      @[S -> Type]
      (K @[S -> Type] (Integer, Term s b))
      ('[] @[S -> Type]))
-> StructureHandler s b ('[] @[S -> Type])
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
(Integer
 -> Term s (PBuiltinList PData)
 -> (PStruct struct s -> Term s r)
 -> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct)
-> StructureHandler s r struct
StructureHandler ((Integer
  -> Term s (PBuiltinList PData)
  -> (PStruct ('[] @[S -> Type]) s -> Term s b)
  -> NP
       @[S -> Type]
       (K @[S -> Type] (Integer, Term s b))
       ('[] @[S -> Type]))
 -> StructureHandler s b ('[] @[S -> Type]))
-> (Integer
    -> Term s (PBuiltinList PData)
    -> (PStruct ('[] @[S -> Type]) s -> Term s b)
    -> NP
         @[S -> Type]
         (K @[S -> Type] (Integer, Term s b))
         ('[] @[S -> Type]))
-> StructureHandler s b ('[] @[S -> Type])
forall a b. (a -> b) -> a -> b
$ \Integer
_ Term s (PBuiltinList PData)
_ PStruct ('[] @[S -> Type]) s -> Term s b
_ -> NP
  @[S -> Type]
  (K @[S -> Type] (Integer, Term s b))
  ('[] @[S -> Type])
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
(All @(S -> Type) PInnermostIsDataDataRepr y,
 All @[S -> Type] (All @(S -> Type) PInnermostIsDataDataRepr) ys) =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
All @(S -> Type) PInnermostIsDataDataRepr y =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
go

    handlers :: Term s (PBuiltinList PData) -> [(Integer, Term s b)]
    handlers :: Term s (PBuiltinList PData) -> [(Integer, Term s b)]
handlers Term s (PBuiltinList PData)
d = NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) struct
-> CollapseTo
     @[S -> Type] @[[S -> Type]] (NP @[S -> Type]) (Integer, Term s b)
forall (xs :: [[S -> Type]]) a.
SListIN @[S -> Type] @[[S -> Type]] (NP @[S -> Type]) xs =>
NP @[S -> Type] (K @[S -> Type] a) xs
-> CollapseTo @[S -> Type] @[[S -> Type]] (NP @[S -> Type]) 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
SOP.hcollapse (NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) struct
 -> CollapseTo
      @[S -> Type] @[[S -> Type]] (NP @[S -> Type]) (Integer, Term s b))
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) struct
-> CollapseTo
     @[S -> Type] @[[S -> Type]] (NP @[S -> Type]) (Integer, Term s b)
forall a b. (a -> b) -> a -> b
$ StructureHandler s b struct
-> Integer
-> Term s (PBuiltinList PData)
-> (PStruct struct s -> Term s b)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) struct
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
StructureHandler s r struct
-> Integer
-> Term s (PBuiltinList PData)
-> (PStruct struct s -> Term s r)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct
unSBR StructureHandler s b struct
handlers' Integer
0 Term s (PBuiltinList PData)
d PStruct struct s -> Term s b
f

  case Term s (PBuiltinList PData) -> [(Integer, Term s b)]
handlers (Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x) of
    [(Integer
_, Term s b
h)] -> Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s b
h
    [(Integer, Term s b)]
_ -> do
      Term s (PBuiltinPair PInteger (PBuiltinList PData))
x' <- Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @b s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      @b s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @b 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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
x
      Term s PInteger
idx <- Term s PInteger -> TermCont @b s (Term s PInteger)
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PInteger -> TermCont @b s (Term s PInteger))
-> Term s PInteger -> TermCont @b s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x'
      Term s (PBuiltinList PData)
ds <- Term s (PBuiltinList PData)
-> TermCont @b s (Term s (PBuiltinList PData))
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PBuiltinList PData)
 -> TermCont @b s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont @b s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
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 :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
x'

      Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s b -> TermCont @b s (Term s b))
-> Term s b -> TermCont @b s (Term s b)
forall a b. (a -> b) -> a -> b
$ [(Integer, Term s b)] -> Term s PInteger -> Term s b
forall (s :: S) (r :: S -> Type).
[(Integer, Term s r)] -> Term s PInteger -> Term s r
groupHandlers (Term s (PBuiltinList PData) -> [(Integer, Term s b)]
handlers Term s (PBuiltinList PData)
ds) Term s PInteger
idx

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

class (PLiftable a, PlutusRepr a ~ PLA.Data) => EachDataLiftable (a :: S -> Type)
instance (PLiftable a, PlutusRepr a ~ PLA.Data) => EachDataLiftable (a :: S -> Type)

class (a ~ AsHaskell b, PLiftable b, PlutusRepr b ~ PLA.Data) => ToAsHaskell (a :: Type) (b :: S -> Type)
instance (a ~ AsHaskell b, PLiftable b, PlutusRepr b ~ PLA.Data) => ToAsHaskell (a :: Type) (b :: S -> Type)

newtype PDataRecPLiftableHelper struct = PDataRecPLiftableHelper
  { forall (struct :: [S -> Type]).
PDataRecPLiftableHelper struct
-> [Data] -> Either LiftError (NP @Type I (RecAsHaskell struct))
unPDataRecPLiftableHelper :: [PLA.Data] -> Either LiftError (NP SOP.I (RecAsHaskell struct))
  }

-- | @since WIP
instance
  forall (struct :: [S -> Type]) (hstruct :: [Type]).
  ( SListI struct
  , All EachDataLiftable struct
  , All PInnermostIsDataDataRepr struct
  , hstruct ~ RecAsHaskell struct
  , SOP.AllZip ToAsHaskell hstruct struct
  ) =>
  PLiftable (PDataRec struct)
  where
  type AsHaskell (PDataRec struct) = SOP SOP.I '[RecAsHaskell struct]
  type PlutusRepr (PDataRec struct) = [PLA.Data]
  haskToRepr :: SOP SOP.I '[RecAsHaskell struct] -> [PLA.Data]
  haskToRepr :: SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
-> [Data]
haskToRepr SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
x =
    let
      g :: forall a b. ToAsHaskell a b => SOP.I a -> SOP.K PLA.Data b
      g :: forall a (b :: S -> Type).
ToAsHaskell a b =>
I a -> K @(S -> Type) Data b
g (SOP.I a
d) = PlutusRepr b -> K @(S -> Type) (PlutusRepr b) b
forall k a (b :: k). a -> K @k a b
SOP.K (PlutusRepr b -> K @(S -> Type) (PlutusRepr b) b)
-> PlutusRepr b -> K @(S -> Type) (PlutusRepr b) b
forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type). PLiftable a => AsHaskell a -> PlutusRepr a
haskToRepr @b a
AsHaskell b
d

      ds :: SOP (SOP.K PLA.Data) '[struct]
      ds :: SOP
  @(S -> Type)
  (K @(S -> Type) Data)
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
ds = Proxy @(Type -> (S -> Type) -> Constraint) ToAsHaskell
-> (forall a (b :: S -> Type).
    ToAsHaskell a b =>
    I a -> K @(S -> Type) Data b)
-> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
-> SOP
     @(S -> Type)
     (K @(S -> Type) Data)
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (c :: k1 -> k2 -> Constraint)
       (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> Type)
       (f :: k1 -> Type) (g :: k2 -> Type).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN @k1 @l1 @k1 @k2 @l1 @l2 (Prod @k1 @l1 h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
forall (c :: Type -> (S -> Type) -> Constraint) (xs :: [[Type]])
       (ys :: [[S -> Type]])
       (proxy :: (Type -> (S -> Type) -> Constraint) -> Type)
       (f :: Type -> Type) (g :: (S -> Type) -> Type).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  c
  xs
  ys =>
proxy c
-> (forall x (y :: S -> Type). c x y => f x -> g y)
-> SOP @Type f xs
-> SOP @(S -> Type) g ys
SOP.htrans (forall {k} (t :: k). Proxy @k t
forall (t :: Type -> (S -> Type) -> Constraint).
Proxy @(Type -> (S -> Type) -> Constraint) t
Proxy @ToAsHaskell) I x -> K @(S -> Type) Data y
forall a (b :: S -> Type).
ToAsHaskell a b =>
I a -> K @(S -> Type) Data b
g SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
x
     in
      SOP
  @(S -> Type)
  (K @(S -> Type) Data)
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> CollapseTo @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) Data
forall (xs :: [[S -> Type]]) a.
SListIN @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) xs =>
SOP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) 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
SOP.hcollapse SOP
  @(S -> Type)
  (K @(S -> Type) Data)
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
ds
  reprToPlut :: forall (s :: S).
PlutusRepr (PDataRec struct) -> PLifted s (PDataRec struct)
reprToPlut PlutusRepr (PDataRec struct)
x = Term s (PDataRec struct) -> PLifted s (PDataRec struct)
forall (s :: S) (a :: S -> Type). Term s a -> PLifted s a
mkPLifted (Term s (PDataRec struct) -> PLifted s (PDataRec struct))
-> Term s (PDataRec struct) -> PLifted s (PDataRec struct)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData) -> Term s (PDataRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PBuiltinList PData) -> Term s (PDataRec struct))
-> Term s (PBuiltinList PData) -> Term s (PDataRec struct)
forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @(PBuiltinList PData) PlutusRepr (PDataRec struct)
AsHaskell (PBuiltinList PData)
x
  plutToRepr :: (forall (s :: S). PLifted s (PDataRec struct))
-> Either LiftError (PlutusRepr (PDataRec struct))
plutToRepr forall (s :: S). PLifted s (PDataRec struct)
x = forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @(PBuiltinList PData) ((forall (s :: S). PLifted s (PBuiltinList PData))
 -> Either LiftError (PlutusRepr (PBuiltinList PData)))
-> (forall (s :: S). PLifted s (PBuiltinList PData))
-> Either LiftError (PlutusRepr (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ PLifted s (PDataRec struct) -> PLifted s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
PLifted s a -> PLifted s b
punsafeCoercePLifted PLifted s (PDataRec struct)
forall (s :: S). PLifted s (PDataRec struct)
x
  reprToHask :: [PLA.Data] -> Either LiftError (SOP SOP.I '[hstruct])
  reprToHask :: [Data]
-> Either
     LiftError (SOP @Type I ((':) @[Type] hstruct ('[] @[Type])))
reprToHask [Data]
x =
    let
      go :: forall y ys. EachDataLiftable y => PDataRecPLiftableHelper ys -> PDataRecPLiftableHelper (y ': ys)
      go :: forall (y :: S -> Type) (ys :: [S -> Type]).
EachDataLiftable y =>
PDataRecPLiftableHelper ys
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
go (PDataRecPLiftableHelper [Data] -> Either LiftError (NP @Type I (RecAsHaskell ys))
rest) = ([Data]
 -> Either
      LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (struct :: [S -> Type]).
([Data] -> Either LiftError (NP @Type I (RecAsHaskell struct)))
-> PDataRecPLiftableHelper struct
PDataRecPLiftableHelper (([Data]
  -> Either
       LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
 -> PDataRecPLiftableHelper ((':) @(S -> Type) y ys))
-> ([Data]
    -> Either
         LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
forall a b. (a -> b) -> a -> b
$ \case
        [] -> LiftError
-> Either
     LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys)))
forall a b. a -> Either a b
Left (LiftError
 -> Either
      LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
-> LiftError
-> Either
     LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys)))
forall a b. (a -> b) -> a -> b
$ Text -> LiftError
OtherLiftError Text
"Not enough fields are provided"
        (Data
d : [Data]
ds) -> do
          AsHaskell y
curr <- forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @y Data
PlutusRepr y
d
          NP @Type I (RecAsHaskell ys)
rest <- [Data] -> Either LiftError (NP @Type I (RecAsHaskell ys))
rest [Data]
ds

          NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
-> Either
     LiftError (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys)))
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
 -> Either
      LiftError
      (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))))
-> NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
-> Either
     LiftError (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys)))
forall a b. (a -> b) -> a -> b
$ AsHaskell y -> I (AsHaskell y)
forall a. a -> I a
SOP.I AsHaskell y
curr I (AsHaskell y)
-> NP @Type I (RecAsHaskell ys)
-> NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I (RecAsHaskell ys)
rest

      y :: PDataRecPLiftableHelper struct
      y :: PDataRecPLiftableHelper struct
y = Proxy @((S -> Type) -> Constraint) EachDataLiftable
-> PDataRecPLiftableHelper ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (EachDataLiftable y, All @(S -> Type) EachDataLiftable ys) =>
    PDataRecPLiftableHelper ys
    -> PDataRecPLiftableHelper ((':) @(S -> Type) y ys))
-> PDataRecPLiftableHelper struct
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> Type) (r :: [k] -> Type).
All @k c xs =>
proxy c
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, All @k c ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (proxy :: ((S -> Type) -> Constraint) -> Type)
       (r :: [S -> Type] -> Type).
proxy EachDataLiftable
-> r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (EachDataLiftable y, All @(S -> Type) EachDataLiftable ys) =>
    r ys -> r ((':) @(S -> Type) y ys))
-> r struct
SOP.cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @EachDataLiftable) (([Data]
 -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> PDataRecPLiftableHelper ('[] @(S -> Type))
forall (struct :: [S -> Type]).
([Data] -> Either LiftError (NP @Type I (RecAsHaskell struct)))
-> PDataRecPLiftableHelper struct
PDataRecPLiftableHelper (([Data]
  -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
 -> PDataRecPLiftableHelper ('[] @(S -> Type)))
-> ([Data]
    -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> PDataRecPLiftableHelper ('[] @(S -> Type))
forall a b. (a -> b) -> a -> b
$ Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
-> [Data]
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. a -> b -> a
const (Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
 -> [Data]
 -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
-> [Data]
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. (a -> b) -> a -> b
$ NP @Type I (RecAsHaskell ('[] @(S -> Type)))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. b -> Either a b
Right NP @Type I ('[] @Type)
NP @Type I (RecAsHaskell ('[] @(S -> Type)))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) PDataRecPLiftableHelper ys
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
(EachDataLiftable y, All @(S -> Type) EachDataLiftable ys) =>
PDataRecPLiftableHelper ys
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
EachDataLiftable y =>
PDataRecPLiftableHelper ys
-> PDataRecPLiftableHelper ((':) @(S -> Type) y ys)
go
     in
      NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
-> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP.SOP (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
 -> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> (NP @Type I (RecAsHaskell struct)
    -> NS
         @[Type]
         (NP @Type I)
         ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> NP @Type I (RecAsHaskell struct)
-> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP @Type I (RecAsHaskell struct)
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
SOP.Z (NP @Type I (RecAsHaskell struct)
 -> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> Either LiftError (NP @Type I (RecAsHaskell struct))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> PDataRecPLiftableHelper struct
-> [Data] -> Either LiftError (NP @Type I (RecAsHaskell struct))
forall (struct :: [S -> Type]).
PDataRecPLiftableHelper struct
-> [Data] -> Either LiftError (NP @Type I (RecAsHaskell struct))
unPDataRecPLiftableHelper PDataRecPLiftableHelper struct
y [Data]
x