From e931fac3bb385a93a4b8da9d95eff284e5e0146a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 16:52:39 -0800
Subject: [PATCH] feat: add `evalTry`

---
 src/Init/Lean/Elab/Tactic/Basic.lean | 18 ++++++++++++++++++
 tests/lean/run/newfrontend1.lean     | 11 +++++++++++
 2 files changed, 29 insertions(+)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 37d9ffae0f..7b78323775 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -191,6 +191,12 @@ partial def evalTactic : Syntax → TacticM Unit
           | none      => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
   | _ => throwError stx "unexpected command"
 
+/-- Adapt a syntax transformation to a regular tactic evaluator. -/
+def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic :=
+fun stx => withMacroExpansion stx $ do
+  stx ← exp stx;
+  evalTactic stx
+
 @[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TacticM α) : TacticM α :=
 adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
 
@@ -271,6 +277,18 @@ fun stx => do
   gs ← getUnsolvedGoals;
   logInfo stx (goalsToMessageData gs)
 
+@[builtinTactic try] def evalTry : Tactic :=
+adaptExpander $ fun stx => match_syntax stx with
+  | `(tactic| try $t) => `(tactic| $t <|> skip)
+  | _         => throwUnsupportedSyntax
+
+/-
+@[builtinTactic repeat] def evalRepeat : Tactic :=
+adaptExpander $ fun stx => match_syntax stx with
+  | `(tactic| repeat $t) => `(tactic| try ($t; repeat $t))
+  | _                    => throwUnsupportedSyntax
+-/
+
 @[builtinTactic «assumption»] def evalAssumption : Tactic :=
 fun stx => liftMetaTactic stx $ fun mvarId => do Meta.assumption mvarId; pure []
 
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index f694f7e364..c9a3319862 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -137,3 +137,14 @@ begin
   exact h3;
   assumption
 end
+
+theorem simple12 (x y z : Nat) : y = z → x = x → x = y → x = z :=
+begin
+  intro h1; intro h2; intro h3;
+  apply @Eq.trans;
+  try exact h1; -- `exact h1` fails
+  traceState;
+  try exact h3;
+  traceState;
+  try exact h1;
+end