{-# 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 (PIsData, pdata, pforgetData, pfromData)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.ListLike (phead, ptail)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PlutusType (
  PContravariant',
  PContravariant'',
  PCovariant',
  PCovariant'',
  PInner,
  PVariant',
  PVariant'',
  PlutusType,
  pcon,
  pcon',
  pmatch,
  pmatch',
 )
import Plutarch.Internal.Term (S, Term, plet, punsafeCoerce, (#), (#$))
import Plutarch.Repr.Internal (
  PRec (PRec, unPRec),
  PStruct (PStruct, unPStruct),
  RecTypePrettyError,
  StructSameRepr,
  UnTermRec,
  UnTermStruct,
  groupHandlers,
 )
import Plutarch.TermCont (pletC, unTermCont)

-- | @since WIP
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 WIP
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 WIP
instance (SListI2 struct, All2 PIsData 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) PIsData 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) PIsData 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 WIP
instance (SListI struct, All PIsData 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) PIsData 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) PIsData 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 WIP
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 WIP
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 WIP
instance PIsData (PDataRec struct)

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

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

-- | @since WIP
instance
  forall (a :: S -> Type) (struct' :: [Type]) (struct :: [S -> Type]).
  ( SOP.Generic (a Any)
  , '[struct'] ~ Code (a Any)
  , struct ~ UnTermRec struct'
  , All PIsData 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)

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

-- | @since WIP
instance
  forall (a :: S -> Type) (struct :: [[S -> Type]]).
  ( SOP.Generic (a Any)
  , struct ~ UnTermStruct (a Any)
  , All2 PIsData 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 PIsData struct =>
  PRec struct s ->
  Term s (PDataRec struct)
pconDataRec :: forall (struct :: [S -> Type]) (s :: S).
All @(S -> Type) PIsData struct =>
PRec struct s -> Term s (PDataRec struct)
pconDataRec (PRec NP @(S -> Type) (Term s) struct
xs) =
  let
    collapesdData :: CollapseTo
  @(S -> Type) @[S -> Type] (NP @(S -> Type)) (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) PIsData
-> (forall (a :: S -> Type).
    PIsData 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 @PIsData) (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 (PAsData a) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData a) -> Term s PData)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata) 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]
CollapseTo
  @(S -> Type) @[S -> Type] (NP @(S -> Type)) (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 PIsData struct) =>
  PStruct struct s ->
  Term s (PDataStruct struct)
pconDataStruct :: forall (struct :: [[S -> Type]]) (s :: S).
(SListI2 @(S -> Type) struct, All2 @(S -> Type) PIsData 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) PIsData
-> (forall (a :: S -> Type).
    PIsData 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 @PIsData) (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 (PAsData a) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData a) -> Term s PData)
-> (Term s a -> Term s (PAsData a)) -> Term s a -> Term s PData
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata) 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 PData -> Term s (PDataStruct struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s (PDataStruct struct))
-> Term s PData -> Term s (PDataStruct struct)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
 -> Term s PData)
-> Term s (PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
-> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s PInteger
-> Term
     s
     (PBuiltinList PData
      :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
forall (s :: S) (a :: 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 H s struct = H {forall (s :: S) (struct :: [S -> Type]).
H s struct
-> forall (r :: S -> Type).
   Term s (PBuiltinList PData)
   -> (PRec struct s -> Term s r) -> Term s r
unH :: forall r. Term s (PBuiltinList PData) -> (PRec struct s -> Term s r) -> Term s r}

pmatchDataRec ::
  forall (struct :: [S -> Type]) b s.
  All PIsData 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) PIsData 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 =
  let
    go :: forall y ys. PIsData y => H s ys -> H s (y ': ys)
    go :: forall (y :: S -> Type) (ys :: [S -> Type]).
PIsData y =>
H s ys -> H s ((':) @(S -> Type) y ys)
go (H forall (r :: S -> Type).
Term s (PBuiltinList PData) -> (PRec ys s -> Term s r) -> Term s r
rest) = (forall (r :: S -> Type).
 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).
 Term s (PBuiltinList PData)
 -> (PRec struct s -> Term s r) -> Term s r)
-> H s struct
H ((forall (r :: S -> Type).
  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).
    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
$ \Term s (PBuiltinList PData)
ds PRec ((':) @(S -> Type) y ys) s -> Term s r
cps ->
      let
        tail :: Term s (PBuiltinList PData)
tail = 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)
ds
        parsed :: Term s y
parsed = forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData @y (Term s (PAsData y) -> Term s y) -> Term s (PAsData y) -> Term s y
forall a b. (a -> b) -> a -> b
$ Term s PData -> Term s (PAsData y)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s PData -> Term s (PAsData y))
-> Term s PData -> Term s (PAsData y)
forall a b. (a -> b) -> a -> b
$ 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)
ds
       in
        Term s (PBuiltinList PData) -> (PRec ys s -> Term s r) -> Term s r
forall (r :: S -> Type).
Term s (PBuiltinList PData) -> (PRec ys s -> Term s r) -> Term s r
rest Term s (PBuiltinList PData)
tail ((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
cps (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 y
parsed 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 b) -> Term s b
record = H s struct
-> forall (r :: S -> Type).
   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).
   Term s (PBuiltinList PData)
   -> (PRec struct s -> Term s r) -> Term s r
unH (H s struct
 -> forall (r :: S -> Type).
    Term s (PBuiltinList PData)
    -> (PRec struct s -> Term s r) -> Term s r)
-> H s struct
-> forall (r :: S -> Type).
   Term s (PBuiltinList PData)
   -> (PRec struct s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PIsData
-> H s ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (PIsData y, All @(S -> Type) PIsData ys) =>
    H s ys -> H s ((':) @(S -> Type) y ys))
-> H s 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 PIsData
-> r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (PIsData y, All @(S -> Type) PIsData 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 @PIsData) ((forall (r :: S -> Type).
 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).
 Term s (PBuiltinList PData)
 -> (PRec struct s -> Term s r) -> Term s r)
-> H s struct
H ((forall (r :: S -> Type).
  Term s (PBuiltinList PData)
  -> (PRec ('[] @(S -> Type)) s -> Term s r) -> Term s r)
 -> H s ('[] @(S -> Type)))
-> (forall (r :: S -> Type).
    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
$ \Term s (PBuiltinList PData)
_ PRec ('[] @(S -> Type)) s -> Term s r
cps -> PRec ('[] @(S -> Type)) s -> Term s r
cps (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]).
(PIsData y, All @(S -> Type) PIsData ys) =>
H s ys -> H s ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
PIsData y =>
H s ys -> H s ((':) @(S -> Type) y ys)
go
   in
    Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> Term s b) -> Term s b
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)
x (Term s (PBuiltinList PData)
-> (PRec struct s -> Term s b) -> Term s b
`record` 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
-> (PStruct struct s -> Term s r)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct
unSBR ::
      Integer ->
      (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 PIsData 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) PIsData 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
  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'

  let
    go :: forall y ys. All PIsData y => StructureHandler s b ys -> StructureHandler s b (y ': ys)
    go :: forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
All @(S -> Type) PIsData y =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
go (StructureHandler Integer
-> (PStruct ys s -> Term s b)
-> NP @[S -> Type] (K @[S -> Type] (Integer, Term s b)) ys
rest) = (Integer
 -> (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
 -> (PStruct struct s -> Term s r)
 -> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct)
-> StructureHandler s r struct
StructureHandler ((Integer
  -> (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
    -> (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 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) PIsData 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
-> (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) (\(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) PIsData)
-> StructureHandler s b ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (All @(S -> Type) PIsData y,
     All @[S -> Type] (All @(S -> Type) PIsData) 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) PIsData)
-> r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (All @(S -> Type) PIsData y,
     All @[S -> Type] (All @(S -> Type) PIsData) 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 PIsData)) ((Integer
 -> (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
 -> (PStruct struct s -> Term s r)
 -> NP @[S -> Type] (K @[S -> Type] (Integer, Term s r)) struct)
-> StructureHandler s r struct
StructureHandler ((Integer
  -> (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
    -> (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
_ 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) PIsData y,
 All @[S -> Type] (All @(S -> Type) PIsData) ys) =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
All @(S -> Type) PIsData y =>
StructureHandler s b ys
-> StructureHandler s b ((':) @[S -> Type] y ys)
go

    handlers :: [(Integer, Term s b)]
    handlers :: [(Integer, Term s b)]
handlers = 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
-> (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
-> (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 PStruct struct s -> Term s b
f

  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 [(Integer, Term s b)]
handlers Term s PInteger
idx