{-# 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)
newtype PDataStruct (struct :: [[S -> Type]]) (s :: S) = PDataStruct {forall (struct :: [[S -> Type]]) (s :: S).
PDataStruct struct s -> PStruct struct s
unPDataStruct :: PStruct struct s}
newtype PDataRec (struct :: [S -> Type]) (s :: S) = PDataRec {forall (struct :: [S -> Type]) (s :: S).
PDataRec struct s -> PRec struct s
unPDataRec :: PRec struct s}
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)
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)
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
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
instance PIsData (PDataRec struct)
instance PIsData (PDataStruct struct)
newtype DeriveAsDataRec (a :: S -> Type) s = DeriveAsDataRec {forall (a :: S -> Type) (s :: S). DeriveAsDataRec a s -> a s
unDeriveAsDataRec :: a s}
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)
newtype DeriveAsDataStruct (a :: S -> Type) s = DeriveAsDataStruct {forall (a :: S -> Type) (s :: S). DeriveAsDataStruct a s -> a s
unDeriveAsDataStruct :: a s}
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)
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
}
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
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