Stuck defining custom syntax

Stream: lean4

[Yuri de Wit]

I am trying to implement a custom syntax in Lean for the first time.

I am stuck on one problem: I would like to reuse rule_ctr in two different contexts so I extracted out its definition from the rule_term into its own syntax cat. However, when implementing rule_term with macro_rules, how do I delegate to the rule_ctr macro_rules?

Right now I get: expected 'numLit', 'rule_term' or numeral

Here is a #MWE (see HERE! for where the error occurs):

-- Syntax
-- ------

-- rule ::=
-- | rule_ctr = rule_term
declare_syntax_cat rule

-- rule_ctr ::=
-- | (ctr term term ...)      # a constructor
declare_syntax_cat rule_ctr

-- rule_term ::=
-- | λvar. term               # a lambda
-- | (term term)              # an application
-- | rule_ctr
-- | num                      # a machine int
-- | let var = term; term     # a local definition
declare_syntax_cat rule_term

-- rule_ctr
--
syntax (name := rule_ctr) "(" ident rule_term* ")" : rule_ctr
macro_rules
| `(rule_ctr| ( $name $arg* )) => sorry

-- rule_term
--
syntax (name := rule_term_lam) "λ" ident "." rule_term : rule_term
syntax (name := rule_term_app) "(" rule_term rule_term ")" : rule_term
syntax (name := rule_term_ctr) rule_ctr : rule_term
syntax (name := rule_term_num) num : rule_term
syntax (name := rule_term_let) "let" ident "=" rule_term rule_term : rule_term
macro_rules
| `(rule_term| λ $var . $term:rule_term) => sorry
| `(rule_term| ( $name:rule_term $arg:rule_term )) => sorry
| `(rule_term| $ctr:rule_ctr ) => sorry       -- <==== HERE!
| `(rule_term| $lit:num) => sorry
| `(rule_term| let $name:ident = $expr:rule_term $body:$rule_term ) => sorry

-- rule
--
syntax rule_ctr "=" rule_term : rule
macro_rules
| `(rule| ( $name $arg * ) = $term:rule_term) => sorry


-- translation from rules to terms
--
syntax "[rules|" rule* "]" : term
macro_rules
| `([rules| $rs:rule* ]) => sorry

[Yuri de Wit]

Humm, or maybe I dont need to explicitly do this in rule_term?

[Sebastian Ullrich]

There is some confusion between the syntax category rule_ctr and the syntax declaration of the same name. You should not use syntax categories if you don't plan to extend them with more than one syntax declaration, use a syntax abbreviation instead:

syntax rule_ctr := "(" ident rule_term* ")"

[Sebastian Ullrich]

You also do not usually need to name syntax declarations

[Yuri de Wit]

Thanks for the feedback.

(1) "There is some confusion between the syntax category rule_ctr and the syntax declaration of the same name" - I see! Sorry, I missed that.

(2) I see that there is one difference betweensyntax rule_ctr := "(" ident rule_term* ")" and syntax "(" ident rule_term* ")" : rule_ctr in the elaborated term: the first uses Lean.ParserDescr.nodeWithAntiquot and the second Lean.ParserDescr.node. Did I just gained the ability to antiquote rule_ctr by using your suggestion?

(3) This seems to be a good rule of thumb: "should not use syntax categories if you don't plan to extend them with more than one syntax declaration".

(4) One consequence of this change to syntax rule_ctr := "(" ident rule_term* ")" is that the compiler rejects:

macro_rules
| `(rule_ctr| ( $name:ident $args:rule_term* )) => sorry

with expected rule_ctr.

[Sebastian Ullrich]

2) Syntax categories are also valid antiquotation kinds, so there's not really any change compared to a single-rule category
4) This is true, but is it even the case that you want the same expansion of rule_ctr in both places in the grammar?

[Yuri de Wit]

Sebastian Ullrich said:

4) This is true, but is it even the case that you want the same expansion of rule_ctr in both places in the grammar?

I will have to think about this probably as I go through with this. But initially, I thought that the rule_ctr would always construct the same term and so I could avoid duplicating the macro_rules item. But it is not that important except understanding/learning.

[Sebastian Ullrich]

Since you already have a `[rules| ] interpretation construct, I assume your syntax will expand as part of such macros, not by itself, in which case it shouldn't matter whether rule_ctr is a category or not.

[Yuri de Wit]

Ok, making progress.

How do I create a quoted $name? I.e. for a constructor (Add 1 2) I would like to create a syntax transformer that generates Term.Ctr "Add" ...:

| `(rule_ctr| ( $name:ident $args:rule_term* )) => `(Term.Ctr $name #[$args,*])

[Yuri de Wit]

This did it:

| `(rule_ctr| ( $name:ident $args:rule_term* )) => `(Term.Ctr $(Lean.quote name.getId.toString) #[$args,*])