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

always print the direction in coe/comp

Browse source
This commit is contained in:
rhiannon morris 2023-08-26 21:19:40 +02:00
parent f3f74d581a
commit ba77c45c64
1 changed files with 7 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -524,12 +524,7 @@ prettyElim dnames tnames (Ann tm ty _) =
!(withPrec Outer (prettyTerm dnames tnames ty)) !(withPrec Outer (prettyTerm dnames tnames ty))
prettyElim dnames tnames (Coe ty p q val _) = prettyElim dnames tnames (Coe ty p q val _) =
parensIfM App =<< parensIfM App =<< do
if isDefaultDir p q then do
ty <- prettyTypeLine dnames tnames ty
val <- prettyTArg dnames tnames val
prettyAppD !coeD [ty, val]
else do
ty <- prettyTypeLine dnames tnames ty ty <- prettyTypeLine dnames tnames ty
p <- prettyDArg dnames p p <- prettyDArg dnames p
q <- prettyDArg dnames q q <- prettyDArg dnames q
@ -545,9 +540,7 @@ prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|] arm0 <- [|prettyCompArm dnames tnames Zero zero <+> semiD|]
arm1 <- prettyCompArm dnames tnames One one arm1 <- prettyCompArm dnames tnames One one
ind <- askAt INDENT ind <- askAt INDENT
if isDefaultDir p q layoutComp [ty, pq] val r [arm0, arm1]
then layoutComp [ty] val r [arm0, arm1]
else layoutComp [ty, pq] val r [arm0, arm1]
prettyElim dnames tnames (TypeCase ty ret arms def _) = do prettyElim dnames tnames (TypeCase ty ret arms def _) = do
arms <- for (toList arms) $ \(k ** body) => do arms <- for (toList arms) $ \(k ** body) => do