From bbb44475e5237b59b5167315182b5d40f5b0cb6a Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Oct 2024 22:03:37 -0700 Subject: [PATCH 1/2] Snapshotting the environment is linear in the number of defns; only do it when necessary! --- src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index 5058b212490..df23e6017a6 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -3645,12 +3645,6 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = List.filter (fun at -> Option.isNone (get_fail_attr1 false at)) ats in - // The `fail` attribute behaves - // differentrly! We only keep that one on the first new decl. - let env0 = Env.snapshot env |> snd in (* we need the snapshot since pushing the let - * will shadow a previous val *) - - (* If this is an expect_failure, check to see if it fails. * If it does, check that the errors match as we normally do. * If it doesn't fail, leave it alone! The typechecker will check the failure. *) @@ -3659,6 +3653,12 @@ and desugar_decl_maybe_fail_attr env (d: decl): (env_t & sigelts) = let attrs = U.deduplicate_terms attrs in match get_fail_attr false attrs with | Some (expected_errs, lax) -> + // The `fail` attribute behaves + // differentrly! We only keep that one on the first new decl. + let env0 = + Env.snapshot env |> snd (* we need the snapshot since pushing the let + * will shadow a previous val *) + in let d = { d with attrs = [] } in let errs, r = Errors.catch_errors (fun () -> Options.with_saved_options (fun () -> From 5a2ee1967dfabdf66a76a8c3b4c3e903abaa0851 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 10:16:03 -0700 Subject: [PATCH 2/2] snap --- ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml index 8d8f4c25d1e..977fd593e8f 100644 --- a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml @@ -9177,9 +9177,6 @@ and (desugar_decl_maybe_fail_attr : (fun at -> let uu___ = get_fail_attr1 false at in FStarC_Compiler_Option.isNone uu___) ats in - let env0 = - let uu___ = FStarC_Syntax_DsEnv.snapshot env in - FStar_Pervasives_Native.snd uu___ in let uu___ = let attrs = FStarC_Compiler_List.map (desugar_term env) @@ -9188,6 +9185,9 @@ and (desugar_decl_maybe_fail_attr : let uu___1 = get_fail_attr false attrs1 in match uu___1 with | FStar_Pervasives_Native.Some (expected_errs, lax) -> + let env0 = + let uu___2 = FStarC_Syntax_DsEnv.snapshot env in + FStar_Pervasives_Native.snd uu___2 in let d1 = { FStarC_Parser_AST.d = (d.FStarC_Parser_AST.d);