[Ur] Obtaining location information

[Adam Chlipala]

It shouldn't be too involved to produce whatever well-typed Ur 
expressions you want to represent locations.

On 03/16/2015 07:40 PM, Sergey Mironov wrote:
> 2015-03-16 3:29 GMT+03:00 Adam Chlipala <adamc at csail.mit.edu>:
>> Let's see if I understand right: you want some token you can write in source
>> code, to be replaced at compile time by the location of the token, along the
>> lines of C's __FILE__ and __LINE__.
> Yes, exactly!
>
>> Yes, it sounds like an easy feature to add.  I would actually do it entirely
>> in the parser.  I'd extend src/urweb.lex with a production for a new
>> reserved identifier for this 'macro', and I'd extend one of the expression
>> nonterminals in src/urweb.grm with a rule that translates the source
>> location of said token into an Ur/Web string literal, using
>> [ErrorMsg.spanToString], getting ahold of the span in the same way that it
>> is already being produced to label each expression with its location for
>> purposes of later error messages.
> The only note from me: I plan to build source urls using the location
> information, so it's better to have an access to line/character
> position as integers. String representation would probably require
> writing a parser  (which is still better than nothing, of cause!)