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

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

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' = PAppL' s c as
-> Term s (ScottFn' as c) -> NP @PType (Term s) as -> Term s c
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' (PAppL' s c as
 -> Term s (ScottFn' as c) -> NP @PType (Term s) as -> Term s c)
-> PAppL' s c as
-> Term s (ScottFn' as c)
-> NP @PType (Term s) as
-> Term s c
forall a b. (a -> b) -> a -> b
$ PAppL' s c ('[] @PType)
-> (forall (y :: PType) (ys :: [PType]).
    SListI @PType ys =>
    PAppL' s c ys -> PAppL' s c ((':) @PType y ys))
-> PAppL' s c as
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 ((Term s (ScottFn' ('[] @PType) c)
 -> NP @PType (Term s) ('[] @PType) -> Term s c)
-> PAppL' s c ('[] @PType)
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 c
Term s (ScottFn' ('[] @PType) c)
f) (\(PAppL' Term s (ScottFn' ys c) -> NP @PType (Term s) ys -> Term s c
prev) -> (Term s (ScottFn' ((':) @PType y ys) c)
 -> NP @PType (Term s) ((':) @PType y ys) -> Term s c)
-> PAppL' s c ((':) @PType y ys)
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 (x :--> ScottFn' ys c)
Term s (ScottFn' ((':) @PType y ys) c)
f Term s (x :--> ScottFn' ys c) -> Term s x -> Term s (ScottFn' ys c)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s x
x) NP @PType (Term s) ys
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 = PAppL s r as
-> Term s (ScottFn as r) -> NP @PType (Term s) as -> Term s r
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 (PAppL s r as
 -> Term s (ScottFn as r) -> NP @PType (Term s) as -> Term s r)
-> PAppL s r as
-> Term s (ScottFn as r)
-> NP @PType (Term s) as
-> Term s r
forall a b. (a -> b) -> a -> b
$ PAppL s r ('[] @PType)
-> (forall (y :: PType) (ys :: [PType]).
    SListI @PType ys =>
    PAppL s r ((':) @PType y ys))
-> PAppL s r as
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 ((Term s (ScottFn ('[] @PType) r)
 -> NP @PType (Term s) ('[] @PType) -> Term s r)
-> PAppL s r ('[] @PType)
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 -> Term s (PDelayed r) -> Term s r
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce Term s (PDelayed r)
Term s (ScottFn ('[] @PType) r)
f) ((Term s (ScottFn ((':) @PType y ys) r)
 -> NP @PType (Term s) ((':) @PType y ys) -> Term s r)
-> PAppL s r ((':) @PType y ys)
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) r)
-> NP @PType (Term s) ((':) @PType y ys) -> Term s r
Term s (ScottFn' ((':) @PType y ys) r)
-> NP @PType (Term s) ((':) @PType y ys) -> Term s r
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' = PLetL s r as
-> NP @PType (Term s) as
-> (NP @PType (Term s) as -> Term s r)
-> Term s r
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 (PLetL s r as
 -> NP @PType (Term s) as
 -> (NP @PType (Term s) as -> Term s r)
 -> Term s r)
-> PLetL s r as
-> NP @PType (Term s) as
-> (NP @PType (Term s) as -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ PLetL s r ('[] @PType)
-> (forall (y :: PType) (ys :: [PType]).
    SListI @PType ys =>
    PLetL s r ys -> PLetL s r ((':) @PType y ys))
-> PLetL s r as
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
  ((NP @PType (Term s) ('[] @PType)
 -> (NP @PType (Term s) ('[] @PType) -> Term s r) -> Term s r)
-> PLetL s r ('[] @PType)
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 NP @PType (Term s) ('[] @PType)
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) -> (NP @PType (Term s) ((':) @PType y ys)
 -> (NP @PType (Term s) ((':) @PType y ys) -> Term s r) -> Term s r)
-> PLetL s r ((':) @PType y ys)
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 -> Term s x -> (Term s x -> Term s r) -> Term s r
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) ys
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' Term s x
-> NP @PType (Term s) ys -> NP @PType (Term s) ((':) @PType x ys)
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 = NP @PType (Term s) x
-> (NP @PType (Term s) x -> Term s r) -> Term s r
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 (NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as)
-> NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as
forall a b. (a -> b) -> a -> b
$ NP @PType (Term s) x
-> NS @[PType] (NP @PType (Term s)) ((':) @[PType] x xs)
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 = SOP @PType (Term s) xs
-> (SOP @PType (Term s) xs -> Term s r) -> Term s r
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 (NS @[PType] (NP @PType (Term s)) xs -> SOP @PType (Term s) xs
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 (NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as)
-> NS @[PType] (NP @PType (Term s)) as -> SOP @PType (Term s) as
forall a b. (a -> b) -> a -> b
$ NS @[PType] (NP @PType (Term s)) xs
-> NS @[PType] (NP @PType (Term s)) ((':) @[PType] x xs)
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' = GPCon' s r as
-> NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as
-> Term s r
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' (GPCon' s r as
 -> NP @PType (Term s) (ScottList as r)
 -> NS @[PType] (NP @PType (Term s)) as
 -> Term s r)
-> GPCon' s r as
-> NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as
-> Term s r
forall a b. (a -> b) -> a -> b
$ Proxy @([PType] -> Constraint) (SListI @PType)
-> GPCon' s r ('[] @[PType])
-> (forall (y :: [PType]) (ys :: [[PType]]).
    (SListI @PType y, All @[PType] (SListI @PType) ys) =>
    GPCon' s r ys -> GPCon' s r ((':) @[PType] 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 :: ([PType] -> Constraint) -> Type)
       (r :: [[PType]] -> Type).
proxy (SListI @PType)
-> r ('[] @[PType])
-> (forall (y :: [PType]) (ys :: [[PType]]).
    (SListI @PType y, All @[PType] (SListI @PType) ys) =>
    r ys -> r ((':) @[PType] y ys))
-> r as
cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [PType] -> Constraint).
Proxy @([PType] -> Constraint) t
Proxy @SListI) ((NP @PType (Term s) (ScottList ('[] @[PType]) r)
 -> NS @[PType] (NP @PType (Term s)) ('[] @[PType]) -> Term s r)
-> GPCon' s r ('[] @[PType])
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) -> (NP @PType (Term s) (ScottList ((':) @[PType] y ys) r)
 -> NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
 -> Term s r)
-> GPCon' s r ((':) @[PType] y ys)
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 -> Term s (ScottFn x r) -> NP @PType (Term s) x -> Term s r
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
Term s (ScottFn x r)
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
NP @PType (Term s) (ScottList ys r)
args NS @[PType] (NP @PType (Term s)) ys
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' =
  SOP @PType (Term s) as
-> (SOP @PType (Term s) as -> Term s (PScottEncoded as r))
-> Term s (PScottEncoded as r)
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) ->
    PScottEncoded as r s -> Term s (PScottEncoded as r)
forall (a :: PType) (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 :: [[PType]]) (r :: PType) (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 @PType (Term s) (ScottList as r) -> Term s r)
-> Term s (ScottFn (ScottList as r) r)
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 -> (NP @PType (Term s) (ScottList as r)
-> NS @[PType] (NP @PType (Term s)) as -> Term s r
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' = GPMatch' s r as
-> (SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
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' (GPMatch' s r as
 -> (SOP @PType (Term s) as -> Term s r)
 -> NP @PType (Term s) (ScottList as r))
-> GPMatch' s r as
-> (SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
forall a b. (a -> b) -> a -> b
$ Proxy @([PType] -> Constraint) (SListI @PType)
-> GPMatch' s r ('[] @[PType])
-> (forall (y :: [PType]) (ys :: [[PType]]).
    (SListI @PType y, All @[PType] (SListI @PType) ys) =>
    GPMatch' s r ys -> GPMatch' s r ((':) @[PType] 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 :: ([PType] -> Constraint) -> Type)
       (r :: [[PType]] -> Type).
proxy (SListI @PType)
-> r ('[] @[PType])
-> (forall (y :: [PType]) (ys :: [[PType]]).
    (SListI @PType y, All @[PType] (SListI @PType) ys) =>
    r ys -> r ((':) @[PType] y ys))
-> r as
cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: [PType] -> Constraint).
Proxy @([PType] -> Constraint) t
Proxy @SListI) (((SOP @PType (Term s) ('[] @[PType]) -> Term s r)
 -> NP @PType (Term s) (ScottList ('[] @[PType]) r))
-> GPMatch' s r ('[] @[PType])
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' (NP @PType (Term s) (ScottList ('[] @[PType]) r)
-> (SOP @PType (Term s) ('[] @[PType]) -> Term s r)
-> NP @PType (Term s) (ScottList ('[] @[PType]) r)
forall a b. a -> b -> a
const NP @PType (Term s) ('[] @PType)
NP @PType (Term s) (ScottList ('[] @[PType]) r)
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) -> ((SOP @PType (Term s) ((':) @[PType] y ys) -> Term s r)
 -> NP @PType (Term s) (ScottList ((':) @[PType] y ys) r))
-> GPMatch' s r ((':) @[PType] y ys)
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 ->
  (NP @PType (Term s) y -> Term s r) -> Term s (ScottFn y r)
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 (NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
-> SOP @PType (Term s) ((':) @[PType] y ys)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
 -> SOP @PType (Term s) ((':) @[PType] y ys))
-> NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
-> SOP @PType (Term s) ((':) @[PType] y ys)
forall a b. (a -> b) -> a -> b
$ NP @PType (Term s) y
-> NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @PType (Term s) y
args)) Term s (ScottFn y r)
-> NP @PType (Term s) (ScottList ys r)
-> NP @PType (Term s) ((':) @PType (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 @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 (NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
-> SOP @PType (Term s) ((':) @[PType] y ys)
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[PType] (NP @PType (Term s)) ys
-> NS @[PType] (NP @PType (Term s)) ((':) @[PType] y ys)
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 = Term s (PScottEncoded as r)
-> (PScottEncoded as r s -> Term s r) -> Term s r
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) -> Term s (ScottFn (ScottList as r) r)
-> NP @PType (Term s) (ScottList as r) -> Term s r
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 ((SOP @PType (Term s) as -> Term s r)
-> NP @PType (Term s) (ScottList as r)
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 = DerivedPInner PlutusTypeScott a s
-> Term s (DerivedPInner PlutusTypeScott a)
forall (a :: PType) (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 :: PType). Term s (PScottEncoded (PCode a) x))
-> PForall @PType (PScottEncoded (PCode a)) s
forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall ((forall (x :: PType). Term s (PScottEncoded (PCode a) x))
 -> PForall @PType (PScottEncoded (PCode a)) s)
-> (forall (x :: PType). Term s (PScottEncoded (PCode a) x))
-> PForall @PType (PScottEncoded (PCode a)) s
forall a b. (a -> b) -> a -> b
$ SOP @PType (Term s) (PCode a) -> Term s (PScottEncoded (PCode a) x)
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) (PCode a)
 -> Term s (PScottEncoded (PCode a) x))
-> SOP @PType (Term s) (PCode a)
-> Term s (PScottEncoded (PCode a) x)
forall a b. (a -> b) -> a -> b
$ a s -> SOP @PType (Term s) (PCode a)
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 = Term s (DerivedPInner PlutusTypeScott a)
-> (DerivedPInner PlutusTypeScott a s -> Term s b) -> Term s b
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
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) x)
x) -> Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) b)
-> (SOP
      @PType
      (Term s)
      (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
    -> Term s b)
-> Term s b
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
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) b)
forall (x :: PType).
Term
  s
  (PScottEncoded
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type]))) x)
x (a s -> Term s b
f (a s -> Term s b)
-> (SOP
      @PType
      (Term s)
      (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
    -> a s)
-> SOP
     @PType
     (Term s)
     (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP
  @PType
  (Term s)
  (ToPType2 (ToSumCode (Rep (a (Any @S))) ('[] @[Type])))
-> a s
forall (a :: PType) (s :: S).
PGeneric a =>
SOP @PType (Term s) (PCode a) -> a s
gpto)