erease CaseFun's type parameters

4 files changed, 58 insertions, 39 deletions

diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index a378815d..4ddf4323 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -873,13 +873,13 @@ toExp = flip runReader [] . flip evalStateT freshTypeVars . f_
         I.Con s n xs    -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.mkConPars n et ++ xs)
         I.TyCon s xs    -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
         I.Fun s xs      -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
-        I.CaseFun s xs n -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (xs ++ [I.Neut n])
+        I.CaseFun s xs n -> asks makeTE >>= \te -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.makeCaseFunPars te n ++ xs ++ [I.Neut n])
         I.Neut (I.App_ a b) -> asks makeTE >>= \te -> do
             let t = I.neutType te a
             app' <$> f_ (I.Neut a, t) <*> (head <$> chain [] t [b])
         I.ELit l -> pure $ ELit l
         I.TType -> pure TType
-        I.PMLabel x _ -> f_ (x, et)
+        x@I.PMLabel{} -> f_ (I.unpmlabel x, et)
         I.FixLabel _ x -> f_ (x, et)
 --        I.LabelEnd x -> f x   -- not possible
         z -> error $ "toExp: " ++ show z
@@ -937,6 +937,7 @@ substE n x = \case
     Fun n' cn xs -> Fun n' cn (map (substE n x) xs)
     TType -> TType
     EApp a b -> app' (substE n x a) (substE n x b)
+    x@ELit{} -> x
     z -> error $ "substE: " ++ ppShow z
 
 app' (Lam _ (PVar _ n) _ x) b = substE n b x
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index bc599fda..56d96726 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -26,7 +26,7 @@ module LambdaCube.Compiler.Infer
     , Infos(..), listInfos, ErrorMsg(..), PolyEnv(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_
     , ImportItems (..)
     , SI(..), Range(..)
-    , nType, neutType, appTy, mkConPars
+    , nType, neutType, appTy, mkConPars, makeCaseFunPars, unpmlabel
     , MaxDB(..)
     ) where
 import Data.Monoid
@@ -66,7 +66,7 @@ data Neutral
     | TyCaseFun__ MaxDB TyCaseFunName [Exp]    -- todo: neutral at the end
     | App__ MaxDB Neutral Exp
     | Var_ !Int                 -- De Bruijn variable
-    | PMLabel_ Exp{-folded expression-} Exp{-unfolded expression-}
+    | PMLabel_ FunName !Int [Exp] Exp{-unfolded expression-}
   deriving (Show)
 
 data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} TyConName Type
@@ -115,6 +115,9 @@ conName a b c d = ConName a b c (get $ snd $ getParams d) d
   where
     get (TyCon s _) = s
 
+makeCaseFunPars te n = case neutType te n of
+    TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs -> take pars xs
+
 pattern Closed :: () => Up a => a -> a
 pattern Closed a <- a where Closed a = closedExp a
 
@@ -230,7 +233,7 @@ data LabelKind
     | -}LabelFix  -- fix unfold label
   deriving (Show)
 
-pattern PMLabel x y  = Neut (PMLabel_ x y)
+pattern PMLabel f i x y  = Neut (PMLabel_ f i x y)
 pattern FixLabel x y = Label LabelFix x y
 
 data LEKind
@@ -242,16 +245,24 @@ pattern LabelEnd x = LabelEnd_ LEPM x
 --pattern ClosedExp x = LabelEnd_ LEClosed x
 
 label LabelFix x y = FixLabel x y
-pmLabel x (UL (LabelEnd y)) = y
-pmLabel x y = PMLabel x y
+pmLabel :: FunName -> Int -> [Exp] -> Exp -> Exp
+pmLabel _ _ _ (unlabel -> LabelEnd y) = y
+pmLabel f i xs y = PMLabel f i xs y
 
 pattern UL a <- (unlabel -> a) where UL = unlabel
 
-unlabel (PMLabel a _) = unlabel a
+unpmlabel (PMLabel f i a _)
+    | i >= 0 = iterateN i Lam $ Fun f $ a ++ downTo 0 i
+    | otherwise = foldl app_ (Fun f $ reverse $ drop (-i) $ reverse a) (reverse $ take (-i) $ reverse a)
+
+unlabel x@PMLabel{} = unlabel (unpmlabel x)
 unlabel (FixLabel _ a) = unlabel a
 --unlabel (LabelEnd_ _ a) = unlabel a
 unlabel a = a
 
+unlabel'' (FixLabel _ a) = unlabel'' a
+unlabel'' a = a
+
 pattern UL' a <- (unlabel' -> a) where UL' = unlabel'
 
 --unlabel (PMLabel a _) = unlabel a
@@ -285,7 +296,7 @@ instance Eq Exp where
     _ == _ = False
 
 instance Eq Neutral where
-    PMLabel_ a _ == PMLabel_ a' _ = a == a'
+    PMLabel_ f i a _ == PMLabel_ f' i' a' _ = (f, i, a) == (f', i', a')
     Fun_ a b == Fun_ a' b' = (a, b) == (a', b')
     CaseFun_ a b c == CaseFun_ a' b' c' = (a, b, c) == (a', b', c')
     TyCaseFun_ a b == TyCaseFun_ a' b' = (a, b) == (a', b')
@@ -365,7 +376,7 @@ instance Subst Exp Exp where
                 CaseFun_ s as n -> evalCaseFun s (f i <$> as) (substNeut n)
                 TyCaseFun_ s as -> eval $ TyCaseFun s $ f i <$> as
                 App_ a b  -> app_ (substNeut a) (f i b)
-                PMLabel_ z v -> pmLabel (f i z) $ f i v
+                PMLabel_ fn c xs v -> pmLabel fn c (f i <$> xs) $ f i v
         f i e | {-i >= maxDB e-} isClosed e = e
         f i e = case e of
             Label lk z v -> label lk (f i z) $ f i v
@@ -385,7 +396,7 @@ instance Up Neutral where
             CaseFun__ md s as ne -> CaseFun__ (upDB n md) s (up_ n i <$> as) (up_ n i ne)
             TyCaseFun__ md s as -> TyCaseFun__ (upDB n md) s $ map (up_ n i) as
             App__ md a b -> App__ (upDB n md) (up_ n i a) (up_ n i b)
-            PMLabel_ x y -> PMLabel_ (up_ n i x) $ up_ n i y
+            PMLabel_ fn c x y -> PMLabel_ fn c (up_ n i <$> x) $ up_ n i y
 
     used i e
         | i >= maxDB e = False
@@ -397,7 +408,7 @@ instance Up Neutral where
         CaseFun_ _ as n -> foldMap (fold f i) as <> fold f i n
         TyCaseFun_ _ as -> foldMap (fold f i) as
         App_ a b -> fold f i a <> fold f i b
-        PMLabel_ x _ -> fold f i x
+        PMLabel_ _ _ x _ -> foldMap (fold f i) x
 
     maxDB_ = \case
         Var_ k -> varDB k
@@ -405,7 +416,7 @@ instance Up Neutral where
         CaseFun__ c _ _ _ -> c
         TyCaseFun__ c _ _ -> c
         App__ c a b -> c
-        PMLabel_ x y -> maxDB_ x
+        PMLabel_ _ _ x _ -> foldMap maxDB_ x
 
     closedExp = \case
         x@Var_{} -> error "impossible"
@@ -413,7 +424,7 @@ instance Up Neutral where
         CaseFun__ _ a as n -> CaseFun__ mempty a as n
         TyCaseFun__ _ a as -> TyCaseFun__ mempty a as
         App__ _ a b -> App__ mempty a b
-        PMLabel_ x y -> PMLabel_ (closedExp x) (closedExp y)
+        PMLabel_ f i x y -> PMLabel_ f i (map closedExp x) (closedExp y)
 
 instance (Subst x a, Subst x b) => Subst x (a, b) where
     subst i x (a, b) = (subst i x a, subst i x b)
@@ -427,13 +438,11 @@ varType err n_ env = f n_ env where
 
 -------------------------------------------------------------------------------- reduction
 
-evalCaseFun (CaseFunName _ t pars) (drop (pars + 1) -> ps) (Con (ConName _ _ i _ _) _ vs)
-    | i /= (-1) = foldl app_ (ps !! i) vs
+evalCaseFun a ps (Con (ConName _ _ i _ _) _ vs)
+    | i /= (-1) = foldl app_ (ps !! (i + 1)) vs
     | otherwise = error "evcf"
 evalCaseFun a b (Neut c) = CaseFun a b c
 evalCaseFun a b (FixLabel _ c) = evalCaseFun a b c
---evalCaseFun a b (Label _ _ _) = error $ "e cf: " ++ show a -- ++ "\n" ++ show x
---evalCaseFun a b x = error $ "ecf: " ++ show a -- ++ "\n" ++ show x
 
 eval = \case
     App a b -> app_ a b
@@ -642,11 +651,13 @@ app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++
 app_ (TyCon s xs) a = TyCon s (xs ++ [a])
 app_ (Label lk x e) a = label lk (app_ x a) $ app_ e a
 app_ (LabelEnd_ k x) a = LabelEnd_ k (app_ x a)   -- ???
-app_ (PMLabel x e) a = pmLabel (app_ x a) $ app_ e a
-app_ (Neut f) a = Neut $ App_ f a --neutApp f a
+--app_ (PMLabel x e) a = pmLabel (neutApp x a) $ app_ e a
+app_ (Neut f) a = neutApp f a
 
---neutApp (PMLabel_ x e) a = pmLabel (app_ x a) (app_ e a)
---neutApp f a = App_ f a
+neutApp (PMLabel_ f i xs e) a
+    = pmLabel f (i-1) (xs ++ [a]) (app_ e a)
+--    | i == 0 = app_ (pmLabel f i xs e) a
+neutApp f a = Neut $ App_ f a
 
 -------------------------------------------------------------------------------- constraints env
 
@@ -748,8 +759,9 @@ neutType te = \case
     App_ f x        -> appTy (neutType te f) x
     Var_ i          -> snd $ varType "C" i te
     Fun_ s ts       -> foldl appTy (nType s) ts
-    CaseFun_ s ts n -> appTy (foldl appTy (nType s) ts) (Neut n)
+    CaseFun_ s ts n -> appTy (foldl appTy (nType s) $ makeCaseFunPars te n ++ ts) (Neut n)
     TyCaseFun_ s ts -> foldl appTy (nType s) ts
+    PMLabel_ s _ a _ -> foldl appTy (nType s) a
 
 appTy (Pi _ a b) x = subst 0 x b
 appTy t x = error $ "appTy: " ++ show t
@@ -999,16 +1011,18 @@ recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
         (Con s n as, zt)      -> checkApps [] zt (Con s n . drop (conParams s)) te (nType s) $ mkConPars n zt ++ as
         (TyCon s as, zt)      -> checkApps [] zt (TyCon s) te (nType s) as
         (Fun s as, zt)        -> checkApps [] zt (Fun s) te (nType s) as
-        (CaseFun s as n, zt)  -> checkApps [] zt (\xs -> evalCaseFun s (init xs) (last xs)) te (nType s) (as ++ [Neut n])
+        (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
         (TyCaseFun s as, zt)  -> checkApps [] zt (TyCaseFun s) te (nType s) as
         (Label lk a x, zt)  -> Label lk (recheck_ msg te (a, zt)) x
-        (PMLabel a x, zt)   -> PMLabel (recheck_ msg te (a, zt)) x
+        (PMLabel f i a x, zt)   -> checkApps [] zt (\xs -> PMLabel f i xs x) te (nType f) a
         (LabelEnd_ k x, zt) -> LabelEnd_ k $ recheck_ msg te (x, zt)
       where
         checkApps acc zt f _ t [] | t == zt = f $ reverse acc
         checkApps acc zt f te t@(Pi h x y) (b_: xs) = checkApps (b: acc) zt f te (appTy t b) xs where b = recheck_ "checkApps" te (b_, x)
         checkApps acc zt f te t _ = error_ $ "checkApps " ++ msg ++ "\n" ++ showEnvExp te{-todo-} (t, TType) ++ "\n\n" ++ showEnvExp e (x, xt)
 
+        getNeut (Neut a) = a
+
 -- Ambiguous: (Int ~ F a) => Int
 -- Not ambiguous: (Show a, a ~ F b) => b
 ambiguityCheck :: String -> Exp -> Maybe String
@@ -1170,7 +1184,7 @@ handleStmt defs = \case
                 )
             $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0]
             )
-        addToEnv (fst s, caseName (snd s)) (lamify ct $ \xs -> evalCaseFun cfn (init xs) (last xs), ct)
+        addToEnv (fst s, caseName (snd s)) (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct)
         let ps' = fst $ getParams vty
             t =   (TType :~> TType)
               :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps'))
@@ -1184,7 +1198,11 @@ handleStmt defs = \case
 mkELet (False, n, mf, ar) x xt = x
 mkELet (True, n, SData mf, ar) x t{-type of x-} = term
   where
-    term = pmLabel (addLams' ar t 0) $ par ar t x 0
+    term = pmLabel (FunName (snd n) mf t) (addLams'' ar t) [] $ par ar t x 0
+
+    addLams'' [] _ = 0
+    addLams'' (h: ar) (Pi h' d t) | h == h' = 1 + addLams'' ar t
+    addLams'' ar@(Visible: _) (Pi h@Hidden d t) = 1 + addLams'' ar t
 
     addLams' [] _ i = Fun (FunName (snd n) mf t) $ downTo 0 i
     addLams' (h: ar) (Pi h' d t) i | h == h' = Lam $ addLams' ar t (i+1)
@@ -1366,7 +1384,7 @@ instance MkDoc Neutral where
       where
         g = mkDoc ts
         f = \case
-            PMLabel_ x _     -> g x
+            PMLabel_ s i xs _ -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM g xs
             Var_ k           -> shAtom <$> shVar k
             App_ a b         -> shApp Visible <$> g a <*> g b
             CstrT' TType a b -> shCstr <$> g a <*> g b
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 0920bc2d..1ce1896f 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -329,7 +329,7 @@ testdata/Prelude.lc 102:6-103:40  Type
 testdata/Prelude.lc 102:22-102:36  Type
 testdata/Prelude.lc 102:23-102:29  Type
 testdata/Prelude.lc 102:31-102:35  Type
-testdata/Prelude.lc 103:7-103:17  RecordC V2 | Type | {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) a) -> RecordC a
+testdata/Prelude.lc 103:7-103:17  RecordC V2 | Type | {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type ('snd String Type) a) -> RecordC a
 testdata/Prelude.lc 103:18-103:40  Type
 testdata/Prelude.lc 103:19-103:26  List Type -> Type
 testdata/Prelude.lc 103:27-103:39  List Type
@@ -434,16 +434,16 @@ testdata/Prelude.lc 169:45-170:164  List V2 -> V2 | V1 -> List V2 -> V2 | V10 |
 testdata/Prelude.lc 169:51-169:52  String
 testdata/Prelude.lc 169:51-169:56  String->Bool
 testdata/Prelude.lc 169:51-169:59  Bool
-testdata/Prelude.lc 169:51-170:164  'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V1) -> V1 | V13
+testdata/Prelude.lc 169:51-170:164  'tuptype ('map (Tuple2 String Type) Type ('snd String Type) V1) -> V1 | V13
 testdata/Prelude.lc 169:53-169:56  {a} -> {b : Eq a} -> a -> a->Bool
 testdata/Prelude.lc 169:57-169:59  V6
 testdata/Prelude.lc 169:62-169:65  {a} -> {b} -> Tuple2 a b -> a
 testdata/Prelude.lc 169:62-169:113  V15
 testdata/Prelude.lc 169:62-170:164  Bool->V16
-testdata/Prelude.lc 169:66-169:113  Tuple2 V15 ('tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V8))
+testdata/Prelude.lc 169:66-169:113  Tuple2 V15 ('tuptype ('map (Tuple2 String Type) Type ('snd String Type) V8))
 testdata/Prelude.lc 169:67-169:79  {a} -> {b} -> a->b
 testdata/Prelude.lc 169:67-169:82  {a} -> V1->a
-testdata/Prelude.lc 169:67-169:109  V0 -> Tuple2 V19 ('tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) V12))
+testdata/Prelude.lc 169:67-169:109  V0 -> Tuple2 V19 ('tuptype ('map (Tuple2 String Type) Type ('snd String Type) V12))
 testdata/Prelude.lc 169:84-169:109  Type
 testdata/Prelude.lc 169:85-169:86  Type
 testdata/Prelude.lc 169:88-169:95  List Type -> Type
@@ -453,7 +453,7 @@ testdata/Prelude.lc 169:97-169:100  {a} -> {b} -> a->b -> List a -> List b
 testdata/Prelude.lc 169:97-169:104  List (Tuple2 V0 V1) -> List V2
 testdata/Prelude.lc 169:101-169:104  {a} -> {b} -> Tuple2 a b -> b
 testdata/Prelude.lc 169:105-169:107  List (Tuple2 String Type)
-testdata/Prelude.lc 169:110-169:112  'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V3)
+testdata/Prelude.lc 169:110-169:112  'tuptype ('map (Tuple2 String Type) Type ('snd String Type) V3)
 testdata/Prelude.lc 170:51-170:58  {a} -> {b : List (Tuple2 String Type)} -> c:String -> {d : 'isKeyC String 'TT c a b} -> RecordC b -> a
 testdata/Prelude.lc 170:51-170:61  {a : List (Tuple2 String Type)} -> b:String -> {c : 'isKeyC String 'TT b V19 a} -> RecordC a -> V21
 testdata/Prelude.lc 170:51-170:65  a:String -> {b : 'isKeyC String 'TT a V17 V10} -> RecordC V11 -> V19
@@ -473,13 +473,13 @@ testdata/Prelude.lc 170:89-170:90  String
 testdata/Prelude.lc 170:91-170:92  Type
 testdata/Prelude.lc 170:93-170:95  List (Tuple2 String Type)
 testdata/Prelude.lc 170:98-170:164  RecordC V1
-testdata/Prelude.lc 170:99-170:109  {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) a) -> RecordC a
-testdata/Prelude.lc 170:110-170:163  'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V9)
+testdata/Prelude.lc 170:99-170:109  {a : List (Tuple2 String Type)} -> 'tuptype ('map (Tuple2 String Type) Type ('snd String Type) a) -> RecordC a
+testdata/Prelude.lc 170:110-170:163  'tuptype ('map (Tuple2 String Type) Type ('snd String Type) V9)
 testdata/Prelude.lc 170:111-170:114  {a} -> {b} -> Tuple2 a b -> b
-testdata/Prelude.lc 170:115-170:162  Tuple2 V16 ('tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V9))
+testdata/Prelude.lc 170:115-170:162  Tuple2 V16 ('tuptype ('map (Tuple2 String Type) Type ('snd String Type) V9))
 testdata/Prelude.lc 170:116-170:128  {a} -> {b} -> a->b
 testdata/Prelude.lc 170:116-170:131  {a} -> V1->a
-testdata/Prelude.lc 170:116-170:158  V0 -> Tuple2 V20 ('tuptype ('map (Tuple2 String Type) Type (\b:Type -> 'snd String Type b) V13))
+testdata/Prelude.lc 170:116-170:158  V0 -> Tuple2 V20 ('tuptype ('map (Tuple2 String Type) Type ('snd String Type) V13))
 testdata/Prelude.lc 170:133-170:158  Type
 testdata/Prelude.lc 170:134-170:135  Type
 testdata/Prelude.lc 170:137-170:144  List Type -> Type
@@ -489,7 +489,7 @@ testdata/Prelude.lc 170:146-170:149  {a} -> {b} -> a->b -> List a -> List b
 testdata/Prelude.lc 170:146-170:153  List (Tuple2 V0 V1) -> List V2
 testdata/Prelude.lc 170:150-170:153  {a} -> {b} -> Tuple2 a b -> b
 testdata/Prelude.lc 170:154-170:156  List (Tuple2 String Type)
-testdata/Prelude.lc 170:159-170:161  'tuptype ('map (Tuple2 String Type) Type (\a:Type -> 'snd String Type a) V4)
+testdata/Prelude.lc 170:159-170:161  'tuptype ('map (Tuple2 String Type) Type ('snd String Type) V4)
 testdata/Prelude.lc 174:1-174:4  Float -> Float -> Float -> VecS Float 4
 testdata/Prelude.lc 174:13-174:15  {a} -> a -> a -> a -> a -> VecS a 4
 testdata/Prelude.lc 174:13-174:17  V5 -> V6 -> V7 -> VecS V8 4
diff --git a/testdata/language-features/adt/adt05.out b/testdata/language-features/adt/adt05.out
index 29167f4f..97b40b5c 100644
--- a/testdata/language-features/adt/adt05.out
+++ b/testdata/language-features/adt/adt05.out
@@ -1 +1 @@
-main
\ No newline at end of file
+main
\ No newline at end of file