{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
module PlutusCore.StdLib.Meta.Data.Tuple
( Tuple (..)
, getTupleType
, tupleTypeTermAt
, tupleTermAt
, tupleDefAt
, bindTuple
, prodN
, prodNConstructor
, prodNAccessor
, getSpineToTuple
) where
import PlutusPrelude (showText)
import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Quote
import Control.Lens.Indexed (ifor, itraverse)
import Data.Traversable
data Tuple term uni ann =
Tuple
{ forall (term :: * -> *) (uni :: * -> *) ann.
Tuple term uni ann -> [Type TyName uni ann]
_tupleElementTypes :: [Type TyName uni ann]
, forall (term :: * -> *) (uni :: * -> *) ann.
Tuple term uni ann -> term ann
_tupleTerm :: term ann
}
getTupleType :: MonadQuote m => ann -> Tuple term uni ann -> m (Type TyName uni ann)
getTupleType :: forall (m :: * -> *) ann (term :: * -> *) (uni :: * -> *).
MonadQuote m =>
ann -> Tuple term uni ann -> m (Type TyName uni ann)
getTupleType ann
ann (Tuple [Type TyName uni ann]
elTys term ann
_) = Quote (Type TyName uni ann) -> m (Type TyName uni ann)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Type TyName uni ann) -> m (Type TyName uni ann))
-> Quote (Type TyName uni ann) -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ do
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
let caseTy :: Type TyName uni ann
caseTy = ann
-> [Type TyName uni ann]
-> Type TyName uni ann
-> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun ann
ann [Type TyName uni ann]
elTys (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
r
Type TyName uni ann -> Quote (Type TyName uni ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> Quote (Type TyName uni ann))
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Quote (Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann TyName
r (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann Type TyName uni ann
caseTy (Type TyName uni ann -> Quote (Type TyName uni ann))
-> Type TyName uni ann -> Quote (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
r
getSpineToTuple
:: (TermLike term TyName Name uni fun, MonadQuote m)
=> ann -> [(Type TyName uni ann, term ann)] -> m (Tuple term uni ann)
getSpineToTuple :: forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> [(Type TyName uni ann, term ann)] -> m (Tuple term uni ann)
getSpineToTuple ann
ann [(Type TyName uni ann, term ann)]
spine = Quote (Tuple term uni ann) -> m (Tuple term uni ann)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Tuple term uni ann) -> m (Tuple term uni ann))
-> Quote (Tuple term uni ann) -> m (Tuple term uni ann)
forall a b. (a -> b) -> a -> b
$ do
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
let ([Type TyName uni ann]
as, [term ann]
xs) = [(Type TyName uni ann, term ann)]
-> ([Type TyName uni ann], [term ann])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type TyName uni ann, term ann)]
spine
caseTy :: Type TyName uni ann
caseTy = ann
-> [Type TyName uni ann]
-> Type TyName uni ann
-> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun ann
ann [Type TyName uni ann]
as (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
r
y :: term ann
y = term ann -> [(ann, term ann)] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (ann -> Name -> term ann
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann Name
f) ((ann
ann,) (term ann -> (ann, term ann)) -> [term ann] -> [(ann, term ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [term ann]
xs)
Tuple term uni ann -> Quote (Tuple term uni ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tuple term uni ann -> Quote (Tuple term uni ann))
-> (term ann -> Tuple term uni ann)
-> term ann
-> Quote (Tuple term uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ann] -> term ann -> Tuple term uni ann
forall (term :: * -> *) (uni :: * -> *) ann.
[Type TyName uni ann] -> term ann -> Tuple term uni ann
Tuple [Type TyName uni ann]
as (term ann -> Tuple term uni ann)
-> (term ann -> term ann) -> term ann -> Tuple term uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann -> TyName -> Kind ann -> term ann -> term ann
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs ann
ann TyName
r (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (term ann -> Quote (Tuple term uni ann))
-> term ann -> Quote (Tuple term uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
ann Name
f Type TyName uni ann
caseTy term ann
y
tupleTypeTermAt
:: (TermLike term TyName Name uni fun, MonadQuote m)
=> ann -> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
tupleTypeTermAt :: forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann
-> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
tupleTypeTermAt ann
ann Int
ind (Tuple [Type TyName uni ann]
elTys term ann
term) = Quote (Type TyName uni ann, term ann)
-> m (Type TyName uni ann, term ann)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Type TyName uni ann, term ann)
-> m (Type TyName uni ann, term ann))
-> Quote (Type TyName uni ann, term ann)
-> m (Type TyName uni ann, term ann)
forall a b. (a -> b) -> a -> b
$ do
[VarDecl TyName Name uni ann]
args <- [Type TyName uni ann]
-> (Int
-> Type TyName uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann))
-> QuoteT Identity [VarDecl TyName Name uni ann]
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
t a -> (i -> a -> f b) -> f (t b)
ifor [Type TyName uni ann]
elTys ((Int
-> Type TyName uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann))
-> QuoteT Identity [VarDecl TyName Name uni ann])
-> (Int
-> Type TyName uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann))
-> QuoteT Identity [VarDecl TyName Name uni ann]
forall a b. (a -> b) -> a -> b
$ \Int
i Type TyName uni ann
ty -> do
Name
n <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName (Text -> QuoteT Identity Name) -> Text -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text
"arg_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
VarDecl TyName Name uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann))
-> VarDecl TyName Name uni ann
-> QuoteT Identity (VarDecl TyName Name uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> Name -> Type TyName uni ann -> VarDecl TyName Name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann Name
n Type TyName uni ann
ty
let selectedTy :: Type TyName uni ann
selectedTy = [Type TyName uni ann]
elTys [Type TyName uni ann] -> Int -> Type TyName uni ann
forall a. HasCallStack => [a] -> Int -> a
!! Int
ind
selectedArg :: term ann
selectedArg = ann -> VarDecl TyName Name uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
mkVar ann
ann (VarDecl TyName Name uni ann -> term ann)
-> VarDecl TyName Name uni ann -> term ann
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni ann]
args [VarDecl TyName Name uni ann] -> Int -> VarDecl TyName Name uni ann
forall a. HasCallStack => [a] -> Int -> a
!! Int
ind
selector :: term ann
selector = [VarDecl TyName Name uni ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni ann]
args term ann
selectedArg
(Type TyName uni ann, term ann)
-> Quote (Type TyName uni ann, term ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Type TyName uni ann
selectedTy
, ann -> term ann -> term ann -> term ann
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann (ann -> term ann -> Type TyName uni ann -> term ann
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst ann
ann term ann
term Type TyName uni ann
selectedTy) term ann
selector
)
tupleTermAt
:: (TermLike term TyName Name uni fun, MonadQuote m)
=> ann -> Int -> Tuple term uni ann -> m (term ann)
tupleTermAt :: forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> Int -> Tuple term uni ann -> m (term ann)
tupleTermAt ann
ann Int
ind Tuple term uni ann
tuple = (Type TyName uni ann, term ann) -> term ann
forall a b. (a, b) -> b
snd ((Type TyName uni ann, term ann) -> term ann)
-> m (Type TyName uni ann, term ann) -> m (term ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann
-> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann
-> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
tupleTypeTermAt ann
ann Int
ind Tuple term uni ann
tuple
tupleDefAt
:: (TermLike term TyName Name uni fun, MonadQuote m)
=> ann
-> Int
-> Name
-> Tuple term uni ann
-> m (TermDef term TyName Name uni ann)
tupleDefAt :: forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann
-> Int
-> Name
-> Tuple term uni ann
-> m (TermDef term TyName Name uni ann)
tupleDefAt ann
ann Int
ind Name
name Tuple term uni ann
tuple = (Type TyName uni ann
-> term ann -> TermDef term TyName Name uni ann)
-> (Type TyName uni ann, term ann)
-> TermDef term TyName Name uni ann
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (VarDecl TyName Name uni ann
-> term ann -> TermDef term TyName Name uni ann
forall var val. var -> val -> Def var val
Def (VarDecl TyName Name uni ann
-> term ann -> TermDef term TyName Name uni ann)
-> (Type TyName uni ann -> VarDecl TyName Name uni ann)
-> Type TyName uni ann
-> term ann
-> TermDef term TyName Name uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann -> Name -> Type TyName uni ann -> VarDecl TyName Name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann Name
name) ((Type TyName uni ann, term ann)
-> TermDef term TyName Name uni ann)
-> m (Type TyName uni ann, term ann)
-> m (TermDef term TyName Name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann
-> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann
-> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
tupleTypeTermAt ann
ann Int
ind Tuple term uni ann
tuple
bindTuple
:: (TermLike term TyName Name uni fun, MonadQuote m)
=> ann -> [Name] -> Tuple term uni ann -> term ann -> m (term ann)
bindTuple :: forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> [Name] -> Tuple term uni ann -> term ann -> m (term ann)
bindTuple ann
ann [Name]
names (Tuple [Type TyName uni ann]
elTys term ann
term) term ann
body = Quote (term ann) -> m (term ann)
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (term ann) -> m (term ann))
-> Quote (term ann) -> m (term ann)
forall a b. (a -> b) -> a -> b
$ do
Name
tup <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"tup"
let tupVar :: Tuple term uni ann
tupVar = [Type TyName uni ann] -> term ann -> Tuple term uni ann
forall (term :: * -> *) (uni :: * -> *) ann.
[Type TyName uni ann] -> term ann -> Tuple term uni ann
Tuple [Type TyName uni ann]
elTys (term ann -> Tuple term uni ann) -> term ann -> Tuple term uni ann
forall a b. (a -> b) -> a -> b
$ ann -> Name -> term ann
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann Name
tup
Type TyName uni ann
tupTy <- ann -> Tuple term uni ann -> QuoteT Identity (Type TyName uni ann)
forall (m :: * -> *) ann (term :: * -> *) (uni :: * -> *).
MonadQuote m =>
ann -> Tuple term uni ann -> m (Type TyName uni ann)
getTupleType ann
ann Tuple term uni ann
tupVar
[TermDef term TyName Name uni ann]
tupDefs <- (Int -> Name -> QuoteT Identity (TermDef term TyName Name uni ann))
-> [Name] -> QuoteT Identity [TermDef term TyName Name uni ann]
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(Int -> a -> f b) -> [a] -> f [b]
itraverse (\Int
i Name
name -> ann
-> Int
-> Name
-> Tuple term uni ann
-> QuoteT Identity (TermDef term TyName Name uni ann)
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann
-> Int
-> Name
-> Tuple term uni ann
-> m (TermDef term TyName Name uni ann)
tupleDefAt ann
ann Int
i Name
name Tuple term uni ann
tupVar) [Name]
names
term ann -> Quote (term ann)
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ann -> Quote (term ann)) -> term ann -> Quote (term ann)
forall a b. (a -> b) -> a -> b
$ ann -> term ann -> term ann -> term ann
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann (ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
ann Name
tup Type TyName uni ann
tupTy (term ann -> term ann) -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ (TermDef term TyName Name uni ann -> term ann -> term ann)
-> term ann -> [TermDef term TyName Name uni ann] -> term ann
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ann -> TermDef term TyName Name uni ann -> term ann -> term ann
forall ann.
ann -> TermDef term TyName Name uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni ann -> term ann -> term ann
termLet ann
ann) term ann
body [TermDef term TyName Name uni ann]
tupDefs) term ann
term
prodN :: Int -> Type TyName uni ()
prodN :: forall (uni :: * -> *). Int -> Type TyName uni ()
prodN Int
arity = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
[TyVarDecl TyName ()]
tyVars <- [Int]
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..(Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()])
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
TyName
tn <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName (Text -> QuoteT Identity TyName) -> Text -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text
"t_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ()))
-> TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tn (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
TyName
resultType <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
let caseType :: Type TyName uni ()
caseType = ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () ((TyVarDecl TyName () -> Type TyName uni ())
-> [TyVarDecl TyName ()] -> [Type TyName uni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ()) [TyVarDecl TyName ()]
tyVars) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
resultType)
Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$
[TyVarDecl TyName ()] -> Type TyName uni () -> Type TyName uni ()
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam [TyVarDecl TyName ()]
tyVars (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$
() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
resultType (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$
()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
caseType (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
resultType)
prodNConstructor :: TermLike term TyName Name uni fun => Int -> term ()
prodNConstructor :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Int -> term ()
prodNConstructor Int
arity = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
[TyVarDecl TyName ()]
tyVars <- [Int]
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..(Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()])
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
TyName
tn <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName (Text -> QuoteT Identity TyName) -> Text -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text
"t_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ()))
-> TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tn (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
TyName
resultType <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
[VarDecl TyName Name uni ()]
args <- [Int]
-> (Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..(Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()])
-> (Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
Name
n <- QuoteT Identity Name -> QuoteT Identity Name
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity Name -> QuoteT Identity Name)
-> QuoteT Identity Name -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName (Text -> QuoteT Identity Name) -> Text -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text
"arg_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ()))
-> VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
n (Type TyName uni () -> VarDecl TyName Name uni ())
-> Type TyName uni () -> VarDecl TyName Name uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () (TyVarDecl TyName () -> Type TyName uni ())
-> TyVarDecl TyName () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName ()]
tyVars [TyVarDecl TyName ()] -> Int -> TyVarDecl TyName ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
Name
caseArg <- QuoteT Identity Name -> QuoteT Identity Name
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity Name -> QuoteT Identity Name)
-> QuoteT Identity Name -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"case"
let caseTy :: Type TyName uni ()
caseTy = ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () ((TyVarDecl TyName () -> Type TyName uni ())
-> [TyVarDecl TyName ()] -> [Type TyName uni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ()) [TyVarDecl TyName ()]
tyVars) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
resultType)
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$
[TyVarDecl TyName ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyAbs [TyVarDecl TyName ()]
tyVars (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
[VarDecl TyName Name uni ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni ()]
args (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
resultType (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
caseArg Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
caseTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
caseArg) ([term ()] -> term ()) -> [term ()] -> term ()
forall a b. (a -> b) -> a -> b
$ (VarDecl TyName Name uni () -> term ())
-> [VarDecl TyName Name uni ()] -> [term ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> VarDecl TyName Name uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
mkVar ()) [VarDecl TyName Name uni ()]
args
prodNAccessor :: TermLike term TyName Name uni fun => Int -> Int -> term ()
prodNAccessor :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Int -> Int -> term ()
prodNAccessor Int
arity Int
index = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
[TyVarDecl TyName ()]
tyVars <- [Int]
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..(Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()])
-> (Int -> QuoteT Identity (TyVarDecl TyName ()))
-> QuoteT Identity [TyVarDecl TyName ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
TyName
tn <- QuoteT Identity TyName -> QuoteT Identity TyName
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName (Text -> QuoteT Identity TyName) -> Text -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text
"t_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ()))
-> TyVarDecl TyName () -> QuoteT Identity (TyVarDecl TyName ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tn (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
let tupleTy :: Type TyName uni ()
tupleTy = Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn (Int -> Type TyName uni ()
forall (uni :: * -> *). Int -> Type TyName uni ()
prodN Int
arity) ((TyVarDecl TyName () -> Type TyName uni ())
-> [TyVarDecl TyName ()] -> [Type TyName uni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ()) [TyVarDecl TyName ()]
tyVars)
selectedTy :: Type TyName uni ()
selectedTy = () -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () (TyVarDecl TyName () -> Type TyName uni ())
-> TyVarDecl TyName () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName ()]
tyVars [TyVarDecl TyName ()] -> Int -> TyVarDecl TyName ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
index
[VarDecl TyName Name uni ()]
args <- [Int]
-> (Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..(Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ((Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()])
-> (Int -> QuoteT Identity (VarDecl TyName Name uni ()))
-> QuoteT Identity [VarDecl TyName Name uni ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
Name
n <- QuoteT Identity Name -> QuoteT Identity Name
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity Name -> QuoteT Identity Name)
-> QuoteT Identity Name -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName (Text -> QuoteT Identity Name) -> Text -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text
"arg_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i
VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ()))
-> VarDecl TyName Name uni ()
-> QuoteT Identity (VarDecl TyName Name uni ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
n (Type TyName uni () -> VarDecl TyName Name uni ())
-> Type TyName uni () -> VarDecl TyName Name uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyVarDecl TyName () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar () (TyVarDecl TyName () -> Type TyName uni ())
-> TyVarDecl TyName () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName ()]
tyVars [TyVarDecl TyName ()] -> Int -> TyVarDecl TyName ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
let selectedArg :: term ()
selectedArg = () -> VarDecl TyName Name uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
mkVar () (VarDecl TyName Name uni () -> term ())
-> VarDecl TyName Name uni () -> term ()
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni ()]
args [VarDecl TyName Name uni ()] -> Int -> VarDecl TyName Name uni ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
index
Name
tupleArg <- QuoteT Identity Name -> QuoteT Identity Name
forall a. Quote a -> Quote a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity Name -> QuoteT Identity Name)
-> QuoteT Identity Name -> QuoteT Identity Name
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"tuple"
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$
[TyVarDecl TyName ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyAbs [TyVarDecl TyName ()]
tyVars (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> Name -> Type TyName uni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
tupleArg Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
tupleTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
tupleArg) Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
selectedTy) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
[VarDecl TyName Name uni ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni ()]
args term ()
selectedArg