Zulip Chat Archive

Stream: lean4

Topic: Dependent Syntax


Mac (May 13 2021 at 22:37):

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 (May 13 2021 at 22:44):

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

Mac (May 13 2021 at 22:50):

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 (May 13 2021 at 22:51):

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 (May 13 2021 at 22:52):

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

Mario Carneiro (May 13 2021 at 22:52):

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 (May 13 2021 at 22:54):

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

Mac (May 13 2021 at 22:55):

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 (May 13 2021 at 22:56):

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 (May 13 2021 at 22:57):

Oh, the $cat parser already exists: parserOfStack

Mario Carneiro (May 13 2021 at 22:58):

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

Mario Carneiro (May 13 2021 at 22:59):

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

Mac (May 13 2021 at 23:08):

Mario Carneiro said:

Oh, the $cat parser already exists: parserOfStack

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

Mac (May 13 2021 at 23:10):

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 (May 13 2021 at 23:16):

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

Mario Carneiro (May 13 2021 at 23:17):

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

Mario Carneiro (May 13 2021 at 23:18):

ultimately it boils down to Environment.evalConst

Mac (May 13 2021 at 23:18):

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 (May 13 2021 at 23:20):

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 (May 13 2021 at 23:21):

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

Mario Carneiro (May 13 2021 at 23:21):

unless by local you mean a local constant

Mario Carneiro (May 13 2021 at 23:22):

which of course can't be evaluated

Mac (May 13 2021 at 23:22):

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 (May 13 2021 at 23:23):

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

Mac (May 13 2021 at 23:23):

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

Mac (May 13 2021 at 23:24):

That's master.

Mac (May 13 2021 at 23:25):

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 (May 13 2021 at 23:25):

weird, my find in files isn't working right

Mario Carneiro (May 13 2021 at 23:26):

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

Mario Carneiro (May 13 2021 at 23:26):

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

Mario Carneiro (May 13 2021 at 23:27):

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

Mario Carneiro (May 13 2021 at 23:27):

they all have representatives in the return type of find?

Mario Carneiro (May 13 2021 at 23:28):

I think constant corresponds to OpaqueVal

Mario Carneiro (May 13 2021 at 23:29):

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 (May 13 2021 at 23:30):

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

Mario Carneiro (May 13 2021 at 23:31):

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

Mac (May 13 2021 at 23:35):

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 (May 13 2021 at 23:37):

constant is a noun, not an adjective in that sentence

Mario Carneiro (May 13 2021 at 23:37):

"declarations of constants"

Mac (May 13 2021 at 23:38):

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

Mac (May 13 2021 at 23:40):

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 (May 13 2021 at 23:41):

Sure, some define multiple constants

Mario Carneiro (May 13 2021 at 23:44):

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

Mario Carneiro (May 13 2021 at 23:47):

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 (May 13 2021 at 23:47):

ah, makes sense


Last updated: Dec 20 2023 at 11:08 UTC