From 5639302989ff7de75279a1d0dc45a411c4d0f55f Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 24 Nov 2023 04:26:31 -0800
Subject: [PATCH] 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   | 12 ++++++++++++
 src/Lean/PrettyPrinter/Delaborator/Options.lean | 11 ++++++-----
 tests/lean/ppBeta.lean                          | 13 +++++++++++++
 tests/lean/ppBeta.lean.expected.out             |  7 +++++++
 4 files changed, 38 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/ppBeta.lean
 create mode 100644 tests/lean/ppBeta.lean.expected.out

diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index f557f93e98..3f2530b694 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/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
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 764bbc0084..c9d5e0a384 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/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
diff --git a/tests/lean/ppBeta.lean b/tests/lean/ppBeta.lean
new file mode 100644
index 0000000000..44fe8f2fda
--- /dev/null
+++ b/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
diff --git a/tests/lean/ppBeta.lean.expected.out b/tests/lean/ppBeta.lean.expected.out
new file mode 100644
index 0000000000..351e60c62d
--- /dev/null
+++ b/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