max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: avoid unnecessary whitespace at LCNF pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-06 18:54:29 -08:00
parent cf13b29760
commit f342d0ea35
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/LCNF/PrettyPrinter.lean
View file

@ -53,15 +53,15 @@ def ppArg (e : Arg) : M Format := do
return "_"
def ppArgs (args : Array Arg) : M Format := do
join args ppArg
prefixJoin " " args ppArg
def ppLetExpr (e : LetExpr) : M Format := do
match e with
| .erased => return "◾"
| .value v => ppExpr v.toExpr
| .proj _ i fvarId => return f!"{← ppFVar fvarId} # {i}"
| .fvar fvarId args => return f!"{← ppFVar fvarId} {← ppArgs args}"
| .const declName us args => return f!"{← ppExpr (.const declName us)} {← ppArgs args}"
| .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}"
| .const declName us args => return f!"{← ppExpr (.const declName us)}{← ppArgs args}"
def ppParam (param : Param) : M Format := do
let borrow := if param.borrow then "@&" else ""
@ -98,7 +98,7 @@ mutual
| .jp decl k => return f!"jp " ++ (← ppFunDecl decl) ++ ";" ++ .line ++ (← ppCode k)
| .cases c => return f!"cases {← ppFVar c.discr} : {← ppExpr c.resultType}{← prefixJoin .line c.alts ppAlt}"
| .return fvarId => return f!"return {← ppFVar fvarId}"
| .jmp fvarId args => return f!"goto {← ppFVar fvarId} {← ppArgs args}"
| .jmp fvarId args => return f!"goto {← ppFVar fvarId}{← ppArgs args}"
| .unreach type =>
if pp.all.get (← getOptions) then
return f!"⊥ : {← ppExpr type}"