Defining syntax

Stream: lean4

[Dan Velleman]

I decided to try to implement the assume syntax in Lean 4. The following seems to work:

syntax "assume" ident " : " term ", " term : term
syntax "assume" ident ", " term : term
macro_rules
  | `(assume $v:ident : $t:term, $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident, $b:term) => `(fun $v => $b)

But it has one unfortunate feature: it requires a comma after the assumption. This seems inconsistent with the syntax used in other situations--for example, have and suffices don't require commas. So is there a way to get rid of the comma? Simply leaving it out of the syntax and macro_rules doesn't seem to work, but I'm not sure why. (Does Lean have trouble parsing two terms in a row with no delimiter between them?)

[Wojciech Nawrocki]

Does Lean have trouble parsing two terms in a row with no delimiter between them?

Yes, foo bar is parsed as a function application. If you know something specific about the first term, e.g. that it's just one identifier you could write ident term and that should parse as two things (I think), but in general term term is not going to work.

[Dan Velleman]

That makes sense. But then how do have and suffices get parsed with no delimiter at the end?

[Mario Carneiro]

it's not that they have no delimiter, the delimiter is allowed to be newline

[Dan Velleman]

So can I require newline as a delimiter in my syntax? How do I do that?

[Mario Carneiro]

actually, the way have does it is using withPosition

[Dan Velleman]

I'm not familiar with withPosition. Where do I learn about that?

[Mario Carneiro]

This almost works, except that the last one probably shouldn't be accepted:

import Lean

syntax withPosition("assume" ident " : " term ", "?) term : term
syntax withPosition("assume" ident ", "?) term : term
macro_rules
  | `(assume $v:ident : $t:term $[,]? $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident $[,]? $b:term) => `(fun $v => $b)

#check assume x : List Nat
       x
#check assume x : List Nat,
       x
#check assume x : List Nat, x
#check assume x
       x
#check assume x,
       x
#check assume x, x
#check assume x x

[Arthur Paulino]

The API is still missing documentation, but this thread helped me with withPosition

[Mario Carneiro]

Here's a version using the new checkLinebreakBefore combinator:

import Lean

def Lean.Parser.commaOrLinebreak : Parser := ", " <|> checkLinebreakBefore >> pushNone
syntax withPosition("assume" ident " : " term Lean.Parser.commaOrLinebreak) term : term
syntax withPosition("assume" ident Lean.Parser.commaOrLinebreak) term : term
macro_rules
  | `(assume $v:ident : $t:term, $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident : $t:term
      $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident, $b:term) => `(fun $v => $b)
  | `(assume $v:ident
      $b:term) => `(fun $v => $b)

#check assume x : List Nat
       x
#check assume x : List Nat,
       x
#check assume x : List Nat, x
#check assume x
       x
#check assume x,
       x
#check assume x, x
#check assume x x -- fails

[Leonardo de Moura]

@Mario Carneiro You can also use

syntax withPosition("assume" ident " : " term (", " <|> linebreak)) term : term
syntax withPosition("assume" ident (", " <|> linebreak)) term : term

[Mario Carneiro]

ah, I was just about to suggest the addition of such a linebreak

[Leonardo de Moura]

You also don't need the extra rules. The following is sufficient.

macro_rules
  | `(assume $v:ident : $t:term , $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident , $b:term) => `(fun $v => $b)

[Leonardo de Moura]

We don't have good documentation for this yet, but Sebastian's PR https://github.com/leanprover/lean4/pull/1226 has several relevant remarks.

[Mario Carneiro]

When using linebreak instead of my hand-rolled version, I'm getting some weird parse results on the ones that use the line break

import Lean

syntax withPosition("assume" ident " : " term (", " <|> linebreak)) term : term
syntax withPosition("assume" ident (", " <|> linebreak)) term : term
macro_rules
  | `(assume $v:ident : $t:term, $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident, $b:term) => `(fun $v => $b)

#check assume x : Nat
       x -- x is colored like text
-- fun x => sorryAx (?m.1038 x) true : (x : Nat) → ?m.1038 x

#check assume x : Nat,
       x  -- x is colored like a variable
-- fun x => x : Nat → Nat

[Leonardo de Moura]

@Mario Carneiro Thanks for reporting. I will investigate it.

[Mario Carneiro]

Leonardo de Moura said:

You also don't need the extra rules. The following is sufficient.

macro_rules
  | `(assume $v:ident : $t:term , $b:term) => `(fun ($v : $t) => $b)
  | `(assume $v:ident , $b:term) => `(fun $v => $b)

How does this work? Is this something in linebreak that causes it to produce a comma, or some magic in the pattern matcher?

[Leonardo de Moura]

Sebastian wrote about this here: https://github.com/leanprover/lean4/pull/1226#discussion_r899029212

[Leonardo de Moura]

The remark also makes it clear what is missing in the example above. The linebreak parser is not adding the pushNone

[Sebastian Ullrich]

group(linebreak) should work

[Leonardo de Moura]

Sebastian Ullrich said:

group(linebreak) should work

Yes, it should, but it looks too bizarre. I was writing a PR that changes the semantics of linebreak to include pushNone.

[Leonardo de Moura]

It feels like parsers such as (", " <|> linebreak) will be heavily used from now on when defining syntax such as assume.

[Sebastian Ullrich]

And that's not the only caveat. linebreak linebreak does not check for two linebreaks.

[Sebastian Ullrich]

Not sure if there are any macros out there that depend on ws being nullary

[Leonardo de Moura]

Sebastian Ullrich said:

And that's not the only caveat. linebreak linebreak does not check for two linebreaks.

Yes, this is not nice :( Another item for https://github.com/leanprover/lean4/issues/638?

[Mario Carneiro]

For the (", " <|> linebreak) case, perhaps orLinebreak(", ") is better to combine the pushNone behavior with the delimiter

[Sebastian Ullrich]

Sebastian Ullrich said:

And that's not the only caveat. linebreak linebreak does not check for two linebreaks.

If we wanted to fix this, we may want to generate an empty token after all

[Mario Carneiro]

Sebastian Ullrich said:

And that's not the only caveat. linebreak linebreak does not check for two linebreaks.

I'm kind of okay with the current behavior, perhaps it just needs a clearer name like checkLinebreakBefore

[Mario Carneiro]

alternatively, it could take an optional parameter like linebreak(2) to check for 2 linebreaks in the previous whitespace

[Sebastian Ullrich]

Leonardo de Moura said:

Sebastian Ullrich said:

group(linebreak) should work

Yes, it should, but it looks too bizarre

Let's fix this properly, once and for all https://github.com/leanprover/lean4/pull/1229