[CakeML-dev] Putting line annotations on declarations
H.Feree at kent.ac.uk
Fri Mar 24 12:31:39 UTC 2017
This would mean adding a new constructor to the datatype "dec" and I'm
not sure this is a good idea as it would induce (again) a lot of changes
in the proofs.
Isn't it sufficient to take the location of the expression?
For example, in a Dletrec, you can merge the locations of the list of
expressions it is composed of. You may miss a few lines if the patterns
are not on the same line, but it is a good approximation.
We could also add location information to patterns (which can be useful
for other reasons) and you would thus get a more accurate location for
declarations, which would only be inaccurate in weird declarations like:
(where you would miss the first line)
Le 24/03/2017 à 10:21, Rikard Hjort a écrit :
> Would it be possible (and desireable) to have the parser put line
> annotations (embodied by the Lannot constructor in the ast) on
> declarations? Right now there are line annotations on expressions only.
> In working with the explorer, we often see places where line annotation
> on declarations would make sense. Sometimes expressions are generated
> directly from declaration (Lets from Dletrecs in mod_to_conScript.sml
> for example), and it would be good if we could show these as actually
> originating from those declarations. Also, I think it would make sense
> if you could see where declarations that appear in later languages
> originate in earlier languages.
> Developers mailing list
> Developers at cakeml.org
More information about the Developers