perf: annotate built-in functions with tagged_return

src/Init/Data/FloatArray/Basic.lean

@@ -42,7 +42,7 @@ instance : EmptyCollection FloatArray where
 def push : FloatArray → Float → FloatArray
   | ⟨ds⟩, b => ⟨ds.push b⟩
 
-@[extern "lean_float_array_size"]
+@[extern "lean_float_array_size", tagged_return]
 def size : (@& FloatArray) → Nat
   | ⟨ds⟩ => ds.size
 

src/Init/Data/SInt/Basic.lean

@@ -150,7 +150,7 @@ Converts an 8-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int8_to_int"]
+@[extern "lean_int8_to_int", tagged_return]
 def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt
 /--
 Converts an 8-bit signed integer to a natural number, mapping all negative numbers to `0`.
@@ -503,7 +503,7 @@ Converts a 16-bit signed integer to an arbitrary-precision integer that denotes
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_int16_to_int"]
+@[extern "lean_int16_to_int", tagged_return]
 def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt
 /--
 Converts a 16-bit signed integer to a natural number, mapping all negative numbers to `0`.

src/Init/Data/String/Basic.lean

@@ -264,7 +264,7 @@ Examples:
 * `"abc".length = 3`
 * `"L∃∀N".length = 4`
 -/
-@[extern "lean_string_length", expose]
+@[extern "lean_string_length", expose, tagged_return]
 def String.length (b : @& String) : Nat :=
   b.toList.length
 
@@ -1652,7 +1652,7 @@ def Slice.pos! (s : Slice) (off : String.Pos.Raw) : s.Pos :=
 
 /-- Advances a valid position on a string to the next valid position, given a proof that the
 position is not the past-the-end position, which guarantees that such a position exists. -/
-@[expose, extern "lean_string_utf8_next_fast"]
+@[expose, extern "lean_string_utf8_next_fast", tagged_return]
 def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
   ofToSlice (Slice.Pos.next pos.toSlice (ne_of_apply_ne Pos.ofToSlice (by simpa)))
 
@@ -2656,7 +2656,7 @@ This is a legacy function. The recommended alternative is `String.Pos.next`, com
 Example:
 * `let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'`
 -/
-@[extern "lean_string_utf8_next_fast", expose]
+@[extern "lean_string_utf8_next_fast", expose, tagged_return]
 def Pos.Raw.next' (s : @& String) (p : @& Pos.Raw) (h : ¬ p.atEnd s) : Pos.Raw :=
   let c := p.get s
   p + c

src/Init/Data/UInt/BasicAux.lean

@@ -57,7 +57,7 @@ Converts an 8-bit unsigned integer to an arbitrary-precision natural number.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_uint8_to_nat"]
+@[extern "lean_uint8_to_nat", tagged_return]
 def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat
 
 instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
@@ -108,7 +108,7 @@ Converts a 16-bit unsigned integer to an arbitrary-precision natural number.
 
 This function is overridden at runtime with an efficient implementation.
 -/
-@[extern "lean_uint16_to_nat"]
+@[extern "lean_uint16_to_nat", tagged_return]
 def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat
 /--
 Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

src/Init/Prelude.lean

@@ -3185,7 +3185,7 @@ This is a cached value, so it is `O(1)` to access. The space allocated for an ar
 its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
 internal detail that's not observable by Lean code.
 -/
-@[extern "lean_array_get_size"]
+@[extern "lean_array_get_size", tagged_return]
 def Array.size {α : Type u} (a : @& Array α) : Nat :=
  a.toList.length
 
@@ -3393,7 +3393,7 @@ Returns the number of bytes in the byte array.
 This is the number of bytes actually in the array, as distinct from its capacity, which is the
 amount of memory presently allocated for the array.
 -/
-@[extern "lean_byte_array_size"]
+@[extern "lean_byte_array_size", tagged_return]
 def ByteArray.size : (@& ByteArray) → Nat
   | ⟨bs⟩ => bs.size
 
@@ -3540,7 +3540,7 @@ The number of bytes used by the string's UTF-8 encoding.
 
 At runtime, this function takes constant time because the byte length of strings is cached.
 -/
-@[extern "lean_string_utf8_byte_size"]
+@[extern "lean_string_utf8_byte_size", tagged_return]
 def String.utf8ByteSize (s : @& String) : Nat :=
   s.toByteArray.size
 

tests/lean/run/tagged_return_2.lean

@@ -0,0 +1,161 @@
+/-! This test asserts that the built-in symbols marked with tagged_return compile correctly -/
+
+/--
+trace: [Compiler.IR] [result]
+    def test1 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := FloatArray.size x_1;
+      ret x_2
+    def test1._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test1 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test1 (a : FloatArray) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test2 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := ByteArray.size x_1;
+      ret x_2
+    def test2._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test2 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test2 (a : ByteArray) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test3 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := Array.size ◾ x_1;
+      ret x_2
+    def test3._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test3 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test3 (a : Array Nat) := a.size
+
+/--
+trace: [Compiler.IR] [result]
+    def test4 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := String.length x_1;
+      ret x_2
+    def test4._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test4 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test4 (a : String) := a.length
+
+/--
+trace: [Compiler.IR] [result]
+    def test5 (x_1 : @& obj) : tobj :=
+      let x_2 : tagged := String.utf8ByteSize x_1;
+      ret x_2
+    def test5._boxed (x_1 : obj) : tobj :=
+      let x_2 : tobj := test5 x_1;
+      dec x_1;
+      ret x_2
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test5 (a : String) := a.utf8ByteSize
+
+/--
+warning: declaration uses 'sorry'
+---
+trace: [Compiler.IR] [result]
+    def test6 (x_1 : @& obj) (x_2 : @& tobj) : tobj :=
+      let x_3 : tagged := String.Pos.next x_1 x_2 ◾;
+      ret x_3
+    def test6._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+      let x_3 : tobj := test6 x_1 x_2;
+      dec x_2;
+      dec x_1;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test6 (a : String) (p : a.Pos) := p.next sorry
+
+/--
+trace: [Compiler.IR] [result]
+    def test8 (x_1 : u8) : tobj :=
+      let x_2 : tagged := UInt8.toNat x_1;
+      ret x_2
+    def test8._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u8 := unbox x_1;
+      let x_3 : tobj := test8 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test8 (a : UInt8) := a.toNat
+
+/--
+trace: [Compiler.IR] [result]
+    def test9 (x_1 : u16) : tobj :=
+      let x_2 : tagged := UInt16.toNat x_1;
+      ret x_2
+    def test9._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u16 := unbox x_1;
+      let x_3 : tobj := test9 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test9 (a : UInt16) := a.toNat
+
+/--
+trace: [Compiler.IR] [result]
+    def test10 (x_1 : u8) : tobj :=
+      let x_2 : tagged := Int8.toInt x_1;
+      ret x_2
+    def test10._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u8 := unbox x_1;
+      let x_3 : tobj := test10 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test10 (a : Int8) := a.toInt
+
+/--
+trace: [Compiler.IR] [result]
+    def test11 (x_1 : u16) : tobj :=
+      let x_2 : tagged := Int16.toInt x_1;
+      ret x_2
+    def test11._boxed (x_1 : tagged) : tobj :=
+      let x_2 : u16 := unbox x_1;
+      let x_3 : tobj := test11 x_2;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test11 (a : Int16) := a.toInt
+
+/--
+warning: declaration uses 'sorry'
+---
+trace: [Compiler.IR] [result]
+    def test12 (x_1 : @& obj) (x_2 : @& tobj) : tobj :=
+      let x_3 : tagged := String.Pos.Raw.next' x_1 x_2 ◾;
+      ret x_3
+    def test12._boxed (x_1 : obj) (x_2 : tobj) : tobj :=
+      let x_3 : tobj := test12 x_1 x_2;
+      dec x_2;
+      dec x_1;
+      ret x_3
+-/
+#guard_msgs in
+set_option trace.compiler.ir.result true in
+def test12 (a : String) (p : String.Pos.Raw) := p.next' a sorry