rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 2 Releases Wiki Activity

pretty printing fixes

This commit is contained in:
rhiannon morris 2023-04-17 21:45:05 +02:00
parent 4ca32928fe
commit 06b159973f
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

@ -113,6 +113,8 @@ data TypeLine a = MkTypeLine BaseName a
export export
PrettyHL a => PrettyHL (TypeLine a) where PrettyHL a => PrettyHL (TypeLine a) where
prettyM (MkTypeLine Unused ty) =
bracks <$> pretty0M ty
prettyM (MkTypeLine i ty) = prettyM (MkTypeLine i ty) =
map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty map bracks $ withPrec Outer $ prettyLams Nothing D [< i] ty
@ -153,7 +155,7 @@ prettyCase' : (PrettyHL a, PrettyHL b, PrettyHL c, Pretty.HasEnv m) =>
prettyCase' intro elim r ret arms = do prettyCase' intro elim r ret arms = do
elim <- pretty0M elim elim <- pretty0M elim
ret <- case r of ret <- case r of
Unused => pretty0M ret Unused => under T r $ pretty0M ret
_ => prettyLams Nothing T [< r] ret _ => prettyLams Nothing T [< r] ret
arms <- prettyArms T arms arms <- prettyArms T arms
pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms] pure $ asep [intro <++> elim, returnD <++> ret, ofD <++> arms]
@ -195,10 +197,8 @@ prettyBoxVal : PrettyHL a => Pretty.HasEnv m => a -> m (Doc HL)
prettyBoxVal val = bracks <$> pretty0M val prettyBoxVal val = bracks <$> pretty0M val
export export
prettyCompPat : Pretty.HasEnv m => Dim d -> DimConst -> BaseName -> m (Doc HL) prettyCompPat : Pretty.HasEnv m => DimConst -> BaseName -> m (Doc HL)
prettyCompPat s e j = pure $ prettyCompPat e j = hsep <$> sequence [pretty0M e, pretty0M $ DV j]
hsep [parens (hsep [!(pretty0M s), hl Syntax "=", !(pretty0M e)]),
!(pretty0M $ DV j)]
export export
toNatLit : Term d n -> Maybe Nat toNatLit : Term d n -> Maybe Nat
@ -217,7 +217,7 @@ parameters (showSubsts : Bool)
[TermSubst] PrettyHL (Term d n) using ElimSubst [TermSubst] PrettyHL (Term d n) using ElimSubst
where where
prettyM (TYPE l) = prettyM (TYPE l) =
parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l) pure $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
prettyM (Pi qty s (S _ (N t))) = do prettyM (Pi qty s (S _ (N t))) = do
dom <- pretty0M $ MkWithQty qty s dom <- pretty0M $ MkWithQty qty s
@ -354,13 +354,14 @@ parameters (showSubsts : Bool)
prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one)) = do prettyM (Comp ty p q val r (S [< z] zero) (S [< o] one)) = do
apps <- prettyApps' (L compD) apps <- prettyApps' (L compD)
[(Nothing, epretty ty), [(Nothing, epretty $ MkTypeLine Unused ty),
(Just "@", epretty p), (Just "@", epretty p),
(Just "@", epretty q), (Just "@", epretty q),
(Nothing, epretty val)] (Nothing, epretty val),
(Just "@", epretty r)]
arms <- prettyArms D arms <- prettyArms D
[([< z], !(prettyCompPat r Zero z), zero.term), [([< z], !(prettyCompPat Zero z), zero.term),
([< o], !(prettyCompPat r One o), one.term)] ([< o], !(prettyCompPat One o), one.term)]
pure $ apps <++> arms pure $ apps <++> arms
prettyM (TypeCase ty ret arms def) = do prettyM (TypeCase ty ret arms def) = do