newline in syntax and macro

Stream: new members

[Mark Aagaard]

I would like to use a newline as a delimiter in a syntax / macro_rule pair, but am having trouble figuring out to enter newline into the syntax rules.

Here's a very artificial MWE.

1. Without any delimiter between $t1 and "{", the parser can't detect the end of $t1.

syntax "foo" term "{" term "}": term

macro_rules
  | `( foo $t1:term { $t2:term } ) => `( $t )
--                               ^ unexpected token ')'; expected '{'

2. Using ";" as a delimiter is successful:

syntax "foo2" term ";" "{" term "}" : term

macro_rules
  | `( foo2 $t1:term ; { $t2:term } ) => `( $t1 )
-- this works, but I'd prefer a newline rather than ";"

3. Some attempts to use a newline instead of ";"

syntax "foo3" term "\n" "{" term "}" : term
-- invalid parser '«termFoo3_{_}»', invalid empty symbol
syntax "foo4" term '\n' "{" term "}" : term
--            ^ unexpected token; expected ':'
 ```

-mark

[Mario Carneiro]

the problem with (1) is that t1 {t2} is already syntax for a term, namely t1 is a function and it is being applied to {t2} which is a set with one element t2

[Mario Carneiro]

so lean parses the whole thing as a term and then says it's still waiting to see a {

[Mario Carneiro]

if you want to block this parse you have to raise the precedence of the first term higher than application

[Mario Carneiro]

e.g.

syntax "foo" term:max "{" term "}": term

[Mario Carneiro]

You can't use "\n" directly as a token because it's whitespace, but there is a linebreak parser you can use there instead

[Mario Carneiro]

it has a similar issue with precedence though. Here's a working version combining both things:

syntax "foo4" term:arg linebreak "{" term "}" : term
macro_rules
  | `( foo4 $t1:term
            { $t2:term } ) => `( $t1 $t2 )

[Mark Aagaard]

Thanks, Mario. Your answer makes sense. I'm working on getting your solutions to work in my actual code. My MWE might have been too minimal.
-mark

[Mark Aagaard]

Mario,

Thanks for the info. I was able to use your suggestion and found the right place to insert :max to get the effect I want.

-mark