{-# 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,
)
newtype PSOPStruct (struct :: [[S -> Type]]) (s :: S) = PSOPStruct
{ forall (struct :: [[S -> Type]]) (s :: S).
PSOPStruct struct s -> PStruct struct s
unPSOPStruct :: PStruct struct s
}
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)
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
newtype PSOPRec (struct :: [S -> Type]) (s :: S) = PSOPRec
{ forall (struct :: [S -> Type]) (s :: S).
PSOPRec struct s -> PRec struct s
unPSOPRec :: PRec struct s
}
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)
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
newtype DeriveAsSOPStruct (a :: S -> Type) s = DeriveAsSOPStruct
{ forall (a :: S -> Type) (s :: S). DeriveAsSOPStruct a s -> a s
unDeriveAsSOPStruct :: a s
}
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)
newtype DeriveAsSOPRec (a :: S -> Type) s = DeriveAsSOPRec
{ forall (a :: S -> Type) (s :: S). DeriveAsSOPRec a s -> a s
unDeriveAsSOPRec :: a s
}
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)
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
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
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)