Zulip Chat Archive

Stream: lean4

Topic: Macro expand to hypotheses


view this post on Zulip Alastair Horn (Apr 15 2021 at 02:24):

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?

view this post on Zulip Sebastian Ullrich (Apr 15 2021 at 07:25):

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.

view this post on Zulip Alastair Horn (Apr 15 2021 at 10:01):

Okay, thanks for your help

view this post on Zulip Mario Carneiro (Apr 15 2021 at 20:37):

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?

view this post on Zulip Sebastian Ullrich (Apr 16 2021 at 07:47):

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.

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:04):

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

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:05):

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

view this post on Zulip Mario Carneiro (Apr 16 2021 at 08:07):

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

view this post on Zulip Sebastian Ullrich (Apr 16 2021 at 08:08):

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.

view this post on Zulip Sebastian Ullrich (Apr 16 2021 at 08:08):

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.

view this post on Zulip Mac (Apr 16 2021 at 19:26):

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).


Last updated: May 18 2021 at 23:14 UTC