tuples are heterogeneous lists

3 files changed, 105 insertions, 109 deletions

diff --git a/lc/Builtins.lc b/lc/Builtins.lc
index 7ad75672..a0b9e5e0 100644
--- a/lc/Builtins.lc
+++ b/lc/Builtins.lc
@@ -1,4 +1,5 @@
 {-# LANGUAGE NoImplicitPrelude #-}
+
 module Builtins
     ( module Internals
     , module Builtins
@@ -26,10 +27,6 @@ type family VecScalar (n :: Nat) a where
     VecScalar 1 a = a
     VecScalar ('Succ ('Succ n)) a = Vec ('Succ ('Succ n)) a
 
--- may be a data family?
-type family TFVec (n :: Nat) a where
-    TFVec n a = Vec n a     -- TODO: check range: n = 2,3,4;  a is Float, Int, Word, Bool
-
 -- todo: use less constructors with more parameters
 data Mat :: Nat -> Nat -> Type -> Type where
   M22F :: Vec 2 Float -> Vec 2 Float -> Mat 2 2 Float
@@ -252,10 +249,12 @@ data RasterContext a :: PrimitiveType -> Type where
   PointCtx            :: PointSize a -> Float -> PointSpriteCoordOrigin                -> RasterContext a Point
   LineCtx             :: Float -> ProvokingVertex                                      -> RasterContext a Line
 
-type family FTRepr' a where
-    -- TODO
-    FTRepr' [a] = a
-    FTRepr' ([a], [b]) = (a, b)
+map _ []     = []
+map f (x:xs) = f x : map f xs
+
+type family ListElem a where ListElem [a] = a
+
+type family HListElem a :: [Type] where HListElem (HList l) = l
 
 data Blending :: Type -> Type where
   NoBlending          ::                                   Blending t
@@ -264,28 +263,15 @@ data Blending :: Type -> Type where
                          -> ((BlendingFactor, BlendingFactor), (BlendingFactor, BlendingFactor))
                          -> Vec 4 Float ->                 Blending Float
 
-{- TODO: more precise kinds
-  FragmentOperation    :: Semantic -> *
-  FragmentOut          :: Semantic -> *
--}
-
 data StencilTests
 data StencilOps
 data Int32
 
 data FragmentOperation :: ImageSemantics -> Type where
-  ColorOp             :: (mask ~ VecScalar d Bool, color ~ VecScalar d c, Num c) => Blending c -> mask
-                                                                   -> FragmentOperation (Color color)
+  ColorOp             :: Num c => Blending c -> VecScalar d Bool   -> FragmentOperation (Color (VecScalar d c))
   DepthOp             :: ComparisonFunction -> Bool                -> FragmentOperation (Depth Float)
   StencilOp           :: StencilTests -> StencilOps -> StencilOps  -> FragmentOperation (Stencil Int32)
 
-type family FragOps (a :: [ImageSemantics]) where
-    FragOps '[t] = (FragmentOperation t)
-    FragOps '[t1, t2] = (FragmentOperation t1, FragmentOperation t2)
-    FragOps '[t1, t2, t3] = (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3)
-    FragOps '[t1, t2, t3, t4] =  (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4)
-    FragOps '[t1, t2, t3, t4, t5] =  (FragmentOperation t1, FragmentOperation t2, FragmentOperation t3, FragmentOperation t4, FragmentOperation t5)
-
 []   ++ ys = ys
 x:xs ++ ys = x : xs ++ ys
 
@@ -294,9 +280,6 @@ foldr f e (x: xs) = f x (foldr f e xs)
 
 concat = foldr (++) []
 
-map _ []     = []
-map f (x:xs) = f x : map f xs
-
 concatMap :: (a -> [b]) -> [a] -> [b]
 concatMap f x = concat (map f x)
 
@@ -315,7 +298,7 @@ mapPrimitive f (PrimTriangle a b c) = PrimTriangle (f a) (f b) (f c)
 -}
 
 fetch_               :: forall a t . (AttributeTuple t) => String -> t -> PrimitiveStream a t
-fetchArrays_         :: forall a t t' . (AttributeTuple t, t ~ FTRepr' t') => t' -> PrimitiveStream a t
+fetchArrays_         :: forall a t t' . (AttributeTuple t, t ~ HList (map ListElem (HListElem t'))) => t' -> PrimitiveStream a t
 
 mapPrimitives :: (a -> b) -> PrimitiveStream p a -> PrimitiveStream p b
 mapPrimitives f = map (mapPrimitive f)
@@ -323,23 +306,6 @@ mapPrimitives f = map (mapPrimitive f)
 fetch s a t = fetch_ @a s t
 fetchArrays a t = fetchArrays_ @a t
 
-remSemantics :: ImageSemantics -> Type
-remSemantics (Color a) = a
-remSemantics (Depth a) = a
-remSemantics (Stencil a) = a
-
-remSemantics_ :: [ImageSemantics] -> Type
-remSemantics_ [] = '()
-remSemantics_ [a] = remSemantics a
-remSemantics_ [a, b] = '(remSemantics a, remSemantics b)
-remSemantics_ [a, b, c] = '(remSemantics a, remSemantics b, remSemantics c)
-remSemantics_ [a, b, c, d] = '(remSemantics a, remSemantics b, remSemantics c, remSemantics d)
-remSemantics_ [a, b, c, d, e] = '(remSemantics a, remSemantics b, remSemantics c, remSemantics d, remSemantics e)
-
-remSemantics' :: [ImageSemantics] -> Type
-remSemantics' (Depth _: x) = remSemantics_ x 
-remSemantics' x = remSemantics_ x 
-
 -------------------
 
 data Maybe a
@@ -379,21 +345,13 @@ data Interpolated t where
                       :: (Floating t) => Interpolated t
   Flat                ::                 Interpolated t
 
-type family InterpolatedType a where
-    InterpolatedType () = ()
-    InterpolatedType (Interpolated a) = a
-    InterpolatedType (Interpolated a, Interpolated b) = (a, b)
-    InterpolatedType (Interpolated a, Interpolated b, Interpolated c) = (a, b, c)
-    InterpolatedType (Interpolated a, Interpolated b, Interpolated c, Interpolated d) = (a, b, c, d)
-    InterpolatedType (Interpolated a, Interpolated b, Interpolated c, Interpolated d, Interpolated e) = (a, b, c, d, e)
-
 rasterizePrimitive
-    :: ( b ~ InterpolatedType interpolation
-       , a ~ JoinTupleType (Vec 4 Float) b )
-    => interpolation                -- tuple of Smooth & Flat
-    -> RasterContext a x
-    -> Primitive a x
-    -> FragmentStream 1 b
+    :: ( map Interpolated b ~ interpolation
+       , a ~ 'Cons (Vec 4 Float) b )
+    => HList interpolation                -- tuple of Smooth & Flat
+    -> RasterContext (HList a) x
+    -> Primitive (HList a) x
+    -> FragmentStream 1 (HList b)
 
 rasterizePrimitives ctx is s = concat (map (rasterizePrimitive is ctx) s)
 
@@ -404,14 +362,19 @@ ColorImage          :: forall a d t color . (Num t, color ~ VecScalar d t)
 DepthImage          :: forall a . Float  -> Image a (Depth Float)
 StencilImage        :: forall a . Int    -> Image a (Stencil Int)
 
-type family SameLayerCounts a where
-    SameLayerCounts (Image n1 t1) = Unit
-    SameLayerCounts (Image n1 t1, Image n2 t2) = EqCT Nat n1 n2
-    SameLayerCounts (Image n1 t1, Image n2 t2, Image n3 t3) = T2 (EqCT Nat n1 n2) (EqCT Nat n1 n3)
+type family ImageLC a :: Nat where ImageLC (Image n t) = n
+
+allSame :: [a] -> Type
+allSame [] = 'Unit
+allSame [x] = 'Unit
+allSame (x: y: xs) = 'T2 (x ~ y) (allSame (y:xs))
+
+sameLayerCounts a = allSame (map 'ImageLC a)
+
 {-
-class DefaultFragOp a where defaultFragOp :: FragmentOperation a
-instance DefaultFragOp (Color (VecS Float 4)) where defaultFragOp = ColorOp NoBlending (V4 True True True True)
-instance DefaultFragOp (Depth Float) where defaultFragOp = DepthOp Less True
+defaultFragOp :: forall (a :: ImageSemantics) -> FragmentOperation a
+defaultFragOp (Color '(VecS Float 4)) = ColorOp NoBlending (V4 True True True True)
+defaultFragOp (Depth 'Float) = DepthOp Less True
 
 class DefaultFragOps a where defaultFragOps :: a
 instance (DefaultFragOp a, DefaultFragOp b) => DefaultFragOps (FragmentOperation a, FragmentOperation b) where
@@ -420,20 +383,35 @@ instance (DefaultFragOp a, DefaultFragOp b) => DefaultFragOps (FragmentOperation
 -}
 data FrameBuffer (n :: Nat) (t :: [ImageSemantics])
 
-Accumulate :: FragOps b -> FragmentStream n (remSemantics' b) -> FrameBuffer n b -> FrameBuffer n b
+remSemantics :: ImageSemantics -> Type
+remSemantics (Color a) = a
+remSemantics (Depth a) = a
+remSemantics (Stencil a) = a
+
+remSemantics' :: [ImageSemantics] -> [Type]
+remSemantics' (Depth _: x) = map remSemantics x 
+remSemantics' x = map remSemantics x 
 
-type family TFFrameBuffer a where
-    TFFrameBuffer (Image n1 t1) = FrameBuffer n1 '[t1]
-    TFFrameBuffer (Image n1 t1, Image n2 t2) = FrameBuffer n1 '[t1, t2]
-    TFFrameBuffer (Image n1 t1, Image n2 t2, Image n3 t3) = FrameBuffer n1 '[t1, t2, t3]
+type family FragmentOperationSem a :: ImageSemantics
+type instance FragmentOperationSem (FragmentOperation x) = x
+
+Accumulate :: forall (n :: Nat) (c :: [Type]) . (b ~ map FragmentOperationSem c) => HList c -> FragmentStream n (HList (remSemantics' b)) -> FrameBuffer n b -> FrameBuffer n b
+
+type family ImageSem a  :: ImageSemantics
+type instance ImageSem (Image n t) = t
+
+tfFrameBuffer t = map 'ImageSem t
 
 class ValidFrameBuffer (a :: [ImageSemantics])
 instance ValidFrameBuffer a -- TODO
 
-FrameBuffer  :: (ValidFrameBuffer b, SameLayerCounts a, FrameBuffer n b ~ TFFrameBuffer a) => a -> FrameBuffer n b
+head (x: _) = x
+
+FrameBuffer  :: forall (a :: [Type]) . (sameLayerCounts a) => HList a -> FrameBuffer (ImageLC (head a)) (tfFrameBuffer a)
 
 accumulate ctx fshader fstr fb = Accumulate ctx (mapFragments fshader fstr) fb
 
+-- todo: remove
 accumulationContext x = x
 
 -- texture support
@@ -480,9 +458,9 @@ PrimClampS                    :: (Num t, a ~ VecScalar d t) => a -> t -> t -> a
 PrimMix                       :: (a ~ VecScalar d Float) => a -> a -> a -> a
 PrimMixS                      :: (a ~ VecScalar d Float) => a -> a -> Float -> a
 PrimMixB                      :: (a ~ VecScalar d Float, b ~ VecScalar d Bool) => a -> a -> b -> a
-PrimStep                      :: (a ~ TFVec d Float) => a -> a -> a
+PrimStep                      :: (a ~ Vec d Float) => a -> a -> a
 PrimStepS                     :: (a ~ VecScalar d Float) => Float -> a -> a
-PrimSmoothStep                :: (a ~ TFVec d Float) => a -> a -> a -> a
+PrimSmoothStep                :: (a ~ Vec d Float) => a -> a -> a -> a
 PrimSmoothStepS               :: (a ~ VecScalar d Float) => Float -> Float -> a -> a
 
 -- Integer/Floatonversion Functions
diff --git a/lc/Internals.lc b/lc/Internals.lc
index 8a8bfe6f..9005cb0f 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -1,11 +1,13 @@
 {-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE TraceTypeCheck #-}
 -- declarations of builtin functions and data types used by the compiler
 module Internals where
 
 -- used for type annotations
 typeAnn x = x
 
+-- used for recognising double parenthesis
+parens x = x
+
 undefined :: forall (a :: Type) . a
 
 primFix :: forall (a :: Type) . (a -> a) -> a
@@ -22,40 +24,17 @@ type family EqCT (t :: Type) (a :: t) (b :: t)
 coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b
 coe a b TT x = unsafeCoerce @a @b x
 -}
--- TODO: generate?
-data Tuple0 = Tuple0
-data Tuple1 a = Tuple1 a
-data Tuple2 a b = Tuple2 a b
-data Tuple3 a b c = Tuple3 a b c
-data Tuple4 a b c d = Tuple4 a b c d
-data Tuple5 a b c d e = Tuple5 a b c d e
 
 -- ... TODO
 
 -- builtin used for overlapping instances
 parEval :: forall a -> a -> a -> a
 
-type family JoinTupleType t1 t2 where
-    -- TODO
-    JoinTupleType a () = a
-    JoinTupleType a (b, c) = (a, b, c)
-    JoinTupleType a (b, c, d) = (a, b, c, d)
-    JoinTupleType a (b, c, d, e) = (a, b, c, d, e)
-    JoinTupleType a b = (a, b)
-
 -- conjuction of constraints
 type family T2 a b
 
 match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t
 
-testmt :: forall (t :: Type) -> t -> t
-testmt 'Type = \'Tuple0 -> 'Tuple0
---testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> & 'Type) 'Tuple0 x undefined) t undefined) x
---testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> 'Type) 'Tuple0 x undefined) t undefined) x
-
---type instance EqCT Type = \'Type 'Type -> 'Unit
---type instance EqCT Type = \'(a, b) '(JoinTupleType a' b') -> '(T2 (EqCT Type a a') (EqCT Type b b'))
-
 type EqCTt = EqCT _
 
 -- builtin conjuction of constraint witnesses
@@ -144,4 +123,40 @@ data List a = Nil | Cons a (List a)
 
 infixr 5 :
 
+data HList :: [Type] -> Type where
+    HNil :: HList '[]
+    HCons :: x -> HList xs -> HList '(x: xs)
+
+hlistConsCase
+    :: forall (e :: Type) (f :: List Type)
+    .  forall (c :: Unit -> Type)
+    -> (e -> HList f -> c 'TT)
+    -> HList (Cons e f)
+    -> c 'TT
+{-
+-- TODO: unsafeCoerce is not really needed here
+hlistConsCase @e @f c fv x = 'HListCase 
+    (\_ _ -> c TT)
+    undefined
+    (\ @t @lt y ys -> fv (unsafeCoerce @t @e y) (unsafeCoerce @(HList lt) @(HList f) ys))
+    x
+-}
+hlistNilCase :: forall (c :: Unit -> Type) -> c 'TT -> HList Nil -> c 'TT
+{-
+hlistNilCase c x v = 'HListCase
+    (\_ _ -> c TT)
+    x
+    (\_ _ -> undefined :: c TT)
+    v
+-}
+
+--testmt :: forall (t :: Type) -> t -> t
+--testmt 'Type = \'Tuple0 -> 'Tuple0
+--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> & 'Type) 'Tuple0 x undefined) t undefined) x
+--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> 'Type) 'Tuple0 x undefined) t undefined) x
+
+--type instance EqCT Type = \'Type 'Type -> 'Unit
+--type instance EqCT Type = \'(a, b) '(JoinTupleType a' b') -> '(T2 (EqCT Type a a') (EqCT Type b b'))
+
+joinTupleType = HCons
 
diff --git a/lc/Prelude.lc b/lc/Prelude.lc
index c3b819d9..25e2331a 100644
--- a/lc/Prelude.lc
+++ b/lc/Prelude.lc
@@ -43,8 +43,8 @@ filter pred (x:xs) = case pred x of
                        True -> (x : filter pred xs)
                        False -> (filter pred xs)
 
-head :: [a] -> a
-head (a: _) = a
+--head :: [a] -> a
+--head (a: _) = a
 
 tail :: [a] -> [a]
 tail (_: xs) = xs
@@ -76,13 +76,6 @@ iterate f x =  x : iterate f (f x)
 fst (a, b) = a
 snd (a, b) = b
 
-tuptype :: [Type] -> Type
-tuptype [] = '()
-tuptype (x:xs) = '(x, tuptype xs)
-
-data RecordC (xs :: [(String, Type)])
-    = RecordCons (tuptype (map snd xs))
-
 False ||| x = x
 True ||| x = True
 
@@ -126,13 +119,23 @@ record :: [(String, Type)] -> Type
 --record xs = RecordCons ({- TODO: sortBy fst-} xs)
 -}
 
+data RecItem = RecItem String Type
+
+recItemType (RecItem _ t) = t
+
+data RecordC (xs :: [RecItem])
+    = RecordCons (HList (map recItemType xs))
+
 isKeyC _ _ [] = 'Empty ""
-isKeyC s t ((s', t'): ss) = if s == s' then t ~ t' else isKeyC s t ss
+isKeyC s t (RecItem s' t': ss) = if s == s' then t ~ t' else isKeyC s t ss
+
+fstTup (HCons a _) = a
+sndTup (HCons _ a) = a
 
 -- todo: don't use unsafeCoerce
-project :: forall a (xs :: [(String, Type)]) . forall (s :: String) -> 'isKeyC s a xs => RecordC xs -> a
-project @a @((s', a'): xs) s @_ (RecordCons ts) | s == s' = fst (unsafeCoerce @_ @(a, tuptype (map snd xs)) ts)
-project @a @((s', a'): xs) s @_ (RecordCons ts) = project @a @xs s @(undefined @(isKeyC s a xs)) (RecordCons (snd (unsafeCoerce @_ @(a, tuptype (map snd xs)) ts)))
+project :: forall a (xs :: [RecItem]) . forall (s :: String) -> 'isKeyC s a xs => RecordC xs -> a
+project @a @(RecItem s' a': xs) s @_ (RecordCons ts) | s == s' = fstTup (unsafeCoerce @_ @(HList '(a : map recItemType xs)) ts)
+project @a @(RecItem s' a': xs) s @_ (RecordCons ts) = project @a @xs s @(undefined @(isKeyC s a xs)) (RecordCons (sndTup (unsafeCoerce @_ @(HList '(a : map recItemType xs)) ts)))
 
 --------------------------------------- HTML colors