{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.TypeLevel.List.TH where

import Prelude hiding (unzip)
import Language.Haskell.TH

unzip :: Int -> DecQ
unzip :: Int -> DecQ
unzip Int
n = do
	Name
xys <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
abc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"
	[Name]
xs <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` [String]
abc
	[Name]
ks <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` ((String
"k" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
abc)
	Name -> Name -> Name -> [Name] -> [Name] -> DecQ
unzipGen (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"Unzip" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"Push" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) Name
xys [Name]
xs [Name]
ks
	where
	abc :: [String]
abc = Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n [String]
varNames

unzipGen :: Name -> Name -> Name -> [Name] -> [Name] -> DecQ
unzipGen :: Name -> Name -> Name -> [Name] -> [Name] -> DecQ
unzipGen Name
uz Name
psh Name
xys [Name]
xs [Name]
ks = do
	Type
t <- (Q Type
forall (m :: * -> *). Quote m => m Type
listT Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT`) (Q Type -> Q Type) -> ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
tupleFromList ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ks
	Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [Q TySynEqn]
-> DecQ
forall (m :: * -> *).
Quote m =>
Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [m TySynEqn]
-> m Dec
closedTypeFamilyD Name
uz [Name -> Type -> TyVarBndr ()
kindedTV Name
xys Type
t]
		FamilyResultSig
noSig Maybe InjectivityAnn
forall a. Maybe a
Nothing
		[Maybe [TyVarBndr ()] -> Q Type -> Q Type -> Q TySynEqn
forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing Q Type
lft0 Q Type
rgt0, Maybe [TyVarBndr ()] -> Q Type -> Q Type -> Q TySynEqn
forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing Q Type
lft1 Q Type
rgt1]
	where
	lft0 :: Q Type
lft0 = Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
uz Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` Q Type
forall (m :: * -> *). Quote m => m Type
promotedNilT
	rgt0 :: Q Type
rgt0 = [Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ (Q Type -> Name -> Q Type
forall a b. a -> b -> a
const Q Type
forall (m :: * -> *). Quote m => m Type
promotedNilT) (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xs
	lft1 :: Q Type
lft1 = Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
uz)
		(Q Type -> Q Type) -> Q Type -> Q Type
forall a b. (a -> b) -> a -> b
$ [Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xs) Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`promotedCons` Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT Name
xys
	rgt1 :: Q Type
rgt1 = (Q Type -> Q Type -> Q Type) -> Q Type -> [Q Type] -> Q Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
psh) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xs) Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
uz Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT Name
xys)

push :: Int -> DecQ
push :: Int -> DecQ
push Int
n = do
	Name
xys <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
abc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s"
	[Name]
xs <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` [String]
abc
	[Name]
ks <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` ((String
"k" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
abc)
	[Name]
xss <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` ((String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s") (String -> String) -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
abc)
	Name -> Name -> [Name] -> [Name] -> [Name] -> DecQ
pushGen (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"Push" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) Name
xys [Name]
xs [Name]
ks [Name]
xss
	where
	abc :: [String]
abc = Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n [String]
varNames

pushGen :: Name -> Name -> [Name] -> [Name] -> [Name] -> DecQ
pushGen :: Name -> Name -> [Name] -> [Name] -> [Name] -> DecQ
pushGen Name
psh Name
xys [Name]
xs [Name]
ks [Name]
xss = Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [Q TySynEqn]
-> DecQ
forall (m :: * -> *).
Quote m =>
Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [m TySynEqn]
-> m Dec
closedTypeFamilyD Name
psh
	((Name -> Type -> TyVarBndr ())
-> [Name] -> [Type] -> [TyVarBndr ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Type -> TyVarBndr ()
kindedTV [Name]
xs (Name -> Type
varK (Name -> Type) -> [Name] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ks) [TyVarBndr ()] -> [TyVarBndr ()] -> [TyVarBndr ()]
forall a. [a] -> [a] -> [a]
++ [Name -> TyVarBndr ()
plainTV Name
xys]) FamilyResultSig
NoSig Maybe InjectivityAnn
forall a. Maybe a
Nothing [Maybe [TyVarBndr ()] -> Q Type -> Q Type -> Q TySynEqn
forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing Q Type
lft Q Type
rgt ]
	where
	lft :: Q Type
lft = (Q Type -> Q Type -> Q Type) -> Q Type -> [Q Type] -> Q Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
psh) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xs)
		Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` [Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xss)
	rgt :: Q Type
rgt = [Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ (Q Type -> Q Type -> Q Type) -> [Q Type] -> [Q Type] -> [Q Type]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
promotedCons (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xs) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xss)

tupleFromList :: Quote m => [m Type] -> m Type
tupleFromList :: forall (m :: * -> *). Quote m => [m Type] -> m Type
tupleFromList [m Type]
ts = (m Type -> m Type -> m Type) -> m Type -> [m Type] -> m Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl m Type -> m Type -> m Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Int -> m Type
forall (m :: * -> *). Quote m => Int -> m Type
tupleT (Int -> m Type) -> Int -> m Type
forall a b. (a -> b) -> a -> b
$ [m Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m Type]
ts) [m Type]
ts

promotedTupleFromList :: Quote m => [m Type] -> m Type
promotedTupleFromList :: forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList [m Type]
ts = (m Type -> m Type -> m Type) -> m Type -> [m Type] -> m Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl m Type -> m Type -> m Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Int -> m Type
forall (m :: * -> *). Quote m => Int -> m Type
promotedTupleT (Int -> m Type) -> Int -> m Type
forall a b. (a -> b) -> a -> b
$ [m Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [m Type]
ts) [m Type]
ts

promotedCons :: Quote m => m Type -> m Type -> m Type
promotedCons :: forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
promotedCons m Type
x m Type
y = m Type
forall (m :: * -> *). Quote m => m Type
promotedConsT m Type -> m Type -> m Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` m Type
x m Type -> m Type -> m Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`appT` m Type
y

varNames :: [String]
varNames :: [String]
varNames = ((Char -> String -> String
forall a. a -> [a] -> [a]
: []) (Char -> String) -> String -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char
'a' .. Char
'z']) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
c] | String
cs <- [String]
varNames, Char
c <- [Char
'a' .. Char
'z'] ]

kindNames :: [String]
kindNames :: [String]
kindNames = (Char
'k' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String) -> [Int] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 :: Int ..]

mkZip :: Int -> DecQ
mkZip :: Int -> DecQ
mkZip Int
n = do
	[Name]
xys <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n [String]
varNames
	[Name]
nus <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n ((Char
'_' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
varNames)
	[Name]
xsys <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n ((String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"s") (String -> String) -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
varNames)
	[Name]
ks <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName (String -> Q Name) -> [String] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
n [String]
kindNames
	Name -> [Name] -> [Name] -> [Name] -> [Name] -> DecQ
mkBar (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"Zip" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) [Name]
xys [Name]
nus [Name]
xsys [Name]
ks

bar :: DecQ
bar :: DecQ
bar = Name -> [Name] -> [Name] -> [Name] -> [Name] -> DecQ
mkBar (String -> Name
mkName String
"Zip2") [String -> Name
mkName String
"x", String -> Name
mkName String
"y"] [String -> Name
mkName String
"_x", String -> Name
mkName String
"_y"] [String -> Name
mkName String
"xs", String -> Name
mkName String
"ys"] [String -> Name
mkName String
"k0", String -> Name
mkName String
"k1"]

mkBar :: Name -> [Name] -> [Name] -> [Name] -> [Name] -> DecQ
mkBar :: Name -> [Name] -> [Name] -> [Name] -> [Name] -> DecQ
mkBar Name
tn [Name]
xy [Name]
nus [Name]
xsys [Name]
ks = Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [Q TySynEqn]
-> DecQ
forall (m :: * -> *).
Quote m =>
Name
-> [TyVarBndr ()]
-> FamilyResultSig
-> Maybe InjectivityAnn
-> [m TySynEqn]
-> m Dec
closedTypeFamilyD Name
tn ((Name -> Type -> TyVarBndr ())
-> [Name] -> [Type] -> [TyVarBndr ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Type -> TyVarBndr ()
kindedTV [Name]
xy ([Type] -> [TyVarBndr ()]) -> [Type] -> [TyVarBndr ()]
forall a b. (a -> b) -> a -> b
$ (Type
listK Type -> Type -> Type
`appK`) (Type -> Type) -> (Name -> Type) -> Name -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type
varK (Name -> Type) -> [Name] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ks) FamilyResultSig
NoSig Maybe InjectivityAnn
forall a. Maybe a
Nothing ([Q TySynEqn] -> DecQ) -> [Q TySynEqn] -> DecQ
forall a b. (a -> b) -> a -> b
$
	 (Int -> Q TySynEqn
mkNil (Int -> Q TySynEqn) -> [Int] -> [Q TySynEqn]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
nus Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) [Q TySynEqn] -> [Q TySynEqn] -> [Q TySynEqn]
forall a. [a] -> [a] -> [a]
++ [
	Maybe [TyVarBndr ()] -> Q Type -> Q Type -> Q TySynEqn
forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing
		((Q Type -> Q Type -> Q Type) -> Q Type -> [Q Type] -> Q Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
tn) ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ (Name -> Name -> Q Type) -> [Name] -> [Name] -> [Q Type]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Name -> Q Type
forall {m :: * -> *}. Quote m => Name -> Name -> m Type
mkPat [Name]
xy [Name]
xsys)
		(([Q Type] -> Q Type
forall (m :: * -> *). Quote m => [m Type] -> m Type
promotedTupleFromList (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xy) Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`promotedCons`
			((Q Type -> Q Type -> Q Type) -> Q Type -> [Q Type] -> Q Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
tn) ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
xsys)))
	]
	where
	mkNil :: Int -> Q TySynEqn
mkNil Int
i = Maybe [TyVarBndr ()] -> Q Type -> Q Type -> Q TySynEqn
forall (m :: * -> *).
Quote m =>
Maybe [TyVarBndr ()] -> m Type -> m Type -> m TySynEqn
tySynEqn Maybe [TyVarBndr ()]
forall a. Maybe a
Nothing
		((Q Type -> Q Type -> Q Type) -> Q Type -> [Q Type] -> Q Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
conT Name
tn) ([Q Type] -> Q Type) -> [Q Type] -> Q Type
forall a b. (a -> b) -> a -> b
$ [Name] -> Int -> [Q Type]
emptyOne [Name]
nus Int
i) Q Type
forall (m :: * -> *). Quote m => m Type
promotedNilT
	mkPat :: Name -> Name -> m Type
mkPat Name
x Name
xs = Name -> m Type
forall (m :: * -> *). Quote m => Name -> m Type
varT Name
x m Type -> m Type -> m Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
`promotedCons` Name -> m Type
forall (m :: * -> *). Quote m => Name -> m Type
varT Name
xs

emptyOne :: [Name] -> Int -> [TypeQ]
emptyOne :: [Name] -> Int -> [Q Type]
emptyOne [Name]
ns Int
i = (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
i [Name]
ns) [Q Type] -> [Q Type] -> [Q Type]
forall a. [a] -> [a] -> [a]
++ [Q Type
forall (m :: * -> *). Quote m => m Type
promotedNilT] [Q Type] -> [Q Type] -> [Q Type]
forall a. [a] -> [a] -> [a]
++ (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
varT (Name -> Q Type) -> [Name] -> [Q Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Name]
ns)

foo :: DecsQ
foo :: DecsQ
foo = [d|
	type family Zip2 (xs :: [k0]) (ys :: [k1]) where
		Zip2 '[] _ys = '[]
		Zip2 _xs '[] = '[]
		Zip2 (x ': xs) (y ': ys) = '(x, y) ': Zip2 xs ys |]