expected "prelude", got "prelude"

Stream: lean4

[Mario Carneiro]

#check (`(Parser.Module.prelude| prelude) : MacroM Syntax)
                              -- ^^^^^^^ expected 'prelude'

Is this an issue involving whether prelude is lexed as a token or an identifier? I notice that it's not a keyword in normal usage.

[Mario Carneiro]

same thing happens with `(Parser.Module.import| import $stx:ident)

[Mac]

I think the problem you're having here is that the module header is not parsed the same as the rest of the module. So I am not surprised that quotations don't work for it.

[Mac]

On the other hand, the header parser does look like a normal parser, so I can get why one would think they would work normally.

[Mac]

Looking deeper, the exact problem seems to be that, by default, "prelude" and "import" are not part of the token list except in the special case of parsing the module header. This line here calls Module.updateTokens which adds the header tokens to the token table as can be see in its definition here. Thus, everywhere else, the prelude and import (and runtime) tokens do not exist, so you can't use them.

[Wojciech Nawrocki]

Btw you probably know this already, but you can hack around this with `(Parser.Module.prelude| $(mkAtom "prelude")). Or not, that doesn't create the right node.

[Mac]

@Wojciech Nawrocki This appears to work:

import Lean
open Lean
def prelude : MacroM Syntax := `(Parser.Module.prelude|
  $(mkNode ``Lean.Parser.Module.prelude #[mkAtom "prelude"]))

(You just need to give it the proper kind manually.)

[Mario Carneiro]

sure, but at that point you may as well just write mkNode ``Lean.Parser.Module.prelude #[mkAtom "prelude"], the quotation is useless

[Mario Carneiro]

(that's what I'm doing atm)

[Mac]

Mario Carneiro said:

sure, but at that point you may as well just write mkNode ``Lean.Parser.Module.prelude #[mkAtom "prelude"], the quotation is useless

True :rolling_on_the_floor_laughing:. I just used the quotation because I wanted to make sure the quotation parser accepted the node.

[Mario Carneiro]

I'm not sure it actually shows that, because I think you can always use `(parser| $stx) and it will just be a no-op

[Mario Carneiro]

the syntax will be in whatever kind is the one expected by the given parser

[Mac]

I thought that might be the case, but @Wojciech Nawrocki example showed that it does do some checking as a simple atom was not atomically wrapped in the parser kind.

[Mario Carneiro]

that's what I mean, it's a no op

[Mario Carneiro]

it doesn't know anything about what stx is, so it assumes that it has whatever kind it's supposed to be producing

[Mac]

Mario Carneiro said:

it doesn't know anything about what stx is, so it assumes that it has whatever kind it's supposed to be producing

My point was that it did not assume that about the atom, it specifically said that it wasn't what is was expected. That is, if it was just a no-op, I would expect it to accept (Parser.Module.prelude| $(mkAtom "prelude")) since there is nothing wrong type-wise with that. It must be doing at least some form of checking to error there but not in the node case.

[Mario Carneiro]

This works though, and produces malformed syntax

import Lean
open Lean
def prelude : MacroM Syntax := `(Parser.Module.prelude| $(mkAtom "prelude"))
#print prelude

[Mac]

Weird, I was getting an error earlier. It was probably just some unrelated syntax mistake I had made that I thought was quotation. XD