Macro expand to hypotheses

Stream: lean4

[Alastair Horn]

Is is possible to create a macro that can be used within theorem, def, variable declarations? For example

-- Doesn't work, bracketedBinder isn't a syntax category
syntax  ident " ≤ " ident : bracketedBinder
macro_rules
  | `(($a ≤ $b)) => `(($a : Subgroup $b))

theorem subgroup_theorem {G : Type} [group G] (H ≤ G) ...

Is this an appropriate use of the macro system?

[Sebastian Ullrich]

Yes, this would be the way to do it, but as you found it's not there yet. One potential complication is that different built-in parsers use different parts of the binder syntax, so it's not quite clear what parser(s) should be made a syntax category and opened up to macro expansion.

[Alastair Horn]

Okay, thanks for your help

[Mario Carneiro]

Sebastian Ullrich said:

Yes, this would be the way to do it, but as you found it's not there yet. One potential complication is that different built-in parsers use different parts of the binder syntax, so it's not quite clear what parser(s) should be made a syntax category and opened up to macro expansion.

Why aren't all parser nonterminals syntax categories? Is there a downside to this?

[Sebastian Ullrich]

Uh, I think you're severely underestimating the number of nonterminals we have. Performance would definitely be an issue, every category is a table of parser closures indexed by first tokens and run using longestMatch, which is significantly more work than a simple parser like p1 <|> p2. But the bigger question is how to extend those nonterminals not with new syntax but with new semantics. Our current categories have dedicated semantics expressed by functions elabTerm/Level/..., where it's easy to unfold macros for the head as the very first step. But many other nonterminals are never given dedicated semantics but are simply matched against as part of a larger macro or elaborator. Recall that Lean/Racket macro expansion is top-down, not bottom-up, so it's not clear how additional macros (or even elaborators, which need to map to an appropriate "core syntax" type) should be automatically applied. Carefully designing support for additional categories manually where beneficial looks like the more realistic approach.

[Mario Carneiro]

I guess "new semantics" is already an issue for the example in the other thread: how does (~) become an ident unless it is mapped to a name? The syntax itself doesn't say how this would happen

[Mario Carneiro]

In the example here, this is resolved by expanding the new syntax to another syntax in the bracketedBinder category, is that always an option?

[Mario Carneiro]

If you wanted to support lean 3 style binders you might have ($x:ident ≤ $y:expr) -> ($x) (H : $x ≤ $y) which is not another syntax in the bracketedBinder category

[Sebastian Ullrich]

Mario Carneiro said:

In the example here, this is resolved by expanding the new syntax to another syntax in the bracketedBinder category, is that always an option?

Yes, but someone has to add that expandMacros call to (all the) right places. And it gets more complicated if you want "elaborators", whatever that should mean for the specific category.

[Sebastian Ullrich]

Mario Carneiro said:

If you wanted to support lean 3 style binders you might have ($x:ident ≤ $y:expr) -> ($x) (H : $x ≤ $y) which is not another syntax in the bracketedBinder category

Yeah, this is a good example for why adding a new category is not trivial, apart from the other binder syntax issue I mentioned in my first post.

[Mac]

Sebastian Ullrich said:

Carefully designing support for additional categories manually where beneficial looks like the more realistic approach.

Given the discussion here and in my custom identifiers thread, it seems like having binders be one of those categories would be ideal. It could allow for local mixfix and notation binding (as in my thread) while also supporting complex hypotheses (as in this thread).