From 80bb6f174d7c468c581e14bf8eaf2def356fe367 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Jun 2020 20:16:11 -0700
Subject: [PATCH] feat: expand `elab` command

cc @Kha
---
 src/Lean/Elab/Syntax.lean    | 34 ++++++++++++++++++++++++++++++++++
 tests/lean/run/elab_cmd.lean | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+)
 create mode 100644 tests/lean/run/elab_cmd.lean

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 3ed39ff4c8..b20f393dfa 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -437,6 +437,40 @@ fun stx => do
 registerTraceClass `Elab.syntax;
 pure ()
 
+/-
+def elabTail := try (" : " >> ident) >> darrow >> termParser
+parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail
+-/
+@[builtinMacro Lean.Parser.Command.elab] def expandElab : Macro :=
+fun stx => do
+  let ref := stx;
+  let prec    := (stx.getArg 1).getArgs;
+  let head    := stx.getArg 2;
+  let args    := (stx.getArg 3).getArgs;
+  let cat     := stx.getArg 5;
+  let rhs     := stx.getArg 7;
+  let catName := cat.getId;
+  kind ← Macro.mkFreshKind catName.eraseMacroScopes;
+  -- build parser
+  stxPart  ← expandMacroHeadIntoSyntaxItem head;
+  stxParts ← args.mapM expandMacroArgIntoSyntaxItem;
+  let stxParts := #[stxPart] ++ stxParts;
+  -- build pattern for `martch_syntax
+  patHead ← expandMacroHeadIntoPattern head;
+  patArgs ← args.mapM expandMacroArgIntoPattern;
+  let pat := Syntax.node kind (#[patHead] ++ patArgs);
+  let kindId    := mkIdentFrom ref kind;
+  if catName == `term then
+    `(syntax $prec* [$kindId] $stxParts* : $cat @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab := fun stx _ => match_syntax stx with | `($pat) => $rhs | _ => Lean.Elab.Term.throwUnsupportedSyntax)
+  else if catName == `command then
+    `(syntax $prec* [$kindId] $stxParts* : $cat @[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab := fun stx => match_syntax stx with | `($pat) => $rhs | _ => Lean.Elab.Command.throwUnsupportedSyntax)
+  else if catName == `tactic then
+    `(syntax $prec* [$kindId] $stxParts* : $cat @[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic := fun stx => match_syntax stx with | `(tactic|$pat) => $rhs | _ => Lean.Elab.Tactic.throwUnsupportedSyntax)
+  else
+    -- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.
+    -- If users want this feature, they add their own `elab` macro that uses this one as a fallback.
+    Macro.throwError ref ("unsupported syntax category '" ++ toString catName ++ "'")
+
 end Command
 end Elab
 end Lean
diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean
new file mode 100644
index 0000000000..3d3b0616b6
--- /dev/null
+++ b/tests/lean/run/elab_cmd.lean
@@ -0,0 +1,35 @@
+import Lean
+
+new_frontend
+
+open Lean.Elab.Term
+open Lean.Elab.Command
+
+elab "∃" b:term "," P:term : term => do
+ ex ← `(Exists (fun $b => $P));
+ elabTerm ex none
+
+elab "#check2" b:term : command => do
+  cmd ← `(#check $b #check $b);
+  elabCommand cmd
+
+#check ∃ x, x > 0
+
+#check ∃ (x : UInt32), x > 0
+
+#check2 10
+
+elab "try" t:tactic : tactic => do
+  t' ← `(tactic| $t <|> skip);
+  Lean.Elab.Tactic.evalTactic t'
+
+theorem tst (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