search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
269 stars 35 forks source link

Do not check that a module name is a keyword #187

Open fblanqui opened 5 years ago

fblanqui commented 5 years ago

https://github.com/Deducteam/lambdapi/blob/3b25ff1cfec2b65f37a9199c349eeded7f3888d3/src/parser.ml#L238 Currently a module name must be any_ident, that is, an escaped_ident or a regular_ident but regular_ident must be different from keywords: https://github.com/Deducteam/lambdapi/blob/3b25ff1cfec2b65f37a9199c349eeded7f3888d3/src/parser.ml#L223 This exclude filenames like set, simpl, intro, proof, etc. I see no reason for such a restriction.

fblanqui commented 5 years ago

@rlepigre : would you have time to take care of this issue?

rlepigre commented 5 years ago

I really don't think that we should "fix" this, because syntax coloring would then become quite hard. Reserving keywords is really the good way to go I think.

fblanqui commented 5 years ago

I disagree. Identifiers should be different from keywords. But there is no reason to do this for module names since they are not first-class objects and are used to qualify identifiers only, and not as identifiers. I don't think that there is such restrictions in other languages/systems.

rlepigre commented 5 years ago

Yes, there is a distinction in other languages: modules cannot usually start with a lowercase letter (e.g., in OCaml). However, in our case that would make the possibility of qualification of modules to reflect the file system more complex. On approach to mitigate the problem is to always name your files starting with an uppercase letter. This way there would be no clash as our keywords all start with a lowercase letter. However, I don't think we want to impose that.

rlepigre commented 5 years ago

And there is a reason: the one I gave above. Which is in fact a very important reason, and you should agree since you known that having a good editor mode is important.

fblanqui commented 5 years ago

But I guess that an editor can easily distinguish in a qualified identifier the path part from the name part.

rlepigre commented 5 years ago

Well, not when you do require ... as M. Here, M could then be a keyword, and it is standalone.

fblanqui commented 5 years ago

It occurs after "as".

rlepigre commented 5 years ago

With a possible comment in the middle.