From e4417dcd4679da9c6b18c02ff667199c572bed89 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Tue, 22 Apr 2008 04:52:44 +0000 Subject: [PATCH 1/1] Improve External Core syntax for newtypes I was confused by the newtype eta-contraction trick before. Newtype declarations are much less redundant now. --- compiler/coreSyn/ExternalCore.lhs | 5 +---- compiler/coreSyn/MkExternalCore.lhs | 20 +++-------------- compiler/coreSyn/PprExternalCore.lhs | 22 +++++------------- utils/ext-core/Check.hs | 41 +++++++++++++++++++++------------- utils/ext-core/Core.hs | 9 ++++---- utils/ext-core/ParsecParser.hs | 20 ++++------------- utils/ext-core/Printer.hs | 12 ++++------ 7 files changed, 48 insertions(+), 81 deletions(-) diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs index d3b6e3a..a326a54 100644 --- a/compiler/coreSyn/ExternalCore.lhs +++ b/compiler/coreSyn/ExternalCore.lhs @@ -10,15 +10,12 @@ data Module data Tdef = Data (Qual Tcon) [Tbind] [Cdef] - | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty) + | Newtype (Qual Tcon) (Qual Tcon) [Tbind] (Maybe Ty) data Cdef = Constr (Qual Dcon) [Tbind] [Ty] | GadtConstr (Qual Dcon) Ty --- Newtype coercion -type Axiom = (Qual Tcon, [Tbind], Kind) - data Vdefg = Rec [Vdef] | Nonrec Vdef diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs index ba0c198..99ea425 100644 --- a/compiler/coreSyn/MkExternalCore.lhs +++ b/compiler/coreSyn/MkExternalCore.lhs @@ -84,14 +84,12 @@ collect_tdefs tcon tdefs | isAlgTyCon tcon = tdef: tdefs where tdef | isNewTyCon tcon = - C.Newtype (qtc tcon) (map make_tbind tyvars) + C.Newtype (qtc tcon) (case newTyConCo_maybe tcon of - Just co -> (qtc co, - map make_tbind vs, - make_kind (mkCoKind l r)) - where (vs,l,r) = coercionAxiom co + Just co -> qtc co Nothing -> pprPanic ("MkExternalCore: newtype tcon\ should have a coercion: ") (ppr tcon)) + (map make_tbind tyvars) repclause | otherwise = C.Data (qtc tcon) (map make_tbind tyvars) @@ -99,18 +97,6 @@ collect_tdefs tcon tdefs where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing | otherwise = Just (make_ty (snd (newTyConRhs tcon))) tyvars = tyConTyVars tcon - coercionAxiom co = - case isCoercionTyCon_maybe co of - -- See Note [Newtype coercions] in - -- types/TyCon - Just (arity,coKindFun) | (l,r) <- (coKindFun $ map mkTyVarTy vs) -> - -- Here we eta-expand the newtype coercion, - -- which makes the ext-core typechecker somewhat simpler. - (tyvars,mkAppTys l extraVs,mkAppTys r extraVs) - where (vs, extraVs) = (take arity tyvars, - map mkTyVarTy $ drop arity tyvars) - Nothing -> pprPanic "MkExternalCore: coercion tcon lacks a kind fun" - (ppr tcon) collect_tdefs _ tdefs = tdefs diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs index fb4fc45..c34f7b8 100644 --- a/compiler/coreSyn/PprExternalCore.lhs +++ b/compiler/coreSyn/PprExternalCore.lhs @@ -54,22 +54,12 @@ ptdef (Data tcon tbinds cdefs) = (text "%data" <+> pqname tcon <+> (hsep (map ptbind tbinds)) <+> char '=') $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs))))) -ptdef (Newtype tcon tbinds (coercion,tbs,k) rep) = --- TODO: I think this is kind of redundant now. --- Here we take apart the newtype tycon in order to get the newtype coercion, --- which needs to be represented in the External Core file because it's not --- straightforward to derive its definition from the newtype declaration alone. --- At the same time, we need the newtype decl to declare the tycon itself. --- Sigh. - text "%newtype" <+> pqname tcon <+> (hsep (map ptbind tbinds)) - $$ indent (axiomclause $$ repclause) - where axiomclause = char '^' - <+> parens (pqname coercion <+> (hsep (map ptbind tbs)) - <+> text "::" - <+> pkind k) - repclause = case rep of - Just ty -> char '=' <+> pty ty - Nothing -> empty +ptdef (Newtype tcon coercion tbinds rep) = + text "%newtype" <+> pqname tcon <+> pqname coercion + <+> (hsep (map ptbind tbinds)) $$ indent repclause + where repclause = case rep of + Just ty -> char '=' <+> pty ty + Nothing -> empty pcdef :: Cdef -> Doc diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index cab3e62..af3bb3c 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -124,13 +124,12 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef tcenv' <- extendM NotTv tcenv (c, Kind k) return (tcenv',tsenv) where k = foldr Karrow Klifted (map snd tbs) - ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = + ch (Newtype (m,c) coVar tbs rhs) = do mn <- getMname requireModulesEq m mn "newtype declaration" tdef False tcenv' <- extendM NotTv tcenv (c, Kind k) -- add newtype axiom to env - tcenv'' <- extendM NotTv tcenv' - (coercion, Coercion $ DefinedCoercion cTbs coercionKind) + tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs tsenv' <- case rhs of Nothing -> return tsenv Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep)) @@ -142,15 +141,30 @@ processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef where ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv) where k = foldr Karrow Klifted (map snd tbs) - ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = + ch (Newtype tc@(_,c) coercion tbs rhs) = let tcenv' = eextend tcenv (c, Kind k) -- add newtype axiom to env - tcenv'' = eextend tcenv' - (coercion, Coercion $ DefinedCoercion cTbs coercionKind) + tcenv'' = case rhs of + Just rep -> + eextend tcenv' + (snd coercion, Coercion $ DefinedCoercion tbs + (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep)) + Nothing -> tcenv' tsenv' = maybe tsenv (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in (tcenv'', tsenv') where k = foldr Karrow Klifted (map snd tbs) + +envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Maybe Ty + -> CheckResult Tcenv +envPlusNewtype tcenv tyCon coVar tbs rhs = + case rhs of + Nothing -> return tcenv + Just rep -> extendM NotTv tcenv + (snd coVar, Coercion $ DefinedCoercion tbs + (foldl Tapp (Tcon tyCon) + (map Tvar (fst (unzip tbs))), + rep)) checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv checkTdef tcenv cenv = ch @@ -173,17 +187,12 @@ checkTdef tcenv cenv = ch (foldr tArrow (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) = + ch (tdef@(Newtype tc _ tbs (Just t))) = do tvenv <- foldM (extendM Tv) eempty tbs - k <- checkTy (tcenv,tvenv) t - -- Makes sure GHC is eta-expanding things properly - require (length tbs == length coTbs) $ - ("Arity mismatch between newtycon and newtype coercion: " - ++ show tdef) - require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef) - axiomTvenv <- foldM (extendM Tv) eempty coTbs - kLhs <- checkTy (tcenv,axiomTvenv) coLhs - kRhs <- checkTy (tcenv,axiomTvenv) coRhs + kRhs <- checkTy (tcenv,tvenv) t + require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef) + kLhs <- checkTy (tcenv,tvenv) + (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs)))) require (kLhs `eqKind` kRhs) ("Kind mismatch in newtype axiom types: " ++ show tdef ++ " kinds: " ++ diff --git a/utils/ext-core/Core.hs b/utils/ext-core/Core.hs index 66270cd..0fb48b8 100644 --- a/utils/ext-core/Core.hs +++ b/utils/ext-core/Core.hs @@ -9,14 +9,15 @@ data Module data Tdef = Data (Qual Tcon) [Tbind] [Cdef] - | Newtype (Qual Tcon) [Tbind] Axiom (Maybe Ty) + -- type constructor; coercion name; type arguments; type rep + -- If we have: (Newtype tc co tbs (Just t)) + -- there is an implicit axiom: + -- co tbs :: tc tbs :=: t + | Newtype (Qual Tcon) (Qual Tcon) [Tbind] (Maybe Ty) data Cdef = Constr (Qual Dcon) [Tbind] [Ty] --- Newtype coercion -type Axiom = (Qual Tcon, [Tbind], (Ty,Ty)) - data Vdefg = Rec [Vdef] | Nonrec Vdef diff --git a/utils/ext-core/ParsecParser.hs b/utils/ext-core/ParsecParser.hs index 42e21e9..4afa924 100644 --- a/utils/ext-core/ParsecParser.hs +++ b/utils/ext-core/ParsecParser.hs @@ -36,7 +36,6 @@ coreModuleName = do corePackageName :: Parser Pname -- Package names can be lowercase or uppercase! --- TODO: update docs corePackageName = identifier <|> upperName coreHierModuleNames :: Parser ([Id], Id) @@ -81,11 +80,11 @@ coreNewtypeDecl = do reserved "newtype" tyCon <- coreQualifiedCon whiteSpace + coercionName <- coreQualifiedCon + whiteSpace tBinds <- coreTbinds - symbol "^" - axiom <- coreAxiom tyRep <- try coreTRep - return $ Newtype tyCon tBinds axiom tyRep + return $ Newtype tyCon coercionName tBinds tyRep coreQualifiedCon :: Parser (Mname, Id) coreQualifiedCon = coreQualifiedGen upperName @@ -109,17 +108,6 @@ coreQualifiedGen p = (try (do -- unqualified name (p >>= (\ res -> return (Nothing, res))) -coreAxiom :: Parser Axiom -coreAxiom = parens (do - coercionName <- coreQualifiedCon - whiteSpace - tbs <- coreTbinds - whiteSpace - symbol "::" - whiteSpace - coercionK <- try equalityKind <|> parens equalityKind - return (coercionName, tbs, coercionK)) - coreTbinds :: Parser [Tbind] coreTbinds = many coreTbind @@ -322,7 +310,7 @@ coreVdef = do coreAtomicExp :: Parser Exp coreAtomicExp = do -- For stupid reasons, the whiteSpace is necessary. --- Without it, (pt coreAppExp "w ^a:B.C ") doesn't work. +-- Without it, (pt coreAppExp "w a:B.C ") doesn't work. whiteSpace res <- choice [try coreDconOrVar, try coreLit, diff --git a/utils/ext-core/Printer.hs b/utils/ext-core/Printer.hs index 2649a00..4e42445 100644 --- a/utils/ext-core/Printer.hs +++ b/utils/ext-core/Printer.hs @@ -66,14 +66,10 @@ ptdef (Data qtcon tbinds cdefs) = (text "%data" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) <+> char '=') $$ indent (braces ((vcat (punctuate (char ';') (map pcdef cdefs))))) -ptdef (Newtype qtcon tbinds (coercion,cTbs,k) tyopt) = - text "%newtype" <+> pqname qtcon <+> (hsep (map ptbind tbinds)) - $$ indent (axiomclause $$ repclause) - where axiomclause = char '^' <+> parens (pqname coercion <+> - (hsep (map ptbind cTbs)) <+> - text "::" - <+> peqkind k) - repclause = case tyopt of +ptdef (Newtype qtcon coercion tbinds tyopt) = + text "%newtype" <+> pqname qtcon <+> pqname coercion + <+> (hsep (map ptbind tbinds)) $$ indent repclause + where repclause = case tyopt of Just ty -> char '=' <+> pty ty Nothing -> empty -- 1.7.10.4