From 9e075e39a55e35e79632f319ec9a2c8bfd0ed3af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 29 Aug 2020 17:05:02 -0700
Subject: [PATCH] feat: eval new `intro` "macro"

It is as powerful as the new `fun` term
---
 src/Lean/Elab/Tactic/Basic.lean | 18 ++++++++++++++---
 tests/lean/run/intromacro.lean  | 36 +++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/intromacro.lean

diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index e00559ff1b..525397e853 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -278,11 +278,23 @@ fun stx => do
 @[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic :=
 fun stx => liftMetaTactic $ fun mvarId => do Meta.assumption mvarId; pure []
 
+private def introStep (n : Name) : TacticM Unit :=
+liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId n; pure [mvarId]
+
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic :=
 fun stx => match_syntax stx with
-  | `(tactic| intro)               => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro1 mvarId; pure [mvarId]
---   | `(tactic| intro $h) => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro mvarId h.getId; pure [mvarId]
-  | _                   => throwUnsupportedSyntax
+  | `(tactic| intro)           => liftMetaTactic $ fun mvarId => do (_, mvarId) ← Meta.intro1 mvarId; pure [mvarId]
+  | `(tactic| intro $h:ident)  => introStep h.getId
+  | `(tactic| intro _)         => introStep `_
+  | `(tactic| intro $pat:term) => do
+    stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h);
+    withMacroExpansion stx stxNew $ evalTactic stxNew
+  | `(tactic| intro $hs*) => do
+    let h0 := hs.get! 0;
+    let hs := hs.extract 1 hs.size;
+    stxNew ← `(tactic| intro $h0:term; intro $hs*);
+    withMacroExpansion stx stxNew $ evalTactic stxNew
+  | _ => throwUnsupportedSyntax
 
 private def getIntrosSize : Expr → Nat
 | Expr.forallE _ _ b _ => getIntrosSize b + 1
diff --git a/tests/lean/run/intromacro.lean b/tests/lean/run/intromacro.lean
new file mode 100644
index 0000000000..cbb1d79696
--- /dev/null
+++ b/tests/lean/run/intromacro.lean
@@ -0,0 +1,36 @@
+new_frontend
+
+structure S :=
+(x y z : Nat := 0)
+
+def f1 : Nat × Nat → S → Nat :=
+begin
+  intro (x, y);
+  intro ⟨a, b, c⟩;
+  exact x+y+a
+end
+
+theorem ex1 : f1 (10, 20) { x := 10 } = 40 :=
+rfl
+
+def f2 : Nat × Nat → S → Nat :=
+begin
+  intro (a, b) { y := y, .. };
+  exact a+b+y
+end
+
+#eval f2 (10, 20) { y := 5 }
+
+theorem ex2 : f2 (10, 20) { y := 5 } = 35 :=
+rfl
+
+def f3 : Nat × Nat → S → S → Nat :=
+begin
+  intro (a, b) { y := y, .. } s;
+  exact a+b+y+s.x
+end
+
+#eval f3 (10, 20) { y := 5 } { x := 1 }
+
+theorem ex3 : f3 (10, 20) { y := 5 } { x := 1 } = 36 :=
+rfl