feat(library/init/lean/compiler/ir/rc): missing optimization

library/init/lean/compiler/ir/rc.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import init.lean.runtime
 import init.lean.compiler.ir.compilerm
 import init.lean.compiler.ir.livevars
 
@@ -169,9 +170,19 @@ private def consumeExpr (m : VarMap) : Expr → Bool
   | none      := true
 | other := true
 
+/- Return true iff `v` at runtime is a scalar value stored in a tagged pointer.
+   We do not need RC operations for this kind of value. -/
+private def isScalarBoxedInTaggedPtr (v : Expr) : Bool :=
+match v with
+| Expr.ctor c ys          := c.size == 0 && c.ssize == 0 && c.usize == 0
+| Expr.lit (LitVal.num n) := n ≤ maxSmallNat
+| _ := false
+
 private def updateVarInfo (ctx : Context) (x : VarId) (t : IRType) (v : Expr) : Context :=
-{ varMap :=
-  ctx.varMap.insert x { ref := t.isObj, persistent := isPersistent v, consume := consumeExpr ctx.varMap v },
+{ varMap := ctx.varMap.insert x {
+      ref := t.isObj && !isScalarBoxedInTaggedPtr v,
+      persistent := isPersistent v,
+      consume := consumeExpr ctx.varMap v },
   .. ctx }
 
 private def addDecIfNeeded (ctx : Context) (x : VarId) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody :=

library/init/lean/runtime.lean

@@ -11,7 +11,13 @@ namespace Lean
 @[extern "lean_closure_max_args"]
 constant closureMaxArgsFn : Unit → Nat := default _
 
+@[extern "lean_max_small_nat"]
+constant maxSmallNatFn : Unit → Nat := default _
+
 def closureMaxArgs : Nat :=
 closureMaxArgsFn ()
 
+def maxSmallNat : Nat :=
+maxSmallNatFn ()
+
 end Lean

src/runtime/object.cpp

@@ -1960,6 +1960,10 @@ extern "C" object * lean_closure_max_args(object *) {
     return mk_nat_obj(static_cast<unsigned>(LEAN_CLOSURE_MAX_ARGS));
 }
 
+extern "C" object * lean_max_small_nat(object *) {
+    return mk_nat_obj(LEAN_MAX_SMALL_NAT);
+}
+
 // =======================================
 // Debugging helper functions