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

-- | @since WIP
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 WIP
  }

-- | @since WIP
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 WIP
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 WIP
  }

-- | @since WIP
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 WIP
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 WIP
-}
newtype DeriveAsSOPStruct (a :: S -> Type) s = DeriveAsSOPStruct
  { forall (a :: S -> Type) (s :: S). DeriveAsSOPStruct a s -> a s
unDeriveAsSOPStruct :: a s
  -- ^ @since WIP
  }

-- | @since WIP
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 WIP
-}
newtype DeriveAsSOPRec (a :: S -> Type) s = DeriveAsSOPRec
  { forall (a :: S -> Type) (s :: S). DeriveAsSOPRec a s -> a s
unDeriveAsSOPRec :: a s
  -- ^ @since WIP
  }

-- | @since WIP
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]
deps [HoistedTerm] -> [HoistedTerm] -> [HoistedTerm]
forall a. Semigroup a => a -> a -> a
<> [HoistedTerm]
handlerDeps)