follow RFC

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -593,18 +593,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
 
--- `@OfNat.ofNat _ n _` ~> `n`
+/--
+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
+
+/--
+Delaborates an `OfNat.ofNat` literal.
+`@OfNat.ofNat _ n _` ~> `n`.
+-/
 @[builtin_delab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
-  let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
-  if ← getPPOption getPPNumeralTypes then
-    let ty ← SubExpr.withNaryArg 0 delab
-    `(($(quote n) : $ty))
-  else
-    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,7 +63,12 @@ register_builtin_option pp.letVarTypes : Bool := {
   group    := "pp"
   descr    := "(pretty printer) display types of let-bound variables"
 }
-register_builtin_option pp.numeralTypes : Bool := {
+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"
@@ -188,7 +193,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 getPPNumeralTypes (o : Options) : Bool := o.get pp.numeralTypes.name pp.numeralTypes.defValue
+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