Dependent Syntax

Stream: lean4

[Mac]

Is there a way to get a syntax/parser to parse an element using a parser dependent on the value of a previously parsed element? For example, something like the following:

syntax "lang" cat:ident "{" $cat "}" : term

The idea in the above example is that the stuff between the braces would be parsed using the specified category cat. I doubt such a thing is available in the syntax notation, but I hope there is at least some way to write a parser that does this.

[Mario Carneiro]

It should definitely be possible if you fall to the lowest level, writing a ParserFn

[Mac]

Assuming that's true, my other two questions would be: How low do I have to go? And, would it possible for cat to be a term that can be reduced into a Name for a category?

[Mario Carneiro]

The next higher level than a ParserFn would be parser combinators, and you should be able to mostly use these with a manual parser for the $cat part

[Mario Carneiro]

I'm not sure what you mean about the term thing

[Mario Carneiro]

The parser will have available the syntax of the previously read tokens, so you can work with raw identifiers easily enough but anything involving type checking is probably not available

[Mario Carneiro]

You don't even have the macro context so you can't write arbitrary MacroM code

[Mac]

Mario Carneiro said:

anything involving type checking is probably not available

Mario Carneiro said:

You don't even have the macro context so you can't write arbitrary MacroM code

That was my curiosity, is it possible (if desired) to perform type-checking and elaboration and such during parsing? For me, the biggest thing would be resolving defs and/or expanding macros.

[Mario Carneiro]

No, that's definitely not possible (deliberately?). The parser monad is quite restricted (and not even really a monad). Resolving defs is possible though, since you have access to the environment

[Mario Carneiro]

Oh, the $cat parser already exists: parserOfStack

[Mario Carneiro]

it takes an index of the number of tokens ago where cat:ident was parsed and parses a e:cat

[Mario Carneiro]

it is used in dynamicQuot aka `(cat| bla)

[Mac]

Mario Carneiro said:

Oh, the $cat parser already exists: parserOfStack

cool, thanks! I definitely missed that while skimming through the source code.

[Mac]

Mario Carneiro said:

Resolving defs is possible though, since you have access to the environment

Any chance you could provide an example of how def resolution works?

I am still very much of a newbie when it comes to understand the inner workings of Lean. Most of what I've learned has come from searching for specific keywords and go to def'ing and then looking at the surrounding code and trying to understand it. So I am still very much missing most of the big picture.

[Mario Carneiro]

I am doing the same thing, of course. Definition lookup can be done using env.find?

[Mario Carneiro]

Oh interesting, you can evaluate things in the parser monad: evalParserConst looks up a parser definition in the environment and runs it

[Mario Carneiro]

ultimately it boils down to Environment.evalConst

[Mac]

Thanks for all the help! :)

Mario Carneiro said:

I am doing the same thing, of course.

Well, apparently, you're much better at it. XD

[Mac]

Mario Carneiro said:

Definition lookup can be done using env.find?

Mario Carneiro said:

ultimately it boils down to Environment.evalConst

Ah but constants are only imported names, correct? Not local ones.

[Mario Carneiro]

env.find? uses fully qualified names, but resolveName will resolve an unqualified name to a qualified name

[Mario Carneiro]

unless by local you mean a local constant

[Mario Carneiro]

which of course can't be evaluated

[Mac]

Yes, but the find? definition has the following comment: "It is safe to use find' because we never overwrite imported declarations." so that seems to imply that only works for imported declarations.

[Mario Carneiro]

I don't see that comment. Are you looking at an old version?

[Mac]

https://github.com/leanprover/lean4/blob/03ba945be179f73ae705191dcd5963e4dd40b84f/src/Lean/Environment.lean#L69

[Mac]

That's master.

[Mac]

I am also not sure what the difference between a "constant declaration" and and non-"constant" one is and how it connects to the de" command.

[Mario Carneiro]

weird, my find in files isn't working right

[Mario Carneiro]

Regarding imported declarations, it's talking about defs that were made in another file

[Mario Carneiro]

any additions to the environment are always attached to the current file

[Mario Carneiro]

There are lots of declarations in lean: constant,axiom, def, theorem, inductive and maybe a few I forget

[Mario Carneiro]

they all have representatives in the return type of find?

[Mario Carneiro]

I think constant corresponds to OpaqueVal

[Mario Carneiro]

constant foo : nat := 1 is like def foo : nat := 1 except the elaborator and the kernel refuse to reduce foo ~> 1, foo acts like an axiomatic constant with no definition

[Mario Carneiro]

it is basically the same as axiom foo : nat except you don't have to worry about inconsistency concerns

[Mario Carneiro]

It's also possible I'm answering entirely the wrong question, "constant" is an overloaded word in lean

[Mac]

Mario Carneiro said:

It's also possible I'm answering entirely the wrong question, "constant" is an overloaded word in lean

True! XD Yeah, I wasn't talking about constant (at least I don't think so). I was talking about the fact that find? returns ConstantInfo which the doc for describes as "information associated with constant definitions" and am wondering what the additional adjective of "constant" is meant to imply.

[Mario Carneiro]

constant is a noun, not an adjective in that sentence

[Mario Carneiro]

"declarations of constants"

[Mac]

lol, I guess technically a noun functioning as an adjective, but still a noun.

[Mac]

Mario Carneiro said:

"declarations of constants"

Yes, but my question with that is what is the difference between a constant definition and a non-constant definition. Don't all definitions define constants (especially since ConstantInfo covers defs, axioms, constants, inductive, etc.)?

[Mario Carneiro]

Sure, some define multiple constants

[Mario Carneiro]

Examples of declarations that don't define constants include notation, open, namespace,attribute

[Mario Carneiro]

ConstantInfo seems to be specifically for answering the question "what kind of declaration does this named constant come from?", which makes sense since it is the return value of find?

[Mac]

ah, makes sense