chore(Lean/Meta/RefinedDiscrTree/Basic): remove privateInPublic (leanprover-community#33589)

This PR fixes cases of `privateInPublic` in the `RefinedDiscrTree` code. The offending pattern is that an instance is defined using a private definition. The solution is to not mark that definition as `private`.

As a result, this PR also adds some documentation to those functions, in particular to `RefinedDiscrTree.format`. I've added an example of what the output may look like.  I also made a small fix to that function, adding a missing newline.

Also avoid a use of `nonrec`.

Author: JovanGerb

Mathlib/Lean/Meta/RefinedDiscrTree/Basic.lean

@@ -50,13 +50,13 @@ inductive Key where
   | proj (typeName : Name) (idx nargs : Nat)
   deriving Inhabited, BEq
 
-set_option backward.privateInPublic true in
-/-
-At the root, `.const` is the most common key, and it is very uncommon
+/-- Compute the hash of a `RefinedDiscrTree.Key`.
+
+Note: at the root, `.const` is the most common key, and it is very uncommon
 to get the same constant name with a different arity.
 So for performance, we just use `hash name` to hash `.const name _`.
 -/
-private nonrec def Key.hash : Key → UInt64
+protected def Key.hash : Key → UInt64
   | .star                => 0
   | .labelledStar id     => mixHash 5 <| hash id
   | .opaque              => 1
@@ -69,12 +69,10 @@ private nonrec def Key.hash : Key → UInt64
   | .«forall»            => 4
   | .proj name idx nargs => mixHash (hash nargs) <| mixHash (hash name) (hash idx)
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : Hashable Key := ⟨Key.hash⟩
 
-set_option backward.privateInPublic true in
-private def Key.format : Key → Format
+/-- Format a `RefinedDiscrTree.Key`. -/
+def Key.format : Key → Format
   | .star                   => f!"*"
   | .labelledStar id        => f!"*{id}"
   | .opaque                 => "◾"
@@ -88,12 +86,8 @@ private def Key.format : Key → Format
   | .forall                 => "∀"
   | .proj name idx nargs    => f!"⟨{name}.{idx}, {nargs}⟩"
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : ToFormat Key := ⟨Key.format⟩
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /--
 Converts an entry (i.e., `List Key`) to the discrimination tree into
 `MessageData` that is more user-friendly.
@@ -186,13 +180,11 @@ inductive StackEntry where
   /-- `.expr` is an expression that will be indexed. -/
   | expr (info : ExprInfo)
 
-set_option backward.privateInPublic true in
-private def StackEntry.format : StackEntry → Format
+/-- Format a `RefinedDiscrTree.StackEntry`. -/
+def StackEntry.format : StackEntry → Format
   | .star => f!".star"
   | .expr info => f!".expr {info.expr}"
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : ToFormat StackEntry := ⟨StackEntry.format⟩
 
 /-- A `LazyEntry` represents a snapshot of the computation of encoding an `Expr` as `Array Key`.
@@ -240,17 +232,15 @@ def mkInitLazyEntry (labelledStars : Bool) : MetaM LazyEntry :=
     labelledStars? := if labelledStars then some #[] else none
   }
 
-set_option backward.privateInPublic true in
-private def LazyEntry.format (entry : LazyEntry) : Format := Id.run do
+/-- Format a `RefinedDiscrTree.LazyEntry`. -/
+def LazyEntry.format (entry : LazyEntry) : Format := Id.run do
   let mut parts := #[f!"stack: {entry.stack}"]
   unless entry.computedKeys == [] do
     parts := parts.push f!"results: {entry.computedKeys}"
   if let some info := entry.previous then
     parts := parts.push f!"todo: {info.expr}"
   return Format.joinSep parts.toList ", "
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance : ToFormat LazyEntry := ⟨LazyEntry.format⟩
 
 /-- Array index of a `Trie α` in the `tries` of a `RefinedDiscrTree`. -/
@@ -302,15 +292,48 @@ namespace RefinedDiscrTree
 
 variable {α : Type}
 
-set_option backward.privateInPublic true in
-private partial def format [ToFormat α] (tree : RefinedDiscrTree α) : Format :=
+/-- Format a `RefinedDiscrTree` as a flowchart.
+- Non-terminal nodes are of the form `{key} =>`, followed by all of the following nodes,
+  indented with 2 more spaces.
+- Terminal nodes have either "entries", containing the return values,
+  or "pending entries", for nodes that have not been evaluated/expanded.
+
+For example:
+```
+Discrimination tree flowchart:
+⟨HMul.hMul, 6⟩ =>
+  ⟨Int, 0⟩ =>
+    ⟨Int, 0⟩ =>
+      * =>
+        * =>
+          *0 =>
+            *0 =>
+              pending entries: #[mul_self]
+            *1 =>
+              entries: #[mul_comm]
+            ⟨Neg.neg, 3⟩ =>
+              ⟨Int, 0⟩ =>
+                * =>
+                  *1 =>
+                    entries: #[mul_neg]
+            1 =>
+              pending entries: #[mul_one]
+          ⟨Neg.neg, 3⟩ =>
+            pending entries: #[neg_mul]
+          1 =>
+            *0 =>
+              entries: #[one_mul]
+```
+-/
+partial def format [ToFormat α] (tree : RefinedDiscrTree α) : Format :=
   let lines := tree.root.fold (init := #[]) fun lines key trie =>
     lines.push (Format.nest 2 f!"{key} =>{Format.line}{go trie}")
   if lines.size = 0 then
     f!"<empty discrimination tree>"
   else
-    "Discrimination tree flowchart:" ++ Format.joinSep lines.toList "\n"
+    "Discrimination tree flowchart:\n" ++ Format.joinSep lines.toList "\n"
 where
+  /-- Auxiliary function for `RefinedDiscrTree.format`. -/
   go (trie : TrieIndex) : Format := Id.run do
     let { values, star, labelledStars, children, pending } := tree.tries[trie]!
     let mut lines := #[]
@@ -329,8 +352,6 @@ where
     else
       Format.joinSep lines.toList "\n"
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 instance [ToFormat α] : ToFormat (RefinedDiscrTree α) := ⟨format⟩
 
 end Lean.Meta.RefinedDiscrTree