feat: have `#print` show precise fields of structures

[kmill]

This PR improves the #print command for structures to show all fields and which parents the fields were inherited from, hiding internal details such as which parents are represented as subobjects. This information is still present in the constructor if needed. The pretty printer for private constants is also improved, and it now handles private names from the current module like any other name; private names from other modules are made hygienic.

Example output for #print Monad:

class Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
number of parameters: 1
parents:
  Monad.toApplicative : Applicative m
  Monad.toBind : Bind m
fields:
  Functor.map : {α β : Type u} → (α → β) → m α → m β
  Functor.mapConst : {α β : Type u} → α → m β → m α
  Pure.pure : {α : Type u} → α → m α
  Seq.seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β
  SeqLeft.seqLeft : {α β : Type u} → m α → (Unit → m β) → m α
  SeqRight.seqRight : {α β : Type u} → m α → (Unit → m β) → m β
  Bind.bind : {α β : Type u} → m α → (α → m β) → m β
constructor:
  Monad.mk.{u, v} {m : Type u → Type v} [toApplicative : Applicative m] [toBind : Bind m] : Monad m
resolution order:
  Monad, Applicative, Bind, Functor, Pure, Seq, SeqLeft, SeqRight

Suggested by Floris van Doorn on Zulip.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6096 has successfully built against this PR. (2024-11-16 00:42:56) View Log
• ✅ Mathlib branch lean-pr-testing-6096 has successfully built against this PR. (2024-11-16 02:46:38) View Log
• ✅ Mathlib branch lean-pr-testing-6096 has successfully built against this PR. (2024-11-19 22:57:31) View Log

[fgdorais]

Is the order of fields lexicographic in indices?

[kmill]

@fgdorais It should be — it's using getStructureFieldsFlattened, which takes the direct fields in order and recursively flattens the subobject fields.