Added __FILELINE__ and it's test file

[briangmilnes]

No description provided.

[briangmilnes]

Guido can you put this in so I can put out Flog and Final please?

[mtzguido]

Hi Brian, can you do the changes we talked about here #3574 (comment). It should return only the basename of the file (no leading directory components) and then the test would work without anything fancy (string_of_list, etc)

[briangmilnes]

All good, rebuild and retested just to be sure.
But it still needs the list_of_string/string_of_list.
Good enough?

[briangmilnes]

I tried to move the string code changes into FStarC_Parser_LexFStar with
| "FILELINE" -> STRING (
let fl = ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")") in
let lfl = BatList.init (BatUTF8.length fl) (fun i -> BatUChar.code (BatUTF8.get fl i)) in
let sfl = BatUTF8.init (BatList.length lfl) (fun i -> BatUChar.chr (BatList.at lfl i)) in
sfl)

but when I

let fl1 = FILELINE in
print_string("|" ^ FILELINE ^ "|" ^ (strlen fl1) ^ "\n");

strlen says F* is typing fl1 as a nat.

Any idea how a STRING () lexeme can end up gettting typed as a nat?

[briangmilnes]

Yet print as a string directly?