feat: pp.numericTypes option for printing number literals with type…

… ascriptions (leanprover#2933)

Implements the pretty printer option `pp.numericTypes` for including a
type ascription for numeric literals. For example, `(2 : Nat)`, `(-2 :
Int)`, and `(-2 / 3 : Rat)`. This is useful for debugging how arithmetic
expressions have elaborated or have been otherwise transformed. For
example, with exponentiation is is helpful knowing whether it is `x ^ (2
: Nat)` or `x ^ (2 : Real)`. This is like the Lean 3 option
`pp.numeralTypes` but it has a wider notion of a numeric literal.

Also implements the pretty printer option `pp.natLit` for including the
`nat_lit` prefix for raw natural number literals.

Closes leanprover#3021

RELEASES.md

@@ -215,6 +215,11 @@ simproc [my_simp] reduceFoo (foo _) := ...
 
 * Add pretty printer settings to omit deeply nested terms (`pp.deepTerms false` and `pp.deepTerms.threshold`) ([PR #3201](https://github.com/leanprover/lean4/pull/3201))
 
+* Add pretty printer options `pp.numeralTypes` and `pp.natLit`.
+  When `pp.numeralTypes` is true, then natural number literals, integer literals, and rational number literals
+  are pretty printed with type ascriptions, such as `(2 : Rat)`, `(-2 : Rat)`, and `(-2 / 3 : Rat)`.
+  When `pp.natLit` is true, then raw natural number literals are pretty printed as `nat_lit 2`.
+  [PR #2933](https://github.com/leanprover/lean4/pull/2933) and [RFC #3021](https://github.com/leanprover/lean4/issues/3021).
 
 v4.5.0
 ---------

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -680,14 +680,81 @@ def delabLetE : Delab := do
 def delabLit : Delab := do
   let Expr.lit l ← getExpr | unreachable!
   match l with
-  | Literal.natVal n => pure $ quote n
-  | Literal.strVal s => pure $ quote s
+  | Literal.natVal n =>
+    if ← getPPOption getPPNatLit then
+      `(nat_lit $(quote n))
+    else
+      return quote n
+  | Literal.strVal s => return quote s
+
+/--
+Core function that delaborates a natural number (an `OfNat.ofNat` literal).
+-/
+def delabOfNatCore (showType : Bool := false) : Delab := do
+  let .app (.app (.app (.const ``OfNat.ofNat ..) _) (.lit (.natVal n))) _ ← getExpr | failure
+  let stx ← annotateTermInfo <| quote n
+  if showType then
+    let ty ← withNaryArg 0 delab
+    `(($stx : $ty))
+  else
+    return stx
+
+/--
+Core function that delaborates a negative integer literal (a `Neg.neg` applied to `OfNat.ofNat`).
+-/
+def delabNegIntCore (showType : Bool := false) : Delab := do
+  guard <| (← getExpr).isAppOfArity ``Neg.neg 3
+  let n ← withAppArg delabOfNatCore
+  let stx ← annotateTermInfo (← `(- $n))
+  if showType then
+    let ty ← withNaryArg 0 delab
+    `(($stx : $ty))
+  else
+    return stx
+
+/--
+Core function that delaborates a rational literal that is the division of an integer literal
+by a natural number literal.
+The division must be homogeneous for it to count as a rational literal.
+-/
+def delabDivRatCore (showType : Bool := false) : Delab := do
+  let e ← getExpr
+  guard <| e.isAppOfArity ``HDiv.hDiv 6
+  guard <| e.getArg! 0 == e.getArg! 1
+  guard <| e.getArg! 0 == e.getArg! 2
+  let p ← withAppFn <| withAppArg <| (delabOfNatCore <|> delabNegIntCore)
+  let q ← withAppArg <| delabOfNatCore
+  let stx ← annotateTermInfo (← `($p / $q))
+  if showType then
+    let ty ← withNaryArg 0 delab
+    `(($stx : $ty))
+  else
+    return stx
 
--- `@OfNat.ofNat _ n _` ~> `n`
+/--
+Delaborates an `OfNat.ofNat` literal.
+`@OfNat.ofNat _ n _` ~> `n`.
+-/
 @[builtin_delab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions <| withOverApp 3 do
-  let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
-  return quote n
+  delabOfNatCore (showType := (← getPPOption getPPNumericTypes))
+
+/--
+Delaborates the negative of an `OfNat.ofNat` literal.
+`[email protected] _ n _` ~> `-n`
+-/
+@[builtin_delab app.Neg.neg]
+def delabNeg : Delab := whenPPOption getPPCoercions do
+  delabNegIntCore (showType := (← getPPOption getPPNumericTypes))
+
+/--
+Delaborates a rational number literal.
+`@OfNat.ofNat _ n _ / @OfNat.ofNat _ m` ~> `n / m`
+and `[email protected] _ n _ / @OfNat.ofNat _ m` ~> `-n / m`
+-/
+@[builtin_delab app.HDiv.hDiv]
+def delabHDiv : Delab := whenPPOption getPPCoercions do
+  delabDivRatCore (showType := (← getPPOption getPPNumericTypes))
 
 -- `@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]

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -63,6 +63,16 @@ register_builtin_option pp.letVarTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display types of let-bound variables"
 }
+register_builtin_option pp.natLit : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display raw natural number literals with `nat_lit` prefix"
+}
+register_builtin_option pp.numericTypes : 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"
@@ -193,6 +203,8 @@ 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 getPPNumericTypes (o : Options) : Bool := o.get pp.numericTypes.name pp.numericTypes.defValue
+def getPPNatLit (o : Options) : Bool := o.get pp.natLit.name (getPPNumericTypes o && !getPPAll o)
 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)

tests/lean/ppNumericTypes.lean

@@ -0,0 +1,99 @@
+import Lean.Data.Rat
+
+/-!
+Tests for `pp.numericTypes` and `pp.natLit`
+
+RFC #3021
+-/
+
+open Lean (Rat)
+
+section
+
+/-!
+Both raw nat lits and non-raw natural numbers pretty print the same by default
+-/
+#check nat_lit 22
+#check 22
+
+set_option pp.natLit true
+
+/-!
+The raw nat lit pretty prints with the `nat_lit` prefix when `pp.natLit` is true.
+-/
+#check nat_lit 22
+#check 22
+
+end
+
+section
+set_option pp.numericTypes true
+
+/-!
+The `pp.numericTypes` option sets `pp.natLit` to true.
+-/
+#check nat_lit 22
+
+/-!
+Natural number literal
+-/
+#check (22 : Rat)
+
+/-!
+Negative integer literal
+-/
+#check (-22 : Rat)
+
+/-!
+Rational literal of two natural numbers
+-/
+#check (22 / 17 : Rat)
+
+/-!
+Rational literal of a negative integer and a rational
+-/
+#check (-22 / 17 : Rat)
+
+/-!
+Not a rational literal since the denominator is negative.
+-/
+#check (-22 / -17 : Rat)
+
+/-!
+Natural number literal for `Fin`.
+-/
+#check (17 : Fin 22)
+
+/-!
+Natural number literal for `Nat`.
+-/
+#check 2
+
+/-!
+Natural number literals in the context of an equation.
+-/
+#check 2 + 1 = 3
+
+/-!
+Testing `pp.all` override. The `2` should not appear with `nat_lit` in the `OfNat.ofNat` expression.
+-/
+set_option pp.all true
+#check 2
+
+end
+
+section
+set_option pp.all true
+
+/-!
+Testing `pp.all`.
+-/
+#check 2
+
+/-!
+Testing `pp.all` when `pp.natLit` is *explicitly* set to true.
+-/
+set_option pp.natLit true
+#check 2
+
+end

tests/lean/ppNumericTypes.lean.expected.out

@@ -0,0 +1,16 @@
+22 : Nat
+22 : Nat
+nat_lit 22 : Nat
+22 : Nat
+nat_lit 22 : Nat
+(22 : Rat) : Rat
+(-22 : Rat) : Rat
+(22 / 17 : Rat) : Rat
+(-22 / 17 : Rat) : Rat
+(-22 : Rat) / (-17 : Rat) : Rat
+(17 : Fin (22 : Nat)) : Fin (22 : Nat)
+(2 : Nat) : Nat
+(2 : Nat) + (1 : Nat) = (3 : Nat) : Prop
+@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2) : Nat
+@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2) : Nat
+@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)) : Nat