From 273a0775d6fcbe475fc46153514b86a0983b509f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Apr 2019 10:27:58 -0700
Subject: [PATCH] perf(library/init/data/array): `mkArray` in Lean doesn't seem
 to buy us anything

The primitive implementation combines all `inc`'s into a single one.
---
 library/init/data/array/basic.lean   | 27 ++++++---------------------
 library/init/data/hashmap/basic.lean |  4 ++--
 src/runtime/object.h                 |  1 +
 3 files changed, 9 insertions(+), 23 deletions(-)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 14e8386135..902c646412 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -40,9 +40,13 @@ def push (a : Array α) (v : α) : Array α :=
     if h₂ : j = a.sz then v
     else a.data ⟨j, Nat.ltOfLeOfNe (Nat.leOfLtSucc h₁) h₂⟩ }
 
+@[extern cpp inline "lean::mk_array(#2, #3)"]
 def mkArray {α : Type u} (n : Nat) (v : α) : Array α :=
-let a : Array α := mkEmpty n in
-n.repeat (λ a, a.push v) a
+{ sz   := n,
+  data := λ _, v}
+
+theorem szMkArrayEq {α : Type u} (n : Nat) (v : α) : (mkArray n v).sz = n :=
+rfl
 
 def empty : Array α :=
 mkEmpty 0
@@ -183,25 +187,6 @@ end Array
 
 export Array (mkArray)
 
-private theorem repeatCorePushSz {α : Type u} : ∀ (n : Nat) (v : α) (a : Array α),
-   (Nat.repeatCore (λ (a : Array α), a.push v) n (a.push v)).sz =
-   (Nat.repeatCore (λ (a : Array α), a.push v) n a).sz.succ
-| 0            _ _ := rfl
-| (Nat.succ n) v a :=
-  show (Nat.repeatCore (λ (a : Array α), a.push v) n ((a.push v).push v)).sz =
-       (Nat.repeatCore (λ (a : Array α), a.push v) n (a.push v)).sz.succ, from
-  repeatCorePushSz n v (a.push v)
-
-theorem szMkArrayEq {α : Type u} (n : Nat) (v : α) : (mkArray n v).sz = n :=
-Nat.recOn n rfl $ λ n ih,
-  have aux₁ : (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz = n, from ih,
-  have aux₂ : (Nat.repeatCore (λ (a : Array α), a.push v) n ((Array.mkEmpty n).push v)).sz =
-              (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz.succ, from
-    repeatCorePushSz _ _ _,
-  have aux₃ : (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz.succ = n.succ, from
-    congrArg _ aux₁,
-  Eq.trans aux₂ aux₃
-
 @[inlineIfReduce] def List.toArrayAux {α : Type u} : List α → Array α → Array α
 | []      r := r
 | (a::as) r := List.toArrayAux as (r.push a)
diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index b98135afed..b65e8479b4 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -24,7 +24,7 @@ let n := if nbuckets = 0 then 8 else nbuckets in
 { size       := 0,
   buckets    :=
   ⟨ mkArray n AssocList.nil,
-    have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from szMkArrayEq _ _,
+    have p₁ : (mkArray n (@AssocList.nil α β)).size = n, from Array.szMkArrayEq _ _,
     have p₂ : n = (if nbuckets = 0 then 8 else nbuckets), from rfl,
     have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0, from
               match nbuckets with
@@ -63,7 +63,7 @@ foldBuckets m.buckets d f
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
 let nbuckets := buckets.val.size * 2 in
 let aux₁ : nbuckets > 0 := Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero) in
-let aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets := szMkArrayEq _ _ in
+let aux₂ : (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets := Array.szMkArrayEq _ _ in
 { size    := size,
   buckets := foldBuckets buckets ⟨mkArray nbuckets AssocList.nil, aux₂.symm ▸ aux₁⟩ (reinsertAux hash) }
 
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 1a58a23574..b6a6ea7e79 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -1430,6 +1430,7 @@ inline object * array_pop(obj_arg a) {
 }
 
 object * array_push(obj_arg a, obj_arg v);
+object * mk_array(obj_arg n, obj_arg v);
 
 // =======================================
 // debugging helper functions