From e4725c07ee3e7e3fc010df418d16f37c39b0af0f Mon Sep 17 00:00:00 2001 From: Péter Diviánszky Date: Wed, 11 May 2016 20:57:07 +0200 Subject: mutual function definitions --- src/LambdaCube/Compiler/Core.hs | 57 +++++++++++++++++++++--------- src/LambdaCube/Compiler/CoreToIR.hs | 19 ++++++++-- src/LambdaCube/Compiler/DesugaredSource.hs | 3 ++ src/LambdaCube/Compiler/Infer.hs | 44 ++++++++++++----------- src/LambdaCube/Compiler/Parser.hs | 14 ++++---- src/LambdaCube/Compiler/Pretty.hs | 1 + src/LambdaCube/Compiler/Statements.hs | 41 ++++++++++----------- 7 files changed, 113 insertions(+), 66 deletions(-) (limited to 'src') diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 27bd6372..487cc4cc 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs @@ -35,7 +35,7 @@ data CaseFunName = CaseFunName FName Type Int{-num of parameters-} data TyCaseFunName = TyCaseFunName FName Type data FunDef - = DeltaDef !Int{-arity-} ([Exp] -> Exp) + = DeltaDef !Int{-arity-} (FreeVars -> [Exp] -> Exp) | NoDef | ExpDef Exp @@ -245,7 +245,7 @@ mkOrdering x = case x of conTypeName :: ConName -> TyConName conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n -mkFun_ _ (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f $ reverse as +mkFun_ md (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f md $ reverse as mkFun_ md f xs y = Neut $ Fun_ md f xs $ hnf y mkFun :: FunName -> [Exp] -> Exp -> Exp @@ -293,6 +293,7 @@ down t x | usedVar t x = Nothing | otherwise = Just $ subst_ t mempty (error $ "impossible: down" ++ ppShow (t,x, getFreeVars x) :: Exp) x instance Eq Exp where + Neut a == Neut a' = a == a' -- try to compare by structure before reduction Reduced a == a' = a == a' a == Reduced a' = a == a' Lam a == Lam a' = a == a' @@ -301,12 +302,11 @@ instance Eq Exp where TyCon a b == TyCon a' b' = (a, b) == (a', b') TType_ f == TType_ f' = f == f' ELit l == ELit l' = l == l' - Neut a == Neut a' = a == a' RHS a == RHS a' = a == a' _ == _ = False instance Eq Neutral where - Fun f a _ == Fun f' a' _ = (f, a) == (f', a') + Fun f a _ == Fun f' a' _ = (f, a) == (f', a') -- try to compare by structure before reduction ReducedN a == a' = a == Neut a' a == ReducedN a' = Neut a == a' CaseFun_ a b c == CaseFun_ a' b' c' = (a, b, c) == (a', b', c') @@ -323,7 +323,7 @@ instance Subst Exp Exp where substNeut e | dbGE i e = Neut e substNeut e = case e of Var_ k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x - CaseFun_ s as n -> evalCaseFun s (f i <$> as) (substNeut n) + CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n) TyCaseFun_ s as n -> evalTyCaseFun s (f i <$> as) (substNeut n) App_ a b -> app_ (substNeut a) (f i b) Fun_ md fn xs v -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v @@ -426,14 +426,26 @@ showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10) f _ 3 = "rd" f _ _ = "th" +pattern FFix f <- Fun (FunName FprimFix _ _ _) [f, _] _ + +getFixLam (Lam (Neut (Fun s@(FunName _ loc _ _) xs _))) + | loc > 0 + , (h, v) <- splitAt loc $ reverse xs + , Neut (Var_ 0) <- last h + = Just (s, v) +getFixLam _ = Nothing + instance MkDoc Neutral where mkDoc pr@(reduce, body) = \case CstrT' t a b -> shCstr (mkDoc pr a) (mkDoc pr (ET b t)) - Fun (FunName _ _ (ExpDef d) _) xs _ | body -> mkDoc (reduce, False) (foldl app_ d xs) - Fun (FunName _ _ (DeltaDef _ d) _) xs _ | body -> text "<>" - Fun (FunName _ _ NoDef _) xs _ | body -> text "<>" + Fun (FunName _ _ (ExpDef d) _) xs _ | body -> mkDoc (reduce, False) (foldl app_ d $ reverse xs) + FFix (getFixLam -> Just (s, xs)) | not body -> foldl DApp (pShow s) $ mkDoc pr <$> xs + FFix f {- | body -} -> foldl DApp "primFix" [{-pShow t -}"_", mkDoc pr f] + Fun (FunName _ _ (DeltaDef n _) _) _ _ | body -> text $ "<>" + Fun (FunName _ _ NoDef _) _ _ | body -> "<>" ReducedN a | reduce -> mkDoc pr a - Fun s xs _ -> foldl DApp (pShow s) (mkDoc pr <$> reverse xs) + Fun s@(FunName _ loc _ _) xs _ -> foldl DApp ({-foldl DHApp (-}pShow s{-) h-}) v + where (h, v) = splitAt loc $ mkDoc pr <$> reverse xs Var_ k -> shVar k App_ a b -> mkDoc pr a `DApp` mkDoc pr b CaseFun_ s@(CaseFunName _ _ p) xs n | body -> text $ "<>" @@ -441,6 +453,7 @@ instance MkDoc Neutral where TyCaseFun_ _ _ _ | body -> text "<>" TyCaseFun_ s [m, t, f] n -> foldl DApp (pShow s) (mkDoc pr <$> [m, t, Neut n, f]) TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun" + _ -> "()" -------------------------------------------------------------------------------- reduction @@ -455,9 +468,19 @@ instance MkDoc Neutral where -} pattern FunName' a t <- FunName a _ _ t - where FunName' a t = fn - where - fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t)) $ getFunDef t a $ \xs -> Neut $ Fun fn (reverse xs) delta) t + where FunName' a t = mkFunDef a t + + +mkFunDef a@(show -> "primFix") t = fn + where + fn = FunName a 0 (DeltaDef (length $ fst $ getParams t) fx) t + fx s xs = Neut $ Fun_ s fn (reverse xs) $ case xs of + _: f: _ -> RHS x where x = f `app_` Neut (Fun_ s fn (reverse xs) $ RHS x) + _ -> delta + +mkFunDef a t = fn + where + fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t) . const) $ getFunDef t a $ \xs -> Neut $ Fun fn (reverse xs) delta) t getFunDef t s f = case show s of "'EqCT" -> Just $ \case (t: a: b: _) -> cstr t a b @@ -541,15 +564,17 @@ getFunDef t s f = case show s of modF x y = x - fromIntegral (floor (x / y)) * y -evalCaseFun a ps (Con n@(ConName _ i _) _ vs) +evalCaseFun _ a ps (Con n@(ConName _ i _) _ vs) | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs | otherwise = error "evcf" where xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps xs !!! i = xs !! i -evalCaseFun a b (Reduced c) = evalCaseFun a b c -evalCaseFun a b (Neut c) = CaseFun a b c -evalCaseFun a b x = error $ "evalCaseFun: " ++ ppShow (a, x) +evalCaseFun fs a b (Reduced c) = evalCaseFun fs a b c +evalCaseFun fs a b (Neut c) = Neut $ CaseFun__ fs a b c +evalCaseFun _ a b x = error $ "evalCaseFun: " ++ ppShow (a, x) + +evalCaseFun' a b c = evalCaseFun (getFreeVars c <> foldMap getFreeVars b) a b c evalTyCaseFun a b (Reduced c) = evalTyCaseFun a b c evalTyCaseFun a b (Neut c) = TyCaseFun a b c diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs index d24a7b11..353560cd 100644 --- a/src/LambdaCube/Compiler/CoreToIR.hs +++ b/src/LambdaCube/Compiler/CoreToIR.hs @@ -865,7 +865,7 @@ mkLam _ = Nothing mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs) mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs) -mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ 0 _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs) +mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ loc _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, drop loc $ chain vs (nType s) xs) mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n]) mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f]) mkCon _ = Nothing @@ -878,15 +878,28 @@ removeRHS 0 (I.RHS x) = Just x removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x removeRHS _ _ = Nothing -mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) 0 (I.ExpDef def_) nt) xs I.RHS{})) ty vs) +mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs) | Just def <- removeRHS (length xs) def_ , all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n = Just (untick n +++ intercalate "_" (filter (/="TT") $ map (filter isAlphaNum . plainShow) hs), toExp $ I.ET (foldl I.app_ def hs) (foldl I.appTy nt hs), tyOf r, xs') where a +++ [] = a a +++ b = a ++ "_" ++ b - (map (expOf . snd) -> hs, map snd -> xs') = span ((==Hidden) . fst) $ chain' vs nt $ reverse xs + (map (expOf . snd) -> hs, map snd -> xs') = splitAt loc $ chain' vs nt $ reverse xs validChar = isAlphaNum +{- +mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs) + | Just def <- removeRHS (length xs) def_ + , all validChar n + = tracePShow (text n, reverse xs, supType . tyOf <$> (r: xs')) Nothing + where + a +++ [] = a + a +++ b = a ++ "_" ++ b + (map (expOf . snd) -> hs, map snd -> xs') = splitAt loc $ chain' vs nt $ reverse xs + validChar = isAlphaNum +mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs) + = tracePShow (text n, take loc $ reverse xs) Nothing +-} mkFunc _ = Nothing chain vs t@(I.Pi Hidden at y) (a: as) = chain vs (I.appTy t a) as diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index e83eb0ea..06849849 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs @@ -269,6 +269,9 @@ data SExp' a | STyped a deriving (Eq) +sLHS _ (SRHS x) = x +sLHS n x = SLHS n x + type SExp = SExp' Void data Binder diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 444dd1b9..089392d1 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs @@ -36,7 +36,6 @@ import LambdaCube.Compiler.Utils import LambdaCube.Compiler.DeBruijn import LambdaCube.Compiler.Pretty hiding (braces, parens) import LambdaCube.Compiler.DesugaredSource hiding (getList) -import LambdaCube.Compiler.Statements (addFix) import LambdaCube.Compiler.Core import LambdaCube.Compiler.InferMonad @@ -49,20 +48,15 @@ varType err n_ env = f n_ env where f n (ELet2 _ (ET x t) es) = if n == 0 then (BLam Visible{-??-}, up 1 t) else second (up 1) $ f (n-1) es f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e -mkELet n x xt env = term +mkELet n x xt env = mkFun fn (Var <$> reverse vs) x where - vs = nub . concat $ grow [] mempty $ free x <> free xt fn = FunName (mkFName n) (length vs) (ExpDef $ foldr addLam x vs) (foldr addPi xt vs) - term = mkFun fn (Var <$> reverse vs) $ getFix x 0 - - getFix (Lam_ db z) i = Lam_ db $ getFix z (i+1) - getFix (DFun FprimFix _ [_, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f - getFix x _ = x - addLam v x = Lam $ rMove v 0 x addPi v x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v 0 x + vs = nub . concat $ grow [] mempty $ free x <> free xt + -- TODO: avoid infinite loop if variable types refer each-other mutually grow accu acc s | Set.null s = accu @@ -101,7 +95,8 @@ envDoc x m = case x of CheckIType t ts -> envDoc ts $ shAnn m (text "??") -- mkDoc ts' t -- CheckSame t ts -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m - ERHS ts -> envDoc ts $ shApp Visible (text "rhs") m + ERHS ts -> envDoc ts $ shApp Visible "rhs" m + ELHS n ts -> envDoc ts $ shApp Visible ("lhs" `DApp` pShow n) m x -> error $ "envDoc: " ++ ppShow x instance MkDoc a => MkDoc (CEnv a) where @@ -162,6 +157,7 @@ data Env | ELet2 SIName ExpType Env | EGlobal | ERHS Env + | ELHS SIName Env | EAssign Int ExpType Env | CheckType_ SI Type Env @@ -185,6 +181,7 @@ parent = \case -- CheckSame _ x -> Right x CheckAppType _ _ _ x _ -> Right x ERHS x -> Right x + ELHS _ x -> Right x EGlobal -> Left () -------------------------------------------------------------------------------- simple typing @@ -230,6 +227,8 @@ substTo i x = subst i x . up1_ (i+1) mkLet x xt y = subst 0 x y --mkLet x xt (ET y yt) = ET (Let (ET x xt) y) yt +ET a at `etApp` e = ET (app_ a e) (appTy at e) + inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType' inferN_ tellTrace = infer where @@ -238,7 +237,7 @@ inferN_ tellTrace = infer where Parens x -> infer te x SAnn x t -> checkN (CheckIType x te) t TType SRHS x -> infer (ERHS te) x - SLHS n x -> infer te x + SLHS n x -> infer (ELHS n te) x SVar sn i -> focusTell te exp $ ET (Var i) $ snd $ varType "C2" i te SLit si l -> focusTell te exp $ ET (ELit l) (nType l) STyped et -> focusTell' te exp et @@ -252,6 +251,9 @@ inferN_ tellTrace = infer where checkN_ te (Parens e) t = checkN_ te e t checkN_ te e t + | SBuiltin "primFix" `SAppV` (SLam Visible _ f) <- e = do + pf <- getDef te mempty "primFix" + checkN (EBind2 (BLam Visible) t $ EApp2 mempty Visible (pf `etApp` t) te) f $ up 1 t | x@(SGlobal (sName -> MatchName n)) `SAppV` SLamV (Wildcard _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e = infer te $ x `SAppV` SLam Visible SType (STyped (ET (subst (v+1) (Var 0) $ up 1 t) TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b -- temporal hack @@ -269,9 +271,9 @@ inferN_ tellTrace = infer where = infer te $ x `SAppV` SLamV (SLamV (STyped (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` SVar siv v -} | SRHS x <- e = checkN (ERHS te) x t - | SLHS n x <- e = checkN te x t + | SLHS n x <- e = checkN (ELHS n 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 + | SLam h a b <- e, Pi h' x y <- t, h == h' = do -- tellType e t let same = checkSame te a x if same then checkN (EBind2 (BLam h) x te) b $ hnf y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType) @@ -311,6 +313,7 @@ inferN_ tellTrace = infer where focus_ :: Env -> ExpType -> IM m ExpType' focus_ env eet@(ET e et) = tellTrace "focus" (showEnvExp env eet) $ case env of ERHS te -> focus_ te (ET (RHS $ hnf e) et) + ELHS n te -> focus_ te (ET (mkELet n e et te) et) -- CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet CheckAppType si h t te b -- App1 h (CheckType t te) b | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of @@ -325,7 +328,7 @@ inferN_ tellTrace = infer where | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b) where cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y) - ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet (mkELet ln x xt te){-let-} xt eet{-in-} + ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet x{-let-} xt eet{-in-} CheckIType x te -> checkN te x $ hnf e CheckType_ si t te | hArgs et > hArgs t @@ -333,7 +336,7 @@ inferN_ tellTrace = infer where | hArgs et < hArgs t, Pi Hidden t1 t2 <- t -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet | otherwise -> focus_ (EBind2_ si BMeta (cstr_ TType t et) te) $ up 1 eet - EApp2 si h (ET a at) te -> focusTell te si $ ET (app_ a e) (appTy at e) -- h?? + EApp2 si h a te -> focusTell te si $ a `etApp` e -- h?? EBind1 si h te b -> infer (EBind2_ (sourceInfo b) h e te) b EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet EBind2_ si (BPi h) a te -> focusTell te si $ ET (Pi h a e) TType @@ -344,6 +347,7 @@ inferN_ tellTrace = infer where ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-} EBind2_ si BMeta tt_ te | ERHS te' <- te -> refocus (ERHS $ EBind2_ si BMeta tt_ te') eet + | ELHS n te' <- te -> refocus (ELHS n $ EBind2_ si BMeta tt_ te') eet | Unit <- tt -> refocus te $ subst 0 TT eet | Empty msg <- tt -> throwError' $ ETypeError (text msg) si | CW (hnf -> T2 x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te @@ -377,6 +381,7 @@ inferN_ tellTrace = infer where EAssign i b te -> case te of ERHS te' -> refocus' (ERHS $ EAssign i b te') eet + ELHS n te' -> refocus' (ELHS n $ EAssign i b te') eet EBind2_ si h x te' | i > 0, Just b' <- down 0 b -> refocus' (EBind2_ si h (subst (i-1) (expr b') x) (EAssign (i-1) b' te')) eet ELet2 le x te' | i > 0, Just b' <- down 0 b @@ -413,7 +418,6 @@ inferN_ tellTrace = infer where _ -> case eet of MEnd x -> throwError' $ ErrorMsg $ "focus todo:" <+> pShow x _ -> case env of --- EBind2 h _ _ -> throwError' $ ErrorMsg $ "focus checkMetas" <+> pShow h _ -> throwError' $ ErrorMsg $ "focus checkMetas:" <$$> pShow env <$$> "---" <$$> pShow eet where refocus_ :: (Env -> CEnv ExpType -> IM m ExpType') -> Env -> CEnv ExpType -> IM m ExpType' @@ -463,7 +467,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b] ET (Con_ md s n as) zt -> checkApps (ppShow s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as ET (TyCon_ md s as) zt -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as - ET (CaseFun s@(CaseFunName _ t pars) as n) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) + ET (Neut (CaseFun__ fs s@(CaseFunName _ t pars) as n)) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun fs s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n]) ET (TyCaseFun s [m, t, f] n) zt -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f] ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a -- TODO: recheck x ET (Let (ET x xt) y) zt -> Let (recheck'' "let" te $ ET x xt) $ recheck_ "let_in" te $ ET y (Pi Visible xt $ up1 zt) -- TODO @@ -493,9 +497,9 @@ handleStmt = \case addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t StLet n mt t_ -> do let t__ = maybe id (flip SAnn) mt t_ - ET x t <- inferTerm n $ trSExp' $ addFix n t__ + ET x t <- inferTerm n $ trSExp' t__ tellType (sourceInfo n) t - addToEnv n (ET (mkELet n x t EGlobal) t) + addToEnv n (ET x t) {- -- hack when (snd (getParams t) == TType) $ do let ps' = fst $ getParams t @@ -551,7 +555,7 @@ handleStmt = \case ) return (e1, es, tcn, cfn, ct, cons) - e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs)) ct + e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (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')) diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 79975251..7ca3d5cb 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs @@ -249,7 +249,7 @@ parseTermProj = level parseTermAtom $ \t -> parseTermAtom = mkLit <$> try_ "literal" parseLit <|> Wildcard (Wildcard SType) <$ reserved "_" - <|> mkLets <$ reserved "let" <*> parseDefs <* reserved "in" <*> setR parseTermLam + <|> mkLets <$ reserved "let" <*> parseDefs sLHS <* reserved "in" <*> setR parseTermLam <|> SGlobal <$> lowerCase <|> SGlobal <$> upperCase_ <|> braces (mkRecord <$> commaSep ((,) <$> lowerCase <* symbol ":" <*> setR parseTermLam)) @@ -434,12 +434,12 @@ parseDef = option {-open type family-}[TypeFamily x $ UncurryS ts t] $ do cs <- (reserved "where" >>) $ identation True $ funAltDef Nothing $ mfilter (== x) upperCase -- closed type family desugared here - runCheck $ fmap Stmt <$> compileStmt (compileGuardTrees id . const Nothing) [TypeAnn x $ UncurryS ts t] cs + runCheck $ fmap Stmt <$> compileStmt SLHS (compileGuardTrees id . const Nothing) [TypeAnn x $ UncurryS ts t] cs <|> pure <$ reserved "instance" <*> funAltDef Nothing upperCase <|> do x <- upperCase (nps, ts) <- telescope $ Just (Wildcard SType) rhs <- deBruijnify nps <$ reservedOp "=" <*> setR parseTermLam - runCheck $ fmap Stmt <$> compileStmt (compileGuardTrees id . const Nothing) + runCheck $ fmap Stmt <$> compileStmt SLHS (compileGuardTrees id . const Nothing) [{-TypeAnn x $ UncurryS ts $ SType-}{-todo-}] [funAlt' x ts (map PVarSimp $ reverse nps) $ noGuards rhs] <|> do try_ "typed ident" $ map (uncurry TypeAnn) <$> typedIds addForalls' [] @@ -465,10 +465,10 @@ parseDef = parseRHS :: String -> BodyParser GuardTrees parseRHS tok = do - mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs) + mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs sLHS) <|> do rhs <- reservedOp tok *> setR parseTermLam - f <- option id $ mkLets <$ reserved "where" <*> parseDefs + f <- option id $ mkLets <$ reserved "where" <*> parseDefs sLHS noGuards <$> trackSI (pure $ f rhs) where guard = do @@ -482,7 +482,7 @@ parseRHS tok = do mkGuards gs wh = mkLets_ lLet wh $ mconcat [foldr (uncurry guardNode') (noGuards e) ge | (ge, e) <- gs] -parseDefs = identation True parseDef >>= runCheck . compileStmt' . concat +parseDefs lhs = identation True parseDef >>= runCheck . compileStmt'_ lhs SRHS SRHS . concat funAltDef parseOpName parseName = do (n, (fee, tss)) <- @@ -555,7 +555,7 @@ parseModule = do { extensions = exts , moduleImports = [(SIName mempty "Prelude", ImportAllBut []) | NoImplicitPrelude `notElem` exts] ++ idefs , moduleExports = join $ snd <$> header - , definitions = \ge -> runParse (parseDefs <* eof) (env { desugarInfo = ge }, st) + , definitions = \ge -> runParse (parseDefs SLHS <* eof) (env { desugarInfo = ge }, st) } parseLC :: FileInfo -> Either ParseError Module diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs index e2ebb5e4..204e4893 100644 --- a/src/LambdaCube/Compiler/Pretty.hs +++ b/src/LambdaCube/Compiler/Pretty.hs @@ -320,6 +320,7 @@ infixl 4 `DApp` pattern DAt x = DGlue (InfixR 20) (DText "@") x pattern DApp x y = DSep (InfixL 10) x y +pattern DHApp x y = DSep (InfixL 10) x (DAt y) pattern DSemi x y = DOp ";" (InfixR (-19)) x y pattern DArr_ s x y = DOp s (InfixR (-1)) x y -- -> => . pattern DCstr x y = DOp "~" (Infix (-2)) x y diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs index 178e5505..9d48ffc2 100644 --- a/src/LambdaCube/Compiler/Statements.hs +++ b/src/LambdaCube/Compiler/Statements.hs @@ -49,17 +49,10 @@ mkLets_ mkLet = mkLets' mkLet . concatMap desugarMutual . sortDefs mkLets' mkLet = f where f [] e = e - f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e) + f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt x) (deBruijnify [n] $ f ds e) f (PrecDef{}: ds) e = f ds e f (x: ds) e = error $ "mkLets: " ++ ppShow x -addFix n x - | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x) - | otherwise = x - -addFix' (StLet n nt nd) = StLet n nt $ addFix n nd -addFix' x = x - type DefinedSet = Set.Set SName addForalls :: DefinedSet -> SExp -> SExp @@ -75,14 +68,14 @@ addForalls defined x = foldl f x [v | v@(sName -> vh:_) <- reverse $ names x, sN ------------------------------------------------------------------------ -compileStmt' = compileStmt'_ SRHS SRHS +compileStmt' = compileStmt'_ SLHS SRHS SRHS -compileStmt'_ ulend lend ds = fmap concat . sequence $ map (compileStmt (\si vt -> compileGuardTree ulend lend (Just si) vt . mconcat) ds) $ groupBy h ds where +compileStmt'_ lhs ulend lend ds = fmap concat . sequence $ map (compileStmt lhs (\si vt -> compileGuardTree ulend lend (Just si) vt . mconcat) ds) $ groupBy h ds where h (FunAlt n _ _) (FunAlt m _ _) = m == n h _ _ = False -compileStmt :: MonadWriter [ParseCheck] m => (SIName -> [(Visibility, SExp)] -> [GuardTrees] -> m SExp) -> [PreStmt] -> [PreStmt] -> m [Stmt] -compileStmt compilegt ds = \case +--compileStmt :: MonadWriter [ParseCheck] m => (SIName -> [(Visibility, SExp)] -> [GuardTrees] -> m SExp) -> [PreStmt] -> [PreStmt] -> m [Stmt] +compileStmt lhs compilegt ds = \case [Instance{}] -> return [] [Class n ps ms] -> do cd <- compileStmt' $ @@ -90,7 +83,7 @@ compileStmt compilegt ds = \case ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'CUnit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'CEmpty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})] cds <- sequence - [ compileStmt'_ SRHS SRHS{-id-} + [ compileStmt'_ SLHS SRHS SRHS{-id-} $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (SCW $ foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t) : as | (m, t) <- ms @@ -106,14 +99,14 @@ compileStmt compilegt ds = \case [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]] tf@[TypeFamily n t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of [] -> return [Primitive n t] - alts -> compileStmt compileGuardTrees' [TypeAnn n t] alts + alts -> compileStmt lhs compileGuardTrees' [TypeAnn n t] alts fs@(FunAlt n vs _: _) -> case groupBy ((==) `on` fst) [(length vs, n) | FunAlt n vs _ <- fs] of [gs@((num, _): _)] | num == 0 && length gs > 1 -> fail $ "redefined " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd <$> gs) | n `elem` [n' | TypeFamily n' _ <- ds] -> return [] | otherwise -> do cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs] - return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ SLHS n cf] + return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ lhs n cf] fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs) [Stmt x] -> return [x] where @@ -134,21 +127,29 @@ desugarValueDef p e = sequence dns = reverse $ getPVars p n = mangleNames dns -getLet (StLet x Nothing (SLHS _ (SRHS dx))) = Just (x, dx) +getLet (StLet x mt dx) = Just (x, mt, dx) getLet _ = Nothing fst' (x, _) = x -- TODO desugarMutual :: {-MonadWriter [ParseCheck] m => -} [Stmt] -> [Stmt] -desugarMutual [x] = [x] -desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do - ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) +desugarMutual [x@Primitive{}] = [x] +desugarMutual [x@Data{}] = [x] +desugarMutual [x@PrecDef{}] = [x] +desugarMutual [StLet n nt nd] = [StLet n nt $ addFix n nt nd] +desugarMutual (traverse getLet -> Just (unzip3 -> (ns, ts, ds))) = fst' $ runWriter $ do + ss <- compileStmt'_ sLHS SRHS SRHS =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) return $ - StLet xy Nothing (addFix xy $ SLHS xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss + StLet xy ty (addFix xy ty $ mkLets' SLet ss $ foldr HCons HNil ds) : ss where + ty = Nothing -- TODO: Just $ HList $ foldr BCons BNil $ const (Wildcard SType) <$> ts xy = mangleNames ns desugarMutual xs = error "desugarMutual" +addFix n nt x + | usedS n x = SBuiltin "primFix" `SAppV` SLam Visible (maybe (Wildcard SType) id nt) (deBruijnify [n] x) + | otherwise = x + mangleNames xs = SIName (foldMap sourceInfo xs) $ "_" ++ intercalate "_" (sName <$> xs) -- cgit v1.2.3