コマンドに対して、そのエラボレータを教えてくれるコマンド

[Seasawher]

メタプロ本に載っている例: https://leanprover-community.github.io/lean4-metaprogramming-book/main/07_elaboration.html#mini-project

elab "#findCElab " c:command : command => do
  let macroRes ← liftMacroM <| expandMacroImpl? (←getEnv) c
  match macroRes with
  | some (name, _) => logInfo s!"Next step is a macro: {name.toString}"
  | none =>
    let kind := c.raw.getKind
    let elabs := commandElabAttribute.getEntries (←getEnv) kind
    match elabs with
    | [] => logInfo s!"There is no elaborators for your syntax, looks like its bad :("
    | _ => logInfo s!"Your syntax may be elaborated by: {elabs.map (fun el => el.declName.toString)}"

#findCElab def lala := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab abbrev lolo := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab #check foo -- even our own syntax!: Your syntax may be elaborated by: [mySpecialCheck, Lean.Elab.Command.elabCheck]
#findCElab open Hi -- Your syntax may be elaborated by: [Lean.Elab.Command.elabOpen]
#findCElab namespace Foo -- Your syntax may be elaborated by: [Lean.Elab.Command.elabNamespace]
#findCElab #findCElab open Bar -- even itself!: Your syntax may be elaborated by: [«_aux_lean_elaboration___elabRules_command#findCElab__1»]

[spinylobster]

661 の改良版として取り込んでみました。

実装が大きくなってしまいましたが、普通に便利すぎるので標準にこんなコマンドが欲しくなりますね…

(欲を言えば、 #expand command ... のようにシンタックスカテゴリを指定できるようにできたら最強になると思うんですが、...の部分で期待するカテゴリが固定できなくなるので流石に無理そう)

import Lean

open Lean Elab Command

/-- syntax category for `#expand` -/
declare_syntax_cat macro_stx
syntax (name := macro_stx.command) command : macro_stx
syntax (name := macro_stx.tactic) tactic : macro_stx
syntax (name := macro_stx.term) term : macro_stx

elab "#print_stx" t:macro_stx : command => do
  logInfo m!"{t.raw.formatStx}"

-- `rfl` は `tactic` だけでなく `term` としても解釈可能
#check rfl

-- こういう場合、`choice`で可能性が表現されている
/-- info: (choice (macro_stx.term `rfl) (macro_stx.tactic (Tactic.tacticRfl "rfl"))) -/
#guard_msgs in #print_stx rfl

partial def getStx (stx : TSyntax `macro_stx) : (Syntax × SyntaxNodeKind) :=
  match stx.raw with
  | Syntax.node _ `choice #[_t1, t2] =>
    -- t1は多分`term`としての解釈で興味のない方なので、t2を選ぶ(ちゃんとした根拠はない)
    getStx (TSyntax.mk t2)
  | Syntax.node _ ``macro_stx.command #[t] => (t, `command)
  | Syntax.node _ ``macro_stx.tactic #[t] => (t, `tactic)
  | Syntax.node _ ``macro_stx.term #[t] => (t, `term)
  | _ => panic! "想定していないパターン"

def findElab (stx : TSyntax `macro_stx) : CommandElabM Unit := do
  let (stx', stxKind) : (Syntax × SyntaxNodeKind) := getStx stx
  let macroRes ← liftMacroM <| expandMacroImpl? (←getEnv) (@TSyntax.mk stxKind stx')
  match macroRes with
  | some (name, _) => logInfo s!"Next step is a macro: {name.toString}"
  | none =>
    let kind := stx'.getKind
    let env ← getEnv
    let elabs : List Name := match stxKind with
    | `command =>
      commandElabAttribute.getEntries env kind
      |>.map (fun el => el.declName)
    | `tactic =>
      Tactic.tacticElabAttribute.getEntries env kind
      |>.map (fun el => el.declName)
    | `term =>
      Term.termElabAttribute.getEntries env kind
      |>.map (fun el => el.declName)
    | _ => panic! "想定していないパターン"
    match elabs with
    | [] => logInfo s!"There is no elaborators for your syntax, looks like its bad :("
    | _ => logInfo s!"Your syntax may be elaborated by: {elabs}"

-- new command for both tactic and command
elab "#expand " stx:macro_stx : command => do
  let (stx', _) : (Syntax × SyntaxNodeKind) := getStx stx

  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? stx' with
  | none => findElab stx
  | some t => logInfo m!"{t}"

#expand 1
#expand 1 + 1
#expand trivial
#expand apply hoge
#expand #check hoge

[Seasawher]

パースできるかチェックするコマンドは、構文カテゴリを引数に取っていたと思います https://lean-ja.github.io/lean-by-example/Command/Declarative/Syntax.html

[Seasawher]

String を入力に取って、コマンド内でパースすればできるかも