From 013f0c9edbca016c2a0777b84e7331c4138eb2b9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 May 2019 18:24:26 -0700
Subject: [PATCH] feat(library/init/lean/compiler/ir/rc): missing optimization

---
 library/init/lean/compiler/ir/rc.lean | 15 +++++++++++++--
 library/init/lean/runtime.lean        |  6 ++++++
 src/runtime/object.cpp                |  4 ++++
 3 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean
index 1f9feff10c..e9d756b4a9 100644
--- a/library/init/lean/compiler/ir/rc.lean
+++ b/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 :=
diff --git a/library/init/lean/runtime.lean b/library/init/lean/runtime.lean
index e5b04d5a67..cbdbe78905 100644
--- a/library/init/lean/runtime.lean
+++ b/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
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index c0a0072f8e..bf4c3cf36d 100644
--- a/src/runtime/object.cpp
+++ b/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