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

rearrange some auto args for better overriding

Browse source
This commit is contained in:
rhiannon morris 2023-02-26 11:21:25 +01:00
parent 82a2f92ddf
commit 4826c35ad6
1 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -33,16 +33,17 @@ returnD = hl Syntax "return"
export covering export covering
prettyBindType : Pretty.HasEnv m => prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
PrettyHL q => PrettyHL a => PrettyHL b => Pretty.HasEnv m =>
List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL) List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
prettyBindType qtys x s arr t = prettyBindType qtys x s arr t =
parensIfM Outer $ hang 2 $ parensIfM Outer $ hang 2 $
parens !(prettyQtyBinds qtys $ TV x) <++> arr parens (hang 2 $ !(prettyQtyBinds qtys (TV x)) <++> colonD
<//> !(prettyM s)) <++> arr
<//> !(under T x $ prettyM t) <//> !(under T x $ prettyM t)
export covering export covering
prettyLams : Pretty.HasEnv m => PrettyHL a => prettyLams : PrettyHL a => Pretty.HasEnv m =>
BinderSort -> List BaseName -> a -> m (Doc HL) BinderSort -> List BaseName -> a -> m (Doc HL)
prettyLams sort names body = do prettyLams sort names body = do
lam <- case sort of T => lamD; D => dlamD lam <- case sort of T => lamD; D => dlamD
@ -51,31 +52,31 @@ prettyLams sort names body = do
parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body
export covering export covering
prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a => prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
f -> List a -> m (Doc HL) f -> List a -> m (Doc HL)
prettyApps fun args = prettyApps fun args =
parensIfM App =<< withPrec Arg parensIfM App =<< withPrec Arg
[|prettyM fun <//> (align . sep <$> traverse prettyM args)|] [|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
export covering export covering
prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL) prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
prettyTuple = map (parens . align . separate commaD) . traverse prettyM prettyTuple = map (parens . align . separate commaD) . traverse prettyM
export covering export covering
prettyArm : Pretty.HasEnv m => PrettyHL a => prettyArm : PrettyHL a => Pretty.HasEnv m =>
(List BaseName, Doc HL, a) -> m (Doc HL) (List BaseName, Doc HL, a) -> m (Doc HL)
prettyArm (xs, pat, body) = prettyArm (xs, pat, body) =
pure $ hang 2 $ sep pure $ hang 2 $ sep
[pat <+> dotD, !(withPrec Outer $ unders T xs $ prettyM body)] [pat <+> dotD, !(withPrec Outer $ unders T xs $ prettyM body)]
export covering export covering
prettyArms : Pretty.HasEnv m => PrettyHL a => prettyArms : PrettyHL a => Pretty.HasEnv m =>
List (List BaseName, Doc HL, a) -> m (Doc HL) List (List BaseName, Doc HL, a) -> m (Doc HL)
prettyArms = map (braces . align . sep) . traverse prettyArm prettyArms = map (braces . align . sep) . traverse prettyArm
export covering export covering
prettyCase : Pretty.HasEnv m => prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c => Pretty.HasEnv m =>
q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) -> q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) ->
m (Doc HL) m (Doc HL)
prettyCase pi elim r ret arms = prettyCase pi elim r ret arms =