Merge pull request #3982 from mtzguido/#check

Introduce #check pragma

Author: mtzguido

bare-tests/.gitignore

@@ -0,0 +1,2 @@
+_cache
+_output

bare-tests/Check.fst

@@ -0,0 +1,12 @@
+module Check
+
+open Prims
+
+#check 1
+#check 1+1
+
+let foo x = x
+
+#push-options "--print_implicits"
+#check foo
+#pop-options

bare-tests/Check.fst.output.expected

@@ -0,0 +1,9 @@
+* Info at Check.fst(5,0-5,8):
+  - Term 1 has type Prims.int
+
+* Info at Check.fst(6,0-6,10):
+  - Term 1 + 1 has type Prims.int
+
+* Info at Check.fst(11,0-11,10):
+  - Term Check.foo has type Prims.Tot (#_: Type -> x: _ -> Prims.Tot _)
+

bare-tests/Makefile

@@ -9,6 +9,12 @@
 FSTAR_ARGS += --no_prelude
 OTHERFLAGS += --already_cached '-Prims,-FStar,-LowStar'  # remove this which test.mk adds by default
 
+OTHERFLAGS += --warn_error -241
+# ^ When running the output rules, we may not have checked files. This
+# is since the rule in ../mk/test.mk only depends on the fst and not on
+# the computed dependencies. That should be fixed. For now, just ignore
+# warnings about missing checked files since it will mess up the output.
+
 FSTAR_ROOT ?= ..
 FSTAR_EXE ?= $(abspath $(FSTAR_ROOT)/stage1/dune/_build/default/fstarc-bare/fstarc1_bare.exe)
 export FSTAR_LIB ?= $(abspath $(FSTAR_ROOT)/ulib)

mk/diff.sh

@@ -20,7 +20,7 @@ else
   # We're gonna fail. If we're running in CI, emit a Github
   # error message.
   if [ -v GITHUB_ENV ]; then
-    DIFFTEXT=$($DIFF "$ACTUAL" "$EXPECTED" | sed 's/$/%0A/' | tr -d '\n')
+    DIFFTEXT=$($DIFF "$EXPECTED" "$ACTUAL" | sed 's/$/%0A/' | tr -d '\n')
     ACTUAL=$(realpath "$ACTUAL")
     ACTUAL="${ACTUAL#$FSTAR_ROOT}"
     EXPECTED=$(realpath "$EXPECTED")

src/ml/FStarC_Parser_LexFStar.ml

@@ -471,6 +471,7 @@ match%sedlex lexbuf with
  | "#pop-options" -> PRAGMA_POP_OPTIONS
  | "#restart-solver" -> PRAGMA_RESTART_SOLVER
  | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH
+ | "#check" -> PRAGMA_CHECK
  | "__SOURCE_FILE__" -> STRING (Filepath.basename (L.source_file lexbuf))
  | "__LINE__" -> INT (string_of_int (L.current_line lexbuf))
  | "__FILELINE__"   -> STRING (Filepath.basename (L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")")

src/ml/FStarC_Parser_Parse.mly

@@ -112,7 +112,7 @@ type tc_constraint = {
 %token IRREDUCIBLE UNFOLDABLE INLINE OPAQUE UNFOLD INLINE_FOR_EXTRACTION
 %token NOEXTRACT
 %token NOEQUALITY UNOPTEQUALITY
-%token PRAGMA_SHOW_OPTIONS PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH
+%token PRAGMA_SHOW_OPTIONS PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH PRAGMA_CHECK
 %token TYP_APP_LESS TYP_APP_GREATER SUBTYPE EQUALTYPE SUBKIND BY
 %token AND ASSERT SYNTH BEGIN ELSE END
 %token EXCEPTION FALSE FUN FUNCTION IF IN MODULE DEFAULT
@@ -224,18 +224,13 @@ startOfNextDeclToken:
 
 pragmaStartToken:
  | PRAGMA_SHOW_OPTIONS
-     { () }
  | PRAGMA_SET_OPTIONS
-     { () }
  | PRAGMA_RESET_OPTIONS
-     { () }
  | PRAGMA_PUSH_OPTIONS
-     { () }
  | PRAGMA_POP_OPTIONS
-     { () }
  | PRAGMA_RESTART_SOLVER
-     { () }
  | PRAGMA_PRINT_EFFECTS_GRAPH
+ | PRAGMA_CHECK
      { () }
 
 /******************************************************************************/
@@ -257,6 +252,8 @@ pragma:
       { RestartSolver }
   | PRAGMA_PRINT_EFFECTS_GRAPH
       { PrintEffectsGraph }
+  | PRAGMA_CHECK t=term
+      { Check t }
 
 attribute:
   | LBRACK_AT x = list(atomicTerm) RBRACK

src/parser/FStarC.Parser.AST.Diff.fst

@@ -455,6 +455,7 @@ let eq_pragma (t1 t2: pragma) =
   | PopOptions, PopOptions -> true
   | RestartSolver, RestartSolver -> true
   | PrintEffectsGraph, PrintEffectsGraph -> true
+  | Check t1, Check t2 -> eq_term t1 t2
   | _ -> false
 
 

src/parser/FStarC.Parser.AST.fst

@@ -858,6 +858,7 @@ let string_of_pragma = function
   | PopOptions -> "pop-options"
   | RestartSolver -> "restart-solver"
   | PrintEffectsGraph -> "print-effects-graph"
+  | Check t -> "check " ^ term_to_string t
 
 let restriction_to_string: FStarC.Syntax.Syntax.restriction -> string =
   let open FStarC.Syntax.Syntax in

src/parser/FStarC.Parser.AST.fsti

@@ -234,6 +234,7 @@ type pragma =
   | PopOptions
   | RestartSolver
   | PrintEffectsGraph
+  | Check of term
 
 type dep_scan_callbacks = {
    scan_term: term -> unit;