From b5a85ef7a597a41aac7fe54b8f22c98a8a1dbc1a Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 20 Nov 2023 16:13:22 -0800
Subject: [PATCH] feat: `pp.numeralTypes` option for printing number literals
 with type ascriptions

This was a pretty printer option in the Lean 3 community edition, and it was useful for debugging how arithmetic expressions elaborated or have been otherwise transformed. For example, the real numbers have two exponentiation operations (Real -> Real -> Real and Real -> Nat -> Real) and it is helpful knowing at a glance which of these is `x ^ 2`.
---
 src/Lean/PrettyPrinter/Delaborator/Builtins.lean |  6 +++++-
 src/Lean/PrettyPrinter/Delaborator/Options.lean  |  6 ++++++
 tests/lean/ppNumeralTypes.lean                   | 14 ++++++++++++++
 tests/lean/ppNumeralTypes.lean.expected.out      |  5 +++++
 4 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/ppNumeralTypes.lean
 create mode 100644 tests/lean/ppNumeralTypes.lean.expected.out

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index a75323940882..7770d064e11b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -600,7 +600,11 @@ def delabLit : Delab := do
 @[builtin_delab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
   let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
-  return quote n
+  if ← getPPOption getPPNumeralTypes then
+    let ty ← SubExpr.withNaryArg 0 delab
+    `(($(quote n) : $ty))
+  else
+    return quote n
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtin_delab app.OfScientific.ofScientific]
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 764bbc008459..a32f060850f5 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -63,6 +63,11 @@ register_builtin_option pp.letVarTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display types of let-bound variables"
 }
+register_builtin_option pp.numeralTypes : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display types of numeric literals"
+}
 register_builtin_option pp.instantiateMVars : Bool := {
   defValue := false -- TODO: default to true?
   group    := "pp"
@@ -183,6 +188,7 @@ def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue
 def getPPLetVarTypes (o : Options) : Bool := o.get pp.letVarTypes.name (getPPAll o)
+def getPPNumeralTypes (o : Options) : Bool := o.get pp.numeralTypes.name pp.numeralTypes.defValue
 def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o)
 def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o)
 def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o)
diff --git a/tests/lean/ppNumeralTypes.lean b/tests/lean/ppNumeralTypes.lean
new file mode 100644
index 000000000000..51d336786de2
--- /dev/null
+++ b/tests/lean/ppNumeralTypes.lean
@@ -0,0 +1,14 @@
+set_option pp.numeralTypes true
+
+#check (17 : Fin 22)
+
+-- Doesn't apply to nat literals
+#check nat_lit 2
+
+#check 2
+
+#check 2 + 1 = 3
+
+set_option pp.all true
+
+#check 2
diff --git a/tests/lean/ppNumeralTypes.lean.expected.out b/tests/lean/ppNumeralTypes.lean.expected.out
new file mode 100644
index 000000000000..294898eabe4d
--- /dev/null
+++ b/tests/lean/ppNumeralTypes.lean.expected.out
@@ -0,0 +1,5 @@
+(17 : Fin (22 : Nat)) : Fin (22 : Nat)
+2 : Nat
+(2 : Nat) : Nat
+(2 : Nat) + (1 : Nat) = (3 : Nat) : Prop
+@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2) : Nat