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

module Plutarch.Repr.Scott (
  PScottStruct (PScottStruct, unPScottStruct),
  PScottRec (PScottRec, unPScottRec),
  PScottStructInner (PScottStructInner),
  PScottRecInner (PScottRecInner),
  DeriveAsScottStruct (DeriveAsScottStruct, unDeriveAsScottStruct),
  DeriveAsScottRec (DeriveAsScottRec, unDeriveAsScottRec),
) where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Exts (Any)
import Generics.SOP (Code, NP (Nil, (:*)), NS (S, Z), SOP (SOP))
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (All, All2, Head, SListI, SListI2)
import Plutarch.Internal.Eq (PEq, (#==))
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  PContravariant',
  PContravariant'',
  PCovariant',
  PCovariant'',
  PInner,
  PVariant',
  PVariant'',
  PlutusType,
  pcon,
  pcon',
  pmatch,
  pmatch',
 )
import Plutarch.Internal.Quantification (PForall)
import Plutarch.Internal.Term (
  PDelayed,
  S,
  Term,
  pdelay,
  pforce,
  phoistAcyclic,
  plam',
  punsafeCoerce,
  (#),
  (:-->),
 )
import Plutarch.Repr.Internal (
  PRec (PRec, unPRec),
  PStruct (PStruct, unPStruct),
  RecTypePrettyError,
  StructSameRepr,
  UnTermRec,
  UnTermStruct,
  grecEq,
  gstructEq,
  pletL,
 )

-- | @since 1.10.0
newtype PScottStruct (struct :: [[S -> Type]]) (s :: S) = PScottStruct
  { forall (struct :: [[S -> Type]]) (s :: S).
PScottStruct struct s -> PStruct struct s
unPScottStruct :: PStruct struct s
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
instance forall struct. (SListI2 struct, PScottStructConstraint struct) => PlutusType (PScottStruct struct) where
  type PInner (PScottStruct struct) = PForall (PScottStructInner struct) -- try `Any`
  type PCovariant' (PScottStruct struct) = All2 PCovariant'' struct
  type PContravariant' (PScottStruct struct) = All2 PContravariant'' struct
  type PVariant' (PScottStruct struct) = All2 PVariant'' struct
  pcon' :: forall (s :: S).
PScottStruct struct s -> Term s (PInner (PScottStruct struct))
pcon' (PScottStruct PStruct struct s
x) = Term
  s
  (ScottFn (ScottList struct (Any @(S -> Type))) (Any @(S -> Type))
   :--> Any @(S -> Type))
-> Term s (PInner (PScottStruct struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term
   s
   (ScottFn (ScottList struct (Any @(S -> Type))) (Any @(S -> Type))
    :--> Any @(S -> Type))
 -> Term s (PInner (PScottStruct struct)))
-> Term
     s
     (ScottFn (ScottList struct (Any @(S -> Type))) (Any @(S -> Type))
      :--> Any @(S -> Type))
-> Term s (PInner (PScottStruct struct))
forall a b. (a -> b) -> a -> b
$ forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI2 @(S -> Type) struct,
 SListI @(S -> Type) (ScottList struct r)) =>
PStruct struct s -> Term s (ScottFn (ScottList struct r) r :--> r)
pconScottStruct @struct PStruct struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PScottStruct struct))
-> (PScottStruct struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PScottStruct struct))
x PScottStruct struct s -> Term s b
f = forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(PScottStructConstraint struct, SListI2 @(S -> Type) struct) =>
Term s (PScottStruct struct)
-> (PStruct struct s -> Term s r) -> Term s r
pmatchScottStruct @struct (Term s (PInner (PScottStruct struct))
-> Term s (PScottStruct struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PScottStruct struct))
x) (PScottStruct struct s -> Term s b
f (PScottStruct struct s -> Term s b)
-> (PStruct struct s -> PScottStruct struct s)
-> PStruct struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct struct s -> PScottStruct struct s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PScottStruct struct s
PScottStruct)

-- NOTE/TODO: Performance has not been tested for this. I feel like this would be terribly slow
-- NOTE: Hoisting here is so that there's no duplicated computation on each argument.
-- GHC freaks out when I put hoist part in a let.

-- | @since 1.10.0
instance (PlutusType (PScottStruct struct), SListI2 struct, All2 PEq struct) => PEq (PScottStruct struct) where
  Term s (PScottStruct struct)
x #== :: forall (s :: S).
Term s (PScottStruct struct)
-> Term s (PScottStruct struct) -> Term s PBool
#== Term s (PScottStruct struct)
y =
    ClosedTerm
  (PScottStruct struct :--> (PScottStruct struct :--> PBool))
-> Term
     s (PScottStruct struct :--> (PScottStruct struct :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s (PScottStruct struct)
 -> Term s (PScottStruct struct) -> Term s PBool)
-> Term
     s (PScottStruct struct :--> (PScottStruct struct :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PScottStruct struct) -> Term s PBool)
-> Term s (c :--> (PScottStruct struct :--> PBool))
plam ((Term s (PScottStruct struct)
  -> Term s (PScottStruct struct) -> Term s PBool)
 -> Term
      s (PScottStruct struct :--> (PScottStruct struct :--> PBool)))
-> (Term s (PScottStruct struct)
    -> Term s (PScottStruct struct) -> Term s PBool)
-> Term
     s (PScottStruct struct :--> (PScottStruct struct :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PScottStruct struct)
x' Term s (PScottStruct struct)
y' ->
          Term s (PScottStruct struct)
-> (PScottStruct struct s -> Term s PBool) -> Term s PBool
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 (PScottStruct struct)
x' ((PScottStruct struct s -> Term s PBool) -> Term s PBool)
-> (PScottStruct struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PScottStruct (PStruct SOP @(S -> Type) (Term s) struct
x'')) ->
            Term s (PScottStruct struct)
-> (PScottStruct struct s -> Term s PBool) -> Term s PBool
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 (PScottStruct struct)
y' ((PScottStruct struct s -> Term s PBool) -> Term s PBool)
-> (PScottStruct struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PScottStruct (PStruct SOP @(S -> Type) (Term s) struct
y'')) ->
              SOP @(S -> Type) (Term s) struct
-> SOP @(S -> Type) (Term s) struct -> Term s PBool
forall (s :: S) (struct :: [[S -> Type]]).
All2 @(S -> Type) PEq struct =>
SOP @(S -> Type) (Term s) struct
-> SOP @(S -> Type) (Term s) struct -> Term s PBool
gstructEq SOP @(S -> Type) (Term s) struct
x'' SOP @(S -> Type) (Term s) struct
y''
      )
      # x
      # y

-- | @since 1.10.0
newtype PScottRec (struct :: [S -> Type]) (s :: S) = PScottRec
  { forall (struct :: [S -> Type]) (s :: S).
PScottRec struct s -> PRec struct s
unPScottRec :: PRec struct s
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
instance SListI struct => PlutusType (PScottRec struct) where
  type PInner (PScottRec struct) = PForall (PScottRecInner struct)
  type PCovariant' (PScottRec struct) = All PCovariant'' struct
  type PContravariant' (PScottRec struct) = All PContravariant'' struct
  type PVariant' (PScottRec struct) = All PVariant'' struct
  pcon' :: forall (s :: S).
PScottRec struct s -> Term s (PInner (PScottRec struct))
pcon' (PScottRec PRec struct s
x) = Term s (PScottRec struct) -> Term s (PInner (PScottRec struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PScottRec struct) -> Term s (PInner (PScottRec struct)))
-> Term s (PScottRec struct) -> Term s (PInner (PScottRec struct))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> Term s (PScottRec struct)
forall (struct :: [S -> Type]) (s :: S).
SListI @(S -> Type) struct =>
PRec struct s -> Term s (PScottRec struct)
pconScottRec PRec struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PScottRec struct))
-> (PScottRec struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PScottRec struct))
x PScottRec struct s -> Term s b
f = Term s (PScottRec struct)
-> (PRec struct s -> Term s b) -> Term s b
forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
Term s (PScottRec struct)
-> (PRec struct s -> Term s r) -> Term s r
pmatchScottRec (Term s (PInner (PScottRec struct)) -> Term s (PScottRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PScottRec struct))
x) (PScottRec struct s -> Term s b
f (PScottRec struct s -> Term s b)
-> (PRec struct s -> PScottRec struct s)
-> PRec struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRec struct s -> PScottRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PScottRec struct s
PScottRec)

-- | @since 1.10.0
instance All PEq struct => PEq (PScottRec struct) where
  Term s (PScottRec struct)
x #== :: forall (s :: S).
Term s (PScottRec struct)
-> Term s (PScottRec struct) -> Term s PBool
#== Term s (PScottRec struct)
y =
    ClosedTerm (PScottRec struct :--> (PScottRec struct :--> PBool))
-> Term s (PScottRec struct :--> (PScottRec struct :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s (PScottRec struct)
 -> Term s (PScottRec struct) -> Term s PBool)
-> Term s (PScottRec struct :--> (PScottRec struct :--> PBool))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (PScottRec struct) -> Term s PBool)
-> Term s (c :--> (PScottRec struct :--> PBool))
plam ((Term s (PScottRec struct)
  -> Term s (PScottRec struct) -> Term s PBool)
 -> Term s (PScottRec struct :--> (PScottRec struct :--> PBool)))
-> (Term s (PScottRec struct)
    -> Term s (PScottRec struct) -> Term s PBool)
-> Term s (PScottRec struct :--> (PScottRec struct :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PScottRec struct)
x' Term s (PScottRec struct)
y' ->
          Term s (PScottRec struct)
-> (PScottRec struct s -> Term s PBool) -> Term s PBool
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 (PScottRec struct)
x' ((PScottRec struct s -> Term s PBool) -> Term s PBool)
-> (PScottRec struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PScottRec (PRec NP @(S -> Type) (Term s) struct
x'')) ->
            Term s (PScottRec struct)
-> (PScottRec struct s -> Term s PBool) -> Term s PBool
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 (PScottRec struct)
y' ((PScottRec struct s -> Term s PBool) -> Term s PBool)
-> (PScottRec struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PScottRec (PRec NP @(S -> Type) (Term s) struct
y'')) ->
              NP @(S -> Type) (Term s) struct
-> NP @(S -> Type) (Term s) struct -> Term s PBool
forall (s :: S) (struct :: [S -> Type]).
All @(S -> Type) PEq struct =>
NP @(S -> Type) (Term s) struct
-> NP @(S -> Type) (Term s) struct -> Term s PBool
grecEq NP @(S -> Type) (Term s) struct
x'' NP @(S -> Type) (Term s) struct
y''
      )
      # x
      # y

-- This could be better

-- | @since 1.10.0
newtype PScottStructInner a r s = PScottStructInner (Term s (ScottFn (ScottList a r) r))

-- | @since 1.10.0
newtype PScottRecInner a r s = PScottRecInner (Term s (ScottFn a r))

-- | @since 1.10.0
newtype DeriveAsScottStruct (a :: S -> Type) s = DeriveAsScottStruct
  { forall (a :: S -> Type) (s :: S). DeriveAsScottStruct a s -> a s
unDeriveAsScottStruct :: a s
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
instance
  forall (a :: S -> Type) (struct :: [[S -> Type]]).
  ( SOP.Generic (a Any)
  , struct ~ UnTermStruct (a Any)
  , SListI2 struct
  , forall s. StructSameRepr s a struct
  , PScottStructConstraint struct
  ) =>
  PlutusType (DeriveAsScottStruct a)
  where
  type PInner (DeriveAsScottStruct a) = PScottStruct (UnTermStruct (a Any))
  type PCovariant' (DeriveAsScottStruct a) = (PCovariant' a)
  type PContravariant' (DeriveAsScottStruct a) = (PContravariant' a)
  type PVariant' (DeriveAsScottStruct a) = (PVariant' a)
  pcon' :: forall (s :: S).
DeriveAsScottStruct a s -> Term s (PInner (DeriveAsScottStruct a))
pcon' (DeriveAsScottStruct a s
x) =
    forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon @(PScottStruct (UnTermStruct (a Any))) (PScottStruct (UnTermStruct (a (Any @S))) s
 -> Term s (PScottStruct (UnTermStruct (a (Any @S)))))
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> Term s (PScottStruct (UnTermStruct (a (Any @S))))
forall a b. (a -> b) -> a -> b
$ PStruct (UnTermStruct (a (Any @S))) s
-> PScottStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PScottStruct struct s
PScottStruct (PStruct (UnTermStruct (a (Any @S))) s
 -> PScottStruct (UnTermStruct (a (Any @S))) s)
-> PStruct (UnTermStruct (a (Any @S))) s
-> PScottStruct (UnTermStruct (a (Any @S))) s
forall a b. (a -> b) -> a -> b
$ SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
-> PStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
 -> PStruct (UnTermStruct (a (Any @S))) s)
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
-> PStruct (UnTermStruct (a (Any @S))) s
forall a b. (a -> b) -> a -> b
$ SOP @Type I (Code (a s))
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: Type -> Type) (g :: (S -> Type) -> Type)
       (xs :: [[Type]]) (ys :: [[S -> Type]]).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  (LiftedCoercible @Type @Type @(S -> Type) f g)
  xs
  ys =>
SOP @Type f xs -> SOP @(S -> Type) g ys
SOP.hcoerce (SOP @Type I (Code (a s))
 -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> SOP @Type I (Code (a s))
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall a b. (a -> b) -> a -> b
$ a s -> SOP @Type I (Code (a s))
forall a. Generic a => a -> Rep a
SOP.from a s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsScottStruct a))
-> (DeriveAsScottStruct a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsScottStruct a))
x DeriveAsScottStruct a s -> Term s b
f =
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch @(PScottStruct (UnTermStruct (a Any))) Term s (PInner (DeriveAsScottStruct a))
Term s (PScottStruct (UnTermStruct (a (Any @S))))
x (DeriveAsScottStruct a s -> Term s b
f (DeriveAsScottStruct a s -> Term s b)
-> (PScottStruct (UnTermStruct (a (Any @S))) s
    -> DeriveAsScottStruct a s)
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsScottStruct a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsScottStruct a s
DeriveAsScottStruct (a s -> DeriveAsScottStruct a s)
-> (PScottStruct (UnTermStruct (a (Any @S))) s -> a s)
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> DeriveAsScottStruct a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to (Rep (a s) -> a s)
-> (PScottStruct (UnTermStruct (a (Any @S))) s -> Rep (a s))
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))) -> Rep (a s)
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: (S -> Type) -> Type) (g :: Type -> Type)
       (xs :: [[S -> Type]]) (ys :: [[Type]]).
AllZipN
  @(S -> Type)
  @[[S -> Type]]
  @(S -> Type)
  @Type
  @[[S -> Type]]
  @[[Type]]
  (Prod @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)))
  (LiftedCoercible @(S -> Type) @Type @Type f g)
  xs
  ys =>
SOP @(S -> Type) f xs -> SOP @Type g ys
SOP.hcoerce (SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
 -> Rep (a s))
-> (PScottStruct (UnTermStruct (a (Any @S))) s
    -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> Rep (a s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct (UnTermStruct (a (Any @S))) s
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> SOP @(S -> Type) (Term s) struct
unPStruct (PStruct (UnTermStruct (a (Any @S))) s
 -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> (PScottStruct (UnTermStruct (a (Any @S))) s
    -> PStruct (UnTermStruct (a (Any @S))) s)
-> PScottStruct (UnTermStruct (a (Any @S))) s
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PScottStruct (UnTermStruct (a (Any @S))) s
-> PStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PScottStruct struct s -> PStruct struct s
unPScottStruct)

-- | @since 1.10.0
newtype DeriveAsScottRec (a :: S -> Type) s = DeriveAsScottRec
  { forall (a :: S -> Type) (s :: S). DeriveAsScottRec a s -> a s
unDeriveAsScottRec :: a s
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
instance
  forall (a :: S -> Type) (struct' :: [Type]) (struct :: [S -> Type]).
  ( SOP.Generic (a Any)
  , '[struct'] ~ Code (a Any)
  , struct ~ UnTermRec struct'
  , SListI struct
  , forall s. StructSameRepr s a '[struct]
  , RecTypePrettyError (Code (a Any))
  ) =>
  PlutusType (DeriveAsScottRec a)
  where
  type PInner (DeriveAsScottRec a) = PScottRec (UnTermRec (Head (Code (a Any))))
  type PCovariant' (DeriveAsScottRec a) = (PCovariant' a)
  type PContravariant' (DeriveAsScottRec a) = (PContravariant' a)
  type PVariant' (DeriveAsScottRec a) = (PVariant' a)
  pcon' :: forall (s :: S).
DeriveAsScottRec a s -> Term s (PInner (DeriveAsScottRec a))
pcon' (DeriveAsScottRec a s
x) =
    PInner (DeriveAsScottRec a) s
-> Term s (PInner (DeriveAsScottRec a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInner (DeriveAsScottRec a) s
 -> Term s (PInner (DeriveAsScottRec a)))
-> PInner (DeriveAsScottRec a) s
-> Term s (PInner (DeriveAsScottRec a))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> PScottRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PScottRec struct s
PScottRec (PRec struct s -> PScottRec struct s)
-> PRec struct s -> PScottRec struct s
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) struct -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (NP @(S -> Type) (Term s) struct -> PRec struct s)
-> NP @(S -> Type) (Term s) struct -> PRec struct s
forall a b. (a -> b) -> a -> b
$ NS
  @[S -> Type]
  (NP @(S -> Type) (Term s))
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NP @(S -> Type) (Term s) struct
forall {k} (f :: k -> Type) (x :: k).
NS @k f ((':) @k x ('[] @k)) -> f x
SOP.unZ (NS
   @[S -> Type]
   (NP @(S -> Type) (Term s))
   ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> NP @(S -> Type) (Term s) struct)
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NP @(S -> Type) (Term s) struct
forall a b. (a -> b) -> a -> b
$ SOP
  @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
SOP.unSOP (SOP
   @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> NS
      @[S -> Type]
      (NP @(S -> Type) (Term s))
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall a b. (a -> b) -> a -> b
$ SOP @Type I (Code (a s))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: Type -> Type) (g :: (S -> Type) -> Type)
       (xs :: [[Type]]) (ys :: [[S -> Type]]).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  (LiftedCoercible @Type @Type @(S -> Type) f g)
  xs
  ys =>
SOP @Type f xs -> SOP @(S -> Type) g ys
SOP.hcoerce (SOP @Type I (Code (a s))
 -> SOP
      @(S -> Type)
      (Term s)
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> SOP @Type I (Code (a s))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall a b. (a -> b) -> a -> b
$ a s -> SOP @Type I (Code (a s))
forall a. Generic a => a -> Rep a
SOP.from a s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (DeriveAsScottRec a))
-> (DeriveAsScottRec a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsScottRec a))
x DeriveAsScottRec a s -> Term s b
f =
    Term s (PInner (DeriveAsScottRec a))
-> (PInner (DeriveAsScottRec a) s -> Term s b) -> Term s b
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PInner (DeriveAsScottRec a))
x (DeriveAsScottRec a s -> Term s b
f (DeriveAsScottRec a s -> Term s b)
-> (PScottRec struct s -> DeriveAsScottRec a s)
-> PScottRec struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsScottRec a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsScottRec a s
DeriveAsScottRec (a s -> DeriveAsScottRec a s)
-> (PScottRec struct s -> a s)
-> PScottRec struct s
-> DeriveAsScottRec a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep (a s) -> a s
forall a. Generic a => Rep a -> a
SOP.to (Rep (a s) -> a s)
-> (PScottRec struct s -> Rep (a s)) -> PScottRec struct s -> a s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP
  @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> Rep (a s)
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (f :: k1 -> Type)
       (g :: k2 -> Type) (xs :: l1) (ys :: l2).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN
   @k1
   @l1
   @k1
   @k2
   @l1
   @l2
   (Prod @k1 @l1 h1)
   (LiftedCoercible @k1 @Type @k2 f g)
   xs
   ys) =>
h1 f xs -> h2 g ys
forall (f :: (S -> Type) -> Type) (g :: Type -> Type)
       (xs :: [[S -> Type]]) (ys :: [[Type]]).
AllZipN
  @(S -> Type)
  @[[S -> Type]]
  @(S -> Type)
  @Type
  @[[S -> Type]]
  @[[Type]]
  (Prod @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)))
  (LiftedCoercible @(S -> Type) @Type @Type f g)
  xs
  ys =>
SOP @(S -> Type) f xs -> SOP @Type g ys
SOP.hcoerce (SOP
   @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> Rep (a s))
-> (PScottRec struct s
    -> SOP
         @(S -> Type)
         (Term s)
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PScottRec struct s
-> Rep (a s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS
  @[S -> Type]
  (NP @(S -> Type) (Term s))
  ((':) @[S -> Type] struct ('[] @[S -> Type]))
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[S -> Type]
   (NP @(S -> Type) (Term s))
   ((':) @[S -> Type] struct ('[] @[S -> Type]))
 -> SOP
      @(S -> Type)
      (Term s)
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> (PScottRec struct s
    -> NS
         @[S -> Type]
         (NP @(S -> Type) (Term s))
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PScottRec struct s
-> SOP
     @(S -> Type) (Term s) ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
forall (a :: [S -> Type] -> Type) (x :: [S -> Type])
       (xs :: [[S -> Type]]).
a x -> NS @[S -> Type] a ((':) @[S -> Type] x xs)
Z @_ @_ @'[]) (NP @(S -> Type) (Term s) struct
 -> NS
      @[S -> Type]
      (NP @(S -> Type) (Term s))
      ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> (PScottRec struct s -> NP @(S -> Type) (Term s) struct)
-> PScottRec struct s
-> NS
     @[S -> Type]
     (NP @(S -> Type) (Term s))
     ((':) @[S -> Type] struct ('[] @[S -> Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRec struct s -> NP @(S -> Type) (Term s) struct
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> NP @(S -> Type) (Term s) struct
unPRec (PRec struct s -> NP @(S -> Type) (Term s) struct)
-> (PScottRec struct s -> PRec struct s)
-> PScottRec struct s
-> NP @(S -> Type) (Term s) struct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PScottRec struct s -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
PScottRec struct s -> PRec struct s
unPScottRec)

-- Helpers

-- What whatever unholy reason, quantification on constrain only works if like this
class SListI (ScottList struct r) => PScottStructConstraint' struct r

instance SListI (ScottList struct r) => PScottStructConstraint' struct r

class (SListI struct, forall r. PScottStructConstraint' struct r) => PScottStructConstraint struct

instance (SListI struct, forall r. PScottStructConstraint' struct r) => PScottStructConstraint struct

--------------------------------------------------------------------------------------

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 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 {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
SOP.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 {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
SOP.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 {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
SOP.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 :: forall as r s. SListI as => Term s (ScottFn as r) -> NP (Term s) as -> Term s r
pappL :: forall (as :: [S -> Type]) (r :: S -> Type) (s :: S).
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 {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
SOP.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')

-- Note, we don't have to use delay unit here because when value is unit, that will be the only branch that will get run.
pconScottRec ::
  forall (struct :: [S -> Type]) (s :: S).
  SListI struct =>
  PRec struct s ->
  Term s (PScottRec struct)
pconScottRec :: forall (struct :: [S -> Type]) (s :: S).
SListI @(S -> Type) struct =>
PRec struct s -> Term s (PScottRec struct)
pconScottRec (PRec NP @(S -> Type) (Term s) struct
xs) = Term s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type))
-> Term s (PScottRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type))
 -> Term s (PScottRec struct))
-> Term
     s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type))
-> Term s (PScottRec struct)
forall a b. (a -> b) -> a -> b
$ (Term s (ScottFn' struct (Any @(S -> Type)))
 -> Term s (Any @(S -> Type)))
-> Term
     s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (Any @(S -> Type)))
-> Term s (c :--> Any @(S -> Type))
plam ((Term s (ScottFn' struct (Any @(S -> Type)))
  -> Term s (Any @(S -> Type)))
 -> Term
      s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type)))
-> (Term s (ScottFn' struct (Any @(S -> Type)))
    -> Term s (Any @(S -> Type)))
-> Term
     s (ScottFn' struct (Any @(S -> Type)) :--> Any @(S -> Type))
forall a b. (a -> b) -> a -> b
$ (Term s (ScottFn' struct (Any @(S -> Type)))
 -> NP @(S -> Type) (Term s) struct -> Term s (Any @(S -> Type)))
-> NP @(S -> Type) (Term s) struct
-> Term s (ScottFn' struct (Any @(S -> Type)))
-> Term s (Any @(S -> Type))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term s (ScottFn' struct (Any @(S -> Type)))
-> NP @(S -> Type) (Term s) struct -> Term s (Any @(S -> Type))
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' NP @(S -> Type) (Term s) struct
xs

pmatchScottRec ::
  forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
  SListI struct =>
  Term s (PScottRec struct) ->
  (PRec struct s -> Term s r) ->
  Term s r
pmatchScottRec :: forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
Term s (PScottRec struct)
-> (PRec struct s -> Term s r) -> Term s r
pmatchScottRec Term s (PScottRec struct)
xs PRec struct s -> Term s r
f = Term s (PScottRec struct) -> Term s (ScottFn' struct r :--> r)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PScottRec struct)
xs Term s (ScottFn' struct r :--> r)
-> Term s (ScottFn' struct r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (NP @(S -> Type) (Term s) struct -> Term s r)
-> Term s (ScottFn' struct 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' (PRec struct s -> Term s r
f (PRec struct s -> Term s r)
-> (NP @(S -> Type) (Term s) struct -> PRec struct s)
-> NP @(S -> Type) (Term s) struct
-> Term s r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP @(S -> Type) (Term s) struct -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec)

---------------------------

-- PScottStruct struct <~> Term s (ScottFn (ScottList struct r)) :--> Term s r)

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)
-> PStruct as s
-> Term s r
unGPCon' :: NP (Term s) (ScottList as r) -> PStruct as s -> Term s r}

gpcon' :: SListI2 as => NP (Term s) (ScottList as r) -> PStruct as s -> 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)
-> PStruct as s -> Term s r
gpcon' = GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> PStruct as s
-> Term s r
forall (s :: S) (r :: S -> Type) (as :: [[S -> Type]]).
GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> PStruct as s
-> Term s r
unGPCon' (GPCon' s r as
 -> NP @(S -> Type) (Term s) (ScottList as r)
 -> PStruct as s
 -> Term s r)
-> GPCon' s r as
-> NP @(S -> Type) (Term s) (ScottList as r)
-> PStruct as s
-> 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
SOP.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)
 -> PStruct ('[] @[S -> Type]) s -> 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)
 -> PStruct as s -> 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)
-> PStruct ys s -> Term s r
prev) -> (NP @(S -> Type) (Term s) (ScottList ((':) @[S -> Type] y ys) r)
 -> PStruct ((':) @[S -> Type] y ys) s -> 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)
 -> PStruct as s -> Term s r)
-> GPCon' s r as
GPCon' \(Term s x
arg :* NP @(S -> Type) (Term s) xs
args) -> \case
      (PStruct (SOP (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]) (r :: S -> Type) (s :: S).
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
      (PStruct (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
xs))) -> NP @(S -> Type) (Term s) (ScottList ys r)
-> PStruct ys s -> Term s r
prev NP @(S -> Type) (Term s) xs
NP @(S -> Type) (Term s) (ScottList ys r)
args (SOP @(S -> Type) (Term s) ys -> PStruct ys s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) ys -> PStruct ys s)
-> SOP @(S -> Type) (Term s) ys -> PStruct ys s
forall a b. (a -> b) -> a -> b
$ 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)

pconScottStruct ::
  forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
  ( SListI2 struct
  , SListI (ScottList struct r)
  ) =>
  PStruct struct s ->
  Term s (ScottFn (ScottList struct r) r :--> r)
pconScottStruct :: forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI2 @(S -> Type) struct,
 SListI @(S -> Type) (ScottList struct r)) =>
PStruct struct s -> Term s (ScottFn (ScottList struct r) r :--> r)
pconScottStruct (PStruct SOP @(S -> Type) (Term s) struct
xs) =
  SOP @(S -> Type) (Term s) struct
-> (SOP @(S -> Type) (Term s) struct
    -> Term s (ScottFn (ScottList struct r) r :--> r))
-> Term s (ScottFn (ScottList struct r) r :--> 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) struct
xs \(SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) struct
fields) ->
    Term s (ScottFn (ScottList struct r) r)
-> Term s (ScottFn (ScottList struct r) r :--> r)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (ScottFn (ScottList struct r) r)
 -> Term s (ScottFn (ScottList struct r) r :--> r))
-> Term s (ScottFn (ScottList struct r) r)
-> Term s (ScottFn (ScottList struct r) r :--> r)
forall a b. (a -> b) -> a -> b
$ (NP @(S -> Type) (Term s) (ScottList struct r) -> Term s r)
-> Term s (ScottFn (ScottList struct 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 struct r)
args -> (NP @(S -> Type) (Term s) (ScottList struct r)
-> PStruct struct s -> Term s r
forall (as :: [[S -> Type]]) (s :: S) (r :: S -> Type).
SListI2 @(S -> Type) as =>
NP @(S -> Type) (Term s) (ScottList as r)
-> PStruct as s -> Term s r
gpcon' NP @(S -> Type) (Term s) (ScottList struct r)
args (SOP @(S -> Type) (Term s) struct -> PStruct struct s
forall (struct :: [[S -> Type]]) (s :: S).
SOP @(S -> Type) (Term s) struct -> PStruct struct s
PStruct (SOP @(S -> Type) (Term s) struct -> PStruct struct s)
-> SOP @(S -> Type) (Term s) struct -> PStruct struct s
forall a b. (a -> b) -> a -> b
$ NS @[S -> Type] (NP @(S -> Type) (Term s)) struct
-> SOP @(S -> Type) (Term s) struct
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)) struct
fields) :: Term s r)

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

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

pmatchScottStruct ::
  forall struct r s.
  ( PScottStructConstraint struct
  , SListI2 struct
  ) =>
  Term s (PScottStruct struct) ->
  (PStruct struct s -> Term s r) ->
  Term s r
pmatchScottStruct :: forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(PScottStructConstraint struct, SListI2 @(S -> Type) struct) =>
Term s (PScottStruct struct)
-> (PStruct struct s -> Term s r) -> Term s r
pmatchScottStruct Term s (PScottStruct struct)
xs PStruct struct s -> Term s r
f = Term s (ScottFn (ScottList struct r) r)
-> NP @(S -> Type) (Term s) (ScottList struct r) -> Term s r
forall (as :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) as =>
Term s (ScottFn as r) -> NP @(S -> Type) (Term s) as -> Term s r
pappL (Term s (PScottStruct struct)
-> Term s (ScottFn (ScottList struct r) r)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PScottStruct struct)
xs) ((PStruct struct s -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList struct r)
forall (as :: [[S -> Type]]) (r :: S -> Type) (s :: S).
SListI2 @(S -> Type) as =>
(PStruct as s -> Term s r)
-> NP @(S -> Type) (Term s) (ScottList as r)
gpmatch' PStruct struct s -> Term s r
f)