From 7d50ab4ba2f80a843946c0a19bf090c7cb4c5e66 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Sun, 11 Feb 2024 16:49:40 +1100 Subject: [PATCH] snap --- .../fstar-lib/generated/FStar_Parser_Const.ml | 2 ++ .../fstar-lib/generated/FStar_Syntax_Util.ml | 2 ++ .../generated/FStar_TypeChecker_Cfg.ml | 32 +++++++++++-------- 3 files changed, 23 insertions(+), 13 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 86a9f8374df..dde5bcc8be5 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -286,6 +286,8 @@ let (deprecated_attr : FStar_Ident.lident) = pconst "deprecated" let (warn_on_use_attr : FStar_Ident.lident) = pconst "warn_on_use" let (inline_let_attr : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "inline_let"] +let (no_inline_let_attr : FStar_Ident.lident) = + p2l ["FStar"; "Pervasives"; "no_inline_let"] let (rename_let_attr : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "rename_let"] let (plugin_attr : FStar_Ident.lident) = diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 76502672fc3..23ea6dce172 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -2393,6 +2393,8 @@ let (tcdecltime_attr : FStar_Syntax_Syntax.term) = fvar_const FStar_Parser_Const.tcdecltime_attr let (inline_let_attr : FStar_Syntax_Syntax.term) = fvar_const FStar_Parser_Const.inline_let_attr +let (no_inline_let_attr : FStar_Syntax_Syntax.term) = + fvar_const FStar_Parser_Const.no_inline_let_attr let (rename_let_attr : FStar_Syntax_Syntax.term) = fvar_const FStar_Parser_Const.rename_let_attr let (t_ctx_uvar_and_sust : FStar_Syntax_Syntax.term) = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index b9aee2a3c90..abbabab25bb 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -2172,21 +2172,27 @@ let (should_reduce_local_let : if uu___1 then true else - (let n = - FStar_TypeChecker_Env.norm_eff_name cfg1.tcenv - lb.FStar_Syntax_Syntax.lbeff in - let uu___3 = - (FStar_Syntax_Util.is_pure_effect n) && - (cfg1.normalize_pure_lets || - (FStar_Syntax_Util.has_attribute - lb.FStar_Syntax_Syntax.lbattrs - FStar_Parser_Const.inline_let_attr)) in + (let uu___3 = + FStar_Syntax_Util.has_attribute lb.FStar_Syntax_Syntax.lbattrs + FStar_Parser_Const.no_inline_let_attr in if uu___3 - then true + then false else - (FStar_Syntax_Util.is_ghost_effect n) && - (Prims.op_Negation - (cfg1.steps).pure_subterms_within_computations))) + (let n = + FStar_TypeChecker_Env.norm_eff_name cfg1.tcenv + lb.FStar_Syntax_Syntax.lbeff in + let uu___5 = + (FStar_Syntax_Util.is_pure_effect n) && + (cfg1.normalize_pure_lets || + (FStar_Syntax_Util.has_attribute + lb.FStar_Syntax_Syntax.lbattrs + FStar_Parser_Const.inline_let_attr)) in + if uu___5 + then true + else + (FStar_Syntax_Util.is_ghost_effect n) && + (Prims.op_Negation + (cfg1.steps).pure_subterms_within_computations)))) let (translate_norm_step : FStar_Pervasives.norm_step -> FStar_TypeChecker_Env.step Prims.list) = fun uu___ ->