From 1d8cf38ff9163eed6f6c0e73a9119afea7b0d9be Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 31 Jan 2024 22:23:32 -0800 Subject: [PATCH] feat: `pp.numericTypes` option for printing number literals with type ascriptions (#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 #3021 --- RELEASES.md | 5 + .../PrettyPrinter/Delaborator/Builtins.lean | 77 ++++++++++++++- .../PrettyPrinter/Delaborator/Options.lean | 12 +++ tests/lean/ppNumericTypes.lean | 99 +++++++++++++++++++ tests/lean/ppNumericTypes.lean.expected.out | 16 +++ 5 files changed, 204 insertions(+), 5 deletions(-) create mode 100644 tests/lean/ppNumericTypes.lean create mode 100644 tests/lean/ppNumericTypes.lean.expected.out diff --git a/RELEASES.md b/RELEASES.md index df138cb6a252..19f75067dd3a 100644 --- a/RELEASES.md +++ b/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 --------- diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 45c675e6bef7..c5c036cac75a 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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. +`-@OfNat.ofNat _ 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 `-@OfNat.ofNat _ 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] diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 4b3f5be6c1b4..d7d40ad8b276 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/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) diff --git a/tests/lean/ppNumericTypes.lean b/tests/lean/ppNumericTypes.lean new file mode 100644 index 000000000000..3acd48538b77 --- /dev/null +++ b/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 diff --git a/tests/lean/ppNumericTypes.lean.expected.out b/tests/lean/ppNumericTypes.lean.expected.out new file mode 100644 index 000000000000..d0bbdd036406 --- /dev/null +++ b/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