From 14347456d7a034fc9de9424271f6a2ffbfc79f3c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jan 2020 13:25:45 -0800
Subject: [PATCH] feat: extensible tactics

---
 src/Init/Lean/Elab/Tactic/Basic.lean | 38 ++++++++++++++++++++--------
 1 file changed, 28 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 05759532a3..6f247a7943 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -160,15 +160,38 @@ private def evalTacticUsing (s : State) (stx : Syntax) : List Tactic → TacticM
 | []                => do
   let refFmt := stx.prettyPrint;
   throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
-| (elabFn::elabFns) => catch (elabFn stx)
+| (evalFn::evalFns) => catch (evalFn stx)
   (fun ex => match ex with
-    | Exception.error _           => throw ex
-    | Exception.unsupportedSyntax => do set s; evalTacticUsing elabFns)
+    | Exception.error _           =>
+      match evalFns with
+      | [] => throw ex
+      | _  => do set s; evalTacticUsing evalFns
+    | Exception.unsupportedSyntax => do set s; evalTacticUsing evalFns)
 
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline] def withMacroExpansion {α} (stx : Syntax) (x : TacticM α) : TacticM α :=
 adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x
 
+@[specialize] private def expandTacticMacroFns (evalTactic : Syntax → TacticM Unit) (stx : Syntax) : List Macro → TacticM Unit
+| []    => throwError stx ("tactic '" ++ toString stx.getKind ++ "' has not been implemented")
+| m::ms => do
+  scp ← getCurrMacroScope;
+  match m stx scp with
+  | none      => expandTacticMacroFns ms
+  | some stx' =>
+    catch
+      (evalTactic stx')
+      (fun ex => match ms with
+        | [] => throw ex
+        | _  => expandTacticMacroFns ms)
+
+@[inline] def expandTacticMacro (evalTactic : Syntax → TacticM Unit) (stx : Syntax) : TacticM Unit := do
+env ← getEnv;
+let k        := stx.getKind;
+let table    := (macroAttribute.ext.getState env).table;
+let macroFns := (table.find? k).getD [];
+expandTacticMacroFns evalTactic stx macroFns
+
 partial def evalTactic : Syntax → TacticM Unit
 | stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
   | Syntax.node k args =>
@@ -182,13 +205,8 @@ partial def evalTactic : Syntax → TacticM Unit
       let table := (tacticElabAttribute.ext.getState s.env).table;
       let k := stx.getKind;
       match table.find? k with
-      | some elabFns => evalTacticUsing s stx elabFns
-        | none         => do
-          scp ← getCurrMacroScope;
-          env ← getEnv;
-          match expandMacro env stx scp with
-          | some stx' => withMacroExpansion stx $ evalTactic stx'
-          | none      => throwError stx ("tactic '" ++ toString k ++ "' has not been implemented")
+      | some evalFns => evalTacticUsing s stx evalFns
+      | none         => expandTacticMacro evalTactic stx
   | _ => throwError stx "unexpected command"
 
 /-- Adapt a syntax transformation to a regular tactic evaluator. -/