From 38d3e37c75d8733ddee23705735b1b64d8822c75 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 12 Oct 2022 16:15:11 -0700
Subject: [PATCH] perf: improve `Unhygienic.run` code

---
 src/Init/Prelude.lean                       |  1 +
 src/Lean/Hygiene.lean                       |  1 +
 tests/lean/unhygienicCode.lean              | 10 +++
 tests/lean/unhygienicCode.lean.expected.out | 90 +++++++++++++++++++++
 4 files changed, 102 insertions(+)
 create mode 100644 tests/lean/unhygienicCode.lean
 create mode 100644 tests/lean/unhygienicCode.lean.expected.out

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 945b184510..7ba3ffa029 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3980,6 +3980,7 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where
 export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
 /-- Construct a synthetic `SourceInfo` from the `ref` in the monad state. -/
+@[inline]
 def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo :=
   return SourceInfo.fromRef (← getRef)
 
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 6b6f6176e1..167177f5a9 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -39,6 +39,7 @@ instance : MonadQuotation Unhygienic where
     let fresh ← modifyGet fun n => (n, n + 1)
     withReader ({ · with scope := fresh}) x
 
+@[inline]
 protected def run {α : Type} (x : Unhygienic α) : α := (x ⟨Syntax.missing, firstFrontendMacroScope⟩).run' (firstFrontendMacroScope+1)
 end Unhygienic
 
diff --git a/tests/lean/unhygienicCode.lean b/tests/lean/unhygienicCode.lean
new file mode 100644
index 0000000000..e2a963fe1f
--- /dev/null
+++ b/tests/lean/unhygienicCode.lean
@@ -0,0 +1,10 @@
+import Lean.Hygiene
+open Lean
+
+set_option trace.Compiler.result true
+set_option trace.compiler.ir.result true
+
+-- The following function should not allocate any closures,
+-- nor any heap object that doesn't appear in the result:
+def foo (n : Nat) : Syntax.Term :=
+  Unhygienic.run `(a + $(quote n))
diff --git a/tests/lean/unhygienicCode.lean.expected.out b/tests/lean/unhygienicCode.lean.expected.out
new file mode 100644
index 0000000000..2feb9c6eae
--- /dev/null
+++ b/tests/lean/unhygienicCode.lean.expected.out
@@ -0,0 +1,90 @@
+
+[result]
+def foo._closed_1 : obj :=
+  let x_1 : obj := ctor_0[Lean.Syntax.missing];
+  let x_2 : u8 := 0;
+  let x_3 : obj := Lean.SourceInfo.fromRef x_1 x_2;
+  ret x_3
+def foo._closed_2 : obj :=
+  let x_1 : obj := "UnhygienicMain";
+  ret x_1
+def foo._closed_3 : obj :=
+  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
+  let x_2 : obj := foo._closed_2;
+  let x_3 : obj := Lean.Name.str._override x_1 x_2;
+  ret x_3
+def foo._closed_4 : obj :=
+  let x_1 : obj := "term_+_";
+  ret x_1
+def foo._closed_5 : obj :=
+  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
+  let x_2 : obj := foo._closed_4;
+  let x_3 : obj := Lean.Name.str._override x_1 x_2;
+  ret x_3
+def foo._closed_6 : obj :=
+  let x_1 : obj := "a";
+  ret x_1
+def foo._closed_7 : obj :=
+  let x_1 : obj := foo._closed_6;
+  let x_2 : obj := String.toSubstring' x_1;
+  ret x_2
+def foo._closed_8 : obj :=
+  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
+  let x_2 : obj := foo._closed_6;
+  let x_3 : obj := Lean.Name.str._override x_1 x_2;
+  ret x_3
+def foo._closed_9 : obj :=
+  let x_1 : obj := foo._closed_3;
+  let x_2 : obj := foo._closed_8;
+  let x_3 : obj := Lean.firstFrontendMacroScope;
+  let x_4 : obj := Lean.addMacroScope x_1 x_2 x_3;
+  ret x_4
+def foo._closed_10 : obj :=
+  let x_1 : obj := ctor_0[List.nil];
+  let x_2 : obj := foo._closed_1;
+  let x_3 : obj := foo._closed_7;
+  let x_4 : obj := foo._closed_9;
+  let x_5 : obj := ctor_3[Lean.Syntax.ident] x_2 x_3 x_4 x_1;
+  ret x_5
+def foo._closed_11 : obj :=
+  let x_1 : obj := "+";
+  ret x_1
+def foo._closed_12 : obj :=
+  let x_1 : obj := foo._closed_1;
+  let x_2 : obj := foo._closed_11;
+  let x_3 : obj := ctor_2[Lean.Syntax.atom] x_1 x_2;
+  ret x_3
+def foo (x_1 : obj) : obj :=
+  let x_2 : obj := Nat.repr x_1;
+  let x_3 : obj := ctor_2[Lean.SourceInfo.none];
+  let x_4 : obj := Lean.Syntax.mkNumLit x_2 x_3;
+  let x_5 : obj := foo._closed_10;
+  let x_6 : obj := foo._closed_12;
+  let x_7 : obj := Array.mkArray3._rarg x_5 x_6 x_4;
+  let x_8 : obj := foo._closed_1;
+  let x_9 : obj := foo._closed_5;
+  let x_10 : obj := ctor_1[Lean.Syntax.node] x_8 x_9 x_7;
+  ret x_10[Compiler.result] size: 21
+    def foo n : Syntax :=
+      let fst.1 := Syntax.missing
+      let fst.2 := 1
+      let _x.3 := false
+      let fst.4 := SourceInfo.fromRef fst.1 _x.3
+      let _x.5 := "UnhygienicMain"
+      let fst.6 := Name.mkStr1 _x.5
+      let _x.7 := "term_+_"
+      let _x.8 := Name.mkStr1 _x.7
+      let _x.9 := "a"
+      let _x.10 := String.toSubstring' _x.9
+      let _x.11 := Name.mkStr1 _x.9
+      let _x.12 := addMacroScope fst.6 _x.11 fst.2
+      let _x.13 := [] _
+      let _x.14 := Syntax.ident fst.4 _x.10 _x.12 _x.13
+      let _x.15 := "+"
+      let _x.16 := Syntax.atom fst.4 _x.15
+      let _x.17 := Nat.repr n
+      let _x.18 := SourceInfo.none
+      let _x.19 := Syntax.mkNumLit _x.17 _x.18
+      let _x.20 := Array.mkArray3 _ _x.14 _x.16 _x.19
+      let _x.21 := Syntax.node fst.4 _x.8 _x.20
+      _x.21