Merge pull request #675 from lean-ja/Seasawher/issue661

expand_tactic と expand_command を統一する

Author: Seasawher

Examples/Command/Declarative/Infix.lean

@@ -51,14 +51,25 @@ open Lean
 
 def lxor (l r : Bool) : Bool := !l && r
 
-/-- コマンドをマクロ展開するコマンド -/
-elab "#expand_command " t:command : command => do
+/-- `#expand` の入力に渡すための構文カテゴリ -/
+declare_syntax_cat macro_stx
+
+-- コマンドとタクティクと項を扱える
+syntax command : macro_stx
+syntax tactic : macro_stx
+syntax term : macro_stx
+
+/-- マクロを展開するコマンド -/
+elab "#expand " t:macro_stx : command => do
+  let t : Syntax := match t.raw with
+  | .node _ _ #[t] => t
+  | _ => t.raw
   match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
 
 /-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
 #guard_msgs in
-  #expand_command infix:50 " LXOR " => lxor
+  #expand infix:50 " LXOR " => lxor
 
 end Infix --#

Examples/Command/Declarative/Postfix.lean

@@ -22,14 +22,25 @@ scoped postfix:200 "!" => factorial
 
 open Lean
 
-/-- コマンドをマクロ展開するコマンド -/
-elab "#expand_command " t:command : command => do
+/-- `#expand` の入力に渡すための構文カテゴリ -/
+declare_syntax_cat macro_stx
+
+-- コマンドとタクティクと項を扱える
+syntax command : macro_stx
+syntax tactic : macro_stx
+syntax term : macro_stx
+
+/-- マクロを展開するコマンド -/
+elab "#expand " t:macro_stx : command => do
+  let t : Syntax := match t.raw with
+  | .node _ _ #[t] => t
+  | _ => t.raw
   match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
 
 /-- info: notation:200 arg✝:200 "!" => factorial arg✝ -/
 #guard_msgs in
-  #expand_command postfix:200 "!" => factorial
+  #expand postfix:200 "!" => factorial
 
 end Postfix --#

Examples/Command/Declarative/Prefix.lean

@@ -18,14 +18,25 @@ scoped prefix:90 "⋄" => Nat.succ
 
 open Lean
 
-/-- コマンドをマクロ展開するコマンド -/
-elab "#expand_command " t:command : command => do
+/-- `#expand` の入力に渡すための構文カテゴリ -/
+declare_syntax_cat macro_stx
+
+-- コマンドとタクティクと項を扱える
+syntax command : macro_stx
+syntax tactic : macro_stx
+syntax term : macro_stx
+
+/-- マクロを展開するコマンド -/
+elab "#expand " t:macro_stx : command => do
+  let t : Syntax := match t.raw with
+  | .node _ _ #[t] => t
+  | _ => t.raw
   match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
 
 /-- info: notation:90 "⋄" arg✝:90 => Nat.succ arg✝ -/
 #guard_msgs in
-  #expand_command prefix:90 "⋄" => Nat.succ
+  #expand prefix:90 "⋄" => Nat.succ
 
 end Prefix --#

Examples/Tactic/Exists.lean

@@ -36,14 +36,25 @@ example : ∃ x : Nat, 3 * x + 1 = 7 := by
 
 open Lean
 
--- タクティクのマクロ展開を調べるためのコマンド
-elab "#expand_tactic " t:tactic : command => do
+/-- `#expand` の入力に渡すための構文カテゴリ -/
+declare_syntax_cat macro_stx
+
+-- コマンドとタクティクと項を扱える
+syntax command : macro_stx
+syntax tactic : macro_stx
+syntax term : macro_stx
+
+/-- マクロを展開するコマンド -/
+elab "#expand " t:macro_stx : command => do
+  let t : Syntax := match t.raw with
+  | .node _ _ #[t] => t
+  | _ => t.raw
   match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
   | none => logInfo m!"Not a macro"
   | some t => logInfo m!"{t}"
 
 /-- info: (refine ⟨1, 2, 3, ?_⟩; try trivial) -/
 #guard_msgs in
-  #expand_tactic exists 1, 2, 3
+  #expand exists 1, 2, 3
 
 end Exists --#