From 4b6e1bee72b81cfe1fb4345af624ce57d0de27f7 Mon Sep 17 00:00:00 2001
From: Amos Robinson <amos.robinson@gmail.com>
Date: Wed, 9 Oct 2024 15:17:02 +1100
Subject: [PATCH] add test for no_inline_let pragma

---
 tests/extraction/Makefile                |  7 ++++++-
 tests/extraction/NoInlineLet.fst         | 15 +++++++++++++++
 tests/extraction/NoInlineLet.ml.expected |  8 ++++++++
 3 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/extraction/NoInlineLet.fst
 create mode 100644 tests/extraction/NoInlineLet.ml.expected

diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
index 84952c9372c..c7b546a16df 100644
--- 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
new file mode 100644
index 00000000000..48d0c90996a
--- /dev/null
+++ b/tests/extraction/NoInlineLet.fst
@@ -0,0 +1,15 @@
+module NoInlineLet
+open FStar.Tactics
+
+let test_no_inline (f: int): int =
+  (* this one shouldn't be inlined in tactics or extraction *)
+  [@@no_inline_let]
+  let x = f + 1 in
+  (* this one will be inlined by the norm tactic in the below test *)
+  let y = x + 2 in
+  y + y
+
+[@@(postprocess_with (fun _ -> norm [delta_only [`%test_no_inline]]; trefl ()))]
+let test_postprocess (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
new file mode 100644
index 00000000000..ea507f656af
--- /dev/null
+++ b/tests/extraction/NoInlineLet.ml.expected
@@ -0,0 +1,8 @@
+open Prims
+let (test_no_inline : Prims.int -> Prims.int) =
+  fun f ->
+    let x = f + Prims.int_one in let y = x + (Prims.of_int (2)) in y + y
+let (test_postprocess : Prims.int -> Prims.int) =
+  fun f ->
+    let x = f + Prims.int_one in
+    (x + (Prims.of_int (2))) + (x + (Prims.of_int (2)))
\ No newline at end of file