make record extension more compact after typechecking

This commit is contained in:
krangelov
2021-10-20 19:57:42 +02:00
parent b6047463a9
commit 64ccd82958
2 changed files with 13 additions and 2 deletions

View File

@@ -554,7 +554,14 @@ checkLType gr g trm typ0 = do
(r',_) <- checkLType gr g r (RecType fields1)
(s',_) <- checkLType gr g s (RecType fields2)
let rec = R ([(l,(Nothing,P r' l)) | (l,_) <- fields1] ++ [(l,(Nothing,P s' l)) | (l,_) <- fields2])
let project t l =
case t of
R rs -> case lookup l rs of
Just (_,t) -> t
Nothing -> error (render ("no value for label" <+> l))
t -> P t l
rec = R ([(l,(Nothing,project r' l)) | (l,_) <- fields1] ++ [(l,(Nothing,project s' l)) | (l,_) <- fields2])
return (rec, typ)
ExtR ty ex -> do

View File

@@ -160,7 +160,11 @@ ppJudgement q (id, AnyInd cann mid) =
_ -> empty
ppPmcfgRule id arg_cats res_cat (PMCFGRule res args lins) =
pp id <+> (':' <+> hsep (intersperse (pp '*') (zipWith ppPmcfgCat arg_cats args)) <+> "->" <+> ppPmcfgCat res_cat res $$
pp id <+> (':' <+>
(if null args
then empty
else hsep (intersperse (pp '*') (zipWith ppPmcfgCat arg_cats args)) <+> "->") <+>
ppPmcfgCat res_cat res $$
'=' <+> brackets (vcat (map (hsep . map ppSymbol) lins)))
ppPmcfgCat :: Ident -> PMCFGCat -> Doc