From 5cc110dd778b698edd39c4637df669ace15ec17b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Nov 2020 08:02:08 -0800
Subject: [PATCH] feat: add `Array.appendCore` for quotations

We need it before we can define the more efficient `Array.append`
---
 src/Init/Prelude.lean        | 11 +++++++++++
 src/Lean/Elab/Quotation.lean |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ad9b55c4c4..9db426d21a 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -993,6 +993,17 @@ def Array.push {α : Type u} (a : Array α) (v : α) : Array α := {
   data := List.concat a.data v
 }
 
+-- Slower `Array.append` used in quotations.
+protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
+  let rec loop (i : Nat) (j : Nat) (as : Array α) : Array α :=
+    dite (Less j bs.size)
+      (fun hlt =>
+        match i with
+        | 0           => as
+        | Nat.succ i' => loop i' (add j 1) (as.push (bs.get ⟨j, hlt⟩)))
+      (fun _ => as)
+  loop bs.size 0 as
+
 class Bind (m : Type u → Type v) :=
   (bind : {α β : Type u} → m α → (α → m β) → m β)
 
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 049e448e6f..e21187fc40 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -83,7 +83,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
       let args ← stx.getArgs.foldlM (fun args arg =>
         if k == nullKind && isAntiquotSplice arg then
           -- antiquotation splice pattern: inject args array
-          `(Array.append $args $(getAntiquotTerm arg))
+          `(Array.appendCore $args $(getAntiquotTerm arg))
         else do
           let arg ← quoteSyntax arg;
           `(Array.push $args $arg)) empty