add test for no_inline_let pragma

FStarLang · Oct 9, 2024 · c13a1e2 · c13a1e2
1 parent 484b8f1
commit c13a1e2
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 1 deletion.
diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
@@ -2,7 +2,7 @@ FSTAR_EXAMPLES=$(realpath ../../examples)
 include $(FSTAR_EXAMPLES)/Makefile.include
 include $(FSTAR_ULIB)/ml/Makefile.include
 
-all: inline_let all_cmi Eta_expand.test Div.test
+all: inline_let all_cmi Eta_expand.test Div.test no_inline_let
 
 %.exe: %.fst | out
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
@@ -25,6 +25,11 @@ inline_let: InlineLet.fst
 	egrep -A 10 test InlineLet.ml | grep -qs "17"
 	@touch $@
 
+no_inline_let: NoInlineLet.fst
+	$(FSTAR) --codegen OCaml NoInlineLet.fst
+	diff -u --strip-trailing-cr NoInlineLet.ml.expected NoInlineLet.ml
+	@touch $@
+
 all_cmi:
 	+$(MAKE) -C cmi all
 

diff --git a/tests/extraction/NoInlineLet.fst b/tests/extraction/NoInlineLet.fst
@@ -0,0 +1,11 @@
+module NoInlineLet
+
+let test_no_inline (f: int): int =
+  [@@no_inline_let]
+  let x = f * 2 in
+  x + x
+
+[@preprocess_with (fun i -> norm [delta_only [`%test_no_inline]])]
+let test_preeprocess (f: int): int =
+  let x = test_no_inline f in
+  x
diff --git a/tests/extraction/NoInlineLet.ml.expected b/tests/extraction/NoInlineLet.ml.expected