add test for no_inline_let pragma

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
 

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

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)))