{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-deprecations #-}

module Plutarch.Internal.ScottEncoding {-# DEPRECATED "Use the new mechanism instead" #-} (PlutusTypeScott, PScottEncoded (PScottEncoded)) where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Generics.SOP (
  All,
  NP (Nil, (:*)),
  NS (S, Z),
  SListI,
  SListI2,
  SOP (SOP),
  case_SList,
  cpara_SList,
  para_SList,
 )
import Plutarch.Internal.Generic (PCode, PGeneric, gpfrom, gpto)
import Plutarch.Internal.PlutusType (
  DerivedPInner,
  PInner,
  PlutusType,
  PlutusTypeStrat,
  PlutusTypeStratConstraint,
  derivedPCon,
  derivedPMatch,
  pcon,
  pcon',
  pmatch,
  pmatch',
 )
import Plutarch.Internal.Quantification (PForall (PForall))
import Plutarch.Internal.Term (
  PDelayed,
  S,
  Term,
  pdelay,
  pforce,
  plam',
  plet,
  (#),
  (:-->),
 )

data PlutusTypeScott

type ScottFn' :: [S -> Type] -> (S -> Type) -> (S -> Type)
type family ScottFn' xs r where
  ScottFn' '[] r = r
  ScottFn' (x ': xs) r = x :--> ScottFn' xs r

type ScottFn :: [S -> Type] -> (S -> Type) -> (S -> Type)
type family ScottFn xs r where
  ScottFn '[] r = PDelayed r
  ScottFn xs r = ScottFn' xs r

-- scottList l r = map (flip scottFn r) l
type ScottList :: [[S -> Type]] -> (S -> Type) -> [S -> Type]
type family ScottList code r where
  ScottList '[] _ = '[]
  ScottList (xs ': xss) r = ScottFn xs r ': ScottList xss r

newtype PScottEncoded a r s = PScottEncoded (Term s (ScottFn (ScottList a r) r))

instance PlutusType (PScottEncoded a r) where
  type PInner (PScottEncoded a r) = ScottFn (ScottList a r) r
  pcon' :: forall (s :: S).
PScottEncoded a r s -> Term s (PInner (PScottEncoded a r))
pcon' (PScottEncoded Term s (ScottFn (ScottList a r) r)
x) = Term s (PInner (PScottEncoded a r))
Term s (ScottFn (ScottList a r) r)
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PScottEncoded a r))
-> (PScottEncoded a r s -> Term s b) -> Term s b
pmatch' Term s (PInner (PScottEncoded a r))
x PScottEncoded a r s -> Term s b
f = PScottEncoded a r s -> Term s b
f (Term s (ScottFn (ScottList a r) r) -> PScottEncoded a r s
forall (a :: [[S -> Type]]) (r :: S -> Type) (s :: S).
Term s (ScottFn (ScottList a r) r) -> PScottEncoded a r s
PScottEncoded Term s (PInner (PScottEncoded a r))
Term s (ScottFn (ScottList a r) r)
x)

newtype PLamL' s b as = PLamL' {forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
PLamL' s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn' as b)
unPLamL' :: (NP (Term s) as -> Term s b) -> Term s (ScottFn' as b)}

-- Explicitly variadic `plam`.
plamL' :: SListI as => (NP (Term s) as -> Term s b) -> Term s (ScottFn' as b)
plamL' :: forall (as :: [S -> Type]) (s :: S) (b :: S -> Type).
SListI @(S -> Type) as =>
(NP @(S -> Type) (Term s) as -> Term s b) -> Term s (ScottFn' as b)
plamL' = PLamL' s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn' as b)
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
PLamL' s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn' as b)
unPLamL' (PLamL' s b as
 -> (NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn' as b))
-> PLamL' s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn' as b)
forall a b. (a -> b) -> a -> b
$ PLamL' s b ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PLamL' s b ys -> PLamL' s b ((':) @(S -> Type) y ys))
-> PLamL' s b as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    SListI @a ys =>
    r ys -> r ((':) @a y ys))
-> r xs
para_SList (((NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b)
 -> Term s (ScottFn' ('[] @(S -> Type)) b))
-> PLamL' s b ('[] @(S -> Type))
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
((NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn' as b))
-> PLamL' s b as
PLamL' \NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b
f -> NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) (\(PLamL' (NP @(S -> Type) (Term s) ys -> Term s b) -> Term s (ScottFn' ys b)
prev) -> ((NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b)
 -> Term s (ScottFn' ((':) @(S -> Type) y ys) b))
-> PLamL' s b ((':) @(S -> Type) y ys)
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
((NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn' as b))
-> PLamL' s b as
PLamL' \NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b
f -> (Term s y -> Term s (ScottFn' ys b))
-> Term s (y :--> ScottFn' ys b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' \Term s y
a -> (NP @(S -> Type) (Term s) ys -> Term s b) -> Term s (ScottFn' ys b)
prev \NP @(S -> Type) (Term s) ys
as -> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b
f (Term s y
a 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
as))

newtype PLamL s b as = PLamL {forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
PLamL s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn as b)
unPLamL :: (NP (Term s) as -> Term s b) -> Term s (ScottFn as b)}

-- `pdelay`s the 0-arity case.
plamL :: SListI as => (NP (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL :: forall (as :: [S -> Type]) (s :: S) (b :: S -> Type).
SListI @(S -> Type) as =>
(NP @(S -> Type) (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL = PLamL s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn as b)
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
PLamL s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn as b)
unPLamL (PLamL s b as
 -> (NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn as b))
-> PLamL s b as
-> (NP @(S -> Type) (Term s) as -> Term s b)
-> Term s (ScottFn as b)
forall a b. (a -> b) -> a -> b
$ PLamL s b ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PLamL s b ((':) @(S -> Type) y ys))
-> PLamL s b as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]). SListI @a ys => r ((':) @a y ys))
-> r xs
case_SList (((NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b)
 -> Term s (ScottFn ('[] @(S -> Type)) b))
-> PLamL s b ('[] @(S -> Type))
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
((NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn as b))
-> PLamL s b as
PLamL \NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b
f -> Term s b -> Term s (PDelayed b)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PDelayed a)
pdelay (Term s b -> Term s (PDelayed b))
-> Term s b -> Term s (PDelayed b)
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s b
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) (((NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b)
 -> Term s (ScottFn ((':) @(S -> Type) y ys) b))
-> PLamL s b ((':) @(S -> Type) y ys)
forall (s :: S) (b :: S -> Type) (as :: [S -> Type]).
((NP @(S -> Type) (Term s) as -> Term s b)
 -> Term s (ScottFn as b))
-> PLamL s b as
PLamL (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b)
-> Term s (ScottFn ((':) @(S -> Type) y ys) b)
(NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s b)
-> Term s (ScottFn' ((':) @(S -> Type) y ys) b)
forall (as :: [S -> Type]) (s :: S) (b :: S -> Type).
SListI @(S -> Type) as =>
(NP @(S -> Type) (Term s) as -> Term s b) -> Term s (ScottFn' as b)
plamL')

newtype PAppL' s r as = PAppL' {forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PAppL' s r as
-> Term s (ScottFn' as r)
-> NP @(S -> Type) (Term s) as
-> Term s r
unPAppL' :: Term s (ScottFn' as r) -> NP (Term s) as -> Term s r}

pappL' :: SListI as => Term s (ScottFn' as c) -> NP (Term s) as -> Term s c
pappL' :: forall (as :: [S -> Type]) (s :: S) (c :: S -> Type).
SListI @(S -> Type) as =>
Term s (ScottFn' as c) -> NP @(S -> Type) (Term s) as -> Term s c
pappL' = PAppL' s c as
-> Term s (ScottFn' as c)
-> NP @(S -> Type) (Term s) as
-> Term s c
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PAppL' s r as
-> Term s (ScottFn' as r)
-> NP @(S -> Type) (Term s) as
-> Term s r
unPAppL' (PAppL' s c as
 -> Term s (ScottFn' as c)
 -> NP @(S -> Type) (Term s) as
 -> Term s c)
-> PAppL' s c as
-> Term s (ScottFn' as c)
-> NP @(S -> Type) (Term s) as
-> Term s c
forall a b. (a -> b) -> a -> b
$ PAppL' s c ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PAppL' s c ys -> PAppL' s c ((':) @(S -> Type) y ys))
-> PAppL' s c as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    SListI @a ys =>
    r ys -> r ((':) @a y ys))
-> r xs
para_SList ((Term s (ScottFn' ('[] @(S -> Type)) c)
 -> NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s c)
-> PAppL' s c ('[] @(S -> Type))
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(Term s (ScottFn' as r) -> NP @(S -> Type) (Term s) as -> Term s r)
-> PAppL' s r as
PAppL' \Term s (ScottFn' ('[] @(S -> Type)) c)
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
Nil -> Term s c
Term s (ScottFn' ('[] @(S -> Type)) c)
f) (\(PAppL' Term s (ScottFn' ys c) -> NP @(S -> Type) (Term s) ys -> Term s c
prev) -> (Term s (ScottFn' ((':) @(S -> Type) y ys) c)
 -> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s c)
-> PAppL' s c ((':) @(S -> Type) y ys)
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(Term s (ScottFn' as r) -> NP @(S -> Type) (Term s) as -> Term s r)
-> PAppL' s r as
PAppL' \Term s (ScottFn' ((':) @(S -> Type) y ys) c)
f (Term s x
x :* NP @(S -> Type) (Term s) xs
xs) -> Term s (ScottFn' ys c) -> NP @(S -> Type) (Term s) ys -> Term s c
prev (Term s (x :--> ScottFn' ys c)
Term s (ScottFn' ((':) @(S -> Type) y ys) c)
f Term s (x :--> ScottFn' ys c) -> Term s x -> Term s (ScottFn' ys c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s x
x) NP @(S -> Type) (Term s) ys
NP @(S -> Type) (Term s) xs
xs)

newtype PAppL s r as = PAppL {forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PAppL s r as
-> Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
unPAppL :: Term s (ScottFn as r) -> NP (Term s) as -> Term s r}

pappL :: SListI as => Term s (ScottFn as r) -> NP (Term s) as -> Term s r
pappL :: forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
pappL = PAppL s r as
-> Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PAppL s r as
-> Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
unPAppL (PAppL s r as
 -> Term s (ScottFn as r)
 -> NP @(S -> Type) (Term s) as
 -> Term s r)
-> PAppL s r as
-> Term s (ScottFn as r)
-> NP @(S -> Type) (Term s) as
-> Term s r
forall a b. (a -> b) -> a -> b
$ PAppL s r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PAppL s r ((':) @(S -> Type) y ys))
-> PAppL s r as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]). SListI @a ys => r ((':) @a y ys))
-> r xs
case_SList ((Term s (ScottFn ('[] @(S -> Type)) r)
 -> NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r)
-> PAppL s r ('[] @(S -> Type))
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r)
-> PAppL s r as
PAppL \Term s (ScottFn ('[] @(S -> Type)) r)
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
Nil -> Term s (PDelayed r) -> Term s r
forall (s :: S) (a :: S -> Type). Term s (PDelayed a) -> Term s a
pforce Term s (PDelayed r)
Term s (ScottFn ('[] @(S -> Type)) r)
f) ((Term s (ScottFn ((':) @(S -> Type) y ys) r)
 -> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r)
-> PAppL s r ((':) @(S -> Type) y ys)
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r)
-> PAppL s r as
PAppL Term s (ScottFn ((':) @(S -> Type) y ys) r)
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
Term s (ScottFn' ((':) @(S -> Type) y ys) r)
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
forall (as :: [S -> Type]) (s :: S) (c :: S -> Type).
SListI @(S -> Type) as =>
Term s (ScottFn' as c) -> NP @(S -> Type) (Term s) as -> Term s c
pappL')

newtype PLetL s r as = PLetL {forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
unPLetL :: NP (Term s) as -> (NP (Term s) as -> Term s r) -> Term s r}

pletL' :: SListI as => NP (Term s) as -> (NP (Term s) as -> Term s r) -> Term s r
pletL' :: forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL' = PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
unPLetL (PLetL s r as
 -> NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r)
 -> Term s r)
-> PLetL s r as
-> NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ PLetL s r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    PLetL s r ys -> PLetL s r ((':) @(S -> Type) y ys))
-> PLetL s r as
forall {a} (xs :: [a]) (r :: [a] -> Type).
SListI @a xs =>
r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    SListI @a ys =>
    r ys -> r ((':) @a y ys))
-> r xs
para_SList
  ((NP @(S -> Type) (Term s) ('[] @(S -> Type))
 -> (NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r)
 -> Term s r)
-> PLetL s r ('[] @(S -> Type))
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r)
-> PLetL s r as
PLetL \NP @(S -> Type) (Term s) ('[] @(S -> Type))
Nil NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r
f -> NP @(S -> Type) (Term s) ('[] @(S -> Type)) -> Term s r
f NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil)
  \(PLetL NP @(S -> Type) (Term s) ys
-> (NP @(S -> Type) (Term s) ys -> Term s r) -> Term s r
prev) -> (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
 -> (NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r)
 -> Term s r)
-> PLetL s r ((':) @(S -> Type) y ys)
forall (s :: S) (r :: S -> Type) (as :: [S -> Type]).
(NP @(S -> Type) (Term s) as
 -> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r)
-> PLetL s r as
PLetL \(Term s x
x :* NP @(S -> Type) (Term s) xs
xs) NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
f -> Term s x -> (Term s x -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s x
x \Term s x
x' ->
    NP @(S -> Type) (Term s) ys
-> (NP @(S -> Type) (Term s) ys -> Term s r) -> Term s r
prev NP @(S -> Type) (Term s) ys
NP @(S -> Type) (Term s) xs
xs (\NP @(S -> Type) (Term s) ys
xs' -> NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys) -> Term s r
f (Term s x
x' Term s x
-> NP @(S -> Type) (Term s) ys
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) x 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
xs'))

pletL :: All SListI as => SOP (Term s) as -> (SOP (Term s) as -> Term s r) -> Term s r
pletL :: forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
All @[S -> Type] (SListI @(S -> Type)) as =>
SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL (SOP (Z NP @(S -> Type) (Term s) x
x)) SOP @(S -> Type) (Term s) as -> Term s r
f = NP @(S -> Type) (Term s) x
-> (NP @(S -> Type) (Term s) x -> Term s r) -> Term s r
forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
NP @(S -> Type) (Term s) as
-> (NP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL' NP @(S -> Type) (Term s) x
x \NP @(S -> Type) (Term s) x
x' -> SOP @(S -> Type) (Term s) as -> Term s r
f (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
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)) as
 -> SOP @(S -> Type) (Term s) as)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) x
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] x xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @(S -> Type) (Term s) x
x')
pletL (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs)) SOP @(S -> Type) (Term s) as -> Term s r
f = SOP @(S -> Type) (Term s) xs
-> (SOP @(S -> Type) (Term s) xs -> Term s r) -> Term s r
forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
All @[S -> Type] (SListI @(S -> Type)) as =>
SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL (NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
-> SOP @(S -> Type) (Term s) xs
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)) xs
xs) \(SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs') -> SOP @(S -> Type) (Term s) as -> Term s r
f (NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
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)) as
 -> SOP @(S -> Type) (Term s) as)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> SOP @(S -> Type) (Term s) as
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
-> NS
     @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] x xs)
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs')

newtype GPCon' s r as = GPCon' {forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> Term s r
unGPCon' :: NP (Term s) (ScottList as r) -> NS (NP (Term s)) as -> Term s r}

{- |
  `gpcon'`, given a *partial* scott encoding (as a `PLamL`) and a sum choice, applies
  that encoding to the sum choice.

  The partial encoding is any tail of the full scott encoded function, such that
  one of its elements corresponds to the sum choice.
-}
gpcon' :: SListI2 as => NP (Term s) (ScottList as r) -> NS (NP (Term s)) as -> Term s r
gpcon' :: forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
SListI2 @(S -> Type) as =>
NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as -> Term s r
gpcon' = GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> Term s r
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> Term s r
unGPCon' (GPCon' s r as
 -> NP @(S -> Type) (Term s) (ScottList as r)
 -> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
 -> Term s r)
-> GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as
-> Term s r
forall a b. (a -> b) -> a -> b
$ Proxy @([S -> Type] -> Constraint) (SListI @(S -> Type))
-> GPCon' s r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SListI @(S -> Type) y,
     All @[S -> Type] (SListI @(S -> Type)) ys) =>
    GPCon' s r ys -> GPCon' s r ((':) @[S -> Type] y ys))
-> GPCon' s r as
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 (SListI @(S -> Type))
-> r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SListI @(S -> Type) y,
     All @[S -> Type] (SListI @(S -> Type)) ys) =>
    r ys -> r ((':) @[S -> Type] y ys))
-> r as
cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [S -> Type] -> Constraint).
Proxy @([S -> Type] -> Constraint) t
Proxy @SListI) ((NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r)
 -> NS @[S -> Type] (NP @(S -> Type) (Term s)) ('[] @[S -> Type])
 -> Term s r)
-> GPCon' s r ('[] @[S -> Type])
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
(NP @(S -> Type) (Term s) (ScottList as r)
 -> NS @[S -> Type] (NP @(S -> Type) (Term s)) as -> Term s r)
-> GPCon' s r as
GPCon' \NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r)
Nil -> \case {}) \(GPCon' NP @(S -> Type) (Term s) (ScottList ys r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) ys -> Term s r
prev) -> (NP @(S -> Type) (Term s) (ScottList ((':) @[S -> Type] y ys) r)
 -> NS
      @[S -> Type] (NP @(S -> Type) (Term s)) ((':) @[S -> Type] y ys)
 -> Term s r)
-> GPCon' s r ((':) @[S -> Type] y ys)
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
(NP @(S -> Type) (Term s) (ScottList as r)
 -> NS @[S -> Type] (NP @(S -> Type) (Term s)) as -> Term s r)
-> GPCon' s r as
GPCon' \(Term s x
arg :* NP @(S -> Type) (Term s) xs
args) -> \case
  Z NP @(S -> Type) (Term s) x
x -> Term s (ScottFn x r) -> NP @(S -> Type) (Term s) x -> Term s r
forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
pappL Term s x
Term s (ScottFn x r)
arg NP @(S -> Type) (Term s) x
x
  S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs -> NP @(S -> Type) (Term s) (ScottList ys r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) ys -> Term s r
prev NP @(S -> Type) (Term s) xs
NP @(S -> Type) (Term s) (ScottList ys r)
args NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs

-- | Generic version of `pcon'`
gpcon ::
  forall as r s.
  (SListI (ScottList as r), SListI2 as) =>
  SOP (Term s) as ->
  Term s (PScottEncoded as r)
gpcon :: forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI @(S -> Type) (ScottList as r), SListI2 @(S -> Type) as) =>
SOP @(S -> Type) (Term s) as -> Term s (PScottEncoded as r)
gpcon SOP @(S -> Type) (Term s) as
fields' =
  SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s (PScottEncoded as r))
-> Term s (PScottEncoded as r)
forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
All @[S -> Type] (SListI @(S -> Type)) as =>
SOP @(S -> Type) (Term s) as
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
pletL SOP @(S -> Type) (Term s) as
fields' \(SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) as
fields) ->
    PScottEncoded as r s -> Term s (PScottEncoded as r)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PScottEncoded as r s -> Term s (PScottEncoded as r))
-> PScottEncoded as r s -> Term s (PScottEncoded as r)
forall a b. (a -> b) -> a -> b
$ Term s (ScottFn (ScottList as r) r) -> PScottEncoded as r s
forall (a :: [[S -> Type]]) (r :: S -> Type) (s :: S).
Term s (ScottFn (ScottList a r) r) -> PScottEncoded a r s
PScottEncoded (Term s (ScottFn (ScottList as r) r) -> PScottEncoded as r s)
-> Term s (ScottFn (ScottList as r) r) -> PScottEncoded as r s
forall a b. (a -> b) -> a -> b
$ (NP @(S -> Type) (Term s) (ScottList as r) -> Term s r)
-> Term s (ScottFn (ScottList as r) r)
forall (as :: [S -> Type]) (s :: S) (b :: S -> Type).
SListI @(S -> Type) as =>
(NP @(S -> Type) (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL \NP @(S -> Type) (Term s) (ScottList as r)
args -> (NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as -> Term s r
forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
SListI2 @(S -> Type) as =>
NP @(S -> Type) (Term s) (ScottList as r)
-> NS @[S -> Type] (NP @(S -> Type) (Term s)) as -> Term s r
gpcon' NP @(S -> Type) (Term s) (ScottList as r)
args NS @[S -> Type] (NP @(S -> Type) (Term s)) as
fields :: Term s r)

newtype GPMatch' s r as = GPMatch' {forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
GPMatch' s r as
-> (SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
unGPMatch' :: (SOP (Term s) as -> Term s r) -> NP (Term s) (ScottList as r)}

gpmatch' ::
  forall as r s.
  SListI2 as =>
  (SOP (Term s) as -> Term s r) ->
  NP (Term s) (ScottList as r)
gpmatch' :: forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
SListI2 @(S -> Type) as =>
(SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
gpmatch' = GPMatch' s r as
-> (SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
GPMatch' s r as
-> (SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
unGPMatch' (GPMatch' s r as
 -> (SOP @(S -> Type) (Term s) as -> Term s r)
 -> NP @(S -> Type) (Term s) (ScottList as r))
-> GPMatch' s r as
-> (SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
forall a b. (a -> b) -> a -> b
$ Proxy @([S -> Type] -> Constraint) (SListI @(S -> Type))
-> GPMatch' s r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SListI @(S -> Type) y,
     All @[S -> Type] (SListI @(S -> Type)) ys) =>
    GPMatch' s r ys -> GPMatch' s r ((':) @[S -> Type] y ys))
-> GPMatch' s r as
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 (SListI @(S -> Type))
-> r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SListI @(S -> Type) y,
     All @[S -> Type] (SListI @(S -> Type)) ys) =>
    r ys -> r ((':) @[S -> Type] y ys))
-> r as
cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [S -> Type] -> Constraint).
Proxy @([S -> Type] -> Constraint) t
Proxy @SListI) (((SOP @(S -> Type) (Term s) ('[] @[S -> Type]) -> Term s r)
 -> NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r))
-> GPMatch' s r ('[] @[S -> Type])
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
((SOP @(S -> Type) (Term s) as -> Term s r)
 -> NP @(S -> Type) (Term s) (ScottList as r))
-> GPMatch' s r as
GPMatch' (NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r)
-> (SOP @(S -> Type) (Term s) ('[] @[S -> Type]) -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r)
forall a b. a -> b -> a
const NP @(S -> Type) (Term s) ('[] @(S -> Type))
NP @(S -> Type) (Term s) (ScottList ('[] @[S -> Type]) r)
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil)) \(GPMatch' (SOP @(S -> Type) (Term s) ys -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList ys r)
prev) -> ((SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys) -> Term s r)
 -> NP @(S -> Type) (Term s) (ScottList ((':) @[S -> Type] y ys) r))
-> GPMatch' s r ((':) @[S -> Type] y ys)
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
((SOP @(S -> Type) (Term s) as -> Term s r)
 -> NP @(S -> Type) (Term s) (ScottList as r))
-> GPMatch' s r as
GPMatch' \SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys) -> Term s r
f ->
  (NP @(S -> Type) (Term s) y -> Term s r) -> Term s (ScottFn y r)
forall (as :: [S -> Type]) (s :: S) (b :: S -> Type).
SListI @(S -> Type) as =>
(NP @(S -> Type) (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL (\NP @(S -> Type) (Term s) y
args -> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys) -> Term s r
f (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
args)) Term s (ScottFn y r)
-> NP @(S -> Type) (Term s) (ScottList ys r)
-> NP
     @(S -> Type)
     (Term s)
     ((':) @(S -> Type) (ScottFn y r) (ScottList ys r))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* (SOP @(S -> Type) (Term s) ys -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList ys r)
prev (\(SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
x) -> SOP @(S -> Type) (Term s) ((':) @[S -> Type] y ys) -> Term s r
f (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)) 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)
S NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
x)))

gpmatch ::
  forall as r s.
  (SListI (ScottList as r), SListI2 as) =>
  Term s (PScottEncoded as r) ->
  (SOP (Term s) as -> Term s r) ->
  Term s r
gpmatch :: forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI @(S -> Type) (ScottList as r), SListI2 @(S -> Type) as) =>
Term s (PScottEncoded as r)
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
gpmatch Term s (PScottEncoded as r)
x' SOP @(S -> Type) (Term s) as -> Term s r
f = Term s (PScottEncoded as r)
-> (PScottEncoded as r s -> Term s r) -> Term s r
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 (PScottEncoded as r)
x' \(PScottEncoded Term s (ScottFn (ScottList as r) r)
x) -> Term s (ScottFn (ScottList as r) r)
-> NP @(S -> Type) (Term s) (ScottList as r) -> Term s r
forall (as :: [S -> Type]) (s :: S) (r :: S -> Type).
SListI @(S -> Type) as =>
Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
pappL Term s (ScottFn (ScottList as r) r)
x ((SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
SListI2 @(S -> Type) as =>
(SOP @(S -> Type) (Term s) as -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
gpmatch' SOP @(S -> Type) (Term s) as -> Term s r
f)

class SListI (ScottList (PCode a) r) => SListIScottList a r
instance SListI (ScottList (PCode a) r) => SListIScottList a r

class
  ( forall r. SListIScottList a r
  , SListI2 (PCode a)
  , PGeneric a
  ) =>
  PlutusTypeScottConstraint a
instance
  ( forall r. SListIScottList a r
  , SListI2 (PCode a)
  , PGeneric a
  ) =>
  PlutusTypeScottConstraint a

instance PlutusTypeStrat PlutusTypeScott where
  type PlutusTypeStratConstraint PlutusTypeScott = PlutusTypeScottConstraint
  type DerivedPInner PlutusTypeScott a = PForall (PScottEncoded (PCode a))
  derivedPCon :: forall (a :: S -> Type) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeScott :: Type)) =>
a s -> Term s (DerivedPInner PlutusTypeScott a)
derivedPCon a s
x = DerivedPInner PlutusTypeScott a s
-> Term s (DerivedPInner PlutusTypeScott a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (DerivedPInner PlutusTypeScott a s
 -> Term s (DerivedPInner PlutusTypeScott a))
-> DerivedPInner PlutusTypeScott a s
-> Term s (DerivedPInner PlutusTypeScott a)
forall a b. (a -> b) -> a -> b
$ (forall (x :: S -> Type). Term s (PScottEncoded (PCode a) x))
-> PForall @(S -> Type) (PScottEncoded (PCode a)) s
forall a (b :: a -> S -> Type) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall ((forall (x :: S -> Type). Term s (PScottEncoded (PCode a) x))
 -> PForall @(S -> Type) (PScottEncoded (PCode a)) s)
-> (forall (x :: S -> Type). Term s (PScottEncoded (PCode a) x))
-> PForall @(S -> Type) (PScottEncoded (PCode a)) s
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) (PCode a)
-> Term s (PScottEncoded (PCode a) x)
forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI @(S -> Type) (ScottList as r), SListI2 @(S -> Type) as) =>
SOP @(S -> Type) (Term s) as -> Term s (PScottEncoded as r)
gpcon (SOP @(S -> Type) (Term s) (PCode a)
 -> Term s (PScottEncoded (PCode a) x))
-> SOP @(S -> Type) (Term s) (PCode a)
-> Term s (PScottEncoded (PCode a) x)
forall a b. (a -> b) -> a -> b
$ a s -> SOP @(S -> Type) (Term s) (PCode a)
forall (a :: S -> Type) (s :: S).
PGeneric a =>
a s -> SOP @(S -> Type) (Term s) (PCode a)
gpfrom a s
x
  derivedPMatch :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeScott :: Type)) =>
Term s (DerivedPInner PlutusTypeScott a)
-> (a s -> Term s b) -> Term s b
derivedPMatch Term s (DerivedPInner PlutusTypeScott a)
x' a s -> Term s b
f = Term s (DerivedPInner PlutusTypeScott a)
-> (DerivedPInner PlutusTypeScott 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 (DerivedPInner PlutusTypeScott a)
x' \(PForall forall (x :: S -> Type).
Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) x)
x) -> Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) b)
-> (SOP
      @(S -> Type)
      (Term s)
      (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
    -> Term s b)
-> Term s b
forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI @(S -> Type) (ScottList as r), SListI2 @(S -> Type) as) =>
Term s (PScottEncoded as r)
-> (SOP @(S -> Type) (Term s) as -> Term s r) -> Term s r
gpmatch Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) b)
forall (x :: S -> Type).
Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) x)
x (a s -> Term s b
f (a s -> Term s b)
-> (SOP
      @(S -> Type)
      (Term s)
      (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
    -> a s)
-> SOP
     @(S -> Type)
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP
  @(S -> Type)
  (Term s)
  (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> a s
forall (a :: S -> Type) (s :: S).
PGeneric a =>
SOP @(S -> Type) (Term s) (PCode a) -> a s
gpto)