From fa55c1e0883ad2dd3793161bd71f12df5f2c14d4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 23 Sep 2020 11:13:23 +0200
Subject: [PATCH] fix: pretty printing loose bvars

Fixes #192
---
 src/Lean/Delaborator.lean             |  2 +-
 src/Lean/PrettyPrinter/Formatter.lean |  4 +++-
 tests/lean/ppExpr.lean                | 11 +++++++++++
 tests/lean/ppExpr.lean.expected.out   |  1 +
 4 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/ppExpr.lean
 create mode 100644 tests/lean/ppExpr.lean.expected.out

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 91d256b3e0..a6237d243e 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -261,7 +261,7 @@ catch
 @[builtinDelab bvar]
 def delabBVar : Delab := do
 Expr.bvar idx _ ← getExpr | unreachable!;
-pure $ mkIdent $ "#" ++ toString idx
+pure $ mkIdent $ mkNameSimple $ "#" ++ toString idx
 
 @[builtinDelab mvar]
 def delabMVar : Delab := do
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 65268524cc..43a303fa84 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -289,7 +289,9 @@ let id := id.simpMacroScopes;
 let s := id.toString;
 if id.isAnonymous then
   pushToken "[anonymous]"
-else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum then
+else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum ||
+  -- loose bvar
+  "#".isPrefixOf s then
   -- not parsable anyway, output as-is
   pushToken s
 else do {
diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
new file mode 100644
index 0000000000..be193c5ac7
--- /dev/null
+++ b/tests/lean/ppExpr.lean
@@ -0,0 +1,11 @@
+import Lean
+new_frontend
+
+/-! Pretty printing tests for `Expr`s that cannot be generated by parsing+elaborating. -/
+
+open Lean
+
+def test (e : Expr) : MetaM Unit :=
+PrettyPrinter.ppExpr Name.anonymous [] e >>= IO.println
+
+#eval test (mkBVar 0)
diff --git a/tests/lean/ppExpr.lean.expected.out b/tests/lean/ppExpr.lean.expected.out
new file mode 100644
index 0000000000..a0a4a0eb17
--- /dev/null
+++ b/tests/lean/ppExpr.lean.expected.out
@@ -0,0 +1 @@
+#0