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

module Plutarch.Repr.SOP (
  PSOPStruct (PSOPStruct, unPSOPStruct),
  PSOPRec (PSOPRec, unPSOPRec),
  DeriveAsSOPStruct (DeriveAsSOPStruct, unDeriveAsSOPStruct),
  DeriveAsSOPRec (DeriveAsSOPRec, unDeriveAsSOPRec),
) where

import Control.Arrow ((&&&))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Exts (Any)
import Generics.SOP (
  Code,
  K (K),
  NP (Nil, (:*)),
  NS (S, Z),
  SOP (SOP),
 )
import Generics.SOP qualified as SOP
import Generics.SOP.Constraint (
  All,
  All2,
  Head,
  SListI,
  SListI2,
 )
import Plutarch.Builtin.Bool (PBool)
import Plutarch.Builtin.Opaque (POpaque)
import Plutarch.Internal.Eq (PEq, (#==))
import Plutarch.Internal.Lift
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  PContravariant',
  PContravariant'',
  PCovariant',
  PCovariant'',
  PInner,
  PVariant',
  PVariant'',
  PlutusType,
  pcon,
  pcon',
  pmatch,
  pmatch',
 )
import Plutarch.Internal.Term (
  RawTerm (RCase, RConstr),
  S,
  Term (Term),
  TermResult (TermResult),
  asRawTerm,
  getDeps,
  getTerm,
  perror,
  phoistAcyclic,
  punsafeCoerce,
  (#),
  (:-->),
 )
import Plutarch.Repr.Internal (
  PRec (PRec, unPRec),
  PStruct (PStruct, unPStruct),
  RecAsHaskell,
  RecTypePrettyError,
  StructAsHaskell,
  StructSameRepr,
  UnTermRec,
  UnTermStruct,
  grecEq,
  gstructEq,
  pletL,
 )

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

-- | @since 1.10.0
instance (SListI2 struct, PSOPStructConstraint struct) => PlutusType (PSOPStruct struct) where
  type PInner (PSOPStruct struct) = POpaque
  type PCovariant' (PSOPStruct struct) = All2 PCovariant'' struct
  type PContravariant' (PSOPStruct struct) = All2 PContravariant'' struct
  type PVariant' (PSOPStruct struct) = All2 PVariant'' struct
  pcon' :: forall (s :: S).
PSOPStruct struct s -> Term s (PInner (PSOPStruct struct))
pcon' (PSOPStruct PStruct struct s
x) = Term s (PSOPStruct struct) -> Term s (PInner (PSOPStruct struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PSOPStruct struct) -> Term s (PInner (PSOPStruct struct)))
-> Term s (PSOPStruct struct)
-> Term s (PInner (PSOPStruct struct))
forall a b. (a -> b) -> a -> b
$ PStruct struct s -> Term s (PSOPStruct struct)
forall (struct :: [[S -> Type]]) (s :: S).
SListI2 @(S -> Type) struct =>
PStruct struct s -> Term s (PSOPStruct struct)
pconSOPStruct PStruct struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PSOPStruct struct))
-> (PSOPStruct struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PSOPStruct struct))
x PSOPStruct struct s -> Term s b
f = Term s (PSOPStruct struct)
-> (PStruct struct s -> Term s b) -> Term s b
forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI2 @(S -> Type) struct, PSOPStructConstraint struct) =>
Term s (PSOPStruct struct)
-> (PStruct struct s -> Term s r) -> Term s r
pmatchSOPStruct (Term s (PInner (PSOPStruct struct)) -> Term s (PSOPStruct struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PSOPStruct struct))
x) (PSOPStruct struct s -> Term s b
f (PSOPStruct struct s -> Term s b)
-> (PStruct struct s -> PSOPStruct struct s)
-> PStruct struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PStruct struct s -> PSOPStruct struct s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PSOPStruct struct s
PSOPStruct)

-- NOTE/TODO: Performance has not been tested for this. I feel like this would be terribly slow
instance (PlutusType (PSOPStruct struct), All2 PEq struct) => PEq (PSOPStruct struct) where
  Term s (PSOPStruct struct)
x #== :: forall (s :: S).
Term s (PSOPStruct struct)
-> Term s (PSOPStruct struct) -> Term s PBool
#== Term s (PSOPStruct struct)
y =
    ClosedTerm (PSOPStruct struct :--> (PSOPStruct struct :--> PBool))
-> Term s (PSOPStruct struct :--> (PSOPStruct struct :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s (PSOPStruct struct)
 -> Term s (PSOPStruct struct) -> Term s PBool)
-> Term s (PSOPStruct struct :--> (PSOPStruct 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 (PSOPStruct struct) -> Term s PBool)
-> Term s (c :--> (PSOPStruct struct :--> PBool))
plam ((Term s (PSOPStruct struct)
  -> Term s (PSOPStruct struct) -> Term s PBool)
 -> Term s (PSOPStruct struct :--> (PSOPStruct struct :--> PBool)))
-> (Term s (PSOPStruct struct)
    -> Term s (PSOPStruct struct) -> Term s PBool)
-> Term s (PSOPStruct struct :--> (PSOPStruct struct :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (PSOPStruct struct)
x' Term s (PSOPStruct struct)
y' ->
          Term s (PSOPStruct struct)
-> (PSOPStruct 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 (PSOPStruct struct)
x' ((PSOPStruct struct s -> Term s PBool) -> Term s PBool)
-> (PSOPStruct struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PSOPStruct (PStruct SOP @(S -> Type) (Term s) struct
x'')) ->
            Term s (PSOPStruct struct)
-> (PSOPStruct 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 (PSOPStruct struct)
y' ((PSOPStruct struct s -> Term s PBool) -> Term s PBool)
-> (PSOPStruct struct s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PSOPStruct (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 PSOPRec (struct :: [S -> Type]) (s :: S) = PSOPRec
  { forall (struct :: [S -> Type]) (s :: S).
PSOPRec struct s -> PRec struct s
unPSOPRec :: PRec struct s
  -- ^ @since 1.10.0
  }

-- | @since 1.10.0
instance SListI struct => PlutusType (PSOPRec struct) where
  type PInner (PSOPRec struct) = POpaque
  type PCovariant' (PSOPRec struct) = All PCovariant'' struct
  type PContravariant' (PSOPRec struct) = All PContravariant'' struct
  type PVariant' (PSOPRec struct) = All PVariant'' struct
  pcon' :: forall (s :: S).
PSOPRec struct s -> Term s (PInner (PSOPRec struct))
pcon' (PSOPRec PRec struct s
x) = Term s (PSOPRec struct) -> Term s (PInner (PSOPRec struct))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term s (PSOPRec struct) -> Term s (PInner (PSOPRec struct)))
-> Term s (PSOPRec struct) -> Term s (PInner (PSOPRec struct))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> Term s (PSOPRec struct)
forall (struct :: [S -> Type]) (s :: S).
SListI @(S -> Type) struct =>
PRec struct s -> Term s (PSOPRec struct)
pconSOPRec PRec struct s
x
  pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PSOPRec struct))
-> (PSOPRec struct s -> Term s b) -> Term s b
pmatch' Term s (PInner (PSOPRec struct))
x PSOPRec struct s -> Term s b
f = Term s (PSOPRec 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 (PSOPRec struct) -> (PRec struct s -> Term s r) -> Term s r
pmatchSOPRec (Term s (PInner (PSOPRec struct)) -> Term s (PSOPRec struct)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner (PSOPRec struct))
x) (PSOPRec struct s -> Term s b
f (PSOPRec struct s -> Term s b)
-> (PRec struct s -> PSOPRec struct s) -> PRec struct s -> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRec struct s -> PSOPRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PSOPRec struct s
PSOPRec)

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

{- |
@via@-derivation helper to derive 'PlutusType' instance using SoP encoding. If your type has
only one constructor prefer using 'DeriveAsSOPRec' instead.

@since 1.10.0
-}
newtype DeriveAsSOPStruct (a :: S -> Type) s = DeriveAsSOPStruct
  { forall (a :: S -> Type) (s :: S). DeriveAsSOPStruct a s -> a s
unDeriveAsSOPStruct :: 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
  , PSOPStructConstraint struct
  ) =>
  PlutusType (DeriveAsSOPStruct a)
  where
  type PInner (DeriveAsSOPStruct a) = PSOPStruct (UnTermStruct (a Any))
  type PCovariant' (DeriveAsSOPStruct a) = PCovariant' a
  type PContravariant' (DeriveAsSOPStruct a) = PContravariant' a
  type PVariant' (DeriveAsSOPStruct a) = PVariant' a
  pcon' :: forall (s :: S).
DeriveAsSOPStruct a s -> Term s (PInner (DeriveAsSOPStruct a))
pcon' (DeriveAsSOPStruct a s
x) =
    forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon @(PSOPStruct (UnTermStruct (a Any))) (PSOPStruct (UnTermStruct (a (Any @S))) s
 -> Term s (PSOPStruct (UnTermStruct (a (Any @S)))))
-> PSOPStruct (UnTermStruct (a (Any @S))) s
-> Term s (PSOPStruct (UnTermStruct (a (Any @S))))
forall a b. (a -> b) -> a -> b
$ PStruct (UnTermStruct (a (Any @S))) s
-> PSOPStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PSOPStruct struct s
PSOPStruct (PStruct (UnTermStruct (a (Any @S))) s
 -> PSOPStruct (UnTermStruct (a (Any @S))) s)
-> PStruct (UnTermStruct (a (Any @S))) s
-> PSOPStruct (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 (DeriveAsSOPStruct a))
-> (DeriveAsSOPStruct a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsSOPStruct a))
x DeriveAsSOPStruct 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 @(PSOPStruct (UnTermStruct (a Any))) Term s (PInner (DeriveAsSOPStruct a))
Term s (PSOPStruct (UnTermStruct (a (Any @S))))
x (DeriveAsSOPStruct a s -> Term s b
f (DeriveAsSOPStruct a s -> Term s b)
-> (PSOPStruct (UnTermStruct (a (Any @S))) s
    -> DeriveAsSOPStruct a s)
-> PSOPStruct (UnTermStruct (a (Any @S))) s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsSOPStruct a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsSOPStruct a s
DeriveAsSOPStruct (a s -> DeriveAsSOPStruct a s)
-> (PSOPStruct (UnTermStruct (a (Any @S))) s -> a s)
-> PSOPStruct (UnTermStruct (a (Any @S))) s
-> DeriveAsSOPStruct 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)
-> (PSOPStruct (UnTermStruct (a (Any @S))) s -> Rep (a s))
-> PSOPStruct (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))
-> (PSOPStruct (UnTermStruct (a (Any @S))) s
    -> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S))))
-> PSOPStruct (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))))
-> (PSOPStruct (UnTermStruct (a (Any @S))) s
    -> PStruct (UnTermStruct (a (Any @S))) s)
-> PSOPStruct (UnTermStruct (a (Any @S))) s
-> SOP @(S -> Type) (Term s) (UnTermStruct (a (Any @S)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PSOPStruct (UnTermStruct (a (Any @S))) s
-> PStruct (UnTermStruct (a (Any @S))) s
forall (struct :: [[S -> Type]]) (s :: S).
PSOPStruct struct s -> PStruct struct s
unPSOPStruct)

{- | @via@-derivation helper for SOP encoding, currently behaves exactly like `DeriveAsSOPStruct`
but can be used only on types with a single constructor. It is separate to leave a room for
future optimizations.

@since 1.10.0
-}
newtype DeriveAsSOPRec (a :: S -> Type) s = DeriveAsSOPRec
  { forall (a :: S -> Type) (s :: S). DeriveAsSOPRec a s -> a s
unDeriveAsSOPRec :: 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 (DeriveAsSOPRec a)
  where
  type PInner (DeriveAsSOPRec a) = PSOPRec (UnTermRec (Head (Code (a Any))))
  type PCovariant' (DeriveAsSOPRec a) = PCovariant' a
  type PContravariant' (DeriveAsSOPRec a) = PContravariant' a
  type PVariant' (DeriveAsSOPRec a) = PVariant' a
  pcon' :: forall (s :: S).
DeriveAsSOPRec a s -> Term s (PInner (DeriveAsSOPRec a))
pcon' (DeriveAsSOPRec a s
x) =
    PInner (DeriveAsSOPRec a) s -> Term s (PInner (DeriveAsSOPRec a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PInner (DeriveAsSOPRec a) s -> Term s (PInner (DeriveAsSOPRec a)))
-> PInner (DeriveAsSOPRec a) s
-> Term s (PInner (DeriveAsSOPRec a))
forall a b. (a -> b) -> a -> b
$ PRec struct s -> PSOPRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PSOPRec struct s
PSOPRec (PRec struct s -> PSOPRec struct s)
-> PRec struct s -> PSOPRec 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 (DeriveAsSOPRec a))
-> (DeriveAsSOPRec a s -> Term s b) -> Term s b
pmatch' Term s (PInner (DeriveAsSOPRec a))
x DeriveAsSOPRec a s -> Term s b
f =
    Term s (PInner (DeriveAsSOPRec a))
-> (PInner (DeriveAsSOPRec 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 (DeriveAsSOPRec a))
x (DeriveAsSOPRec a s -> Term s b
f (DeriveAsSOPRec a s -> Term s b)
-> (PSOPRec struct s -> DeriveAsSOPRec a s)
-> PSOPRec struct s
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a s -> DeriveAsSOPRec a s
forall (a :: S -> Type) (s :: S). a s -> DeriveAsSOPRec a s
DeriveAsSOPRec (a s -> DeriveAsSOPRec a s)
-> (PSOPRec struct s -> a s)
-> PSOPRec struct s
-> DeriveAsSOPRec 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)
-> (PSOPRec struct s -> Rep (a s)) -> PSOPRec 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))
-> (PSOPRec struct s
    -> SOP
         @(S -> Type)
         (Term s)
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PSOPRec 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])))
-> (PSOPRec struct s
    -> NS
         @[S -> Type]
         (NP @(S -> Type) (Term s))
         ((':) @[S -> Type] struct ('[] @[S -> Type])))
-> PSOPRec 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])))
-> (PSOPRec struct s -> NP @(S -> Type) (Term s) struct)
-> PSOPRec 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)
-> (PSOPRec struct s -> PRec struct s)
-> PSOPRec struct s
-> NP @(S -> Type) (Term s) struct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PSOPRec struct s -> PRec struct s
forall (struct :: [S -> Type]) (s :: S).
PSOPRec struct s -> PRec struct s
unPSOPRec)

-- Helpers

class SListI (PCaseTy r struct) => PSOPStructConstraint' struct r

instance SListI (PCaseTy r struct) => PSOPStructConstraint' struct r

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

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

-- Take struct first for consistency
type family PHandlerTy r (struct :: [S -> Type]) :: S -> Type where
  PHandlerTy r '[] = r
  PHandlerTy r (x ': xs) = x :--> PHandlerTy r xs

type family PCaseTy r (struct :: [[S -> Type]]) :: [S -> Type] where
  PCaseTy _ '[] = '[]
  PCaseTy r (x ': xs) = PHandlerTy r x ': PCaseTy r xs

pconSOPRec ::
  forall (struct :: [S -> Type]) (s :: S). SListI struct => PRec struct s -> Term s (PSOPRec struct)
pconSOPRec :: forall (struct :: [S -> Type]) (s :: S).
SListI @(S -> Type) struct =>
PRec struct s -> Term s (PSOPRec struct)
pconSOPRec (PRec NP @(S -> Type) (Term s) struct
xs) = (Word64 -> TermMonad TermResult) -> Term s (PSOPRec struct)
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s (PSOPRec struct))
-> (Word64 -> TermMonad TermResult) -> Term s (PSOPRec struct)
forall a b. (a -> b) -> a -> b
$ \Word64
i -> do
  [(RawTerm, [HoistedTerm])]
ts <- NP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct
-> CollapseTo
     @(S -> Type)
     @[S -> Type]
     (NP @(S -> Type))
     (RawTerm, [HoistedTerm])
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> Type)) a
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
SOP.hcollapse (NP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct
 -> CollapseTo
      @(S -> Type)
      @[S -> Type]
      (NP @(S -> Type))
      (RawTerm, [HoistedTerm]))
-> TermMonad
     (NP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct)
-> TermMonad
     (CollapseTo
        @(S -> Type)
        @[S -> Type]
        (NP @(S -> Type))
        (RawTerm, [HoistedTerm]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (a :: S -> Type).
 Term s a -> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a))
-> NP @(S -> Type) (Term s) struct
-> TermMonad
     (NP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct)
forall (xs :: [S -> Type]) (g :: Type -> Type)
       (f :: (S -> Type) -> Type) (f' :: (S -> Type) -> Type).
(SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs,
 Applicative g) =>
(forall (a :: S -> Type). f a -> g (f' a))
-> NP @(S -> Type) f xs -> g (NP @(S -> Type) f' xs)
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l)
       (g :: Type -> Type) (f :: k -> Type) (f' :: k -> Type).
(HSequence @k @l h, SListIN @k @l h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
SOP.htraverse' (\Term s a
x -> (RawTerm, [HoistedTerm])
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall k a (b :: k). a -> K @k a b
K ((RawTerm, [HoistedTerm])
 -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> (TermResult -> (RawTerm, [HoistedTerm]))
-> TermResult
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> TermMonad TermResult
-> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s a -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s a
x Word64
i) NP @(S -> Type) (Term s) struct
xs
  let
    term :: RawTerm
term = Word64 -> [RawTerm] -> RawTerm
RConstr Word64
0 ([RawTerm] -> RawTerm) -> [RawTerm] -> RawTerm
forall a b. (a -> b) -> a -> b
$ (RawTerm, [HoistedTerm]) -> RawTerm
forall a b. (a, b) -> a
fst ((RawTerm, [HoistedTerm]) -> RawTerm)
-> [(RawTerm, [HoistedTerm])] -> [RawTerm]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
ts
    deps :: [HoistedTerm]
deps = [[HoistedTerm]] -> [HoistedTerm]
forall a. Monoid a => [a] -> a
mconcat ([[HoistedTerm]] -> [HoistedTerm])
-> [[HoistedTerm]] -> [HoistedTerm]
forall a b. (a -> b) -> a -> b
$ (RawTerm, [HoistedTerm]) -> [HoistedTerm]
forall a b. (a, b) -> b
snd ((RawTerm, [HoistedTerm]) -> [HoistedTerm])
-> [(RawTerm, [HoistedTerm])] -> [[HoistedTerm]]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
ts
  TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> TermResult -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult RawTerm
term [HoistedTerm]
deps

-- TODO: better name
newtype MSR s r struct = MSR
  { forall (s :: S) (r :: S -> Type) (struct :: [S -> Type]).
MSR s r struct
-> (PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
unMSR :: (PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
  }

sopHandler ::
  forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S). SListI struct => (PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
sopHandler :: forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
(PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
sopHandler PRec struct s -> Term s r
f =
  let
    go :: MSR s r ys -> MSR s r (y ': ys)
    go :: forall (ys :: [S -> Type]) (y :: S -> Type).
MSR s r ys -> MSR s r ((':) @(S -> Type) y ys)
go (MSR (PRec ys s -> Term s r) -> Term s (PHandlerTy r ys)
rest) = ((PRec ((':) @(S -> Type) y ys) s -> Term s r)
 -> Term s (PHandlerTy r ((':) @(S -> Type) y ys)))
-> MSR s r ((':) @(S -> Type) y ys)
forall (s :: S) (r :: S -> Type) (struct :: [S -> Type]).
((PRec struct s -> Term s r) -> Term s (PHandlerTy r struct))
-> MSR s r struct
MSR (((PRec ((':) @(S -> Type) y ys) s -> Term s r)
  -> Term s (PHandlerTy r ((':) @(S -> Type) y ys)))
 -> MSR s r ((':) @(S -> Type) y ys))
-> ((PRec ((':) @(S -> Type) y ys) s -> Term s r)
    -> Term s (PHandlerTy r ((':) @(S -> Type) y ys)))
-> MSR s r ((':) @(S -> Type) y ys)
forall a b. (a -> b) -> a -> b
$ \PRec ((':) @(S -> Type) y ys) s -> Term s r
f ->
      (Term s y -> Term s (PHandlerTy r ys))
-> Term s (y :--> PHandlerTy r ys)
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 (PHandlerTy r ys))
-> Term s (c :--> PHandlerTy r ys)
plam ((Term s y -> Term s (PHandlerTy r ys))
 -> Term s (y :--> PHandlerTy r ys))
-> (Term s y -> Term s (PHandlerTy r ys))
-> Term s (y :--> PHandlerTy r ys)
forall a b. (a -> b) -> a -> b
$ \Term s y
x -> (PRec ys s -> Term s r) -> Term s (PHandlerTy r ys)
rest ((PRec ys s -> Term s r) -> Term s (PHandlerTy r ys))
-> (PRec ys s -> Term s r) -> Term s (PHandlerTy r ys)
forall a b. (a -> b) -> a -> b
$ \(PRec NP @(S -> Type) (Term s) ys
rest') -> PRec ((':) @(S -> Type) y ys) s -> Term s r
f (PRec ((':) @(S -> Type) y ys) s -> Term s r)
-> PRec ((':) @(S -> Type) y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ((':) @(S -> Type) y ys)
-> PRec ((':) @(S -> Type) y ys) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec (Term s y
x 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
rest')

    handler :: Term s (PHandlerTy r struct)
    handler :: Term s (PHandlerTy r struct)
handler = MSR s r struct
-> (PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
forall (s :: S) (r :: S -> Type) (struct :: [S -> Type]).
MSR s r struct
-> (PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
unMSR (MSR s r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    SListI @(S -> Type) ys =>
    MSR s r ys -> MSR s r ((':) @(S -> Type) y ys))
-> MSR s r struct
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 (((PRec ('[] @(S -> Type)) s -> Term s r)
 -> Term s (PHandlerTy r ('[] @(S -> Type))))
-> MSR s r ('[] @(S -> Type))
forall (s :: S) (r :: S -> Type) (struct :: [S -> Type]).
((PRec struct s -> Term s r) -> Term s (PHandlerTy r struct))
-> MSR s r struct
MSR (((PRec ('[] @(S -> Type)) s -> Term s r)
  -> Term s (PHandlerTy r ('[] @(S -> Type))))
 -> MSR s r ('[] @(S -> Type)))
-> ((PRec ('[] @(S -> Type)) s -> Term s r)
    -> Term s (PHandlerTy r ('[] @(S -> Type))))
-> MSR s r ('[] @(S -> Type))
forall a b. (a -> b) -> a -> b
$ \PRec ('[] @(S -> Type)) s -> Term s r
f -> PRec ('[] @(S -> Type)) s -> Term s r
f (PRec ('[] @(S -> Type)) s -> Term s r)
-> PRec ('[] @(S -> Type)) s -> Term s r
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) ('[] @(S -> Type))
-> PRec ('[] @(S -> Type)) s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) MSR s r ys -> MSR s r ((':) @(S -> Type) y ys)
forall (ys :: [S -> Type]) (y :: S -> Type).
MSR s r ys -> MSR s r ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
SListI @(S -> Type) ys =>
MSR s r ys -> MSR s r ((':) @(S -> Type) y ys)
go) PRec struct s -> Term s r
f
   in
    Term s (PHandlerTy r struct)
handler

pmatchSOPRec ::
  forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S). SListI struct => Term s (PSOPRec struct) -> (PRec struct s -> Term s r) -> Term s r
pmatchSOPRec :: forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
Term s (PSOPRec struct) -> (PRec struct s -> Term s r) -> Term s r
pmatchSOPRec Term s (PSOPRec struct)
xs PRec struct s -> Term s r
f = (Word64 -> TermMonad TermResult) -> Term s r
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s r)
-> (Word64 -> TermMonad TermResult) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Word64
i -> do
  (RawTerm
term, [HoistedTerm]
deps) <- (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> (RawTerm, [HoistedTerm]))
-> TermMonad TermResult -> TermMonad (RawTerm, [HoistedTerm])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s (PSOPRec struct) -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s (PSOPRec struct)
xs Word64
i
  (RawTerm
handlerTerm, [HoistedTerm]
handlerDeps) <- (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> (RawTerm, [HoistedTerm]))
-> TermMonad TermResult -> TermMonad (RawTerm, [HoistedTerm])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s (PHandlerTy r struct) -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm ((PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
(PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
sopHandler PRec struct s -> Term s r
f) Word64
i
  TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> TermResult -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult (RawTerm -> [RawTerm] -> RawTerm
RCase RawTerm
term (RawTerm -> [RawTerm]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure RawTerm
handlerTerm)) ([HoistedTerm]
deps [HoistedTerm] -> [HoistedTerm] -> [HoistedTerm]
forall a. Semigroup a => a -> a -> a
<> [HoistedTerm]
handlerDeps)

pconSOPStruct ::
  forall (struct :: [[S -> Type]]) (s :: S). SListI2 struct => PStruct struct s -> Term s (PSOPStruct struct)
pconSOPStruct :: forall (struct :: [[S -> Type]]) (s :: S).
SListI2 @(S -> Type) struct =>
PStruct struct s -> Term s (PSOPStruct struct)
pconSOPStruct (PStruct SOP @(S -> Type) (Term s) struct
xs') = SOP @(S -> Type) (Term s) struct
-> (SOP @(S -> Type) (Term s) struct -> Term s (PSOPStruct struct))
-> Term s (PSOPStruct struct)
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 @(S -> Type) (Term s) struct -> Term s (PSOPStruct struct))
 -> Term s (PSOPStruct struct))
-> (SOP @(S -> Type) (Term s) struct -> Term s (PSOPStruct struct))
-> Term s (PSOPStruct struct)
forall a b. (a -> b) -> a -> b
$ \SOP @(S -> Type) (Term s) struct
xs -> (Word64 -> TermMonad TermResult) -> Term s (PSOPStruct struct)
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s (PSOPStruct struct))
-> (Word64 -> TermMonad TermResult) -> Term s (PSOPStruct struct)
forall a b. (a -> b) -> a -> b
$ \Word64
i -> do
  [(RawTerm, [HoistedTerm])]
ts <- SOP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct
-> CollapseTo
     @(S -> Type)
     @[[S -> Type]]
     (SOP @(S -> Type))
     (RawTerm, [HoistedTerm])
forall (xs :: [[S -> Type]]) a.
SListIN @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) xs =>
SOP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) a
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
SOP.hcollapse (SOP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct
 -> CollapseTo
      @(S -> Type)
      @[[S -> Type]]
      (SOP @(S -> Type))
      (RawTerm, [HoistedTerm]))
-> TermMonad
     (SOP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct)
-> TermMonad
     (CollapseTo
        @(S -> Type)
        @[[S -> Type]]
        (SOP @(S -> Type))
        (RawTerm, [HoistedTerm]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (a :: S -> Type).
 Term s a -> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a))
-> SOP @(S -> Type) (Term s) struct
-> TermMonad
     (SOP @(S -> Type) (K @(S -> Type) (RawTerm, [HoistedTerm])) struct)
forall (xs :: [[S -> Type]]) (g :: Type -> Type)
       (f :: (S -> Type) -> Type) (f' :: (S -> Type) -> Type).
(SListIN @(S -> Type) @[[S -> Type]] (SOP @(S -> Type)) xs,
 Applicative g) =>
(forall (a :: S -> Type). f a -> g (f' a))
-> SOP @(S -> Type) f xs -> g (SOP @(S -> Type) f' xs)
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l)
       (g :: Type -> Type) (f :: k -> Type) (f' :: k -> Type).
(HSequence @k @l h, SListIN @k @l h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
SOP.htraverse' (\Term s a
x -> (RawTerm, [HoistedTerm])
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall k a (b :: k). a -> K @k a b
K ((RawTerm, [HoistedTerm])
 -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> (TermResult -> (RawTerm, [HoistedTerm]))
-> TermResult
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> TermMonad TermResult
-> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s a -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s a
x Word64
i) SOP @(S -> Type) (Term s) struct
xs
  let
    idx :: Int
idx = SOP @(S -> Type) (Term s) struct -> Int
forall k l (h :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (xs :: l).
HIndex @k @l h =>
h f xs -> Int
forall (f :: (S -> Type) -> Type) (xs :: [[S -> Type]]).
SOP @(S -> Type) f xs -> Int
SOP.hindex SOP @(S -> Type) (Term s) struct
xs
    term :: RawTerm
term = Word64 -> [RawTerm] -> RawTerm
RConstr (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
idx) ([RawTerm] -> RawTerm) -> [RawTerm] -> RawTerm
forall a b. (a -> b) -> a -> b
$ (RawTerm, [HoistedTerm]) -> RawTerm
forall a b. (a, b) -> a
fst ((RawTerm, [HoistedTerm]) -> RawTerm)
-> [(RawTerm, [HoistedTerm])] -> [RawTerm]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
ts
    deps :: [HoistedTerm]
deps = [[HoistedTerm]] -> [HoistedTerm]
forall a. Monoid a => [a] -> a
mconcat ([[HoistedTerm]] -> [HoistedTerm])
-> [[HoistedTerm]] -> [HoistedTerm]
forall a b. (a -> b) -> a -> b
$ (RawTerm, [HoistedTerm]) -> [HoistedTerm]
forall a b. (a, b) -> b
snd ((RawTerm, [HoistedTerm]) -> [HoistedTerm])
-> [(RawTerm, [HoistedTerm])] -> [[HoistedTerm]]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
ts
  TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> TermResult -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult RawTerm
term [HoistedTerm]
deps

newtype MSS s r struct = MSS
  { forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
MSS s r struct
-> (PStruct struct s -> Term s r)
-> NP @(S -> Type) (Term s) (PCaseTy r struct)
unMSS :: (PStruct struct s -> Term s r) -> NP (Term s) (PCaseTy r struct)
  }

pmatchSOPStruct ::
  forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
  (SListI2 struct, PSOPStructConstraint struct) =>
  Term s (PSOPStruct struct) ->
  (PStruct struct s -> Term s r) ->
  Term s r
pmatchSOPStruct :: forall (struct :: [[S -> Type]]) (r :: S -> Type) (s :: S).
(SListI2 @(S -> Type) struct, PSOPStructConstraint struct) =>
Term s (PSOPStruct struct)
-> (PStruct struct s -> Term s r) -> Term s r
pmatchSOPStruct Term s (PSOPStruct struct)
xs PStruct struct s -> Term s r
h = (Word64 -> TermMonad TermResult) -> Term s r
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s r)
-> (Word64 -> TermMonad TermResult) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Word64
i -> do
  (RawTerm
term, [HoistedTerm]
deps) <- (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> (RawTerm, [HoistedTerm]))
-> TermMonad TermResult -> TermMonad (RawTerm, [HoistedTerm])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s (PSOPStruct struct) -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s (PSOPStruct struct)
xs Word64
i

  let
    go :: forall y ys r s. SListI y => MSS s r ys -> MSS s r (y ': ys)
    go :: forall (y :: [S -> Type]) (ys :: [[S -> Type]]) (r :: S -> Type)
       (s :: S).
SListI @(S -> Type) y =>
MSS s r ys -> MSS s r ((':) @[S -> Type] y ys)
go (MSS (PStruct ys s -> Term s r)
-> NP @(S -> Type) (Term s) (PCaseTy r ys)
rest) = ((PStruct ((':) @[S -> Type] y ys) s -> Term s r)
 -> NP @(S -> Type) (Term s) (PCaseTy r ((':) @[S -> Type] y ys)))
-> MSS s r ((':) @[S -> Type] y ys)
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
((PStruct struct s -> Term s r)
 -> NP @(S -> Type) (Term s) (PCaseTy r struct))
-> MSS s r struct
MSS (((PStruct ((':) @[S -> Type] y ys) s -> Term s r)
  -> NP @(S -> Type) (Term s) (PCaseTy r ((':) @[S -> Type] y ys)))
 -> MSS s r ((':) @[S -> Type] y ys))
-> ((PStruct ((':) @[S -> Type] y ys) s -> Term s r)
    -> NP @(S -> Type) (Term s) (PCaseTy r ((':) @[S -> Type] y ys)))
-> MSS s r ((':) @[S -> Type] y ys)
forall a b. (a -> b) -> a -> b
$ \PStruct ((':) @[S -> Type] y ys) s -> Term s r
f ->
      let
        handler :: Term s (PHandlerTy r y)
handler = (PRec y s -> Term s r) -> Term s (PHandlerTy r y)
forall (struct :: [S -> Type]) (r :: S -> Type) (s :: S).
SListI @(S -> Type) struct =>
(PRec struct s -> Term s r) -> Term s (PHandlerTy r struct)
sopHandler (\(PRec NP @(S -> Type) (Term s) y
x) -> PStruct ((':) @[S -> Type] y ys) s -> Term s r
f (PStruct ((':) @[S -> Type] y ys) s -> Term s r)
-> PStruct ((':) @[S -> Type] y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ 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
x)
        f' :: PStruct ys s -> Term s r
f' (PStruct (SOP NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
x)) = PStruct ((':) @[S -> Type] y ys) s -> Term s r
f (PStruct ((':) @[S -> Type] y ys) s -> Term s r)
-> PStruct ((':) @[S -> Type] y ys) s -> Term s r
forall a b. (a -> b) -> a -> b
$ 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
$ 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)
SOP.S NS @[S -> Type] (NP @(S -> Type) (Term s)) ys
x
       in
        Term s (PHandlerTy r y)
handler Term s (PHandlerTy r y)
-> NP @(S -> Type) (Term s) (PCaseTy r ys)
-> NP
     @(S -> Type)
     (Term s)
     ((':) @(S -> Type) (PHandlerTy r y) (PCaseTy r ys))
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) (PCaseTy r ys)
rest PStruct ys s -> Term s r
f'

    handlers' :: NP (Term s) (PCaseTy r struct)
    handlers' :: NP @(S -> Type) (Term s) (PCaseTy r struct)
handlers' = MSS s r struct
-> (PStruct struct s -> Term s r)
-> NP @(S -> Type) (Term s) (PCaseTy r struct)
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
MSS s r struct
-> (PStruct struct s -> Term s r)
-> NP @(S -> Type) (Term s) (PCaseTy r struct)
unMSS (Proxy @([S -> Type] -> Constraint) (SListI @(S -> Type))
-> MSS s r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SListI @(S -> Type) y,
     All @[S -> Type] (SListI @(S -> Type)) ys) =>
    MSS s r ys -> MSS s r ((':) @[S -> Type] y ys))
-> MSS s r struct
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 struct
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) (PCaseTy r ('[] @[S -> Type])))
-> MSS s r ('[] @[S -> Type])
forall (s :: S) (r :: S -> Type) (struct :: [[S -> Type]]).
((PStruct struct s -> Term s r)
 -> NP @(S -> Type) (Term s) (PCaseTy r struct))
-> MSS s r struct
MSS (((PStruct ('[] @[S -> Type]) s -> Term s r)
  -> NP @(S -> Type) (Term s) (PCaseTy r ('[] @[S -> Type])))
 -> MSS s r ('[] @[S -> Type]))
-> ((PStruct ('[] @[S -> Type]) s -> Term s r)
    -> NP @(S -> Type) (Term s) (PCaseTy r ('[] @[S -> Type])))
-> MSS s r ('[] @[S -> Type])
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) (PCaseTy r ('[] @[S -> Type]))
-> (PStruct ('[] @[S -> Type]) s -> Term s r)
-> NP @(S -> Type) (Term s) (PCaseTy r ('[] @[S -> Type]))
forall a b. a -> b -> a
const NP @(S -> Type) (Term s) ('[] @(S -> Type))
NP @(S -> Type) (Term s) (PCaseTy r ('[] @[S -> Type]))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) MSS s r ys -> MSS s r ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
(SListI @(S -> Type) y,
 All @[S -> Type] (SListI @(S -> Type)) ys) =>
MSS s r ys -> MSS s r ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]) (r :: S -> Type)
       (s :: S).
SListI @(S -> Type) y =>
MSS s r ys -> MSS s r ((':) @[S -> Type] y ys)
go) PStruct struct s -> Term s r
h

  [(RawTerm, [HoistedTerm])]
handlers <- NP
  @(S -> Type)
  (K @(S -> Type) (RawTerm, [HoistedTerm]))
  (PCaseTy r struct)
-> CollapseTo
     @(S -> Type)
     @[S -> Type]
     (NP @(S -> Type))
     (RawTerm, [HoistedTerm])
forall (xs :: [S -> Type]) a.
SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs =>
NP @(S -> Type) (K @(S -> Type) a) xs
-> CollapseTo @(S -> Type) @[S -> Type] (NP @(S -> Type)) a
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse @k @l h, SListIN @k @l h xs) =>
h (K @k a) xs -> CollapseTo @k @l h a
SOP.hcollapse (NP
   @(S -> Type)
   (K @(S -> Type) (RawTerm, [HoistedTerm]))
   (PCaseTy r struct)
 -> CollapseTo
      @(S -> Type)
      @[S -> Type]
      (NP @(S -> Type))
      (RawTerm, [HoistedTerm]))
-> TermMonad
     (NP
        @(S -> Type)
        (K @(S -> Type) (RawTerm, [HoistedTerm]))
        (PCaseTy r struct))
-> TermMonad
     (CollapseTo
        @(S -> Type)
        @[S -> Type]
        (NP @(S -> Type))
        (RawTerm, [HoistedTerm]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (a :: S -> Type).
 Term s a -> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a))
-> NP @(S -> Type) (Term s) (PCaseTy r struct)
-> TermMonad
     (NP
        @(S -> Type)
        (K @(S -> Type) (RawTerm, [HoistedTerm]))
        (PCaseTy r struct))
forall (xs :: [S -> Type]) (g :: Type -> Type)
       (f :: (S -> Type) -> Type) (f' :: (S -> Type) -> Type).
(SListIN @(S -> Type) @[S -> Type] (NP @(S -> Type)) xs,
 Applicative g) =>
(forall (a :: S -> Type). f a -> g (f' a))
-> NP @(S -> Type) f xs -> g (NP @(S -> Type) f' xs)
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l)
       (g :: Type -> Type) (f :: k -> Type) (f' :: k -> Type).
(HSequence @k @l h, SListIN @k @l h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
SOP.htraverse' (\Term s a
x -> (RawTerm, [HoistedTerm])
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall k a (b :: k). a -> K @k a b
K ((RawTerm, [HoistedTerm])
 -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> (TermResult -> (RawTerm, [HoistedTerm]))
-> TermResult
-> K @(S -> Type) (RawTerm, [HoistedTerm]) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TermResult -> RawTerm
getTerm (TermResult -> RawTerm)
-> (TermResult -> [HoistedTerm])
-> TermResult
-> (RawTerm, [HoistedTerm])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: Type -> Type -> Type) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& TermResult -> [HoistedTerm]
getDeps) (TermResult -> K @(S -> Type) (RawTerm, [HoistedTerm]) a)
-> TermMonad TermResult
-> TermMonad (K @(S -> Type) (RawTerm, [HoistedTerm]) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Term s a -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s a
x Word64
i) NP @(S -> Type) (Term s) (PCaseTy r struct)
handlers'
  let
    handlerTerms :: [RawTerm]
handlerTerms = (RawTerm, [HoistedTerm]) -> RawTerm
forall a b. (a, b) -> a
fst ((RawTerm, [HoistedTerm]) -> RawTerm)
-> [(RawTerm, [HoistedTerm])] -> [RawTerm]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
handlers
    handlerDeps :: [HoistedTerm]
handlerDeps = [[HoistedTerm]] -> [HoistedTerm]
forall a. Monoid a => [a] -> a
mconcat ([[HoistedTerm]] -> [HoistedTerm])
-> [[HoistedTerm]] -> [HoistedTerm]
forall a b. (a -> b) -> a -> b
$ (RawTerm, [HoistedTerm]) -> [HoistedTerm]
forall a b. (a, b) -> b
snd ((RawTerm, [HoistedTerm]) -> [HoistedTerm])
-> [(RawTerm, [HoistedTerm])] -> [[HoistedTerm]]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RawTerm, [HoistedTerm])]
handlers

  TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> TermResult -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ RawTerm -> [HoistedTerm] -> TermResult
TermResult (RawTerm -> [RawTerm] -> RawTerm
RCase RawTerm
term [RawTerm]
handlerTerms) ([HoistedTerm]
handlerDeps [HoistedTerm] -> [HoistedTerm] -> [HoistedTerm]
forall a. Semigroup a => a -> a -> a
<> [HoistedTerm]
deps)

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

class (a ~ AsHaskell b, PLiftable b) => ToAsHaskell (a :: Type) (b :: S -> Type)
instance (a ~ AsHaskell b, PLiftable b) => ToAsHaskell (a :: Type) (b :: S -> Type)

newtype PSOPRecPLiftableHelper (struct :: [S -> Type]) = PSOPRecPLiftableHelper
  { forall (struct :: [S -> Type]).
PSOPRecPLiftableHelper struct
-> PLiftedClosed (PSOPRec struct)
-> Either LiftError (NP @Type I (RecAsHaskell struct))
unPSOPRecPLiftableHelper ::
      PLiftedClosed (PSOPRec struct) ->
      Either LiftError (SOP.NP SOP.I (RecAsHaskell struct))
  }

-- | @since WIP
instance
  forall (struct :: [S -> Type]) (hstruct :: [Type]).
  ( SListI struct
  , hstruct ~ RecAsHaskell struct
  , SOP.AllZip ToAsHaskell hstruct struct
  , SOP.All PLiftable struct
  ) =>
  PLiftable (PSOPRec struct)
  where
  type AsHaskell (PSOPRec struct) = SOP SOP.I '[RecAsHaskell struct]
  type PlutusRepr (PSOPRec struct) = PLiftedClosed (PSOPRec struct)
  haskToRepr :: AsHaskell (PSOPRec struct) -> PlutusRepr (PSOPRec struct)
haskToRepr AsHaskell (PSOPRec struct)
x =
    let
      f :: forall a b s. ToAsHaskell a b => SOP.I a -> Term s b
      f :: forall a (b :: S -> Type) (s :: S).
ToAsHaskell a b =>
I a -> Term s b
f = forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @b (AsHaskell b -> Term s b)
-> (I (AsHaskell b) -> AsHaskell b) -> I (AsHaskell b) -> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I (AsHaskell b) -> AsHaskell b
forall a. I a -> a
SOP.unI
     in
      (forall (s :: S). Term s (PSOPRec struct))
-> PLiftedClosed (PSOPRec struct)
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> PLiftedClosed a
mkPLiftedClosed ((forall (s :: S). Term s (PSOPRec struct))
 -> PLiftedClosed (PSOPRec struct))
-> (forall (s :: S). Term s (PSOPRec struct))
-> PLiftedClosed (PSOPRec struct)
forall a b. (a -> b) -> a -> b
$
        PSOPRec struct s -> Term s (PSOPRec struct)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSOPRec struct s -> Term s (PSOPRec struct))
-> PSOPRec struct s -> Term s (PSOPRec struct)
forall a b. (a -> b) -> a -> b
$
          PRec struct s -> PSOPRec struct s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PSOPRec struct s
PSOPRec (PRec struct s -> PSOPRec struct s)
-> PRec struct s -> PSOPRec 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
$
                  Proxy @(Type -> (S -> Type) -> Constraint) ToAsHaskell
-> (forall x (y :: S -> Type). ToAsHaskell x y => I x -> Term s y)
-> SOP @Type I ((':) @[Type] hstruct ('[] @[Type]))
-> 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) (c :: k1 -> k2 -> Constraint)
       (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> Type)
       (f :: k1 -> Type) (g :: k2 -> Type).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN @k1 @l1 @k1 @k2 @l1 @l2 (Prod @k1 @l1 h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
forall (c :: Type -> (S -> Type) -> Constraint) (xs :: [[Type]])
       (ys :: [[S -> Type]])
       (proxy :: (Type -> (S -> Type) -> Constraint) -> Type)
       (f :: Type -> Type) (g :: (S -> Type) -> Type).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  c
  xs
  ys =>
proxy c
-> (forall x (y :: S -> Type). c x y => f x -> g y)
-> SOP @Type f xs
-> SOP @(S -> Type) g ys
SOP.htrans (forall {k} (t :: k). Proxy @k t
forall (t :: Type -> (S -> Type) -> Constraint).
Proxy @(Type -> (S -> Type) -> Constraint) t
Proxy @ToAsHaskell) I x -> Term s y
forall x (y :: S -> Type). ToAsHaskell x y => I x -> Term s y
forall a (b :: S -> Type) (s :: S).
ToAsHaskell a b =>
I a -> Term s b
f SOP @Type I ((':) @[Type] hstruct ('[] @[Type]))
AsHaskell (PSOPRec struct)
x
  reprToHask :: PlutusRepr (PSOPRec struct)
-> Either LiftError (AsHaskell (PSOPRec struct))
reprToHask PlutusRepr (PSOPRec struct)
x =
    let
      go :: forall y ys. (SOP.SListI ys, PLiftable y) => PSOPRecPLiftableHelper ys -> PSOPRecPLiftableHelper (y ': ys)
      go :: forall (y :: S -> Type) (ys :: [S -> Type]).
(SListI @(S -> Type) ys, PLiftable y) =>
PSOPRecPLiftableHelper ys
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
go (PSOPRecPLiftableHelper PLiftedClosed (PSOPRec ys)
-> Either LiftError (NP @Type I (RecAsHaskell ys))
rest) = (PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
 -> Either
      LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (struct :: [S -> Type]).
(PLiftedClosed (PSOPRec struct)
 -> Either LiftError (NP @Type I (RecAsHaskell struct)))
-> PSOPRecPLiftableHelper struct
PSOPRecPLiftableHelper ((PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
  -> Either
       LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
 -> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys))
-> (PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
    -> Either
         LiftError (NP @Type I (RecAsHaskell ((':) @(S -> Type) y ys))))
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
forall a b. (a -> b) -> a -> b
$ \PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
x -> do
        NP @Type I (RecAsHaskell ys)
rest' <-
          PLiftedClosed (PSOPRec ys)
-> Either LiftError (NP @Type I (RecAsHaskell ys))
rest (PLiftedClosed (PSOPRec ys)
 -> Either LiftError (NP @Type I (RecAsHaskell ys)))
-> PLiftedClosed (PSOPRec ys)
-> Either LiftError (NP @Type I (RecAsHaskell ys))
forall a b. (a -> b) -> a -> b
$
            (forall (s :: S). Term s (PSOPRec ys))
-> PLiftedClosed (PSOPRec ys)
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> PLiftedClosed a
mkPLiftedClosed ((forall (s :: S). Term s (PSOPRec ys))
 -> PLiftedClosed (PSOPRec ys))
-> (forall (s :: S). Term s (PSOPRec ys))
-> PLiftedClosed (PSOPRec ys)
forall a b. (a -> b) -> a -> b
$
              Term s (PSOPRec ((':) @(S -> Type) y ys))
-> (PSOPRec ((':) @(S -> Type) y ys) s -> Term s (PSOPRec ys))
-> Term s (PSOPRec ys)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
-> forall (s :: S). Term s (PSOPRec ((':) @(S -> Type) y ys))
forall (a :: S -> Type).
PLiftedClosed a -> forall (s :: S). Term s a
getPLiftedClosed PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
x) ((PSOPRec ((':) @(S -> Type) y ys) s -> Term s (PSOPRec ys))
 -> Term s (PSOPRec ys))
-> (PSOPRec ((':) @(S -> Type) y ys) s -> Term s (PSOPRec ys))
-> Term s (PSOPRec ys)
forall a b. (a -> b) -> a -> b
$ \case
                (PSOPRec (PRec (Term s x
_ :* NP @(S -> Type) (Term s) xs
ds))) -> PSOPRec ys s -> Term s (PSOPRec ys)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSOPRec ys s -> Term s (PSOPRec ys))
-> PSOPRec ys s -> Term s (PSOPRec ys)
forall a b. (a -> b) -> a -> b
$ PRec ys s -> PSOPRec ys s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PSOPRec struct s
PSOPRec (PRec ys s -> PSOPRec ys s) -> PRec ys s -> PSOPRec ys s
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) xs -> PRec xs s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec NP @(S -> Type) (Term s) xs
ds
        AsHaskell y
curr <-
          ( forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @y ((forall (s :: S). PLifted s y) -> Either LiftError (PlutusRepr y))
-> (forall (s :: S). PLifted s y)
-> Either LiftError (PlutusRepr y)
forall a b. (a -> b) -> a -> b
$
              Term s y -> PLifted s y
forall (s :: S) (a :: S -> Type). Term s a -> PLifted s a
mkPLifted (Term s y -> PLifted s y) -> Term s y -> PLifted s y
forall a b. (a -> b) -> a -> b
$
                Term s (PSOPRec ((':) @(S -> Type) y ys))
-> (PSOPRec ((':) @(S -> Type) y ys) s -> Term s y) -> Term s y
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
-> forall (s :: S). Term s (PSOPRec ((':) @(S -> Type) y ys))
forall (a :: S -> Type).
PLiftedClosed a -> forall (s :: S). Term s a
getPLiftedClosed PLiftedClosed (PSOPRec ((':) @(S -> Type) y ys))
x) ((PSOPRec ((':) @(S -> Type) y ys) s -> Term s y) -> Term s y)
-> (PSOPRec ((':) @(S -> Type) y ys) s -> Term s y) -> Term s y
forall a b. (a -> b) -> a -> b
$ \case
                  (PSOPRec (PRec (Term s x
d :* NP @(S -> Type) (Term s) xs
_))) -> Term s y
Term s x
d
            )
            Either LiftError (PlutusRepr y)
-> (PlutusRepr y -> Either LiftError (AsHaskell y))
-> Either LiftError (AsHaskell y)
forall a b.
Either LiftError a
-> (a -> Either LiftError b) -> Either LiftError b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @y

        NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
-> Either
     LiftError (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys)))
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
 -> Either
      LiftError
      (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))))
-> NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
-> Either
     LiftError (NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys)))
forall a b. (a -> b) -> a -> b
$ AsHaskell y -> I (AsHaskell y)
forall a. a -> I a
SOP.I AsHaskell y
curr I (AsHaskell y)
-> NP @Type I (RecAsHaskell ys)
-> NP @Type I ((':) @Type (AsHaskell y) (RecAsHaskell ys))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @Type I (RecAsHaskell ys)
rest'
     in
      NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
-> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP.SOP (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
 -> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> (NP @Type I (RecAsHaskell struct)
    -> NS
         @[Type]
         (NP @Type I)
         ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> NP @Type I (RecAsHaskell struct)
-> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP @Type I (RecAsHaskell struct)
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] (RecAsHaskell struct) ('[] @[Type]))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
SOP.Z
        (NP @Type I (RecAsHaskell struct)
 -> SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
-> Either LiftError (NP @Type I (RecAsHaskell struct))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell struct) ('[] @[Type])))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (PSOPRecPLiftableHelper struct
-> PLiftedClosed (PSOPRec struct)
-> Either LiftError (NP @Type I (RecAsHaskell struct))
forall (struct :: [S -> Type]).
PSOPRecPLiftableHelper struct
-> PLiftedClosed (PSOPRec struct)
-> Either LiftError (NP @Type I (RecAsHaskell struct))
unPSOPRecPLiftableHelper (PSOPRecPLiftableHelper struct
 -> PLiftedClosed (PSOPRec struct)
 -> Either LiftError (NP @Type I (RecAsHaskell struct)))
-> PSOPRecPLiftableHelper struct
-> PLiftedClosed (PSOPRec struct)
-> Either LiftError (NP @Type I (RecAsHaskell struct))
forall a b. (a -> b) -> a -> b
$ Proxy @((S -> Type) -> Constraint) PLiftable
-> PSOPRecPLiftableHelper ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (PLiftable y, All @(S -> Type) PLiftable ys) =>
    PSOPRecPLiftableHelper ys
    -> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys))
-> PSOPRecPLiftableHelper struct
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 PLiftable
-> r ('[] @(S -> Type))
-> (forall (y :: S -> Type) (ys :: [S -> Type]).
    (PLiftable y, All @(S -> Type) PLiftable ys) =>
    r ys -> r ((':) @(S -> Type) y ys))
-> r struct
SOP.cpara_SList (forall {k} (t :: k). Proxy @k t
forall (t :: (S -> Type) -> Constraint).
Proxy @((S -> Type) -> Constraint) t
Proxy @PLiftable) ((PLiftedClosed (PSOPRec ('[] @(S -> Type)))
 -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> PSOPRecPLiftableHelper ('[] @(S -> Type))
forall (struct :: [S -> Type]).
(PLiftedClosed (PSOPRec struct)
 -> Either LiftError (NP @Type I (RecAsHaskell struct)))
-> PSOPRecPLiftableHelper struct
PSOPRecPLiftableHelper ((PLiftedClosed (PSOPRec ('[] @(S -> Type)))
  -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
 -> PSOPRecPLiftableHelper ('[] @(S -> Type)))
-> (PLiftedClosed (PSOPRec ('[] @(S -> Type)))
    -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> PSOPRecPLiftableHelper ('[] @(S -> Type))
forall a b. (a -> b) -> a -> b
$ Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
-> PLiftedClosed (PSOPRec ('[] @(S -> Type)))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. a -> b -> a
const (Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
 -> PLiftedClosed (PSOPRec ('[] @(S -> Type)))
 -> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type)))))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
-> PLiftedClosed (PSOPRec ('[] @(S -> Type)))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. (a -> b) -> a -> b
$ NP @Type I (RecAsHaskell ('[] @(S -> Type)))
-> Either LiftError (NP @Type I (RecAsHaskell ('[] @(S -> Type))))
forall a b. b -> Either a b
Right NP @Type I ('[] @Type)
NP @Type I (RecAsHaskell ('[] @(S -> Type)))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil) PSOPRecPLiftableHelper ys
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
(SListI @(S -> Type) ys, PLiftable y) =>
PSOPRecPLiftableHelper ys
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
forall (y :: S -> Type) (ys :: [S -> Type]).
(PLiftable y, All @(S -> Type) PLiftable ys) =>
PSOPRecPLiftableHelper ys
-> PSOPRecPLiftableHelper ((':) @(S -> Type) y ys)
go) PlutusRepr (PSOPRec struct)
PLiftedClosed (PSOPRec struct)
x
  {-# INLINEABLE reprToPlut #-}
  reprToPlut :: forall (s :: S).
PlutusRepr (PSOPRec struct) -> PLifted s (PSOPRec struct)
reprToPlut = PlutusRepr (PSOPRec struct) -> PLifted s (PSOPRec struct)
PLiftedClosed (PSOPRec struct) -> PLifted s (PSOPRec struct)
forall (a :: S -> Type) (s :: S). PLiftedClosed a -> PLifted s a
pliftedFromClosed
  {-# INLINEABLE plutToRepr #-}
  plutToRepr :: (forall (s :: S). PLifted s (PSOPRec struct))
-> Either LiftError (PlutusRepr (PSOPRec struct))
plutToRepr = PLiftedClosed (PSOPRec struct)
-> Either LiftError (PLiftedClosed (PSOPRec struct))
forall a b. b -> Either a b
Right (PLiftedClosed (PSOPRec struct)
 -> Either LiftError (PLiftedClosed (PSOPRec struct)))
-> ((forall (s :: S). PLifted s (PSOPRec struct))
    -> PLiftedClosed (PSOPRec struct))
-> (forall (s :: S). PLifted s (PSOPRec struct))
-> Either LiftError (PLiftedClosed (PSOPRec struct))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (s :: S). PLifted s (PSOPRec struct))
-> PLiftedClosed (PSOPRec struct)
forall (a :: S -> Type).
(forall (s :: S). PLifted s a) -> PLiftedClosed a
pliftedToClosed

newtype PSOPStructPLiftableHelper struct = PSOPStructPLiftableHelper
  { forall (struct :: [[S -> Type]]).
PSOPStructPLiftableHelper struct
-> PLiftedClosed (PSOPStruct struct)
-> Either LiftError (SOP @Type I (StructAsHaskell struct))
unPSOPStructPLiftableHelper ::
      PLiftedClosed (PSOPStruct struct) ->
      Either LiftError (SOP SOP.I (StructAsHaskell struct))
  }

class (SOP.AllZip ToAsHaskell (RecAsHaskell y) y, All PLiftable y) => SOPEntryConstraints y
instance (SOP.AllZip ToAsHaskell (RecAsHaskell y) y, All PLiftable y) => SOPEntryConstraints y

class (SListI2 ys, PSOPStructConstraint ys) => SOPRestConstraint ys
instance (SListI2 ys, PSOPStructConstraint ys) => SOPRestConstraint ys

-- | @since WIP
instance
  forall (struct :: [[S -> Type]]) (hstruct :: [[Type]]).
  ( SListI2 struct
  , hstruct ~ StructAsHaskell struct
  , SOP.AllZip2 ToAsHaskell hstruct struct
  , SOP.All2 PLiftable struct
  , MyAll SOPEntryConstraints SOPRestConstraint struct
  , PSOPStructConstraint struct
  ) =>
  PLiftable (PSOPStruct struct)
  where
  type AsHaskell (PSOPStruct struct) = SOP SOP.I (StructAsHaskell struct)
  type PlutusRepr (PSOPStruct struct) = PLiftedClosed (PSOPStruct struct)
  haskToRepr :: SOP SOP.I hstruct -> PLiftedClosed (PSOPStruct struct)
  haskToRepr :: SOP @Type I hstruct -> PLiftedClosed (PSOPStruct struct)
haskToRepr SOP @Type I hstruct
x =
    let
      f :: forall a b s. ToAsHaskell a b => SOP.I a -> Term s b
      f :: forall a (b :: S -> Type) (s :: S).
ToAsHaskell a b =>
I a -> Term s b
f = forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @b (AsHaskell b -> Term s b)
-> (I (AsHaskell b) -> AsHaskell b) -> I (AsHaskell b) -> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I (AsHaskell b) -> AsHaskell b
forall a. I a -> a
SOP.unI
     in
      (forall (s :: S). Term s (PSOPStruct struct))
-> PLiftedClosed (PSOPStruct struct)
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> PLiftedClosed a
mkPLiftedClosed ((forall (s :: S). Term s (PSOPStruct struct))
 -> PLiftedClosed (PSOPStruct struct))
-> (forall (s :: S). Term s (PSOPStruct struct))
-> PLiftedClosed (PSOPStruct struct)
forall a b. (a -> b) -> a -> b
$ PSOPStruct struct s -> Term s (PSOPStruct struct)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSOPStruct struct s -> Term s (PSOPStruct struct))
-> PSOPStruct struct s -> Term s (PSOPStruct struct)
forall a b. (a -> b) -> a -> b
$ PStruct struct s -> PSOPStruct struct s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PSOPStruct struct s
PSOPStruct (PStruct struct s -> PSOPStruct struct s)
-> PStruct struct s -> PSOPStruct struct s
forall a b. (a -> b) -> a -> b
$ 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
$ Proxy @(Type -> (S -> Type) -> Constraint) ToAsHaskell
-> (forall x (y :: S -> Type). ToAsHaskell x y => I x -> Term s y)
-> SOP @Type I hstruct
-> SOP @(S -> Type) (Term s) struct
forall k1 l1 k2 l2 (h1 :: (k1 -> Type) -> l1 -> Type)
       (h2 :: (k2 -> Type) -> l2 -> Type) (c :: k1 -> k2 -> Constraint)
       (xs :: l1) (ys :: l2) (proxy :: (k1 -> k2 -> Constraint) -> Type)
       (f :: k1 -> Type) (g :: k2 -> Type).
(HTrans @k1 @l1 @k2 @l2 h1 h2,
 AllZipN @k1 @l1 @k1 @k2 @l1 @l2 (Prod @k1 @l1 h1) c xs ys) =>
proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> h1 f xs
-> h2 g ys
forall (c :: Type -> (S -> Type) -> Constraint) (xs :: [[Type]])
       (ys :: [[S -> Type]])
       (proxy :: (Type -> (S -> Type) -> Constraint) -> Type)
       (f :: Type -> Type) (g :: (S -> Type) -> Type).
AllZipN
  @Type
  @[[Type]]
  @Type
  @(S -> Type)
  @[[Type]]
  @[[S -> Type]]
  (Prod @Type @[[Type]] (SOP @Type))
  c
  xs
  ys =>
proxy c
-> (forall x (y :: S -> Type). c x y => f x -> g y)
-> SOP @Type f xs
-> SOP @(S -> Type) g ys
SOP.htrans (forall {k} (t :: k). Proxy @k t
forall (t :: Type -> (S -> Type) -> Constraint).
Proxy @(Type -> (S -> Type) -> Constraint) t
Proxy @ToAsHaskell) I x -> Term s y
forall x (y :: S -> Type). ToAsHaskell x y => I x -> Term s y
forall a (b :: S -> Type) (s :: S).
ToAsHaskell a b =>
I a -> Term s b
f SOP @Type I hstruct
x
  reprToHask :: PLiftedClosed (PSOPStruct struct) -> Either LiftError (SOP SOP.I hstruct)
  reprToHask :: PLiftedClosed (PSOPStruct struct)
-> Either LiftError (SOP @Type I hstruct)
reprToHask PLiftedClosed (PSOPStruct struct)
x =
    let
      go ::
        forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
        (SOPRestConstraint ys, SOPEntryConstraints y) =>
        PSOPStructPLiftableHelper ys ->
        PSOPStructPLiftableHelper (y ': ys)
      go :: forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
(SOPRestConstraint ys, SOPEntryConstraints y) =>
PSOPStructPLiftableHelper ys
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
go (PSOPStructPLiftableHelper PLiftedClosed (PSOPStruct ys)
-> Either LiftError (SOP @Type I (StructAsHaskell ys))
rest) = (PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
 -> Either
      LiftError (SOP @Type I (StructAsHaskell ((':) @[S -> Type] y ys))))
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
forall (struct :: [[S -> Type]]).
(PLiftedClosed (PSOPStruct struct)
 -> Either LiftError (SOP @Type I (StructAsHaskell struct)))
-> PSOPStructPLiftableHelper struct
PSOPStructPLiftableHelper ((PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
  -> Either
       LiftError (SOP @Type I (StructAsHaskell ((':) @[S -> Type] y ys))))
 -> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys))
-> (PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
    -> Either
         LiftError (SOP @Type I (StructAsHaskell ((':) @[S -> Type] y ys))))
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
forall a b. (a -> b) -> a -> b
$ \PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
d -> do
        let
          isCurrent :: Bool
          isCurrent :: Bool
isCurrent =
            (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). Term s a) -> AsHaskell a
plift ((forall (s :: S). Term s PBool) -> AsHaskell PBool)
-> (forall (s :: S). Term s PBool) -> AsHaskell PBool
forall a b. (a -> b) -> a -> b
$
              Term s (PSOPStruct ((':) @[S -> Type] y ys))
-> (PSOPStruct ((':) @[S -> Type] y ys) 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 (PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
-> forall (s :: S). Term s (PSOPStruct ((':) @[S -> Type] y ys))
forall (a :: S -> Type).
PLiftedClosed a -> forall (s :: S). Term s a
getPLiftedClosed PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
d) ((PSOPStruct ((':) @[S -> Type] y ys) s -> Term s PBool)
 -> Term s PBool)
-> (PSOPStruct ((':) @[S -> Type] y ys) s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
                (PSOPStruct (PStruct (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
_)))) -> forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PBool Bool
AsHaskell PBool
False
                (PSOPStruct (PStruct (SOP (Z NP @(S -> Type) (Term s) x
_)))) -> forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PBool Bool
AsHaskell PBool
True

        if Bool
isCurrent
          then do
            SOP @Type I ((':) @[Type] (RecAsHaskell y) ('[] @[Type]))
curr <-
              ( forall (a :: S -> Type).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (PlutusRepr a)
plutToRepr @(PSOPRec y) ((forall (s :: S). PLifted s (PSOPRec y))
 -> Either LiftError (PlutusRepr (PSOPRec y)))
-> (forall (s :: S). PLifted s (PSOPRec y))
-> Either LiftError (PlutusRepr (PSOPRec y))
forall a b. (a -> b) -> a -> b
$
                  Term s (PSOPRec y) -> PLifted s (PSOPRec y)
forall (s :: S) (a :: S -> Type). Term s a -> PLifted s a
mkPLifted (Term s (PSOPRec y) -> PLifted s (PSOPRec y))
-> Term s (PSOPRec y) -> PLifted s (PSOPRec y)
forall a b. (a -> b) -> a -> b
$
                    Term s (PSOPStruct ((':) @[S -> Type] y ys))
-> (PSOPStruct ((':) @[S -> Type] y ys) s -> Term s (PSOPRec y))
-> Term s (PSOPRec y)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
-> forall (s :: S). Term s (PSOPStruct ((':) @[S -> Type] y ys))
forall (a :: S -> Type).
PLiftedClosed a -> forall (s :: S). Term s a
getPLiftedClosed PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
d) ((PSOPStruct ((':) @[S -> Type] y ys) s -> Term s (PSOPRec y))
 -> Term s (PSOPRec y))
-> (PSOPStruct ((':) @[S -> Type] y ys) s -> Term s (PSOPRec y))
-> Term s (PSOPRec y)
forall a b. (a -> b) -> a -> b
$ \case
                      (PSOPStruct (PStruct (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
_x')))) -> Term s (PSOPRec y)
forall (s :: S) (a :: S -> Type). Term s a
perror
                      (PSOPStruct (PStruct (SOP (Z NP @(S -> Type) (Term s) x
x')))) -> PSOPRec y s -> Term s (PSOPRec y)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSOPRec y s -> Term s (PSOPRec y))
-> PSOPRec y s -> Term s (PSOPRec y)
forall a b. (a -> b) -> a -> b
$ PRec y s -> PSOPRec y s
forall (struct :: [S -> Type]) (s :: S).
PRec struct s -> PSOPRec struct s
PSOPRec (PRec y s -> PSOPRec y s) -> PRec y s -> PSOPRec y s
forall a b. (a -> b) -> a -> b
$ NP @(S -> Type) (Term s) x -> PRec x s
forall (struct :: [S -> Type]) (s :: S).
NP @(S -> Type) (Term s) struct -> PRec struct s
PRec NP @(S -> Type) (Term s) x
x'
                )
                Either LiftError (PlutusRepr (PSOPRec y))
-> (PlutusRepr (PSOPRec y)
    -> Either LiftError (AsHaskell (PSOPRec y)))
-> Either LiftError (AsHaskell (PSOPRec y))
forall a b.
Either LiftError a
-> (a -> Either LiftError b) -> Either LiftError b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (a :: S -> Type).
PLiftable a =>
PlutusRepr a -> Either LiftError (AsHaskell a)
reprToHask @(PSOPRec y)

            SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys)))
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
 -> Either
      LiftError
      (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))))
-> SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys)))
forall a b. (a -> b) -> a -> b
$ case SOP @Type I ((':) @[Type] (RecAsHaskell y) ('[] @[Type]))
curr of
              (SOP (Z (NP @Type I (RecAsHaskell y)
curr' :: NP SOP.I (RecAsHaskell y)))) -> NS @[Type] (NP @Type I) ((':) @[Type] x (StructAsHaskell ys))
-> SOP @Type I ((':) @[Type] x (StructAsHaskell ys))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) ((':) @[Type] x (StructAsHaskell ys))
 -> SOP @Type I ((':) @[Type] x (StructAsHaskell ys)))
-> NS @[Type] (NP @Type I) ((':) @[Type] x (StructAsHaskell ys))
-> SOP @Type I ((':) @[Type] x (StructAsHaskell ys))
forall a b. (a -> b) -> a -> b
$ NP @Type I (RecAsHaskell y)
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z NP @Type I (RecAsHaskell y)
curr'
              SOP @Type I ((':) @[Type] (RecAsHaskell y) ('[] @[Type]))
_ -> [Char]
-> SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
forall a. HasCallStack => [Char] -> a
error [Char]
"no B"
          else do
            SOP NS @[Type] (NP @Type I) (StructAsHaskell ys)
next <-
              PLiftedClosed (PSOPStruct ys)
-> Either LiftError (SOP @Type I (StructAsHaskell ys))
rest (PLiftedClosed (PSOPStruct ys)
 -> Either LiftError (SOP @Type I (StructAsHaskell ys)))
-> PLiftedClosed (PSOPStruct ys)
-> Either LiftError (SOP @Type I (StructAsHaskell ys))
forall a b. (a -> b) -> a -> b
$
                (forall (s :: S). Term s (PSOPStruct ys))
-> PLiftedClosed (PSOPStruct ys)
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> PLiftedClosed a
mkPLiftedClosed ((forall (s :: S). Term s (PSOPStruct ys))
 -> PLiftedClosed (PSOPStruct ys))
-> (forall (s :: S). Term s (PSOPStruct ys))
-> PLiftedClosed (PSOPStruct ys)
forall a b. (a -> b) -> a -> b
$
                  Term s (PSOPStruct ((':) @[S -> Type] y ys))
-> (PSOPStruct ((':) @[S -> Type] y ys) s
    -> Term s (PSOPStruct ys))
-> Term s (PSOPStruct ys)
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
-> forall (s :: S). Term s (PSOPStruct ((':) @[S -> Type] y ys))
forall (a :: S -> Type).
PLiftedClosed a -> forall (s :: S). Term s a
getPLiftedClosed PLiftedClosed (PSOPStruct ((':) @[S -> Type] y ys))
d) ((PSOPStruct ((':) @[S -> Type] y ys) s -> Term s (PSOPStruct ys))
 -> Term s (PSOPStruct ys))
-> (PSOPStruct ((':) @[S -> Type] y ys) s
    -> Term s (PSOPStruct ys))
-> Term s (PSOPStruct ys)
forall a b. (a -> b) -> a -> b
$ \case
                    (PSOPStruct (PStruct (SOP (S NS @[S -> Type] (NP @(S -> Type) (Term s)) xs
x')))) -> PSOPStruct ys s -> Term s (PSOPStruct ys)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PSOPStruct ys s -> Term s (PSOPStruct ys))
-> PSOPStruct ys s -> Term s (PSOPStruct ys)
forall a b. (a -> b) -> a -> b
$ PStruct ys s -> PSOPStruct ys s
forall (struct :: [[S -> Type]]) (s :: S).
PStruct struct s -> PSOPStruct struct s
PSOPStruct (PStruct ys s -> PSOPStruct ys s)
-> PStruct ys s -> PSOPStruct ys s
forall a b. (a -> b) -> a -> b
$ 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
x'
                    (PSOPStruct (PStruct (SOP (Z NP @(S -> Type) (Term s) x
_x')))) -> Term s (PSOPStruct ys)
forall (s :: S) (a :: S -> Type). Term s a
perror

            SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys)))
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
 -> Either
      LiftError
      (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))))
-> SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> Either
     LiftError
     (SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys)))
forall a b. (a -> b) -> a -> b
$ NS
  @[Type]
  (NP @Type I)
  ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS
   @[Type]
   (NP @Type I)
   ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
 -> SOP
      @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys)))
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
-> SOP @Type I ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) (StructAsHaskell ys)
-> NS
     @[Type]
     (NP @Type I)
     ((':) @[Type] (RecAsHaskell y) (StructAsHaskell ys))
forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S NS @[Type] (NP @Type I) (StructAsHaskell ys)
next
     in
      ( PSOPStructPLiftableHelper struct
-> PLiftedClosed (PSOPStruct struct)
-> Either LiftError (SOP @Type I (StructAsHaskell struct))
forall (struct :: [[S -> Type]]).
PSOPStructPLiftableHelper struct
-> PLiftedClosed (PSOPStruct struct)
-> Either LiftError (SOP @Type I (StructAsHaskell struct))
unPSOPStructPLiftableHelper (PSOPStructPLiftableHelper struct
 -> PLiftedClosed (PSOPStruct struct)
 -> Either LiftError (SOP @Type I (StructAsHaskell struct)))
-> PSOPStructPLiftableHelper struct
-> PLiftedClosed (PSOPStruct struct)
-> Either LiftError (SOP @Type I (StructAsHaskell struct))
forall a b. (a -> b) -> a -> b
$
          Proxy @([S -> Type] -> Constraint) SOPEntryConstraints
-> Proxy @([[S -> Type]] -> Constraint) SOPRestConstraint
-> PSOPStructPLiftableHelper ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SOPEntryConstraints y, SOPRestConstraint ys,
     MyAll @[S -> Type] SOPEntryConstraints SOPRestConstraint ys) =>
    PSOPStructPLiftableHelper ys
    -> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys))
-> PSOPStructPLiftableHelper struct
forall k (c :: k -> Constraint) (d :: [k] -> Constraint)
       (xs :: [k]) (r :: [k] -> Type).
MyAll @k c d xs =>
Proxy @(k -> Constraint) c
-> Proxy @([k] -> Constraint) d
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, d ys, MyAll @k c d ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (r :: [[S -> Type]] -> Type).
Proxy @([S -> Type] -> Constraint) SOPEntryConstraints
-> Proxy @([[S -> Type]] -> Constraint) SOPRestConstraint
-> r ('[] @[S -> Type])
-> (forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
    (SOPEntryConstraints y, SOPRestConstraint ys,
     MyAll @[S -> Type] SOPEntryConstraints SOPRestConstraint ys) =>
    r ys -> r ((':) @[S -> Type] y ys))
-> r struct
my_cpara_SList
            (forall {k} (t :: k). Proxy @k t
forall (t :: [S -> Type] -> Constraint).
Proxy @([S -> Type] -> Constraint) t
Proxy @SOPEntryConstraints)
            (forall {k} (t :: k). Proxy @k t
forall (t :: [[S -> Type]] -> Constraint).
Proxy @([[S -> Type]] -> Constraint) t
Proxy @SOPRestConstraint)
            ((PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
 -> Either
      LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))))
-> PSOPStructPLiftableHelper ('[] @[S -> Type])
forall (struct :: [[S -> Type]]).
(PLiftedClosed (PSOPStruct struct)
 -> Either LiftError (SOP @Type I (StructAsHaskell struct)))
-> PSOPStructPLiftableHelper struct
PSOPStructPLiftableHelper ((PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
  -> Either
       LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))))
 -> PSOPStructPLiftableHelper ('[] @[S -> Type]))
-> (PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
    -> Either
         LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))))
-> PSOPStructPLiftableHelper ('[] @[S -> Type])
forall a b. (a -> b) -> a -> b
$ Either LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
-> PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
-> Either
     LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
forall a b. a -> b -> a
const (Either
   LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
 -> PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
 -> Either
      LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))))
-> Either
     LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
-> PLiftedClosed (PSOPStruct ('[] @[S -> Type]))
-> Either
     LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
forall a b. (a -> b) -> a -> b
$ SOP @Type I (StructAsHaskell ('[] @[S -> Type]))
-> Either
     LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))
 -> Either
      LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type]))))
-> SOP @Type I (StructAsHaskell ('[] @[S -> Type]))
-> Either
     LiftError (SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
forall a b. (a -> b) -> a -> b
$ NS @[Type] (NP @Type I) (StructAsHaskell ('[] @[S -> Type]))
-> SOP @Type I (StructAsHaskell ('[] @[S -> Type]))
forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP (NS @[Type] (NP @Type I) (StructAsHaskell ('[] @[S -> Type]))
 -> SOP @Type I (StructAsHaskell ('[] @[S -> Type])))
-> NS @[Type] (NP @Type I) (StructAsHaskell ('[] @[S -> Type]))
-> SOP @Type I (StructAsHaskell ('[] @[S -> Type]))
forall a b. (a -> b) -> a -> b
$ [Char]
-> NS @[Type] (NP @Type I) (StructAsHaskell ('[] @[S -> Type]))
forall a. HasCallStack => [Char] -> a
error [Char]
"absurd: empty SOP")
            PSOPStructPLiftableHelper ys
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
(SOPRestConstraint ys, SOPEntryConstraints y) =>
PSOPStructPLiftableHelper ys
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
forall (y :: [S -> Type]) (ys :: [[S -> Type]]).
(SOPEntryConstraints y, SOPRestConstraint ys,
 MyAll @[S -> Type] SOPEntryConstraints SOPRestConstraint ys) =>
PSOPStructPLiftableHelper ys
-> PSOPStructPLiftableHelper ((':) @[S -> Type] y ys)
go
      )
        PLiftedClosed (PSOPStruct struct)
x
  {-# INLINEABLE reprToPlut #-}
  reprToPlut :: forall (s :: S).
PlutusRepr (PSOPStruct struct) -> PLifted s (PSOPStruct struct)
reprToPlut = PlutusRepr (PSOPStruct struct) -> PLifted s (PSOPStruct struct)
PLiftedClosed (PSOPStruct struct) -> PLifted s (PSOPStruct struct)
forall (a :: S -> Type) (s :: S). PLiftedClosed a -> PLifted s a
pliftedFromClosed
  {-# INLINEABLE plutToRepr #-}
  plutToRepr :: (forall (s :: S). PLifted s (PSOPStruct struct))
-> Either LiftError (PlutusRepr (PSOPStruct struct))
plutToRepr = PLiftedClosed (PSOPStruct struct)
-> Either LiftError (PLiftedClosed (PSOPStruct struct))
forall a b. b -> Either a b
Right (PLiftedClosed (PSOPStruct struct)
 -> Either LiftError (PLiftedClosed (PSOPStruct struct)))
-> ((forall (s :: S). PLifted s (PSOPStruct struct))
    -> PLiftedClosed (PSOPStruct struct))
-> (forall (s :: S). PLifted s (PSOPStruct struct))
-> Either LiftError (PLiftedClosed (PSOPStruct struct))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (s :: S). PLifted s (PSOPStruct struct))
-> PLiftedClosed (PSOPStruct struct)
forall (a :: S -> Type).
(forall (s :: S). PLifted s a) -> PLiftedClosed a
pliftedToClosed

-- "my" copy of `cpara_SList` that allows you to add constraint on the "rest" part of the type
type family MyAllF (c :: k -> Constraint) (d :: [k] -> Constraint) (xs :: [k]) :: Constraint where
  MyAllF _c _d '[] = ()
  MyAllF c d (x ': xs) = (c x, d xs, MyAll c d xs)

class (MyAllF c d xs, SListI xs) => MyAll (c :: k -> Constraint) (d :: [k] -> Constraint) (xs :: [k]) where
  my_cpara_SList ::
    Proxy c ->
    Proxy d ->
    r '[] ->
    (forall y ys. (c y, d ys, MyAll c d ys) => r ys -> r (y ': ys)) ->
    r xs

instance MyAll c d '[] where
  my_cpara_SList :: forall (r :: [k] -> Type).
Proxy @(k -> Constraint) c
-> Proxy @([k] -> Constraint) d
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, d ys, MyAll @k c d ys) =>
    r ys -> r ((':) @k y ys))
-> r ('[] @k)
my_cpara_SList Proxy @(k -> Constraint) c
_p Proxy @([k] -> Constraint) d
_d r ('[] @k)
nil forall (y :: k) (ys :: [k]).
(c y, d ys, MyAll @k c d ys) =>
r ys -> r ((':) @k y ys)
_cons = r ('[] @k)
nil
  {-# INLINE my_cpara_SList #-}

instance (c x, d xs, MyAll c d xs) => MyAll c d (x ': xs) where
  my_cpara_SList :: forall (r :: [a] -> Type).
Proxy @(a -> Constraint) c
-> Proxy @([a] -> Constraint) d
-> r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    (c y, d ys, MyAll @a c d ys) =>
    r ys -> r ((':) @a y ys))
-> r ((':) @a x xs)
my_cpara_SList Proxy @(a -> Constraint) c
p Proxy @([a] -> Constraint) d
d r ('[] @a)
nil forall (y :: a) (ys :: [a]).
(c y, d ys, MyAll @a c d ys) =>
r ys -> r ((':) @a y ys)
cons =
    r xs -> r ((':) @a x xs)
forall (y :: a) (ys :: [a]).
(c y, d ys, MyAll @a c d ys) =>
r ys -> r ((':) @a y ys)
cons (Proxy @(a -> Constraint) c
-> Proxy @([a] -> Constraint) d
-> r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    (c y, d ys, MyAll @a c d ys) =>
    r ys -> r ((':) @a y ys))
-> r xs
forall k (c :: k -> Constraint) (d :: [k] -> Constraint)
       (xs :: [k]) (r :: [k] -> Type).
MyAll @k c d xs =>
Proxy @(k -> Constraint) c
-> Proxy @([k] -> Constraint) d
-> r ('[] @k)
-> (forall (y :: k) (ys :: [k]).
    (c y, d ys, MyAll @k c d ys) =>
    r ys -> r ((':) @k y ys))
-> r xs
forall (r :: [a] -> Type).
Proxy @(a -> Constraint) c
-> Proxy @([a] -> Constraint) d
-> r ('[] @a)
-> (forall (y :: a) (ys :: [a]).
    (c y, d ys, MyAll @a c d ys) =>
    r ys -> r ((':) @a y ys))
-> r xs
my_cpara_SList Proxy @(a -> Constraint) c
p Proxy @([a] -> Constraint) d
d r ('[] @a)
nil r ys -> r ((':) @a y ys)
forall (y :: a) (ys :: [a]).
(c y, d ys, MyAll @a c d ys) =>
r ys -> r ((':) @a y ys)
cons)
  {-# INLINE my_cpara_SList #-}