{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Plutarch.Internal.ScottEncoding (PlutusTypeScott, PScottEncoded (PScottEncoded)) where

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 (PDelayed, PType, Term, pdelay, pforce, plam', plet, (#), (:-->))
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))

data PlutusTypeScott

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

type ScottFn :: [PType] -> PType -> PType
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 :: [[PType]] -> PType -> [PType]
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 (ScottFn (ScottList a r) r)
x
  pmatch' :: forall (s :: S) (b :: PType).
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 (forall (a :: [[PType]]) (r :: PType) (s :: S).
Term s (ScottFn (ScottList a r) r) -> PScottEncoded a r s
PScottEncoded Term s (PInner (PScottEncoded a r))
x)

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

newtype PLamL s b as = PLamL {forall (s :: S) (b :: PType) (as :: [PType]).
PLamL s b as
-> (NP @PType (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 :: [PType]) (s :: S) (b :: PType).
SListI @PType as =>
(NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL = forall (s :: S) (b :: PType) (as :: [PType]).
PLamL s b as
-> (NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b)
unPLamL forall a b. (a -> b) -> a -> b
$ forall {k} (xs :: [k]) (r :: [k] -> Type).
SListI @k xs =>
r ('[] @k)
-> (forall (y :: k) (ys :: [k]). SListI @k ys => r ((':) @k y ys))
-> r xs
case_SList (forall (s :: S) (b :: PType) (as :: [PType]).
((NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b))
-> PLamL s b as
PLamL \NP @PType (Term s) ('[] @PType) -> Term s b
f -> forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay forall a b. (a -> b) -> a -> b
$ NP @PType (Term s) ('[] @PType) -> Term s b
f forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) (forall (s :: S) (b :: PType) (as :: [PType]).
((NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b))
-> PLamL s b as
PLamL forall (as :: [PType]) (s :: S) (b :: PType).
SListI @PType as =>
(NP @PType (Term s) as -> Term s b) -> Term s (ScottFn' as b)
plamL')

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

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

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

newtype GPCon' s r as = GPCon' {forall (s :: S) (r :: PType) (as :: [[PType]]).
GPCon' s r as
-> NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (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 :: [[PType]]) (s :: S) (r :: PType).
SListI2 @PType as =>
NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as -> Term s r
gpcon' = forall (s :: S) (r :: PType) (as :: [[PType]]).
GPCon' s r as
-> NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as
-> Term s r
unGPCon' forall a b. (a -> b) -> a -> b
$ 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
cpara_SList (forall {k} (t :: k). Proxy @k t
Proxy @SListI) (forall (s :: S) (r :: PType) (as :: [[PType]]).
(NP @PType (Term s) (ScottList as r)
 -> NS @[PType] (NP @PType (Term s)) as -> Term s r)
-> GPCon' s r as
GPCon' \NP @PType (Term s) (ScottList ('[] @[PType]) r)
Nil -> \case {}) \(GPCon' NP @PType (Term s) (ScottList ys r)
-> NS @[PType] (NP @PType (Term s)) ys -> Term s r
prev) -> forall (s :: S) (r :: PType) (as :: [[PType]]).
(NP @PType (Term s) (ScottList as r)
 -> NS @[PType] (NP @PType (Term s)) as -> Term s r)
-> GPCon' s r as
GPCon' \(Term s x
arg :* NP @PType (Term s) xs
args) -> \case
  Z NP @PType (Term s) x
x -> forall (as :: [PType]) (s :: S) (r :: PType).
SListI @PType as =>
Term s (ScottFn as r) -> NP @PType (Term s) as -> Term s r
pappL Term s x
arg NP @PType (Term s) x
x
  S NS @[PType] (NP @PType (Term s)) xs
xs -> NP @PType (Term s) (ScottList ys r)
-> NS @[PType] (NP @PType (Term s)) ys -> Term s r
prev NP @PType (Term s) xs
args NS @[PType] (NP @PType (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 :: [[PType]]) (r :: PType) (s :: S).
(SListI @PType (ScottList as r), SListI2 @PType as) =>
SOP @PType (Term s) as -> Term s (PScottEncoded as r)
gpcon SOP @PType (Term s) as
fields' =
  forall (as :: [[PType]]) (s :: S) (r :: PType).
All @[PType] (SListI @PType) as =>
SOP @PType (Term s) as
-> (SOP @PType (Term s) as -> Term s r) -> Term s r
pletL SOP @PType (Term s) as
fields' \(SOP NS @[PType] (NP @PType (Term s)) as
fields) ->
    forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: [[PType]]) (r :: PType) (s :: S).
Term s (ScottFn (ScottList a r) r) -> PScottEncoded a r s
PScottEncoded forall a b. (a -> b) -> a -> b
$ forall (as :: [PType]) (s :: S) (b :: PType).
SListI @PType as =>
(NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL \NP @PType (Term s) (ScottList as r)
args -> (forall (as :: [[PType]]) (s :: S) (r :: PType).
SListI2 @PType as =>
NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as -> Term s r
gpcon' NP @PType (Term s) (ScottList as r)
args NS @[PType] (NP @PType (Term s)) as
fields :: Term s r)

newtype GPMatch' s r as = GPMatch' {forall (s :: S) (r :: PType) (as :: [[PType]]).
GPMatch' s r as
-> (SOP @PType (Term s) as -> Term s r)
-> NP @PType (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 :: [[PType]]) (r :: PType) (s :: S).
SListI2 @PType as =>
(SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
gpmatch' = forall (s :: S) (r :: PType) (as :: [[PType]]).
GPMatch' s r as
-> (SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
unGPMatch' forall a b. (a -> b) -> a -> b
$ 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
cpara_SList (forall {k} (t :: k). Proxy @k t
Proxy @SListI) (forall (s :: S) (r :: PType) (as :: [[PType]]).
((SOP @PType (Term s) as -> Term s r)
 -> NP @PType (Term s) (ScottList as r))
-> GPMatch' s r as
GPMatch' (forall a b. a -> b -> a
const forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil)) \(GPMatch' (SOP @PType (Term s) ys -> Term s r)
-> NP @PType (Term s) (ScottList ys r)
prev) -> forall (s :: S) (r :: PType) (as :: [[PType]]).
((SOP @PType (Term s) as -> Term s r)
 -> NP @PType (Term s) (ScottList as r))
-> GPMatch' s r as
GPMatch' \SOP @PType (Term s) ((':) @[PType] y ys) -> Term s r
f ->
  forall (as :: [PType]) (s :: S) (b :: PType).
SListI @PType as =>
(NP @PType (Term s) as -> Term s b) -> Term s (ScottFn as b)
plamL (\NP @PType (Term s) y
args -> SOP @PType (Term s) ((':) @[PType] y ys) -> Term s r
f (forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @PType (Term s) y
args)) forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* (SOP @PType (Term s) ys -> Term s r)
-> NP @PType (Term s) (ScottList ys r)
prev (\(SOP NS @[PType] (NP @PType (Term s)) ys
x) -> SOP @PType (Term s) ((':) @[PType] y ys) -> Term s r
f (forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[PType] (NP @PType (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 :: [[PType]]) (r :: PType) (s :: S).
(SListI @PType (ScottList as r), SListI2 @PType as) =>
Term s (PScottEncoded as r)
-> (SOP @PType (Term s) as -> Term s r) -> Term s r
gpmatch Term s (PScottEncoded as r)
x' SOP @PType (Term s) as -> Term s r
f = forall (a :: PType) (s :: S) (b :: PType).
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) -> forall (as :: [PType]) (s :: S) (r :: PType).
SListI @PType as =>
Term s (ScottFn as r) -> NP @PType (Term s) as -> Term s r
pappL Term s (ScottFn (ScottList as r) r)
x (forall (as :: [[PType]]) (r :: PType) (s :: S).
SListI2 @PType as =>
(SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
gpmatch' SOP @PType (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 :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (PlutusTypeScott :: Type)) =>
a s -> Term s (DerivedPInner PlutusTypeScott a)
derivedPCon a s
x = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall forall a b. (a -> b) -> a -> b
$ forall (as :: [[PType]]) (r :: PType) (s :: S).
(SListI @PType (ScottList as r), SListI2 @PType as) =>
SOP @PType (Term s) as -> Term s (PScottEncoded as r)
gpcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S).
PGeneric a =>
a s -> SOP @PType (Term s) (PCode a)
gpfrom a s
x
  derivedPMatch :: forall (a :: PType) (s :: S) (b :: PType).
(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 = forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (DerivedPInner PlutusTypeScott a)
x' \(PForall forall (x :: PType). Term s (PScottEncoded (PCode a) x)
x) -> forall (as :: [[PType]]) (r :: PType) (s :: S).
(SListI @PType (ScottList as r), SListI2 @PType as) =>
Term s (PScottEncoded as r)
-> (SOP @PType (Term s) as -> Term s r) -> Term s r
gpmatch forall (x :: PType). Term s (PScottEncoded (PCode a) x)
x (a s -> Term s b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PGeneric a =>
SOP @PType (Term s) (PCode a) -> a s
gpto)