{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.HeteroParList.Tuple.TH where

import Control.Monad
import Language.Haskell.TH

import Data.TypeLevel.Tuple.MapIndex qualified as TMapIndex
import Data.HeteroParList qualified as HeteroParList
import Data.HeteroParList (pattern (:**))

mkMap :: Int -> Int -> DecsQ
mkMap :: Int -> Int -> DecsQ
mkMap Int
i Int
n = do
	[Name]
ts <- 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]
typeVarNames
	[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]
kindVarNames
	Name -> Name -> [Name] -> [Name] -> Int -> DecsQ
barAll Name
cn Name
fn [Name]
ts [Name]
ks Int
i
	where
	cn :: Name
cn = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"Map" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
	fn :: Name
fn = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"map" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

barAll :: Name -> Name -> [Name] -> [Name] -> Int -> DecsQ
barAll :: Name -> Name -> [Name] -> [Name] -> Int -> DecsQ
barAll Name
cn Name
fn [Name]
ts [Name]
ks Int
i =
	[Q Dec] -> DecsQ
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Name -> Name -> [Name] -> [Name] -> Int -> Q Dec
barRaw Name
cn Name
fn [Name]
ts [Name]
ks Int
i, Name -> Name -> Q Dec
barRaw0 Name
cn Name
fn, Name -> Name -> [Name] -> Q Dec
barRaw1 Name
cn Name
fn [Name]
ts]

bar :: DecQ
bar :: Q Dec
bar = Name -> Name -> [Name] -> [Name] -> Int -> Q Dec
barRaw (String -> Name
mkName String
"Map0_2") (String -> Name
mkName String
"map0_2") [String -> Name
mkName String
"a", String -> Name
mkName String
"b"] [String -> Name
mkName String
"k0", String -> Name
mkName String
"k1"] Int
0

barRaw :: Name -> Name -> [Name] -> [Name] -> Int -> DecQ
barRaw :: Name -> Name -> [Name] -> [Name] -> Int -> Q Dec
barRaw Name
cn Name
fn [Name]
ts [Name]
ks Int
i = Q Cxt -> Name -> [TyVarBndr ()] -> [FunDep] -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m Cxt -> Name -> [TyVarBndr ()] -> [FunDep] -> [m Dec] -> m Dec
classD (Cxt -> Q Cxt
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) Name
cn
	[Name -> Kind -> TyVarBndr ()
kindedTV (String -> Name
mkName String
"ss") Kind
sskind] [] [Name -> Q Kind -> Q Dec
forall (m :: * -> *). Quote m => Name -> m Kind -> m Dec
sigD Name
fn Q Kind
map0_2type]
	where
	sskind :: Kind
sskind = Kind -> Kind
listKind (Kind -> Kind) -> (Cxt -> Kind) -> Cxt -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt -> Kind
tupleKind (Cxt -> Kind) -> Cxt -> Kind
forall a b. (a -> b) -> a -> b
$ Name -> Kind
varK (Name -> Kind) -> [Name] -> Cxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ks
	map0_2type :: Q Kind
map0_2type = Q Kind
ftype Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`arrT` (Q Kind
stype Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`arrT` Q Kind
dtype)
	ftype :: Q Kind
ftype = do
		[TyVarBndr Specificity]
abcs <- (Name -> Name -> Q (TyVarBndr Specificity))
-> [Name] -> [Name] -> Q [TyVarBndr Specificity]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Name -> Name -> Q (TyVarBndr Specificity)
forall {m :: * -> *}.
Quote m =>
Name -> Name -> m (TyVarBndr Specificity)
kindedInvis [Name]
ts [Name]
ks
		[TyVarBndr Specificity] -> Q Cxt -> Q Kind -> Q Kind
forall (m :: * -> *).
Quote m =>
[TyVarBndr Specificity] -> m Cxt -> m Kind -> m Kind
forallT	[TyVarBndr Specificity]
abcs (Cxt -> Q Cxt
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) (Q Kind
tab Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`arrT` Q Kind
tb)
	kindedInvis :: Name -> Name -> m (TyVarBndr Specificity)
kindedInvis Name
v Name
t = Name -> Specificity -> m Kind -> m (TyVarBndr Specificity)
forall (m :: * -> *).
Quote m =>
Name -> Specificity -> m Kind -> m (TyVarBndr Specificity)
kindedInvisTV Name
v Specificity
SpecifiedSpec (m Kind -> m (TyVarBndr Specificity))
-> (Kind -> m Kind) -> Kind -> m (TyVarBndr Specificity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> m Kind
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> m (TyVarBndr Specificity))
-> Kind -> m (TyVarBndr Specificity)
forall a b. (a -> b) -> a -> b
$ Name -> Kind
varK Name
t
	tab :: Q Kind
tab = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"t") Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` [Q Kind] -> Q Kind
forall (m :: * -> *). Quote m => [m Kind] -> m Kind
promotedTupleType (Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (Name -> Q Kind) -> [Name] -> [Q Kind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ts)
	tb :: Q Kind
tb = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"t'") Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT ([Name]
ts [Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
	stype :: Q Kind
stype = Q Kind
pl Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"t") Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"ss")
	dtype :: Q Kind
dtype = Q Kind
pl Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"t'") Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` (Int -> Int -> Q Kind
m0_2 Int
i ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ts) Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"ss"))

bar0 :: DecQ
bar0 :: Q Dec
bar0 = Name -> Name -> Q Dec
barRaw0 (String -> Name
mkName String
"Map0_2") (String -> Name
mkName String
"map0_2")

barRaw0 :: Name -> Name -> DecQ
barRaw0 :: Name -> Name -> Q Dec
barRaw0 Name
cn Name
fn = Q Cxt -> Q Kind -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m Cxt -> m Kind -> [m Dec] -> m Dec
instanceD ([Q Kind] -> Q Cxt
forall (m :: * -> *). Quote m => [m Kind] -> m Cxt
cxt [])
	(Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
cn Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Q Kind
forall (m :: * -> *). Quote m => m Kind
promotedNilT)
	[Name -> [Q Clause] -> Q Dec
forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
funD Name
fn [[Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
clause [Q Pat
forall (m :: * -> *). Quote m => m Pat
wildP, Name -> [Q Pat] -> Q Pat
forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
conP 'HeteroParList.Nil []] (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB (Q Exp -> Q Body) -> Q Exp -> Q Body
forall a b. (a -> b) -> a -> b
$ Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
conE 'HeteroParList.Nil) []]]

bar1 :: DecQ
bar1 :: Q Dec
bar1 = Name -> Name -> [Name] -> Q Dec
barRaw1 (String -> Name
mkName String
"Map0_2") (String -> Name
mkName String
"map0_2") [String -> Name
mkName String
"a", String -> Name
mkName String
"b"]

barRaw1 :: Name -> Name -> [Name] -> DecQ
barRaw1 :: Name -> Name -> [Name] -> Q Dec
barRaw1 Name
cn Name
fn [Name]
ts = Q Cxt -> Q Kind -> [Q Dec] -> Q Dec
forall (m :: * -> *).
Quote m =>
m Cxt -> m Kind -> [m Dec] -> m Dec
instanceD ([Q Kind] -> Q Cxt
forall (m :: * -> *). Quote m => [m Kind] -> m Cxt
cxt [Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
cn Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"ts")])
	(Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
cn Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT`
		([Q Kind] -> Q Kind
forall (m :: * -> *). Quote m => [m Kind] -> m Kind
promotedTupleType (Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (Name -> Q Kind) -> [Name] -> [Q Kind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ts) Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`promotedConsType`
			Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT (String -> Name
mkName String
"ts")))
	[Name -> [Q Clause] -> Q Dec
forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
funD Name
fn [[Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
clause
		[Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP (Name -> Q Pat) -> Name -> Q Pat
forall a b. (a -> b) -> a -> b
$ String -> Name
mkName String
"f", Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP (String -> Name
mkName String
"x") Q Pat -> Q Pat -> Q Pat
forall (m :: * -> *). Quote m => m Pat -> m Pat -> m Pat
`heteroConsP` Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP (String -> Name
mkName String
"xs")]
		(Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB (Q Exp -> Q Body) -> Q Exp -> Q Body
forall a b. (a -> b) -> a -> b
$ Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE (String -> Name
mkName String
"f") Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`appE` Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE (String -> Name
mkName String
"x") Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`heteroCons`
			(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE Name
fn Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`appE` Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE (String -> Name
mkName String
"f") Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
`appE` Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE (String -> Name
mkName String
"xs")))
		[]]]

pl :: TypeQ
pl :: Q Kind
pl = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT ''HeteroParList.PL

m0_2 :: Int -> Int -> TypeQ
-- m0_2 i n = conT $ mkNameG_tc "typelevel-tools" "Data.TypeLevel.MapIndex" ("M" ++ show i ++ "_" ++ show n)
m0_2 :: Int -> Int -> Q Kind
m0_2 Int
i Int
n = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT (Name -> Q Kind) -> (String -> Name) -> String -> Q Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
mkName (String -> Q Kind) -> String -> Q Kind
forall a b. (a -> b) -> a -> b
$ String
"TMapIndex.M" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

tupleKind :: [Kind] -> Kind
tupleKind :: Cxt -> Kind
tupleKind Cxt
ks = (Kind -> Kind -> Kind) -> Kind -> Cxt -> Kind
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Kind -> Kind -> Kind
appK (Int -> Kind
tupleK (Int -> Kind) -> Int -> Kind
forall a b. (a -> b) -> a -> b
$ Cxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Cxt
ks) Cxt
ks

listKind :: Kind -> Kind
listKind :: Kind -> Kind
listKind = (Kind
listK Kind -> Kind -> Kind
`appK`)

arrT :: Quote m => m Type -> m Type -> m Type
m Kind
t1 arrT :: forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`arrT` m Kind
t2 = m Kind
forall (m :: * -> *). Quote m => m Kind
arrowT m Kind -> m Kind -> m Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` m Kind
t1 m Kind -> m Kind -> m Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` m Kind
t2

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

promotedConsType :: Quote m => m Type -> m Type -> m Type
promotedConsType :: forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
promotedConsType m Kind
t m Kind
ts = m Kind
forall (m :: * -> *). Quote m => m Kind
promotedConsT m Kind -> m Kind -> m Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` m Kind
t m Kind -> m Kind -> m Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` m Kind
ts

heteroCons :: Quote m => m Exp -> m Exp -> m Exp
heteroCons :: forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
heteroCons m Exp
x m Exp
xs = Maybe (m Exp) -> m Exp -> Maybe (m Exp) -> m Exp
forall (m :: * -> *).
Quote m =>
Maybe (m Exp) -> m Exp -> Maybe (m Exp) -> m Exp
infixE (m Exp -> Maybe (m Exp)
forall a. a -> Maybe a
Just m Exp
x) (Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
conE '(:**)) (m Exp -> Maybe (m Exp)
forall a. a -> Maybe a
Just m Exp
xs)

heteroConsP :: Quote m => m Pat -> m Pat -> m Pat
heteroConsP :: forall (m :: * -> *). Quote m => m Pat -> m Pat -> m Pat
heteroConsP m Pat
p m Pat
ps = m Pat -> Name -> m Pat -> m Pat
forall (m :: * -> *). Quote m => m Pat -> Name -> m Pat -> m Pat
infixP m Pat
p '(:**) m Pat
ps

typeVarNames :: [String]
typeVarNames :: [String]
typeVarNames = ((Char -> String -> String
forall a. a -> [a] -> [a]
: String
"") (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]
typeVarNames, Char
c <- [Char
'a' .. Char
'z'] ]

kindVarNames :: [String]
kindVarNames :: [String]
kindVarNames = (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 ..]