rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

print dimension app with an @

Browse source
This commit is contained in:
rhiannon morris 2023-02-26 11:22:44 +01:00
parent ab63edf572
commit eaf679edf7
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -53,10 +53,13 @@ prettyLams sort names body = do
export covering export covering
prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m => prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
f -> List a -> m (Doc HL) Maybe (Doc HL) -> f -> List a -> m (Doc HL)
prettyApps fun args = prettyApps pfx fun args =
parensIfM App =<< withPrec Arg parensIfM App =<< withPrec Arg
[|prettyM fun <//> (align . sep <$> traverse prettyM args)|] [|prettyM fun <//> (align . sep <$> traverse prettyArg args)|]
where
prettyArg : a -> m (Doc HL)
prettyArg x = maybe id (\p => map (hl Delim p <+>)) pfx $ prettyM x
export covering export covering
prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL) prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
@ -141,7 +144,7 @@ mutual
prettyVar TVar TVarErr (!ask).tnames i prettyVar TVar TVarErr (!ask).tnames i
prettyM (e :@ s) = prettyM (e :@ s) =
let GotArgs {fun, args, _} = getArgs' e [s] in let GotArgs {fun, args, _} = getArgs' e [s] in
prettyApps fun args prettyApps Nothing fun args
prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
pat <- (parens . separate commaD . map (hl TVar)) <$> pat <- (parens . separate commaD . map (hl TVar)) <$>
traverse prettyM [x, y] traverse prettyM [x, y]
@ -151,7 +154,7 @@ mutual
[([], prettyTag t, b) | (t, b) <- SortedMap.toList arms] [([], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
prettyM (e :% d) = prettyM (e :% d) =
let GotDArgs {fun, args, _} = getDArgs' e [d] in let GotDArgs {fun, args, _} = getDArgs' e [d] in
prettyApps fun args prettyApps (Just "@") fun args
prettyM (s :# a) = prettyM (s :# a) =
parensIfM Ann $ hang 2 $ parensIfM Ann $ hang 2 $
!(withPrec AnnL $ prettyM s) <++> !annD !(withPrec AnnL $ prettyM s) <++> !annD