search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Added __FILELINE__ and it's test file #3597

Open briangmilnes opened 3 weeks ago

briangmilnes commented 1 week ago

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

mtzguido commented 1 week ago

Hi Brian, can you do the changes we talked about here https://github.com/FStarLang/FStar/pull/3574#issuecomment-2427810488. 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 commented 1 week ago

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

briangmilnes commented 1 week ago

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 commented 1 week ago

Yet print as a string directly?