diff --git a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml index e4ef505d01f..5943d01b513 100644 --- a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml +++ b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml @@ -473,6 +473,7 @@ match%sedlex lexbuf with | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH | "__SOURCE_FILE__" -> STRING (L.source_file lexbuf) | "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false) + | "__FL__" -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")") | Plus anywhite -> token lexbuf | newline -> L.new_line lexbuf; token lexbuf diff --git a/tests/micro-benchmarks/Test.LexemeFL.fst b/tests/micro-benchmarks/Test.LexemeFL.fst new file mode 100644 index 00000000000..b289abf8a93 --- /dev/null +++ b/tests/micro-benchmarks/Test.LexemeFL.fst @@ -0,0 +1,13 @@ +/// A new lexeme __FL__ has been added to show file and line (file(line)) to make writing tests easier. +/// This file is line sensitive any edit will change the value of __FL__. +module Test.LexemeFL + +open FStar.String +module LT = FStar.List.Tot +// Kinda funky to get a good validation time test, added Strings in other PR will fix this. +// The lexer is sending back some strange character that we have to adjust. +let fl = __FL__ +let _ = assert(fl <> "") +let fl' = string_of_list (list_of_string "Test.LexemFL.fst(11)") +let _ = assert_norm((strlen fl') = 20) +let _ = assert_norm(fl' = "Test.LexemFL.fst(11)")