Reserved characters in macro rules?

Stream: general

[Cayden Codel]

I'm trying to write syntax/macro rules for a data format similar to JSON. In this format, unordered lists of data (i.e., multisets) are enclosed in double angle brackets (<< ... >>) in the same way that lists are enclosed in square brackets ([ ... ]). Writing a syntax for this is simple enough:

import Lean.Syntax

inductive JsonLike
  | bool (b : Bool)
  | multiset (elems : Array JsonLike)
  -- | ...     -- Other cases here

declare_syntax_cat jsonlike (behavior := symbol)
syntax "true" : jsonlike
syntax "false" : jsonlike
-- Other rules for lists, objects, identifiers
syntax "<<" jsonlike,*,? ">>" : jsonlike
syntax "jsonlike% " jsonlike : term

However, I'm having trouble writing a macro_rules for the double angle brackets syntax:

macro_rules
| `(jsonlike% true)  => `(JsonLike.bool Bool.true)
| `(jsonlike% false) => `(JsonLike.bool Bool.false)
| `(jsonlike% <<$[$xs],*>>) => `(JsonLike.multiset #[$[jsonlike% $xs],*])

Lean gives the error unexpected token '<'; expected jsonlike. It seems like '<' is a reserved character for macro rules. Is there any way to include them?

(These syntax/macro rules are largely copied from Lean.Data.Json.Elab.)

[Thomas Murrills]

I think the issue is simply the (behavior := symbol) on declare_syntax_cat! :)

[Cayden Codel]

So it is - removing it fixed the issue.

What does (behavior := symbol) do? I copied this over from Lean.Data.Json.Elab without knowing what it does :sweat_smile:

[Thomas Murrills]

Hmm, the docstrings on Parser.LeadingIdentBehavior constructors aren’t much help to me, since they don’t tell me when we’d want one or the other (besides something about avoiding creating a reserved symbol for each tactic). It is possible that you do want behavior := symbol, and that this should actually be fixed another way! Someone who is more familiar with how this particular knob works will probably have a more reliable answer… :)

[Cayden Codel]

Well it looks like I have a patch for now. Thanks!

[Notification Bot]

Cayden Codel has marked this topic as resolved.

[Thomas Murrills]

This might be worth investigating further, though, because e.g. that true’s might leak into generic parsing of true; it should probably be a non reserved symbol (&"true") but that breaks the macro rules too. (Maybe behavior := symbol helps do this without & somehow?)

[Thomas Murrills]

Another option is to leave behavior := symbol as is and write

syntax atomic("<<") jsonlike,* ">>" : jsonlike

I did this on a hunch that this would try to parse << “at the same level” as < (i.e. sort of as though it was a single token) as parsing < instead of << seemed to be the issue.

[Thomas Murrills]

This is probably safer, as it seems it won’t expose true and false to the world as jsonlikes, but I’m still surprised at the behavior and interaction with behavior := symbol—mainly because < cannot be part of an ident, so I don’t understand why LeadingIdentBehavior is even relevant.

[Notification Bot]

Kunil Lee has marked this topic as unresolved.