Keep track of source location information of identifiers to provide detailed error messages for type checking

[gjveltink]

I am currently working on a large specification (already 600 LOC but expected to go to at least 2000 LOC) and got the following error message.

##### PARSING SPECIFICATION #####
Reading input from file '/Users/Shared/mCRL2/Course/Examples/04. Case Studies/07. Festo/Festo/Festo_spec.mcrl2'...
type checking process specification...
The variable id:ID clashes with the user defined function id:SM_Identification -> ID.
The given specification is not a valid mCRL2 specification

In working with such a large specification, I regularly run into naming clashes during refactoring or extending the specification (as there is effectively just one name space).
I am afraid that the request for modularisation of mCRL2 might be too far-fetched for now, even though this is an interesting topic in itself, but would it be possible to at least improve the error messages such that they contain e.g. line number information?
In the case above it would be nice to know the line of the variable 'id'.

Cheers!

Gert

[gjveltink]

… one more thought on the actual error message.

Why is the parser incapable of distinguishing between the variable "id" and the function "id(…)" in the first place?
I would assume that the "lpar" in "id(…)" would be sufficient to disambiguate between the two options in this case.

Sure, if I would have defined a constant "map id: ID", then the parser would be in trouble, but also in the case above?

[mlaveaux]

I am not too familiar with the parsing and type checking aspects, but I believe parsing has succeeded at this point (where we do differentiate between identifiers and function applications). However, the error message is about type checking, where there is indeed an explicit check for whether variable names do not clash with user defined constructs. I am not sure if this is necessary or just makes further processing easier with assumptions. However, at the point of type checking we have no source information anymore.