From d7b35e4156a499b4a072e34fb4b6cd9b133465cf Mon Sep 17 00:00:00 2001 From: Péter Diviánszky Date: Sat, 7 May 2016 09:34:54 +0200 Subject: introduce let in core (not used yet) --- src/LambdaCube/Compiler/Core.hs | 30 ++++++++++++++++++++++++++---- src/LambdaCube/Compiler/DesugaredSource.hs | 12 ++++++------ src/LambdaCube/Compiler/Infer.hs | 18 +++++++++++------- src/LambdaCube/Compiler/Parser.hs | 4 ++-- src/LambdaCube/Compiler/Statements.hs | 12 ++++++------ 5 files changed, 51 insertions(+), 25 deletions(-) (limited to 'src/LambdaCube/Compiler') diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 273791a7..0a221d2c 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs @@ -148,6 +148,7 @@ data Exp | Pi_ !MaxDB Visibility Exp Exp | Neut Neutral | RHS Exp{-always in hnf-} + | Let_ !MaxDB ExpType Exp data Neutral = Var_ !Int{-De Bruijn index-} @@ -155,7 +156,6 @@ data Neutral | CaseFun__ !MaxDB CaseFunName [Exp] Neutral | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral | Fun_ !MaxDB FunName [Exp]{-given parameters, reversed-} Exp{-unfolded expression, in hnf-} --- | Let_ !MaxDB -------------------------------------------------------------------------------- auxiliary functions and patterns @@ -163,7 +163,10 @@ type Type = Exp data ExpType = ET {expr :: Exp, ty :: Type} deriving (Eq) - +{- +pattern ET a b <- ET_ a b + where ET a b = ET_ a (hnf b) +-} instance Rearrange ExpType where rearrange l f (ET e t) = ET (rearrange l f e) (rearrange l f t) @@ -201,6 +204,13 @@ pattern Lam y <- Lam_ _ y where Lam y = Lam_ (lowerDB (maxDB_ y)) y pattern Pi v x y <- Pi_ _ v x y where Pi v x y = Pi_ (maxDB_ x <> lowerDB (maxDB_ y)) v x y +pattern Let x y <- Let_ _ x y + where Let x y = Let_ (maxDB_ x <> lowerDB (maxDB_ y)) x y + +pattern SubstLet x <- (substLet -> Just x) + +substLet (Let x y) = Just $ subst 0 (expr x) y +substLet _ = Nothing pattern CaseFun a b c = Neut (CaseFun_ a b c) pattern TyCaseFun a b c = Neut (TyCaseFun_ a b c) @@ -306,9 +316,14 @@ mkFun :: FunName -> [Exp] -> Exp -> Exp mkFun f xs e = mkFun_ (foldMap maxDB_ xs) f xs e pattern ReducedN y <- Fun f _ (RHS y) -pattern Reduced y <- Neut (ReducedN y) +pattern Reduced y <- (reduce -> Just y) + +-- TODO: too much hnf call +reduce (Neut (ReducedN y)) = Just $ hnf y +reduce (SubstLet x) = Just $ hnf x +reduce _ = Nothing -hnf (Reduced y) = y +hnf (reduce -> Just y) = y hnf a = a outputType = tTyCon0 FOutput $ error "cs 9" @@ -385,6 +400,7 @@ instance Subst Exp Exp where Con_ md s n as -> Con_ (md <> upDB i dx) s n $ f i <$> as Pi_ md h a b -> Pi_ (md <> upDB i dx) h (f i a) (f (i+1) b) TyCon_ md s as -> TyCon_ (md <> upDB i dx) s $ f i <$> as + Let_ md a b -> Let_ (md <> upDB i dx) (subst_ i dx x a) (f (i+1) b) RHS a -> RHS $ hnf $ f i a instance Rearrange Exp where @@ -396,6 +412,7 @@ instance Rearrange Exp where Con_ md s pn as -> Con_ (upDB_ g i md) s pn $ map (f i) as TyCon_ md s as -> TyCon_ (upDB_ g i md) s $ map (f i) as Neut x -> Neut $ rearrange i g x + Let x y -> Let (rearrange i g x) (rearrange (i+1) g y) RHS x -> RHS $ rearrange i g x instance Rearrange Neutral where @@ -421,6 +438,7 @@ instance Up Exp where TType_ _ -> mempty ELit{} -> mempty Neut x -> foldVar f i x + Let x y -> foldVar f i x <> foldVar f (i+1) y RHS x -> foldVar f i x instance Up Neutral where @@ -445,6 +463,7 @@ instance HasMaxDB Exp where Pi_ c _ _ _ -> c Con_ c _ _ _ -> c TyCon_ c _ _ -> c + Let_ c _ _ -> c TType_ _ -> mempty ELit{} -> mempty @@ -481,6 +500,7 @@ instance ClosedExp Exp where e@TType_{} -> e e@ELit{} -> e Neut a -> Neut $ closedExp a + Let a b -> Let_ mempty a b RHS a -> RHS (closedExp a) instance ClosedExp Neutral where @@ -519,6 +539,7 @@ instance MkDoc Exp where TType -> text "Type" ELit l -> pShow l Neut x -> mkDoc pr x + Let a b -> shLet_ (pShow a) (pShow b) RHS x -> text "_rhs" `DApp` mkDoc pr x showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10) @@ -719,6 +740,7 @@ app_ :: Exp -> Exp -> Exp app_ (Lam x) a = subst 0 a x app_ (Con s n xs) a = if n < conParams s then Con s (n+1) xs else Con s n (xs ++ [a]) app_ (TyCon s xs) a = TyCon s (xs ++ [a]) +app_ (SubstLet f) a = app_ f a app_ (Neut f) a = neutApp f a where neutApp (ReducedN x) a = app_ x a -- ??? diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index d47726d0..325338bf 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs @@ -533,22 +533,22 @@ shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b -------------------------------------------------------------------------------- statement data Stmt - = Let SIName (Maybe SExp) SExp + = StLet SIName (Maybe SExp) SExp | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-} | PrecDef SIName Fixity -pattern Primitive n t = Let n (Just t) (SBuiltin "undefined") +pattern Primitive n t = StLet n (Just t) (SBuiltin "undefined") instance PShow Stmt where pShow stmt = vcat . map DResetFreshNames $ case stmt of Primitive n t -> pure $ shAnn (pShow n) (pShow t) - Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] + StLet n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)] Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs]) PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i instance DeBruijnify SIName Stmt where deBruijnify_ k v = \case - Let sn mt e -> Let sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e) + StLet sn mt e -> StLet sn (deBruijnify_ k v <$> mt) (deBruijnify_ k v e) x -> error $ "deBruijnify @ " ++ ppShow x -------------------------------------------------------------------------------- statement with dependencies @@ -570,7 +570,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes where need = Set.toList $ case s of PrecDef{} -> mempty - Let _ mt e -> foldMap names mt <> names e + StLet _ mt e -> foldMap names mt <> names e Data _ ps t cs -> foldMap (names . snd) ps <> names t <> foldMap (names . snd) cs names = foldName Set.singleton @@ -581,7 +581,7 @@ sortDefs xs = map snValue <$> scc snId snChildren snRevChildren nodes where def = \case PrecDef{} -> mempty - Let n _ _ -> [n] + StLet n _ _ -> [n] Data n _ _ cs -> n: map fst cs -------------------------------------------------------------------------------- module diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index 3b8bdd5a..38269b0e 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs @@ -227,6 +227,9 @@ inferN e s = do 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 + inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType' inferN_ tellTrace = infer where @@ -243,7 +246,7 @@ inferN_ tellTrace = infer where SApp_ si h a b -> infer (EApp1 (si `validate` [sourceInfo a, sourceInfo b]) h te b) a SBind_ si h _ a b -> infer ((if h /= BMeta then CheckType_ (sourceInfo exp) TType else id) $ EBind1 si h te $ (if isPi h then TyType else id) b) a - checkN :: Env -> SExp2 -> Type -> IM m ExpType' + checkN :: Env -> SExp2 -> Type{-hnf-} -> IM m ExpType' checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t checkN_ te (Parens e) t = checkN_ te e t @@ -269,10 +272,10 @@ inferN_ tellTrace = infer where | 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 y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType) + 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) | Pi Hidden a b <- t = do bb <- notHiddenLam e - if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) b + if bb then checkN (EBind2 (BLam Hidden) a te) (up1 e) $ hnf b else infer (CheckType_ (sourceInfo e) t te) e | otherwise = infer (CheckType_ (sourceInfo e) t te) e where @@ -313,15 +316,15 @@ inferN_ tellTrace = infer where _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet EApp1 si h te b - | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x + | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b $ hnf x | Pi Hidden x y <- et, h == Visible -> focus_ (EApp1 mempty Hidden env $ Wildcard $ Wildcard SType) eet -- e b --> e _ b -- | CheckType (Pi Hidden _ _) te' <- te -> error "ok" -- | CheckAppType Hidden _ te' _ <- te -> error "ok" | 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 $ subst 0 (mkELet ln x xt te){-let-} eet{-in-} - CheckIType x te -> checkN te x e + ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet (mkELet ln x xt te){-let-} xt eet{-in-} + CheckIType x te -> checkN te x $ hnf e CheckType_ si t te | hArgs et > hArgs t -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet @@ -461,6 +464,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt 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 (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 ET (RHS x) zt -> RHS $ recheck_ msg te (ET x zt) where checkApps s acc zt f _ t [] @@ -485,7 +489,7 @@ handleStmt = \case t <- inferType n $ trSExp' t_ tellType (sourceInfo n) t addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t - Let n mt t_ -> do + StLet n mt t_ -> do let t__ = maybe id (flip SAnn) mt t_ ET x t <- inferTerm n $ trSExp' $ addFix n t__ tellType (sourceInfo n) t diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index f4ea8489..1d5139b8 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs @@ -131,7 +131,7 @@ mkDesugarInfo ss = DesugarInfo , consMap = Map.fromList $ [(sName cn, Left ((CaseName $ sName t, pars ty), second pars <$> cs)) | Data t ps ty cs <- ss, (cn, ct) <- cs] ++ [(sName t, Right $ pars $ UncurryS ps ty) | Data t ps ty _ <- ss] --- ++ [(t, Right $ length xs) | Let (_, t) _ (Just ty) xs _ <- ss] +-- ++ [(t, Right $ length xs) | StLet (_, t) _ (Just ty) xs _ <- ss] ++ [("'Type", Right 0)] , definedSet = Set.singleton "'Type" <> foldMap defined ss } @@ -139,7 +139,7 @@ mkDesugarInfo ss = DesugarInfo pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo defined = \case - Let sn _ _ -> Set.singleton $ sName sn + StLet sn _ _ -> Set.singleton $ sName sn Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs PrecDef{} -> mempty diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs index 42f02b07..1ce2beb6 100644 --- a/src/LambdaCube/Compiler/Statements.hs +++ b/src/LambdaCube/Compiler/Statements.hs @@ -49,7 +49,7 @@ mkLets_ mkLet = mkLets' mkLet . concatMap desugarMutual . sortDefs mkLets' mkLet = f where f [] e = e - f (Let 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 (addFix n x)) (deBruijnify [n] $ f ds e) f (PrecDef{}: ds) e = f ds e f (x: ds) e = error $ "mkLets: " ++ ppShow x @@ -57,7 +57,7 @@ addFix n x | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x) | otherwise = x -addFix' (Let n nt nd) = Let n nt $ addFix n nd +addFix' (StLet n nt nd) = StLet n nt $ addFix n nd addFix' x = x type DefinedSet = Set.Set SName @@ -97,7 +97,7 @@ compileStmt compilegt ds = \case -- , let ts = fst $ getParamsS $ up1 t , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0 | Instance n' i cstrs alts <- ds, n' == n - , Let m' ~Nothing e <- alts, m' == m + , StLet m' ~Nothing e <- alts, m' == m , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")] -- , let ic = patVars i ] @@ -113,7 +113,7 @@ compileStmt compilegt ds = \case | 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 [Let n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) cf] + return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == 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,7 +134,7 @@ desugarValueDef p e = sequence dns = reverse $ getPVars p n = mangleNames dns -getLet (Let x Nothing (SRHS dx)) = Just (x, dx) +getLet (StLet x Nothing (SRHS dx)) = Just (x, dx) getLet _ = Nothing fst' (x, _) = x -- TODO @@ -144,7 +144,7 @@ desugarMutual [x] = [x] desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy) return $ - Let xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss + StLet xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss where xy = mangleNames ns desugarMutual xs = error "desugarMutual" -- cgit v1.2.3