Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/v…

…alidation-time with a Test.LexemeFL.fst that checks __FL__

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

tests/Makefile

@@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
 ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += validation-time
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))

tests/validation-time/Makefile

@@ -0,0 +1,22 @@
+#
+# This does nothing but the default validation as these are validation time test modules.
+# Most are let _ = assert(...) which is extremely cool to test at validation time! 
+# 
+
+WARN_ERROR=--warn_error -321
+FSTAR_HOME=../..
+FSTAR_FILES=$(wildcard *.fst)
+FSTAR_EXAMPLES=$(realpath ../../examples)
+include $(FSTAR_EXAMPLES)/Makefile.include
+
+all: verify-all
+
+include $(FSTAR_HOME)/examples/Makefile.common
+
+verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+
+clean:
+	$(call msg, "CLEAN")
+	$(Q)rm -f .depend
+	$(Q)rm -rf _cache
+	$(Q)rm -rf _output

tests/validation-time/README.md

@@ -0,0 +1,5 @@
+
+  This directory contains tests that run on Make all which only validate F* files.
+ This allows validation time tests. If any validation fails, the file's tests fail.
+
+  Tests for an F* module FStar.M can be named Test.FStar.M.fst by default.

tests/validation-time/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.Tactics.V2
+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((strlen fl') = 20) by compute()
+let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()