From e9e858a4484905a0bfe97c4f05c3924ead02eed8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 2 Sep 2024 23:26:00 +0200
Subject: [PATCH] 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          |  7 -------
 src/Lean/PrettyPrinter.lean |  9 +++++----
 src/kernel/for_each_fn.cpp  | 10 ----------
 3 files changed, 5 insertions(+), 21 deletions(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 166eac5ee26b..85e374e52a16 100644
--- a/src/Lean/Expr.lean
+++ b/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.
diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index da12b25b747e..d0515d37b9b5 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/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
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index 34147ecb40e3..101e64215b22 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/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_);