module Clr.ListTuple where
import Data.Kind
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
type family ListToTuple (t :: [Type]) :: Type where
ListToTuple '[] = ()
ListToTuple (a ': '[]) = (a)
ListToTuple (a ': b ': '[]) = (a,b)
ListToTuple (a ': b ': c ': '[]) = (a,b,c)
ListToTuple (a ': b ': c ': d ': '[]) = (a,b,c,d)
ListToTuple (a ': b ': c ': d ': e ': '[]) = (a,b,c,d,e)
ListToTuple (a ': b ': c ': d ': e ': f ': '[]) = (a,b,c,d,e,f)
ListToTuple (a ': b ': c ': d ': e ': f ': g ': '[]) = (a,b,c,d,e,f,g)
ListToTuple (a ': b ': c ': d ': e ': f ': g ': h ': '[]) = (a,b,c,d,e,f,g,h)
ListToTuple (a ': b ': c ': d ': e ': f ': g ': h ': i ': '[]) = (a,b,c,d,e,f,g,h,i)
ListToTuple (a ': b ': c ': d ': e ': f ': g ': h ': i ': j ': '[]) = (a,b,c,d,e,f,g,h,i,j)
ListToTuple (a ': b ': c ': d ': e ': f ': g ': h ': i ': j ': k ': '[]) = (a,b,c,d,e,f,g,h,i,j,k)
type family TupleToList (t::Type) :: [Type] where
TupleToList () = '[]
TupleToList (a,b) = '[a, b]
TupleToList (a,b,c) = '[a, b, c]
TupleToList (a,b,c,d) = '[a, b, c, d]
TupleToList (a,b,c,d,e) = '[a, b, c, d, e]
TupleToList (a,b,c,d,e,f) = '[a, b, c, d, e, f]
TupleToList (a,b,c,d,e,f,g) = '[a, b, c, d, e, f, g]
TupleToList (a,b,c,d,e,f,g,h) = '[a, b, c, d, e, f, g, h]
TupleToList (a,b,c,d,e,f,g,h,i) = '[a, b, c, d, e, f, g, h, i]
TupleToList (a,b,c,d,e,f,g,h,i,j) = '[a, b, c, d, e, f, g, h, i, j]
TupleToList (a,b,c,d,e,f,g,h,i,j,k) = '[a, b, c, d, e, f, g, h, i, j, k]
TupleToList (a) = '[a]
type family TupleSize (x::tupleKind) :: Nat where
TupleSize a = ListSize (TupleToList a)
type family ArgCount (x::tupleKind) :: Nat where
ArgCount () = 1
ArgCount a = TupleSize a
type family ListSize (x::k) :: Nat where
ListSize '[] = 0
ListSize (x ': xs) = 1 + (ListSize xs)
type family Elem (a :: k) (xs::[k]) :: Bool where
Elem a '[] = 'False
Elem a (x ': xs) = a == x || (Elem a xs)
type family Concat (a::[[t]]) :: [t] where
Concat '[] = '[]
Concat (x ': xs) = x `Append` (Concat xs)
type family Append (a::[t]) (b::[t]) :: [t] where
Append '[] ys = ys
Append (x ': xs) ys = x ': (xs `Append` ys)
type family CatMaybes (l :: [Maybe k]) :: [k] where
CatMaybes '[] = '[]
CatMaybes ('Just x ': xs) = x ': CatMaybes xs
CatMaybes ('Nothing ': xs) = CatMaybes xs
type family PrependIf (b :: Bool) (x :: k) (xs :: [k]) :: [k] where
PrependIf 'True x xs = x ': xs
PrependIf 'False x xs = xs
type family Index (x::[t]) (n::Nat) :: t where
Index (x ': xs) 0 = x
Index (x ': xs) n = Index xs (n1)
Index xs n = TypeError (Text "Out of bounds")