naming `macro_rules` expansion function

Stream: lean4

[Andrés Goens]

I'm trying to do something along the lines of @Arthur Paulino 's FxyLang parser, discussed it this other thread. He defines explicit functions to create his program's AST as an inductive type Program:

partial def mkProgram : Syntax → Except String Program
  | `(program| skip) => return Program.skip

However I want to use my embedded syntax instead, defined by macro_rules, i.e. something like

macro_rules
   | `(program| skip) => `(Program.skip)

I suppose the macro_rules macro generates some similar function to @Arthur Paulino 's mkProgram under the hood, but I can't really figure out from the Lean4 source code what that does precisely (i.e. what is matchAltExpr| |, etc) nor how it would be named/its type.

I imagine I should be able to use those functions to parse a file using the same trick (i.e. piggybacking the Lean4 parser) and at the same keep the syntax extensions, right?

[Arthur Paulino]

By using macro_rules, what you're doing is more similar to what I did on the MetaDebug.lean file. It means that, while on VSCode, editing a .lean file and seeing stuff happen in the Lean Infoview, Lean will replace skip by Program.skip and you would be able to write Fxy code in your Lean file.

The use case for mkProgram is different. It doesn't turn Lean syntax into more Lean syntax. Instead, it turns Lean syntax into a term of my end goal type (Program). This is how the real parser works, because I don't want to create a term of Program while editing a Lean file in VS Code. I want to create a term of Program while running the binary file of my compiled Fxy interpreter.

Does it make sense?

[Andrés Goens]

Yep, I understand the difference as to what the two approaches do. I guess I want to have my cake and eat it too :grinning: I want to be able to use both, so I want to be able to use my Syntax in my lean source code, which shows up in emacs (no vscode :wink: here), as well as parse it from a file I read in the file system.

My point is that macro_rules is just a macro that generates some function used by the delaborator. If we're using the lean4 parser anyway, we can also uss those macros to generate the internal data structure (AST) as well. I just want to understand what macro_rules is doing under the hood to be able to do so

[Arthur Paulino]

Then I believe you'll need to do a hack to read your source code as if you were reading Lean code. I'd advise against this solution :upside_down:

Of course it wouldn't be so simple. You would also need a way to include the right imports to have the syntax definitions, your macro_rules, your types and every other function you'd need to run your code. As well as a call to actually run the program. Then you'd write it to disk and run it as a script.

Roughly speaking, you'd programmatically generate a file similar to MetaDebug.lean and then you'd bravely run it

I can't even count the number of layers of hacks involved in this solution

[Andrés Goens]

Hm, I guess what you're suggesting is for me to create a lean file programatically and then read it, and I agree, that does sound like a hack I'd like to avoid. But I don't understand why I can't use the delaborator to parse it using the Lean 4 parser, just as you do in your code. When I write something like

macro_rules
  |  `(program| skip) => `(Program.skip)

Lean is, under the hood, generating a function very similar to your

partial def mkProgram : Syntax → Except String Program
  | `(program| skip) => return Program.skip

isn't it? Why can't I just use that?

[Mario Carneiro]

By the way if you want to "have your cake and eat it too" I would recommend doing it the other way around: use Arthur's method to get a value of type Program and then reflect it to a Syntax using a Quote Program instance. The main downside of this is that you will lose syntax metadata information like file positions, and you also can't create "non-canonical" syntax which e.g. calls functions generating Program other than the constructors (although I don't know why you would want to do this)

[Arthur Paulino]

@Andrés Goens you can't do that because macro_rules instructs the Lean compiler how to deal with Lean code. Thus you need to be running Lean code for them to take place

[Mario Carneiro]

Andrés Goens said:

Lean is, under the hood, generating a function very similar to your

partial def mkProgram : Syntax → Except String Program
  | `(program| skip) => return Program.skip

isn't it? Why can't I just use that?

No, lean is not creating anything like the second function on its own. The desugared function looks more like:

partial def mkProgram : Syntax → Except String Syntax
  | `(program| skip) => return mkNode ``Program.skip []

That is, it is creating syntax objects with references to the names Program.skip et al. Within the context of a running lean environment (which you do not have at run time without having to go to some trouble with importModules and shipping the lean library along with your binary), you can elaborate this and evaluate it using the interpreter to produce an actual Program value, but it is not easy by any stretch. It just so happens that lean is already set up to do just this when you are in the middle of evaluating a lean file, which is why this is relatively easier at compile time.

[Andrés Goens]

thanks for the explanation, that's insightful! To be fair, you also need to ship the lean library alongside your binary in the above approach, using the lean parser :sweat_smile: But I think I understand the difference, you'd need quite a bit more as you'd have to be able to parse arbitrary lean terms if you just write the macro expansion and want to parse the desugared version, compared to just using the parsing function for your terms (and no Lean terms). Is that more or less what's happening?

[Mario Carneiro]

There is a difference: if you import Lean then you are statically linking against the lean library, but if you use importModules then you are dynamically linking the lean library. Static linking is generally easier since the resulting binary is all-in-one and has all the functions you want, while dynamic linking means you need to put some dlls (well, oleans) somewhere on the user's computer and make sure you can find it

[Mario Carneiro]

Static linking also means that the linker can remove any unused functions from the binary, which is probably going to be a lot if you just use the parser