[CakeML-dev] Putting line annotations on declarations

Hugo Férée H.Feree at kent.ac.uk
Fri Mar 24 12:31:39 UTC 2017


Hi,

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:

let
x =
e in
e'

(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
> https://lists.cakeml.org/listinfo/developers



More information about the Developers mailing list