{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Plutarch.Repr.Newtype (
DeriveAsNewtype (DeriveAsNewtype, unDeriveAsNewtype),
) where
import Data.Kind (Type)
import GHC.Exts (Any)
import Generics.SOP (
Code,
I (I),
NP (Nil, (:*)),
NS (Z),
SOP (SOP),
)
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (Head)
import Plutarch.Internal.PlutusType (
PContravariant',
PCovariant',
PInner,
PVariant',
PlutusType,
pcon',
pmatch',
)
import Plutarch.Internal.Term (S, Term)
newtype DeriveAsNewtype (a :: S -> Type) s = DeriveAsNewtype
{ forall (a :: S -> Type) (s :: S). DeriveAsNewtype a s -> a s
unDeriveAsNewtype :: a s
}
type family UnTermSingle (x :: Type) :: S -> Type where
UnTermSingle (Term _ a) = a
class (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt
instance (SOP.Generic (a s), Code (a s) ~ '[ '[Term s pt]]) => H s a pt
instance
forall (a :: S -> Type) (pt :: S -> Type).
( pt ~ UnTermSingle (Head (Head (Code (a Any))))
, forall s. H s a pt
) =>
PlutusType (DeriveAsNewtype a)
where
type PInner (DeriveAsNewtype a) = UnTermSingle (Head (Head (Code (a Any))))
type PCovariant' (DeriveAsNewtype a) = PCovariant' a
type PContravariant' (DeriveAsNewtype a) = PContravariant' a
type PVariant' (DeriveAsNewtype a) = PVariant' a
pcon' :: forall s. DeriveAsNewtype a s -> Term s (PInner (DeriveAsNewtype a))
pcon' :: forall (s :: S).
DeriveAsNewtype a s -> Term s (PInner (DeriveAsNewtype a))
pcon' (DeriveAsNewtype a s
x) =
case NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall {k} (f :: k -> Type) (x :: k).
NS @k f ((':) @k x ('[] @k)) -> f x
SOP.unZ (NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type)))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
forall a b. (a -> b) -> a -> b
$ SOP
@Type
I
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
SOP.unSOP (a s -> Rep (a s)
forall a. Generic a => a -> Rep a
SOP.from a s
x :: SOP I '[ '[Term s pt]]) of
(I x
x) :* NP @Type I xs
Nil -> x
Term s pt
x :: Term s pt
pmatch' :: forall s b. Term s (PInner (DeriveAsNewtype a)) -> (DeriveAsNewtype a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsNewtype a))
-> (DeriveAsNewtype a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsNewtype a))
x DeriveAsNewtype a s -> Term s b
f =
DeriveAsNewtype a s -> Term s b
f (a s -> DeriveAsNewtype a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsNewtype a s
DeriveAsNewtype (a s -> DeriveAsNewtype a s) -> a s -> DeriveAsNewtype a s
forall a b. (a -> b) -> a -> b
$ Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to ((NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
@Type
I
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
@Type
I
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
-> SOP
@Type
I
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z (NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type])))
-> NP @Type I ((':) @Type (Term s pt) ('[] @Type))
-> NS
@[Type]
(NP @Type I)
((':) @[Type] ((':) @Type (Term s pt) ('[] @Type)) ('[] @[Type]))
forall a b. (a -> b) -> a -> b
$ Term s (PInner (DeriveAsNewtype a))
-> I (Term s (PInner (DeriveAsNewtype a)))
forall a. a -> I a
I Term s (PInner (DeriveAsNewtype a))
x I (Term s (PInner (DeriveAsNewtype a)))
-> NP @Type I ('[] @Type)
-> NP
@Type
I
((':) @Type (Term s (PInner (DeriveAsNewtype a))) ('[] @Type))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I ('[] @Type)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) :: SOP I '[ '[Term s pt]]))