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

pretty printing fixes

Browse source
This commit is contained in:
rhiannon morris 2024-04-12 21:52:51 +02:00
parent a1d8fd4ab5
commit 7883a3cae7
2 changed files with 10 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -229,7 +229,6 @@ prettyDTApps dnames tnames f xs = do
private private
record CaseArm opts d n where record CaseArm opts d n where
constructor MkCaseArm constructor MkCaseArm
{0 dinner, ninner : Nat}
pat : Doc opts pat : Doc opts
dbinds : BTelescope d dinner -- 🍴 dbinds : BTelescope d dinner -- 🍴
tbinds : BTelescope n ninner tbinds : BTelescope n ninner
@ -297,7 +296,7 @@ prettyCase_ : {opts : _} ->
Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) -> Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
Eff Pretty (Doc opts) Eff Pretty (Doc opts)
prettyCase_ dnames tnames intro head ret body = do prettyCase_ dnames tnames intro head ret body = do
head <- assert_total prettyElim dnames tnames head head <- withPrec Outer $ assert_total prettyElim dnames tnames head
ret <- prettyCaseRet dnames tnames ret ret <- prettyCaseRet dnames tnames ret
bodys <- prettyCaseBody dnames tnames body bodys <- prettyCaseBody dnames tnames body
return <- returnD; of_ <- ofD return <- returnD; of_ <- ofD
@ -325,11 +324,6 @@ private
LetExpr : Nat -> Nat -> Nat -> Type LetExpr : Nat -> Nat -> Nat -> Type
LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n') LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
private
PrettyLetResult : LayoutOpts -> Nat -> Type
PrettyLetResult opts d =
Exists $ \n => (BContext n, Term d n, SnocList (Doc opts))
-- [todo] factor out this and the untyped version somehow -- [todo] factor out this and the untyped version somehow
export export
splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n) splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
@ -364,9 +358,10 @@ prettyLets dnames xs lets = snd <$> go lets where
Nothing => do Nothing => do
e <- withPrec Outer $ assert_total prettyElim dnames tnames e e <- withPrec Outer $ assert_total prettyElim dnames tnames e
eq <- cstD; d <- askAt INDENT eq <- cstD; d <- askAt INDENT
inn <- inD
pure $ ifMultiline pure $ ifMultiline
(hsep [hdr, eq, e]) (hsep [hdr, eq, e, inn])
(vsep [hdr, indent d $ hsep [eq, e]]) (vsep [hdr, indent d $ hsep [eq, e, inn]])
go : forall b. Telescope (LetBinder d) a b -> go : forall b. Telescope (LetBinder d) a b ->
Eff Pretty (BContext b, SnocList (Doc opts)) Eff Pretty (BContext b, SnocList (Doc opts))
@ -437,13 +432,10 @@ prettyDisp u = map Just $ hl Universe =<<
ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u) ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u)
prettyTerm dnames tnames (TYPE l _) = prettyTerm dnames tnames (TYPE l _) = do
case !(askAt FLAVOR) of type <- hl Syntax . text =<< ifUnicode "★" "Type"
Unicode => do level <- prettyDisp l
star <- hl Syntax "★" pure $ maybe type (type <+>) level
level <- hl Universe $ text $ superscript $ show l
pure $ hcat [star, level]
Ascii => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
prettyTerm dnames tnames (IOState _) = prettyTerm dnames tnames (IOState _) =
ioStateD ioStateD

2
lib/Quox/Typing/Context.idr
View file

@ -391,5 +391,5 @@ export
prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts) prettyWhnfContext : {opts : _} -> WhnfContext d n -> Eff Pretty (Doc opts)
prettyWhnfContext ctx = prettyWhnfContext ctx =
let Val n = ctx.termLen in let Val n = ctx.termLen in
separateTight !commaD <$> sepSingle . exceptLast (<+> comma) . toList <$>
prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx prettyTContext' ctx.dnames (replicate n "_") ctx.tnames ctx.tctx