module Data.Tuple.Ops.Cons (cons, Cons, Consable) where
import GHC.Generics (Generic(..), (:*:)(..), (:+:)(..), URec, Rec0, C1, D1, S1, M1(..), U1, K1(..))
import GHC.TypeLits (Symbol)
import Type.Family.List
import Data.Tuple.Ops.Internal
class ConsableR va rb where
consR :: (Generic vb, Rep vb ~ D1 (MetaOfD1 (Rep vb)) rb) => va -> vb -> rb x -> ConsR va rb vb x
type family ConsR va rb vb where
ConsR va (C1 mc U1) vb = UnD1 (Rep va)
ConsR va (C1 mc (S1 ms (URec b))) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb))
ConsR va (b0 :+: b1) vb = RepOfTuple "(,)" (S1 MetaS (Rec0 va) :*: S1 MetaS (Rec0 vb))
ConsR va (RepOfTuple tcon (b0 :*: b1)) vb = RepOfTuple (TupleConSucc tcon) (N (L (S1 MetaS (Rec0 va) :*: b0 :*: b1)))
instance (Generic a, Rep a ~ D1 (MetaOfD1 (Rep a)) (UnD1 (Rep a))) => ConsableR a (C1 mc U1) where
consR a _ _ = unM1 $ from a
instance ConsableR va (C1 mc (S1 ms (URec b))) where
consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b))
instance ConsableR va (b0 :+: b1) where
consR a b _ = M1 (M1 (K1 a) :*: M1 (K1 b))
instance (Linearize b0, Linearize b1,
Normalize ((S1 MetaS (Rec0 va) :< L b0 ++ L b1)),
AppDistributive (L b0)) => ConsableR va (RepOfTuple tcon (b0 :*: b1)) where
consR a b _ = M1 $ normalize $ linearize $ (M1 (K1 a) :: S1 MetaS (Rec0 va) x) :*: unM1 (unM1 (from b))
type family TupleConSucc (a :: Symbol) where
TupleConSucc "(,)" = "(,,)"
TupleConSucc "(,,)" = "(,,,)"
TupleConSucc "(,,,)" = "(,,,,)"
TupleConSucc "(,,,,)" = "(,,,,,)"
TupleConSucc "(,,,,,)" = "(,,,,,,)"
TupleConSucc "(,,,,,,)" = "(,,,,,,,)"
TupleConSucc "(,,,,,,,)" = "(,,,,,,,,)"
TupleConSucc "(,,,,,,,,)" = "(,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,)" = "(,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,)" = "(,,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,,)" = "(,,,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,)"
TupleConSucc "(,,,,,,,,,,,,,,,)" = "(,,,,,,,,,,,,,,,,)"
type family Cons a b where
Cons z (a,b) = (z,a,b)
Cons z (a,b,c) = (z,a,b,c)
Cons z (a,b,c,d) = (z,a,b,c,d)
Cons z (a,b,c,d,e) = (z,a,b,c,d,e)
Cons z (a,b,c,d,e,f) = (z,a,b,c,d,e,f)
Cons z (a,b,c,d,e,f,g) = (z,a,b,c,d,e,f,g)
Cons z (a,b,c,d,e,f,g,h) = (z,a,b,c,d,e,f,g,h)
Cons z (a,b,c,d,e,f,g,h,i) = (z,a,b,c,d,e,f,g,h,i)
Cons z (a,b,c,d,e,f,g,h,i,j) = (z,a,b,c,d,e,f,g,h,i,j)
Cons z (a,b,c,d,e,f,g,h,i,j,k) = (z,a,b,c,d,e,f,g,h,i,j,k)
Cons z (a,b,c,d,e,f,g,h,i,j,k,l) = (z,a,b,c,d,e,f,g,h,i,j,k,l)
Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m)
Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n)
Cons z (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) = (z,a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)
Cons z () = z
Cons z a = (z,a)
type Consable a b c = (Generic a, Generic b, Generic c, Cons a b ~ c,
Rep b ~ D1 (MetaOfD1 (Rep b)) (UnD1 (Rep b)),
Rep c ~ D1 (MetaOfD1 (Rep c)) (UnD1 (Rep c)),
ConsableR a (UnD1 (Rep b)),
ConsR a (UnD1 (Rep b)) b ~ (UnD1 (Rep c)))
cons :: Consable a b c => a -> b -> c
cons a b = to $ M1 $ consR a b (unM1 $ from b)