Multi commands macro

Stream: lean4

[Patrick Massot]

How can I define a macro that expands to a sequence of commands? Say I want #foo to be read as

#check Nat
#eval 1 + 1
def x := 0

[Patrick Massot]

Note my actual commands don't generate output.

[Mario Carneiro]

stop_at_first_error

[Mario Carneiro]

you can also use `(...) which is overloaded to work on commands

[Mario Carneiro]

macro "#foo" : command => `(
  #check Nat
  #eval 1 + 1
  def x := 0
)

#foo

[Patrick Massot]

Thanks! I was trying to be too specific and used `(command|...) instead of `(...)

[Patrick Massot]

While you're here, do you remember whether there was any discussion of having the ProofWidgets4 lib depend on Std?

[Mario Carneiro]

do you mean the other way around?

[Patrick Massot]

I mean I want to contribute something to ProofWidgets4 but I need something that is in Std.

[Patrick Massot]

And currently ProofWidgets4 does not require Std in its lakefile

[Patrick Massot]

which seems weird since I thought every Lean lib except for core and Std is meant to require Std.

[Patrick Massot]

The thing I need is

/-- Gets the LSP range from a `String.Range`. -/
def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }

/-- Gets the LSP range of syntax `stx`. -/
def Lean.FileMap.rangeOfStx? (text : FileMap) (stx : Syntax) : Option Lsp.Range :=
  text.utf8RangeToLspRange <$> stx.getRange?

which I think depend on nothing, so I could copy-paste, but then I would need to avoid the name clash for libs importing both Std and ProofWidgets4.

[Mario Carneiro]

Probably you should ask @Wojciech Nawrocki about that, I am not maintaining ProofWidgets

[Mario Carneiro]

It's definitely not the case that all Lean projects depend on Std; doc-gen, Qq, repl, and oleanparser are some lean projects off the top of my head that don't depend on std

[Patrick Massot]

I know you are not maintaining it, that's why I wrote "do you remember whether there was any discussion".

[Patrick Massot]

Do you think those lib try to be independent of Std or is this a historical accident?

[Mario Carneiro]

No I don't believe there has been any discussion

[Mario Carneiro]

Part of it might be that ProofWidgets might be aiming to be a dependency of Std

[Mario Carneiro]

although I don't think Std will be taking any dependencies, for user convenience, meaning that in that case Std would just absorb the whole library

[Mario Carneiro]

with the current state of things I think it would be fine to just have ProofWidgets depend on Std

[Patrick Massot]

Ok, we'll see what Wojciech say.

[Patrick Massot]

Actually the list of command thing doesn't work. Could you remind me how to ask Lean to show what macro expand to? Also stop_at_first_error is in Mathlib so I definitely cannot use it here.

[Mario Carneiro]

I don't know any good way to see macro expansions, other than finding them in the info tree (set_option trace.Elab.info true). @Sebastian Ullrich ?

[Mario Carneiro]

stop_at_first_error is very simple, it could be relocated to std. I don't know anything else that has no added behaviors; mutual ... end may work but it also has some extra stuff

[Sebastian Ullrich]

trace.Elab.step is the most direct way to debug macro expansion, though I don't know if the output is more helpful than Elab.info

[Patrick Massot]

I think I'm lost in nested macros. Is there a way to write something like

macro "mkMacro" name:str : command =>
`(macro $name : command => `(#check Nat))

do that mkMacro foo will define a macro foo expanding to #check Nat?

[Patrick Massot]

ie mkMacro foo would expand to macro "foo" : command => `(#check Nat)

[Patrick Massot]

To be clear, the part I don't know is what to put instead of $name on the second line.

[Alex Keizer]

Almost right, you just have to specify what category $name is.

macro "mkMacro" name:str : command =>
`(macro $name:str : command => `(#check Nat))

[Patrick Massot]

Thanks!

[Patrick Massot]

Next level of complexity is: what if instead of having name as an argument to my outside macro I compute a Lean.Name from other arguments. How can I turn that into a TSyntax `name?

[Patrick Massot]

Actually I have a hard time asking the right question. I have somewhere a function which looks like

open Lean Elab Tactic in
def foo (myName: Name) (myStr : String) (myOtherName : Name) (stx : Syntax) : TacticM Unit := sorry

and I want a macro like

macro "mkTactic" myStr:str myStr':str myFun:ident : command => do
  let newName : Name := .str `foo (myStr.getString ++ "_bar")
  sorry

such that mkTactic "baz" "Hello" myfun expands to elab stx:"baz" : tactic => foo `foo.baz_bar "Hello" `myfun stx

[Alex Keizer]

Names are usually turned into identifiers (ident) with the mkIdent function. But, you don't want an identifier, you want a string literal (that is what the str category means), so for that you need mkStrLit, which takes as argument a String object

[Patrick Massot]

I've tried endless random combinations of those functions without getting anywhere.

[Patrick Massot]

Could you try to do the example described above?

[Patrick Massot]

You can replace the body of foo with done for instance.

[Mario Carneiro]

import Lean

open Lean Elab Tactic
def foo (myName: Name) (myStr : String) (myOtherName : Name) (stx : Syntax) : TacticM Unit :=
  println! "called foo {myName} {myStr} {myOtherName} {stx}"

macro "mkTactic" myStr:str myStr':str myFun:ident : command => do
  let newName : Name := .str `foo (myStr.getString ++ "_bar")
  `(elab stx:$myStr:str : $(mkIdent `tactic) =>
      foo $(quote newName) $myStr':str $(quote myFun.getId) stx)

mkTactic "baz" "Hello" myfun

example : true := by
  baz -- called foo foo.baz_bar Hello myfun "baz"

[Patrick Massot]

Thanks a lot Mario! I was missing quote.