-- | @tuple@s of various sizes and related functions.

{-# LANGUAGE GADTs             #-}
{-# LANGUAGE OverloadedStrings #-}

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
import PlutusCore.Quote

import Control.Lens.Indexed (ifor, itraverse)
import Data.Traversable

-- | A Plutus Core (Scott-encoded) tuple.
data Tuple term uni ann where
    Tuple :: TermLike term TyName Name uni fun =>
        { Tuple term uni ann -> [Type TyName uni ann]
_tupleElementTypes :: [Type TyName uni ann] -- ^ The types of elements of a tuple.
        , Tuple term uni ann -> term ann
_tupleTerm         :: term ann              -- ^ A term representation of the tuple.
        } -> Tuple term uni ann

-- | Get the type of a 'Tuple'.
--
-- > getTupleType _ (Tuple [a1, ... , an] _) = all r. (a1 -> ... -> an -> r) -> r
getTupleType :: MonadQuote m => ann -> Tuple term uni ann -> m (Type TyName uni ann)
getTupleType :: 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 (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 (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

-- | Convert a Haskell spine of 'Term's to a PLC 'Tuple'.
--
-- > getSpineToTuple _ [(a1, x1), ... , (an, xn)] =
-- >     Tuple [a1, ... , an] (/\(r :: *) -> \(f :: a1 -> ... -> an -> r) -> f x1 ... xn)
getSpineToTuple
    :: (TermLike term TyName Name uni fun, MonadQuote m)
    => ann -> [(Type TyName uni ann, term ann)] -> m (Tuple term uni ann)
getSpineToTuple :: 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 (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 = 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
mkIterApp ann
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) [term ann]
xs
    Tuple term uni ann -> Quote (Tuple term uni ann)
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 :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
[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 (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 (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

-- | Get the type of the ith element of a 'Tuple' along with the element itself.
--
-- > tupleTypeTermAt _ i (Tuple [a0, ... , an] term) =
-- >     (ai, term {ai} (\(x0 : a0) ... (xn : an) -> xi))
tupleTypeTermAt
    :: (TermLike term TyName Name uni fun, MonadQuote m)
    => ann -> Int -> Tuple term uni ann -> m (Type TyName uni ann, term ann)
tupleTypeTermAt :: 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 (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 fun ann]
args <- [Type TyName uni ann]
-> (Int
    -> Type TyName uni ann
    -> QuoteT Identity (VarDecl TyName Name uni fun ann))
-> QuoteT Identity [VarDecl TyName Name uni fun 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 fun ann))
 -> QuoteT Identity [VarDecl TyName Name uni fun ann])
-> (Int
    -> Type TyName uni ann
    -> QuoteT Identity (VarDecl TyName Name uni fun ann))
-> QuoteT Identity [VarDecl TyName Name uni fun 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 fun ann
-> QuoteT Identity (VarDecl TyName Name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun ann
 -> QuoteT Identity (VarDecl TyName Name uni fun ann))
-> VarDecl TyName Name uni fun ann
-> QuoteT Identity (VarDecl TyName Name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> Name -> Type TyName uni ann -> VarDecl TyName Name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun 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. [a] -> Int -> a
!! Int
ind
        selectedArg :: term ann
selectedArg = ann -> VarDecl TyName Name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ann
ann (VarDecl TyName Name uni fun ann -> term ann)
-> VarDecl TyName Name uni fun ann -> term ann
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni fun ann]
args [VarDecl TyName Name uni fun ann]
-> Int -> VarDecl TyName Name uni fun ann
forall a. [a] -> Int -> a
!! Int
ind
        selector :: term ann
selector    = [VarDecl TyName Name uni fun ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni fun ann]
args term ann
selectedArg

    (Type TyName uni ann, term ann)
-> Quote (Type TyName uni ann, term ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( Type TyName uni ann
selectedTy
        , 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 (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
        )

-- | Get the ith element of a 'Tuple'.
tupleTermAt
    :: (TermLike term TyName Name uni fun, MonadQuote m)
    => ann -> Int -> Tuple term uni ann -> m (term ann)
tupleTermAt :: 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

-- | Get the ith element of a 'Tuple' as a 'TermDef'.
tupleDefAt
    :: (TermLike term TyName Name uni fun, MonadQuote m)
    => ann
    -> Int
    -> Name
    -> Tuple term uni ann
    -> m (TermDef term TyName Name uni fun ann)
tupleDefAt :: ann
-> Int
-> Name
-> Tuple term uni ann
-> m (TermDef term TyName Name uni fun ann)
tupleDefAt ann
ann Int
ind Name
name Tuple term uni ann
tuple = (Type TyName uni ann
 -> term ann -> TermDef term TyName Name uni fun ann)
-> (Type TyName uni ann, term ann)
-> TermDef term TyName Name uni fun ann
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (VarDecl TyName Name uni fun ann
-> term ann -> TermDef term TyName Name uni fun ann
forall var val. var -> val -> Def var val
Def (VarDecl TyName Name uni fun ann
 -> term ann -> TermDef term TyName Name uni fun ann)
-> (Type TyName uni ann -> VarDecl TyName Name uni fun ann)
-> Type TyName uni ann
-> term ann
-> TermDef term TyName Name uni fun ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Name -> Type TyName uni ann -> VarDecl TyName Name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
ann Name
name) ((Type TyName uni ann, term ann)
 -> TermDef term TyName Name uni fun ann)
-> m (Type TyName uni ann, term ann)
-> m (TermDef term TyName Name uni fun 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

-- | Bind all elements of a 'Tuple' inside a 'Term'.
--
-- > bindTuple _ [x_1, ... , x_n] (Tuple [a1, ... , an] term) body =
-- >     (\(tup : all r. (a_1 -> ... -> a_n -> r) -> r) ->
-- >       let x_1 = _1 tup
-- >           ...
-- >           x_n = _n tup
-- >         in body
-- >     ) term
bindTuple
    :: (TermLike term TyName Name uni fun, MonadQuote m)
    => ann -> [Name] -> Tuple term uni ann -> term ann -> m (term ann)
bindTuple :: 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 (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 :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
[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 (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 fun ann]
tupDefs <- (Int
 -> Name -> QuoteT Identity (TermDef term TyName Name uni fun ann))
-> [Name] -> QuoteT Identity [TermDef term TyName Name uni fun ann]
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
(i -> a -> f b) -> t a -> f (t b)
itraverse (\Int
i Name
name -> ann
-> Int
-> Name
-> Tuple term uni ann
-> QuoteT Identity (TermDef term TyName Name uni fun 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 fun ann)
tupleDefAt ann
ann Int
i Name
name Tuple term uni ann
tupVar) [Name]
names
    term ann -> Quote (term ann)
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 (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 (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 fun ann -> term ann -> term ann)
-> term ann -> [TermDef term TyName Name uni fun ann] -> term ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ann -> TermDef term TyName Name uni fun ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
termLet ann
ann) term ann
body [TermDef term TyName Name uni fun ann]
tupDefs) term ann
term

-- | Given an arity @n@, create the n-ary product type.
--
-- @\(T_1 :: *) .. (T_n :: *) . all (R :: *) . (T_1 -> .. -> T_n -> R) -> R@
prodN :: Int -> Type TyName uni ()
prodN :: 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 (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 (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 (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 (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 (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
$
        -- \T_1 .. T_n
        [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
$
        -- all R
        () -> 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
$
        -- (T_1 -> .. -> T_n -> r) -> r
        ()
-> 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 ()
caseType (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
resultType)

-- | Given an arity @n@, create the constructor for n-ary products.
--
-- @
--     /\(T_1 :: *) .. (T_n :: *) .
--         \(arg_1 : T_1) .. (arg_n : T_n) .
--             /\(R :: *).
--                 \(case : T_1 -> .. -> T_n -> R) -> case arg_1 .. arg_n
-- @
prodNConstructor :: TermLike term TyName Name uni fun => Int -> term ()
prodNConstructor :: 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 (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 (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 (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 fun ()]
args <- [Int]
-> (Int -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> QuoteT Identity [VarDecl TyName Name uni fun ()]
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 fun ()))
 -> QuoteT Identity [VarDecl TyName Name uni fun ()])
-> (Int -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> QuoteT Identity [VarDecl TyName Name uni fun ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
        Name
n <- QuoteT Identity Name -> QuoteT Identity Name
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 fun ()
-> QuoteT Identity (VarDecl TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun ()
 -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> VarDecl TyName Name uni fun ()
-> QuoteT Identity (VarDecl TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni fun ()
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl () Name
n (Type TyName uni () -> VarDecl TyName Name uni fun ())
-> Type TyName uni () -> VarDecl TyName Name uni fun ()
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. [a] -> Int -> a
!! Int
i

    Name
caseArg <- QuoteT Identity Name -> QuoteT Identity Name
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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$
        -- /\T_1 .. T_n
        [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
$
        -- \arg_1 .. arg_n
        [VarDecl TyName Name uni fun ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni fun ()]
args (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
        -- /\R
        () -> TyName -> Kind () -> term () -> term ()
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
$
        -- \case
        () -> Name -> Type TyName uni () -> term () -> term ()
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 ()
caseTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
        -- case arg_1 .. arg_n
        () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
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 fun () -> term ())
-> [VarDecl TyName Name uni fun ()] -> [term ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> VarDecl TyName Name uni fun () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ()) [VarDecl TyName Name uni fun ()]
args

-- | Given an arity @n@ and an index @i@, create a function for accessing the i'th component of a n-tuple.
--
-- @
--     /\(T_1 :: *) .. (T_n :: *) .
--         \(tuple : all (R :: *) . (T_1 -> .. -> T_n -> R) -> R)) .
--             tuple {T_i} (\(arg_1 : T_1) .. (arg_n : T_n) . arg_i)
-- @
prodNAccessor :: TermLike term TyName Name uni fun => Int -> Int -> term ()
prodNAccessor :: 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 (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 (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 ann tyname (uni :: * -> *).
ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
mkIterTyApp () (Int -> Type TyName uni ()
forall (uni :: * -> *). Int -> Type TyName uni ()
prodN Int
arity) ((TyVarDecl TyName () -> Type TyName uni ())
-> [TyVarDecl TyName ()] -> [Type TyName uni ()]
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. [a] -> Int -> a
!! Int
index

    [VarDecl TyName Name uni fun ()]
args <- [Int]
-> (Int -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> QuoteT Identity [VarDecl TyName Name uni fun ()]
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 fun ()))
 -> QuoteT Identity [VarDecl TyName Name uni fun ()])
-> (Int -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> QuoteT Identity [VarDecl TyName Name uni fun ()]
forall a b. (a -> b) -> a -> b
$ \Int
i -> do
        Name
n <- QuoteT Identity Name -> QuoteT Identity Name
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 fun ()
-> QuoteT Identity (VarDecl TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun ()
 -> QuoteT Identity (VarDecl TyName Name uni fun ()))
-> VarDecl TyName Name uni fun ()
-> QuoteT Identity (VarDecl TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni fun ()
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl () Name
n (Type TyName uni () -> VarDecl TyName Name uni fun ())
-> Type TyName uni () -> VarDecl TyName Name uni fun ()
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. [a] -> Int -> a
!! Int
i
    let selectedArg :: term ()
selectedArg = () -> VarDecl TyName Name uni fun () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar () (VarDecl TyName Name uni fun () -> term ())
-> VarDecl TyName Name uni fun () -> term ()
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni fun ()]
args [VarDecl TyName Name uni fun ()]
-> Int -> VarDecl TyName Name uni fun ()
forall a. [a] -> Int -> a
!! Int
index

    Name
tupleArg <- QuoteT Identity Name -> QuoteT Identity Name
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 (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$
        -- /\T_1 .. T_n
        [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
$
        -- \tuple :: (tupleN T_1 .. T_n)
        () -> Name -> Type TyName uni () -> term () -> term ()
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 ()
tupleTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
        -- tuple {T_i}
        () -> term () -> term () -> term ()
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 (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 (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
tupleArg) Type TyName uni ()
selectedTy) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
        -- \arg_1 .. arg_n . arg_i
        [VarDecl TyName Name uni fun ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni fun ()]
args term ()
selectedArg