generate functions in shaders

4 files changed, 145 insertions, 97 deletions

diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs
index 62f7a49e..5f7bd4fd 100644
--- a/src/LambdaCube/Compiler.hs
+++ b/src/LambdaCube/Compiler.hs
@@ -130,7 +130,7 @@ ioFetch paths imp n = do
 
 splitMPath fn = (joinPath as, intercalate "." $ bs ++ [y])
   where
-    (as, bs) = span (\x -> null x || x == "." || x == "/" || isLower (head x)) xs
+    (as, bs) = span (\x -> null x || not (isUpper $ head x)) xs
     (xs, y) = map takeDirectory . splitPath *** id $ splitFileName $ dropExtension fn
 
 
@@ -161,11 +161,11 @@ loadModule imp mname = do
                                 ExportId (snd -> d) -> case  Map.lookup d $ getPolyEnv x of
                                     Just def -> PolyEnv (Map.singleton d def) mempty
                                     Nothing  -> error $ d ++ " is not defined"
-                                ExportModule (snd -> m) | m == snd (splitMPath mname) -> x
+                                ExportModule (snd -> m) | m == snd (splitMPath fname) -> x
                                 ExportModule m -> case [ ms
                                                        | ((m', is), ms) <- zip (moduleImports e) ms, m' == m] of
                                     [PolyEnv x infos] -> PolyEnv x mempty   -- TODO
-                                    []  -> error "empty export list"
+                                    []  -> error $ "empty export list: " ++ show (fname, m, map fst $ moduleImports e, snd (splitMPath fname))
                                     _   -> error "export list: internal error"
                 modify $ Map.insert fname $ Right (x', src)
                 return (fname, x')
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 1d9f9017..42dcd1bb 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -27,7 +27,7 @@ import qualified LambdaCube.Linear as IR
 
 import LambdaCube.Compiler.Pretty
 import Text.PrettyPrint.Compact (nest)
-import LambdaCube.Compiler.Infer hiding (Con, Lam, Pi, TType, Var, ELit)
+import LambdaCube.Compiler.Infer hiding (Con, Lam, Pi, TType, Var, ELit, Func)
 import qualified LambdaCube.Compiler.Infer as I
 import LambdaCube.Compiler.Parser (up, Up (..))
 
@@ -337,7 +337,7 @@ compFrag x = case x of
 
 -- todo: remove
 toGLSLType msg (TTuple []) = "void"
-toGLSLType msg x = showGLSLType msg $ compInputType x
+toGLSLType msg x = showGLSLType msg $ compInputType msg x
 
 -- move to lambdacube-ir?
 showGLSLType msg = \case
@@ -369,40 +369,44 @@ showGLSLType msg = \case
     IR.FTexture2D -> "sampler2D"
     t -> error $ "toGLSLType: " ++ msg ++ " " ++ show t
 
-compInputType x = case x of
-  TFloat          -> IR.Float
-  TVec 2 TFloat   -> IR.V2F
-  TVec 3 TFloat   -> IR.V3F
-  TVec 4 TFloat   -> IR.V4F
-  TBool           -> IR.Bool
-  TVec 2 TBool    -> IR.V2B
-  TVec 3 TBool    -> IR.V3B
-  TVec 4 TBool    -> IR.V4B
-  TInt            -> IR.Int
-  TVec 2 TInt     -> IR.V2I
-  TVec 3 TInt     -> IR.V3I
-  TVec 4 TInt     -> IR.V4I
-  TWord           -> IR.Word
-  TVec 2 TWord    -> IR.V2U
-  TVec 3 TWord    -> IR.V3U
-  TVec 4 TWord    -> IR.V4U
-  TMat 2 2 TFloat -> IR.M22F
-  TMat 2 3 TFloat -> IR.M23F
-  TMat 2 4 TFloat -> IR.M24F
-  TMat 3 2 TFloat -> IR.M32F
-  TMat 3 3 TFloat -> IR.M33F
-  TMat 3 4 TFloat -> IR.M34F
-  TMat 4 2 TFloat -> IR.M42F
-  TMat 4 3 TFloat -> IR.M43F
-  TMat 4 4 TFloat -> IR.M44F
-  x -> error $ "compInputType " ++ ppShow x
+supType = isJust . compInputType_
+
+compInputType_ x = case x of
+  TFloat          -> Just IR.Float
+  TVec 2 TFloat   -> Just IR.V2F
+  TVec 3 TFloat   -> Just IR.V3F
+  TVec 4 TFloat   -> Just IR.V4F
+  TBool           -> Just IR.Bool
+  TVec 2 TBool    -> Just IR.V2B
+  TVec 3 TBool    -> Just IR.V3B
+  TVec 4 TBool    -> Just IR.V4B
+  TInt            -> Just IR.Int
+  TVec 2 TInt     -> Just IR.V2I
+  TVec 3 TInt     -> Just IR.V3I
+  TVec 4 TInt     -> Just IR.V4I
+  TWord           -> Just IR.Word
+  TVec 2 TWord    -> Just IR.V2U
+  TVec 3 TWord    -> Just IR.V3U
+  TVec 4 TWord    -> Just IR.V4U
+  TMat 2 2 TFloat -> Just IR.M22F
+  TMat 2 3 TFloat -> Just IR.M23F
+  TMat 2 4 TFloat -> Just IR.M24F
+  TMat 3 2 TFloat -> Just IR.M32F
+  TMat 3 3 TFloat -> Just IR.M33F
+  TMat 3 4 TFloat -> Just IR.M34F
+  TMat 4 2 TFloat -> Just IR.M42F
+  TMat 4 3 TFloat -> Just IR.M43F
+  TMat 4 4 TFloat -> Just IR.M44F
+  _ -> Nothing
+
+compInputType msg x = fromMaybe (error $ "compInputType " ++ msg ++ " " ++ ppShow x) $ compInputType_ x
 
 is234 = (`elem` [2,3,4])
 
 
 compAttribute x = case x of
   ETuple a -> concatMap compAttribute a
-  A1 "Attribute" (EString s) -> [(s, compInputType $ tyOf x)]
+  A1 "Attribute" (EString s) -> [(s, compInputType "compAttr" $ tyOf x)]
   x -> error $ "compAttribute " ++ ppShow x
 
 compList (A2 "Cons" a x) = compValue a : compList x
@@ -430,7 +434,7 @@ compAttributeValue x = checkLength $ go x
 
     go = \case
       ETuple a -> concatMap go a
-      a -> let A1 "List" (compInputType -> t) = tyOf a
+      a -> let A1 "List" (compInputType "compAV" -> t) = tyOf a
                values = compList a
            in
             [(length values,(t,foldr (flatten t) (emptyArray t) values))]
@@ -524,6 +528,7 @@ genGLSLs backend
            uniformDecls vertUniforms
         <> [shaderDecl (caseWO "attribute" "in") (text t) (text n) | (n, t) <- zip vertInNames vertIns]
         <> vertOutDecls "out"
+        <> map shaderF vertFuncs
         <> [mainFunc $
                [shaderLet (text n) x | (n, x) <- zip vertOutNamesWithPosition vertGLSL]
             <> [shaderLet "gl_PointSize" x | Just x <- [ptGLSL]]
@@ -534,6 +539,7 @@ genGLSLs backend
            uniformDecls fragUniforms
         <> vertOutDecls "in"
         <> [shaderDecl "out" (toGLSLType "4" tfrag) fragColorName | noUnit tfrag, backend == OpenGL33]
+        <> map shaderF fragFuncs
         <> [mainFunc $
                [shaderStmt $ "if" <+> parens ("!" <> parens filt) <+> "discard" | Just filt <- [filtGLSL]]
             <> [shaderLet fragColorName $ fromMaybe (text $ head vertOutNames) fragGLSL | noUnit tfrag]
@@ -547,14 +553,41 @@ genGLSLs backend
         Just (etaRed -> Just (vertIns, verts)) -> (toGLSLType "3" <$> vertIns, eTuple verts)
         Nothing      -> ([], [mkTVar 0 tvert])
 
-    (((vertGLSL, ptGLSL), vertUniforms), ((filtGLSL, fragGLSL), fragUniforms)) = flip evalState shaderNames $ (,)
-        <$> runWriterT ((,)
-            <$> traverse (genGLSL' vertInNames . (,) vertIns) verts
-            <*> traverse (genGLSL' vertOutNamesWithPosition . red) rp)
-        <*> runWriterT ((,)
-            <$> traverse (genGLSL' vertOutNames . red) ffilter
-            <*> traverse (genGLSL' vertOutNames . red) frag)
+    (((vertGLSL, ptGLSL), (vertUniforms, vertFuncs)), ((filtGLSL, fragGLSL), (fragUniforms, fragFuncs))) = flip evalState shaderNames $ do
+        ((g1, (us1, verts)), (g2, (us2, frags))) <- (,)
+            <$> runWriterT ((,)
+                <$> traverse (genGLSL' vertInNames . (,) vertIns) verts
+                <*> traverse (genGLSL' vertOutNamesWithPosition . red) rp)
+            <*> runWriterT ((,)
+                <$> traverse (genGLSL' vertOutNames . red) ffilter
+                <*> traverse (genGLSL' vertOutNames . red) frag)
+        (,) <$> ((,) g1 <$> fixFuncs us1 [] verts) <*> ((,) g2 <$> fixFuncs us2 [] frags)
+
+    fixFuncs :: Uniforms -> [(SName, (Doc, ExpTV, [ExpTV]))] -> Map.Map SName (ExpTV, ExpTV, [ExpTV]) -> State [SName] (Uniforms, [(SName, (Doc, ExpTV, [ExpTV]))])
+    fixFuncs us fsb fsa
+        | Map.null fsa = return (us, fsb)
+        | otherwise = do
+            (unzip -> (defs, unzip -> (us', fs'))) <- forM fsa' $ \(fn, (def, ty, tys)) -> do
+                let
+                    removeLams 0 x = x
+                    removeLams i (ELam _ x) = removeLams (i-1) x
+                    removeLams i (Lam Hidden _ x) = removeLams i x
+                    removeLams i x = error $ "removeLams: " ++ fn ++ " " ++ show i ++ " " ++ show x
+
+                runWriterT $ genGLSL (reverse $ take (length tys) funArgs) $ removeLams (length tys) def
+            let fsb' = zipWith combine fsa' defs <> fsb
+            fixFuncs (us <> mconcat us') fsb' (Map.filterWithKey (\k _ -> k `notElem` map fst fsb') $ mconcat fs')
+      where
+        fsa' = Map.toList fsa
+        combine (fn, (_, ty, tys)) def = (fn, (def, ty, tys))
+
+    shaderF (fn, (def, ty, tys))
+        = shaderFunc' (toGLSLType "44" ty) (text fn)
+                     (zipWith (<+>) (map (toGLSLType "45") tys) (map text funArgs))
+                     def
 
+
+    funArgs      = map (("z" ++) . show) [0..]
     shaderNames  = map (("s" ++) . show)  [0..]
     vertInNames  = map (("vi" ++) . show) [1..length vertIns]
     vertOutNames = map (("vo" ++) . show) [1..length vertOuts]
@@ -583,6 +616,9 @@ genGLSLs backend
       <> [shaderFunc "vec4" "texture2D" ["sampler2D s", "vec2 uv"] [shaderReturn "texture(s,uv)"] | backend == OpenGL33]
       <> xs
 
+    shaderFunc' ot n [] b = shaderLet (ot <+> n) b
+    shaderFunc' ot n ps b = shaderFunc ot n ps [shaderReturn b]
+
     shaderFunc outtype name pars body = nest 4 (outtype <+> name <> tupled pars <+> "{" <$$> vcat body) <$$> "}"
     mainFunc xs = shaderFunc "void" "main" [] xs
     shaderStmt xs = nest 4 $ xs <> ";"
@@ -606,12 +642,16 @@ data Uniform
 
 type Uniforms = Map String (Uniform, IR.InputType)
 
-genGLSL :: [SName] -> ExpTV -> WriterT Uniforms (State [String]) Doc
+tellUniform x = tell (x, mempty)
+
+genGLSL :: [SName] -> ExpTV -> WriterT (Uniforms, Map.Map SName (ExpTV, ExpTV, [ExpTV])) (State [String]) Doc
 genGLSL dns e = case e of
 
   ELit a -> pure $ text $ show a
   Var i _ -> pure $ text $ dns !! i
 
+  Func fn def ty xs -> tell (mempty, Map.singleton fn (def, ty, map tyOf xs)) >> call fn xs
+
   Con cn xs -> case cn of
     "primIfThenElse" -> case xs of [a, b, c] -> hsep <$> sequence [gen a, pure "?", gen b, pure ":", gen c]
 
@@ -620,15 +660,15 @@ genGLSL dns e = case e of
 
     "Uniform" -> case xs of
         [EString s] -> do
-            tell $ Map.singleton s $ (,) UUniform $ compInputType $ tyOf e
+            tellUniform $ Map.singleton s $ (,) UUniform $ compInputType "unif" $ tyOf e
             pure $ text s
     "Sampler" -> case xs of
         [_, _, A1 "Texture2DSlot" (EString s)] -> do
-            tell $ Map.singleton s $ (,) UTexture2DSlot IR.FTexture2D{-compInputType $ tyOf e  -- TODO-}
+            tellUniform $ Map.singleton s $ (,) UTexture2DSlot IR.FTexture2D{-compInputType $ tyOf e  -- TODO-}
             pure $ text s
         [_, _, A2 "Texture2D" (A2 "V2" (EInt w) (EInt h)) b] -> do
             s <- newName
-            tell $ Map.singleton s $ (,) (UTexture2D w h b) IR.FTexture2D
+            tellUniform $ Map.singleton s $ (,) (UTexture2D w h b) IR.FTexture2D
             pure $ text s
 
     'P':'r':'i':'m':n | n'@(_:_) <- trName (dropS n) -> call n' xs
@@ -735,7 +775,7 @@ genGLSL dns e = case e of
             "==" -> "=="
 
             n | n `elem` ["primNegateWord", "primNegateInt", "primNegateFloat"] -> "-_"
-            n | n `elem` ["V2", "V3", "V4"] -> toGLSLType "5" $ tyOf e
+            n | n `elem` ["V2", "V3", "V4"] -> toGLSLType (n ++ " " ++ show (length xs)) $ tyOf e
             _ -> ""
 
     -- not supported
@@ -793,7 +833,7 @@ genGLSL dns e = case e of
 data ExpTV = ExpTV_ Exp Exp [Exp]
   deriving (Show, Eq)
 
-pattern ExpTV a b c <- ExpTV_ a b c where ExpTV a b c = ExpTV_ (unLab' a) (unLab' b) c
+pattern ExpTV a b c <- ExpTV_ a b c where ExpTV a b c = ExpTV_ (a) (unLab' b) c
 
 type Ty = ExpTV
 
@@ -809,7 +849,8 @@ pattern Con h b     <- (mkCon -> Just (h, b))
 pattern App a b     <- (mkApp -> Just (a, b))
 pattern Var a b     <- (mkVar -> Just (a, b))
 pattern ELit l      <- ExpTV (I.ELit l) _ _
-pattern TType       <- ExpTV I.TType _ _
+pattern TType       <- ExpTV (unLab' -> I.TType) _ _
+pattern Func fn def ty xs <- (mkFunc -> Just (fn, def, ty, xs))
 
 pattern EString s <- ELit (LString s)
 pattern EFloat s  <- ELit (LFloat s)
@@ -818,26 +859,33 @@ pattern EInt s    <- ELit (LInt s)
 t .@ vs = ExpTV t I.TType vs
 infix 1 .@
 
-mkVar (ExpTV (I.Var i) t vs) = Just (i, t .@ vs)
+mkVar (ExpTV (unLab' -> I.Var i) t vs) = Just (i, t .@ vs)
 mkVar _ = Nothing
 
-mkPi (ExpTV (I.Pi b x y) _ vs) = Just (b, x .@ vs, y .@ addToEnv x vs)
+mkPi (ExpTV (unLab' -> I.Pi b x y) _ vs) = Just (b, x .@ vs, y .@ addToEnv x vs)
 mkPi _ = Nothing
 
-mkLam (ExpTV (I.Lam y) (I.Pi b x yt) vs) = Just (b, x .@ vs, ExpTV y yt $ addToEnv x vs)
+mkLam (ExpTV (unLab' -> I.Lam y) (I.Pi b x yt) vs) = Just (b, x .@ vs, ExpTV y yt $ addToEnv x vs)
 mkLam _ = Nothing
 
-mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (conType et s) $ mkConPars n et ++ xs)
-mkCon (ExpTV (TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
-mkCon (ExpTV (Neut (I.Fun s i (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
-mkCon (ExpTV (CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [Neut n])
-mkCon (ExpTV (TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, Neut n, f])
+mkCon (ExpTV (unLab' -> I.Con s n xs) et vs) = Just (untick $ show s, chain vs (conType et s) $ mkConPars n et ++ xs)
+mkCon (ExpTV (unLab' -> TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (unLab' -> Neut (I.Fun s i (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (unLab' -> CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [Neut n])
+mkCon (ExpTV (unLab' -> TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, Neut n, f])
 mkCon _ = Nothing
 
-mkApp (ExpTV (Neut (I.App_ a b)) et vs) = Just (ExpTV (Neut a) t vs, head $ chain vs t [b])
+mkApp (ExpTV (unLab' -> Neut (I.App_ a b)) et vs) = Just (ExpTV (Neut a) t vs, head $ chain vs t [b])
   where t = neutType' (mkEnv vs) a
 mkApp _ = Nothing
 
+mkFunc r@(ExpTV (I.Func n def nt xs) ty vs) | all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n
+    = Just (untick n, toExp (def, nt), tyOf r, xs')
+  where
+    xs' = chain vs nt $ reverse xs
+    validChar = isAlphaNum
+mkFunc _ = Nothing
+
 chain vs t@(I.Pi Hidden at y) (a: as) = chain vs (appTy t a) as
 chain vs t xs = chain' vs t xs
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 329ed140..ee78422d 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -18,10 +18,9 @@ module LambdaCube.Compiler.Infer
     ( Binder (..), SName, Lit(..), Visibility(..)
     , Exp (..), Neutral (..), ExpType, GlobalEnv
     , pattern Var, pattern CaseFun, pattern TyCaseFun, pattern App_
-    , pattern Con, pattern TyCon, pattern Pi, pattern Lam, pattern Fun, pattern ELit
+    , pattern Con, pattern TyCon, pattern Pi, pattern Lam, pattern Fun, pattern ELit, pattern Func, pattern LabelEnd
     , outputType, boolType, trueExp
     , down, Subst (..), free
-    , litType
     , initEnv, Env(..), pattern EBind2
     , SI(..), Range(..) -- todo: remove
     , Info(..), Infos, listAllInfos, listTypeInfos, listTraceInfos
@@ -65,7 +64,7 @@ data Exp
 pattern ELit a <- (unfixlabel -> ELit_ a) where ELit = ELit_
 
 data Neutral
-    = Fun_  MaxDB FunName !Int{-number of missing parameters-} [Exp]{-given parameters, reversed-} Neutral{-unfolded expression-}{-not neut?-}
+    = Fun_ MaxDB FunName [Exp]{-local vars-} !Int{-number of missing parameters-} [Exp]{-given parameters, reversed-} Neutral{-unfolded expression-}{-not neut?-}
     | CaseFun__   MaxDB CaseFunName   [Exp] Neutral
     | TyCaseFun__ MaxDB TyCaseFunName [Exp] Neutral
     | App__ MaxDB Neutral Exp
@@ -78,7 +77,7 @@ data ConName = ConName SName Int{-ordinal number, e.g. Zero:0, Succ:1-} Type
 
 data TyConName = TyConName SName Int{-num of indices-} Type [(ConName, Type)]{-constructors-} CaseFunName
 
-data FunName = FunName SName Type
+data FunName = FunName SName (Maybe Exp) Type
 
 data CaseFunName = CaseFunName SName Type Int{-num of parameters-}
 
@@ -92,8 +91,8 @@ instance Show ConName where show (ConName n _ _) = n
 instance Eq ConName where ConName _ n _ == ConName _ n' _ = n == n'
 instance Show TyConName where show (TyConName n _ _ _ _) = n
 instance Eq TyConName where TyConName n _ _ _ _ == TyConName n' _ _ _ _ = n == n'
-instance Show FunName where show (FunName n _) = n
-instance Eq FunName where FunName n _ == FunName n' _ = n == n'
+instance Show FunName where show (FunName n _ _) = n
+instance Eq FunName where FunName n _ _ == FunName n' _ _ = n == n'
 instance Show CaseFunName where show (CaseFunName n _ _) = caseName n
 instance Eq CaseFunName where CaseFunName n _ _ == CaseFunName n' _ _ = n == n'
 instance Show TyCaseFunName where show (TyCaseFunName n _) = MatchName n
@@ -109,13 +108,13 @@ pattern NoLE <- (isNoLabelEnd -> True)
 isNoLabelEnd (LabelEnd_ _) = False
 isNoLabelEnd _ = True
 
-pattern Fun f i xs n <- Fun_ _ f i xs n where Fun f i xs n = Fun_ (foldMap maxDB_ xs {- <> iterateN i lowerDB (maxDB_ n)-}) f i xs n
-pattern UTFun a t b <- Neut (Fun (FunName a t) _ (reverse -> b) NoLE)
+pattern Fun f i xs n <- Fun_ _ f _ i xs n where Fun f i xs n = Fun_ (foldMap maxDB_ xs {- <> iterateN i lowerDB (maxDB_ n)-}) f [] i xs n
+pattern UTFun a t b <- Neut (Fun (FunName a _ t) _ (reverse -> b) NoLE)
 pattern UFunN a b <- UTFun a _ b
 pattern DFun_ fn xs <- Fun fn 0 (reverse -> xs) (Delta _) where
-    DFun_ fn@(FunName n _) xs = Fun fn 0 (reverse xs) d where
+    DFun_ fn@(FunName n _ _) xs = Fun fn 0 (reverse xs) d where
         d = Delta $ SData $ getFunDef n $ \xs -> Neut $ Fun fn 0 (reverse xs) d
-pattern TFun' a t b = DFun_ (FunName a t) b
+pattern TFun' a t b = DFun_ (FunName a Nothing t) b
 pattern TFun a t b = Neut (TFun' a t b)
 
 pattern CaseFun_ a b c <- CaseFun__ _ a b c where CaseFun_ a b c = CaseFun__ (foldMap maxDB_ b <> maxDB_ c) a b c
@@ -184,12 +183,9 @@ pattern Succ n      <- ConN "Succ" (n:_) where Succ n = tCon "Succ" 1 (TNat :~>
 
 pattern CstrT t a b = Neut (CstrT' t a b)
 pattern CstrT' t a b = TFun' "'EqCT" (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b]
---pattern ReflCstr x  = TFun "reflCstr" (TType :~> CstrT TType (Var 0) (Var 0)) [x]
 pattern Coe a b w x = TFun "coe" (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x]
 pattern ParEval t a b = TFun "parEval" (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b]
-pattern Undef t     = TFun "undefined" (Pi Hidden TType (Var 0)) [t]
 pattern T2 a b      = TFun "'T2" (TType :~> TType :~> TType) [a, b]
-pattern T2C a b     = TFun "t2C" (Unit :~> Unit :~> Unit) [a, b]
 pattern CSplit a b c <- UFunN "'Split" [a, b, c]
 
 pattern EInt a      = ELit (LInt a)
@@ -243,7 +239,7 @@ trueExp = EBool True
 pattern LabelEnd x = Neut (LabelEnd_ x)
 
 pmLabel' :: FunName -> Int -> [Exp] -> Exp -> Exp
-pmLabel' (FunName _ _) 0 as (Neut (Delta (SData f))) = f $ reverse as
+pmLabel' (FunName _ _ _) 0 as (Neut (Delta (SData f))) = f $ reverse as
 pmLabel' f i xs (unfixlabel -> Neut y) = Neut $ Fun f i xs y
 pmLabel' f i xs y = error $ "pmLabel: " ++ show (f, i, length xs, y)
 
@@ -259,6 +255,15 @@ numLams x = 0
 pattern FL' y <- Fun f 0 xs (LabelEnd_ y)
 pattern FL y <- Neut (FL' y)
 
+pattern Func n def ty xs <- (mkFunc -> Just (n, def, ty, xs))
+
+mkFunc (Neut (Fun (FunName n (Just def) ty) 0 xs LabelEnd_{})) | Just def' <- removeLams (length xs) def = Just (n, def', ty, xs)
+mkFunc _ = Nothing
+
+removeLams 0 (LabelEnd x) = Just x
+removeLams n (Lam x) | n > 0 = Lam <$> removeLams (n-1) x
+removeLams _ _ = Nothing
+
 unfixlabel (FL y) = unfixlabel y
 unfixlabel a = a
 
@@ -393,7 +398,7 @@ instance Up Neutral where
         CaseFun__ c _ _ _ -> c
         TyCaseFun__ c _ _ _ -> c
         App__ c a b -> c
-        Fun_ c _ _ _ _ -> c
+        Fun_ c _ _ _ _ _ -> c
         LabelEnd_ x -> maxDB_ x
         Delta{} -> mempty
 
@@ -402,7 +407,7 @@ instance Up Neutral where
         CaseFun__ _ a as n -> CaseFun__ mempty a (closedExp <$> as) (closedExp n)
         TyCaseFun__ _ a as n -> TyCaseFun__ mempty a (closedExp <$> as) (closedExp n)
         App__ _ a b -> App__ mempty (closedExp a) (closedExp b)
-        Fun_ _ f i x y -> Fun_ mempty f i (closedExp <$> x) y
+        Fun_ _ f l i x y -> Fun_ mempty f l i (closedExp <$> x) y
         LabelEnd_ a -> LabelEnd_ (closedExp a)
         d@Delta{} -> d
 
@@ -454,7 +459,7 @@ evalCoe a b t d = Coe a b t d
 getFunDef s f = case s of
     "unsafeCoerce" -> \case xs@[_, _, x] -> case x of x@FL{} -> x; Neut{} -> f xs; _ -> x
     "'EqCT" -> \case [t, a, b] -> cstr t a b
-    "reflCstr" -> \case [a] -> reflCstr a
+    "reflCstr" -> \case [a] -> TT
     "coe" -> \case [a, b, t, d] -> evalCoe a b t d
     "'T2" -> \case [a, b] -> t2 a b
     "t2C" -> \case [a, b] -> t2C a b
@@ -551,19 +556,8 @@ cstr = f []
 
     isElemTy n = n `elem` ["'Bool", "'Float", "'Int"]
 
-
-reflCstr = \case
-{-
-    Unit -> TT
-    TType -> TT  -- ?
-    Con n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
-    TyCon n xs -> foldl (t2C te{-todo: more precise env-}) TT $ map (reflCstr te{-todo: more precise env-}) xs
-    x -> {-error $ "reflCstr: " ++ show x-} ReflCstr x
--}
-    x -> TT
-
 t2C (unfixlabel -> TT) (unfixlabel -> TT) = TT
-t2C a b = T2C a b
+t2C a b = TFun "t2C" (Unit :~> Unit :~> Unit) [a, b]
 
 t2 (unfixlabel -> Unit) a = a
 t2 a (unfixlabel -> Unit) = a
@@ -696,7 +690,7 @@ litType = \case
 
 class NType a where nType :: a -> Type
 
-instance NType FunName where nType (FunName _ t) = t
+instance NType FunName where nType (FunName _ _ t) = t
 instance NType TyConName where nType (TyConName _ _ t _ _) = t
 instance NType CaseFunName where nType (CaseFunName _ t _) = t
 instance NType TyCaseFunName where nType (TyCaseFunName _ t) = t
@@ -802,19 +796,22 @@ inferN_ tellTrace = infer  where
     checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t
 
     checkN_ te e t
-            -- temporal hack
-        | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
+        | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
             = infer te $ x `SAppV` SLam Visible SType (STyped mempty (subst (v+1) (Var 0) $ up 1 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b
             -- temporal hack
-        | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e
-            = infer te $ x `SAppV` STyped mempty (Lam $ subst (v+1) (Var 0) $ up 1 t, TNat :~> TType) `SAppV` a `SAppV` b `SAppV` SVar siv v
+        | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e
+            = infer te $ x `SAppV` SLamV (STyped mempty (subst (v+1) (Var 0) $ up1_ (v+2) $ up 1 t, TType)) `SAppV` a `SAppV` b `SAppV` SVar siv v
+            -- temporal hack
+        | x@(SGlobal (si, "'VecSCase")) `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v <- e
+        , TVec (Var n') _ <- snd $ varType "xx" v te
+            = infer te $ x `SAppV` SLamV (SLamV (STyped mempty (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar siv v
+
 {-
             -- temporal hack
-        | x@(SGlobal "'VecSCase") `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v <- e
-            = infer te $ x `SAppV` (SLamV (SLamV (STyped (subst (v+1) (Var 0) $ up 2 t, TType)))) `SAppV` a `SAppV` b `SAppV` c `SAppV` SVar v
+        | x@(SGlobal (si, "'HListCase")) `SAppV` SLamV (SLamV (Wildcard _)) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e
+        , TVec (Var n') _ <- snd $ varType "xx" v te
+            = infer te $ x `SAppV` SLamV (SLamV (STyped mempty (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` SVar siv v
 -}
-            -- temporal hack
-        | SGlobal (si, "undefined") <- e = focus_' te e (Undef t, t)
         | SLabelEnd x <- e = checkN (ELabelEnd te) x t
         | SApp si h a b <- e = infer (CheckAppType si h t te b) a
         | SLam h a b <- e, Pi h' x y <- t, h == h'  = do
@@ -1143,7 +1140,7 @@ handleStmt defs = \case
   Primitive n mf (trSExp' -> t_) -> do
         t <- inferType =<< ($ t_) <$> addF
         tellType (fst n) t
-        addToEnv n mf $ flip (,) t $ lamify t $ Neut . DFun_ (FunName (snd n) t)
+        addToEnv n mf $ flip (,) t $ lamify t $ Neut . DFun_ (FunName (snd n) Nothing t)
   Let n mf mt t_ -> do
         af <- addF
         let t__ = maybe id (flip SAnn . af) mt t_
@@ -1224,7 +1221,7 @@ withEnv e = local $ second (<> e)
 mkELet (False, n) x xt = x
 mkELet (True, n) x xt = term
   where
-    fn = FunName (snd n) xt
+    fn = FunName (snd n) (Just x) xt
 
     term = pmLabel fn 0 [] $ getFix x 0
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index aa9efe28..1bdf19f2 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -280,6 +280,9 @@ instance Up Void where
 
 instance Up a => Up (SExp' a) where
     up_ n = mapS' (\sn j i -> SVar sn $ if j < i then j else j+n) (+1)
+        where
+            mapS' = mapS__ (\i si x -> STyped si $ up_ n i x) (const . SGlobal)
+
     fold f = foldS (\i si x -> fold f i x) mempty $ \sn j i -> f j i
     maxDB_ _ = error "maxDB @SExp"