From 412c3f59780173f50427a3889f1f44bfcdf342be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Feb 2020 13:53:18 -0800
Subject: [PATCH] feat: add `evalChoice`

cc @Kha
---
 src/Init/Lean/Elab/Tactic/Basic.lean | 15 +++++++++++++++
 tests/lean/run/tacticExtOverlap.lean | 27 +++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)
 create mode 100644 tests/lean/run/tacticExtOverlap.lean

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 0132236a17..8893140a75 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -297,6 +297,21 @@ match newGoals with
 @[builtinTactic seq] def evalSeq : Tactic :=
 fun stx => (stx.getArg 0).forSepArgsM evalTactic
 
+partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
+| i =>
+  if h : i < tactics.size then
+    let tactic := tactics.get ⟨i, h⟩;
+    catch
+      (evalTactic tactic)
+      (fun ex => match ex with
+        | Exception.unsupportedSyntax => evalChoiceAux (i+1)
+        | _ => throw ex)
+  else
+    throwUnsupportedSyntax
+
+@[builtinTactic choice] def evalChoice : Tactic :=
+fun stx => evalChoiceAux stx.getArgs 0
+
 @[builtinTactic skip] def evalSkip : Tactic :=
 fun stx => pure ()
 
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
new file mode 100644
index 0000000000..befde51446
--- /dev/null
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -0,0 +1,27 @@
+new_frontend
+
+open Lean
+
+syntax [myintro] "intros" (sepBy ident ",") : tactic
+
+macro_rules [myintro]
+| `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom none "intros", mkNullNode x.getSepElems]
+
+theorem tst1 {p q : Prop} : p → q → p :=
+begin
+  intros h1, h2;
+  assumption
+end
+
+theorem tst2 {p q : Prop} : p → q → p :=
+begin
+  intros h1; -- the builtin and myintro overlap here.
+  intros h2; -- the builtin and myintro overlap here.
+  assumption
+end
+
+theorem tst3 {p q : Prop} : p → q → p :=
+begin
+  intros h1 h2;
+  assumption
+end