Zulip Chat Archive

Stream: lean4

Topic: Typed Macro Issues?


François G. Dorais (Jun 29 2022 at 21:33):

I'm running into a couple of issues updating code after the "Typed Macro" update. I managed to fix them all so far but I'm puzzled by some of the solutions.

For example, this macro:

macro "mwe" name:ident rest:tacticSeq : tactic => `(tactic| intro $name:ident; ($rest))

Doesn't work without specifying $name:ident on the RHS. It seems like intro expects a matchAlt argument by default instead of an ident. This is probably a bug.

The parentheses around $rest are also necessary for some reason. This might be a feature but I don't understand why this is necessary.

Sebastian Ullrich (Jun 29 2022 at 21:48):

Thanks for the feedback! The intro issue is an artifact resulting from the fact that there are actually two separate intro tactics, for idents and for matchAlts, would be feasible but maybe a bit complex to make that still work. The second issue is "technically correct", without parentheses Lean expects a single tactic at that point. We could define a coercion to insert the parentheses for us.

François G. Dorais (Jun 29 2022 at 22:13):

Thanks Sebastian! That makes sense. The $rest issue makes total sense now. It would be convenient to have a coercion since I had quite a few cases of that to fix.

Thanks for the explanation of the intro issue! Is this an instance "the matchAlt case is tried before the ident case because the matchAlt case was defined last" or is it more complex than that?

Sebastian Ullrich (Jun 30 2022 at 07:58):

intro $name is in fact parsed into a choice node of both tactics

     [(choice
       (Tactic.intro "intro" [(term.pseudo.antiquot "$" [] `name [])])
       (Tactic.introMatch "intro" (Term.matchAlts.antiquot "$" [] `name [])))

We would have to select and generate the correct alternative given name : TSyntax [`term, `matchAlt]


Last updated: Dec 20 2023 at 11:08 UTC