feat: pp.beta to apply beta reduction when pretty printing (#2864)

This was a Lean 3 pretty printer option. While this pretty printer
option tends to lead to confusing situations when set, it has been
frequently requested. [It is
possible](https://github.com/leanprover-community/mathlib4/pull/7910) to
implement this pretty printer option as a user, but it comes with some
artifacts -- for instance, expressions in hovers are not beta reduced.
Adding this as a core pp option is cleanest.

(We should consider having hooks into the tactic evaluator to allow
users to transform the tactic state between tactics. This would enable
beta reducing the entire local context for real, which would be useful
for teaching.)

Closes #715

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -277,6 +277,17 @@ end Delaborator
 open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze)
 
+/-- Custom version of `Lean.Core.betaReduce` to beta reduce expressions for the `pp.beta` option.
+We do not want to beta reduce the application in `let_fun` annotations. -/
+private partial def betaReduce' (e : Expr) : CoreM Expr :=
+  Core.transform e (pre := fun e => do
+    if isLetFun e then
+      return .done <| e.updateMData! (.app (← betaReduce' e.mdataExpr!.appFn!) (← betaReduce' e.mdataExpr!.appArg!))
+    else if e.isHeadBetaTarget then
+      return .visit e.headBeta
+    else
+      return .continue)
+
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
@@ -291,6 +302,7 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
     catch _ => pure ()
   withOptions (fun _ => opts) do
     let e ← if getPPInstantiateMVars opts then instantiateMVars e else pure e
+    let e ← if getPPBeta opts then betaReduce' e else pure e
     let optionsPerPos ←
       if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
         topDownAnalyze e

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -68,6 +68,11 @@ register_builtin_option pp.instantiateMVars : Bool := {
   group    := "pp"
   descr    := "(pretty printer) instantiate mvars before delaborating"
 }
+register_builtin_option pp.beta : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) apply beta-reduction when pretty printing"
+}
 register_builtin_option pp.structureInstances : Bool := {
   defValue := true
   group    := "pp"
@@ -152,11 +157,6 @@ register_builtin_option g_pp_locals_full_names : Bool := {
   group    := "pp"
   descr    := "(pretty printer) show full names of locals"
 }
-register_builtin_option g_pp_beta : Bool := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) apply beta-reduction when pretty printing"
-}
 register_builtin_option g_pp_goal_compact : Bool := {
   defValue := false
   group    := "pp"
@@ -196,6 +196,7 @@ def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
+def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o)
 def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue

tests/lean/ppBeta.lean

@@ -0,0 +1,13 @@
+#check (fun x => x) Nat
+
+#check let_fun x := Nat; x
+
+set_option pp.beta true
+
+#check (fun x => x) Nat
+
+#check let_fun x := Nat; x
+
+set_option pp.all true
+
+#check (fun x => x) Nat

tests/lean/ppBeta.lean.expected.out

@@ -0,0 +1,7 @@
+(fun x => x) Nat : Type
+let_fun x := Nat;
+x : Type
+Nat : Type
+let_fun x := Nat;
+x : Type
+Nat : Type