Add [@@no_inline_let] annotation

src/parser/FStar.Parser.Const.fst

@@ -352,6 +352,7 @@ let steps_unmeta        = psconst "unmeta"
 let deprecated_attr = pconst "deprecated"
 let warn_on_use_attr = pconst "warn_on_use"
 let inline_let_attr = p2l ["FStar"; "Pervasives"; "inline_let"]
+let no_inline_let_attr = p2l ["FStar"; "Pervasives"; "no_inline_let"]
 let rename_let_attr = p2l ["FStar"; "Pervasives"; "rename_let"]
 let plugin_attr     = p2l ["FStar"; "Pervasives"; "plugin"]
 let tcnorm_attr    =  p2l ["FStar"; "Pervasives"; "tcnorm"]

src/syntax/FStar.Syntax.Util.fst

@@ -1008,6 +1008,7 @@ let tac_opaque_attr = exp_string "tac_opaque"
 let dm4f_bind_range_attr = fvar_const PC.dm4f_bind_range_attr
 let tcdecltime_attr = fvar_const PC.tcdecltime_attr
 let inline_let_attr = fvar_const PC.inline_let_attr
+let no_inline_let_attr = fvar_const PC.no_inline_let_attr
 let rename_let_attr = fvar_const PC.rename_let_attr
 
 let t_ctx_uvar_and_sust = fvar_const PC.ctx_uvar_and_subst_lid

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -431,13 +431,15 @@ let should_reduce_local_let cfg lb =
   else if cfg.steps.pure_subterms_within_computations &&
           U.has_attribute lb.lbattrs PC.inline_let_attr
   then true //1. we're extracting, and it's marked @inline_let
+  else if U.has_attribute lb.lbattrs PC.no_inline_let_attr
+  then false //Or, 2. do not unfold as it's explicitly marked as @no_inline_let
   else
     let n = Env.norm_eff_name cfg.tcenv lb.lbeff in
     if U.is_pure_effect n &&
        (cfg.normalize_pure_lets
         || U.has_attribute lb.lbattrs PC.inline_let_attr)
-    then true //Or, 2. it's pure and we either not extracting, or it's marked @inline_let
-    else U.is_ghost_effect n && //Or, 3. it's ghost and we're not extracting
+    then true //Or, 3. it's pure and we are either not extracting, or it's marked @inline_let
+    else U.is_ghost_effect n && //Or, 4. it's ghost and we're not extracting
          not (cfg.steps.pure_subterms_within_computations)
 
 let translate_norm_step = function

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

ulib/FStar.Pervasives.fst

@@ -141,6 +141,8 @@ let rec false_elim #_ _ = false_elim ()
 
 let inline_let = ()
 
+let no_inline_let = ()
+
 let rename_let _ = ()
 
 let plugin _ = ()

ulib/FStar.Pervasives.fsti

@@ -847,6 +847,12 @@ type __internal_ocaml_attributes =
     size. *)
 val inline_let : unit
 
+(** The [no_inline_let] attribute on a local let-binding prevents the
+    normalizer from unfolding the definition of a local let-binding. This
+    attribute can be useful when processing definitions with tactics, as
+    otherwise the normalizer will eagerly unfold all pure definitions. *)
+val no_inline_let : unit
+
 (** The [rename_let] attribute support a form of metaprogramming for
     the names of let-bound variables used in extracted code.