chore: use Expr.numObjs instead of lean_expr_size_shared (#5239)

Remark: declarations like `sizeWithSharing` must be in `IO` since they
are not functions.

The commit also uses the more efficient `ShareCommon.shareCommon'`.

src/Lean/Expr.lean

@@ -1899,13 +1899,6 @@ with initial value `a`. -/
 def foldlM {α : Type} {m} [Monad m] (f : α → Expr → m α) (init : α) (e : Expr) : m α :=
   Prod.snd <$> StateT.run (e.traverseChildren (fun e' => fun a => Prod.mk e' <$> f a e')) init
 
-/--
-Returns the size of `e` as a DAG, i.e. the number of unique `Expr` constructor objects reachable
-from `e`.
--/
-@[extern "lean_expr_size_shared"]
-opaque sizeWithSharing (e : Expr) : Nat
-
 /--
 Returns the size of `e` as a tree, i.e. nodes reachable via multiple paths are counted multiple
 times.

src/Lean/PrettyPrinter.lean

@@ -9,6 +9,7 @@ import Lean.PrettyPrinter.Parenthesizer
 import Lean.PrettyPrinter.Formatter
 import Lean.Parser.Module
 import Lean.ParserCompiler
+import Lean.Util.NumObjs
 import Lean.Util.ShareCommon
 namespace Lean
 
@@ -43,11 +44,11 @@ register_builtin_option pp.exprSizes : Bool := {
     (size disregarding sharing/size with sharing/size with max sharing)"
 }
 
-private def maybePrependExprSizes (e : Expr) (f : Format) : MetaM Format :=
-  return if pp.exprSizes.get (← getOptions) then
-    f!"[size {e.sizeWithoutSharing}/{e.sizeWithSharing}/{ShareCommon.shareCommon e |>.sizeWithSharing}] {f}"
+private def maybePrependExprSizes (e : Expr) (f : Format) : MetaM Format := do
+  if pp.exprSizes.get (← getOptions) then
+    return f!"[size {e.sizeWithoutSharing}/{← e.numObjs}/{← (ShareCommon.shareCommon' e).numObjs}] {f}"
   else
-    f
+    return f
 
 def ppExpr (e : Expr) : MetaM Format := do
   ppUsing e delab >>= maybePrependExprSizes e

src/kernel/for_each_fn.cpp

@@ -161,16 +161,6 @@ void for_each(expr const & e, std::function<bool(expr const &, unsigned)> && f)
     return for_each_offset_fn(f)(e);
 }
 
-extern "C" LEAN_EXPORT obj_res lean_expr_size_shared(b_obj_arg e_) {
-    expr const & e = TO_REF(expr, e_);
-    size_t size = 0;
-    for_each_fn<true>([&](expr const &) {
-        size++;
-        return true;
-    })(e);
-    return usize_to_nat(size);
-}
-
 extern "C" LEAN_EXPORT obj_res lean_find_expr(b_obj_arg p, b_obj_arg e_) {
     lean_object * found = nullptr;
     expr const & e = TO_REF(expr, e_);