feat: new #reduce elaborator

closes #4465

src/Init/Notation.lean

@@ -559,10 +559,20 @@ set_option linter.missingDocs false in
 syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all"
 
 /--
-`#reduce e` computes normal form for expression `e`. By default, `proofs` and `types` are not reduced.
-**Warning:** This is a potentially very expensive operation. Consider using `#eval e` for evaluating/executing expressions.
+`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
+involves applying reduction rules until no further reduction is possible.
+
+By default, proofs and types within the expression are not reduced. Use modifiers
+`(proofs := true)`  and `(types := true)` to reduce them.
+Recall that propositions are types in Lean.
+
+**Warning:** This can be a computationally expensive operation,
+especially for complex expressions.
+
+Consider using `#eval <expression>` for simple evaluation/execution
+of expressions.
 -/
-syntax (name := reduceCmd) "#reduce " ("(" &"proofs" " := " &"true" ")")? ("(" &"types" " := " &"true" ")")? term : command
+syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command
 
 /--
 A message filter specification for `#guard_msgs`.

src/Lean/Elab/BuiltinCommand.lean

@@ -262,16 +262,22 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
 
 @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true)
 
-@[builtin_command_elab Lean.Parser.Command.reduce] def elabReduce : CommandElab
-  | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
-    let e ← Term.elabTerm term none
-    Term.synthesizeSyntheticMVarsNoPostponing
-    let e ← Term.levelMVarToParam (← instantiateMVars e)
-    -- TODO: add options or notation for setting the following parameters
-    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false)
-      logInfoAt tk e
+@[builtin_command_elab Lean.reduceCmd] def elabReduce : CommandElab
+  | `(#reduce%$tk $term) => go tk term
+  | `(#reduce%$tk (proofs := true) $term) => go tk term (skipProofs := false)
+  | `(#reduce%$tk (types := true) $term) => go tk term (skipTypes := false)
+  | `(#reduce%$tk (proofs := true) (types := true) $term) => go tk term (skipProofs := false) (skipTypes := false)
   | _ => throwUnsupportedSyntax
+where
+  go (tk : Syntax) (term : Syntax) (skipProofs := true) (skipTypes := true) : CommandElabM Unit :=
+    withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
+      let e ← Term.elabTerm term none
+      Term.synthesizeSyntheticMVarsNoPostponing
+      let e ← Term.levelMVarToParam (← instantiateMVars e)
+      -- TODO: add options or notation for setting the following parameters
+      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+        let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes)
+        logInfoAt tk e
 
 def hasNoErrorMessages : CommandElabM Bool := do
   return !(← get).messages.hasErrors

tests/lean/run/4465.lean

@@ -0,0 +1,29 @@
+/-- info: { val := { val := ⟨0, ⋯⟩ }, valid := ⋯ } -/
+#guard_msgs in
+#reduce Char.ofNat (nat_lit 0)
+
+/--
+info: { val := { val := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ },
+  valid := Or.inl (Nat.le_of_ble_eq_true rfl) }
+-/
+#guard_msgs in
+set_option pp.proofs true in
+#reduce Char.ofNat (nat_lit 0)
+
+/-- info: 2 = 1 + 1 -/
+#guard_msgs in
+#reduce 2 = 1 + 1
+
+/-- info: 2 = 2 -/
+#guard_msgs in
+#reduce (types := true) 2 = 1 + 1
+
+/-- info: Eq.refl (2 + 2) -/
+#guard_msgs in
+set_option pp.proofs true in
+#reduce Eq.refl (2+2)
+
+/-- info: Eq.refl 4 -/
+#guard_msgs in
+set_option pp.proofs true in
+#reduce (proofs := true) Eq.refl (2+2)