lambdapi
lambdapi copied to clipboard
Deducteam
Do not check that a module name is a keyword
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.
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.
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.
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.
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.
But I guess that an editor can easily distinguish in a qualified identifier the path part from the name part.
Well, not when you do require ... as M. Here, M could then be a keyword, and it is standalone.