From fbe748cd5da049ccf4f4fedae0ef995e1d635f35 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 17 Oct 2024 22:03:37 -0700 Subject: [PATCH 1/5] 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 71326574542763c647e344ce75210c9e041f57c5 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 10:16:03 -0700 Subject: [PATCH 2/5] 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); From bccb5d6dd4443e49e645be8492f7fa85533fa052 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 11:19:42 -0700 Subject: [PATCH 3/5] coalesce top-level definitions into a map for faster lookup during desugaring (avoiding linear scan) --- .../generated/FStarC_Syntax_DsEnv.ml | 44 +++++++++++++------ src/syntax/FStarC.Syntax.DsEnv.fst | 15 +++++-- 2 files changed, 42 insertions(+), 17 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml index f78b51f4af0..5b1ddf64318 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml @@ -59,7 +59,7 @@ type scope_mod = | Module_abbrev of FStarC_Syntax_Syntax.module_abbrev | Open_module_or_namespace of FStarC_Syntax_Syntax.open_module_or_namespace - | Top_level_def of FStarC_Ident.ident + | Top_level_defs of Prims.bool FStarC_Compiler_Util.psmap | Record_or_dc of record_or_dc let (uu___is_Local_binding : scope_mod -> Prims.bool) = fun projectee -> @@ -85,11 +85,12 @@ let (uu___is_Open_module_or_namespace : scope_mod -> Prims.bool) = let (__proj__Open_module_or_namespace__item___0 : scope_mod -> FStarC_Syntax_Syntax.open_module_or_namespace) = fun projectee -> match projectee with | Open_module_or_namespace _0 -> _0 -let (uu___is_Top_level_def : scope_mod -> Prims.bool) = +let (uu___is_Top_level_defs : scope_mod -> Prims.bool) = fun projectee -> - match projectee with | Top_level_def _0 -> true | uu___ -> false -let (__proj__Top_level_def__item___0 : scope_mod -> FStarC_Ident.ident) = - fun projectee -> match projectee with | Top_level_def _0 -> _0 + match projectee with | Top_level_defs _0 -> true | uu___ -> false +let (__proj__Top_level_defs__item___0 : + scope_mod -> Prims.bool FStarC_Compiler_Util.psmap) = + fun projectee -> match projectee with | Top_level_defs _0 -> _0 let (uu___is_Record_or_dc : scope_mod -> Prims.bool) = fun projectee -> match projectee with | Record_or_dc _0 -> true | uu___ -> false @@ -882,10 +883,12 @@ let try_lookup_id'' : | FStar_Pervasives_Native.Some id1 -> find_in_module_with_includes eikind find_in_module Cont_ignore env1 ns id1) - | Top_level_def id' when - let uu___1 = FStarC_Ident.string_of_id id' in - let uu___2 = FStarC_Ident.string_of_id id in - uu___1 = uu___2 -> lookup_default_id Cont_ignore id + | Top_level_defs ids when + let uu___1 = + let uu___2 = FStarC_Ident.string_of_id id in + FStarC_Compiler_Util.psmap_try_find ids uu___2 in + FStar_Pervasives_Native.uu___is_Some uu___1 -> + lookup_default_id Cont_ignore id | Record_or_dc r when is_exported_id_field eikind -> let uu___1 = FStarC_Ident.lid_of_ids curmod_ns in find_in_module_with_includes Exported_id_field @@ -2566,6 +2569,23 @@ let (push_sigelt' : Prims.bool -> env -> FStarC_Syntax_Syntax.sigelt -> env) | uu___1 -> (env3, [((FStarC_Syntax_Util.lids_of_sigelt s), s)]) in match uu___ with | (env4, lss) -> + let push_top_level_def id stack = + match stack with + | (Top_level_defs ids)::rest -> + let uu___1 = + let uu___2 = + let uu___3 = FStarC_Ident.string_of_id id in + FStarC_Compiler_Util.psmap_add ids uu___3 true in + Top_level_defs uu___2 in + uu___1 :: rest + | uu___1 -> + let uu___2 = + let uu___3 = + let uu___4 = FStarC_Compiler_Util.psmap_empty () in + let uu___5 = FStarC_Ident.string_of_id id in + FStarC_Compiler_Util.psmap_add uu___4 uu___5 true in + Top_level_defs uu___3 in + uu___2 :: stack in (FStarC_Compiler_List.iter (fun uu___2 -> match uu___2 with @@ -2573,12 +2593,10 @@ let (push_sigelt' : Prims.bool -> env -> FStarC_Syntax_Syntax.sigelt -> env) FStarC_Compiler_List.iter (fun lid -> (let uu___4 = - let uu___5 = - let uu___6 = FStarC_Ident.ident_of_lid lid in - Top_level_def uu___6 in + let uu___5 = FStarC_Ident.ident_of_lid lid in let uu___6 = FStarC_Compiler_Effect.op_Bang globals in - uu___5 :: uu___6 in + push_top_level_def uu___5 uu___6 in FStarC_Compiler_Effect.op_Colon_Equals globals uu___4); (match () with diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index 56419a1be69..531baea74c9 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -49,7 +49,7 @@ type scope_mod = | Rec_binding of rec_binding | Module_abbrev of module_abbrev | Open_module_or_namespace of open_module_or_namespace -| Top_level_def of ident (* top-level definition for an unqualified identifier x to be resolved as curmodule.x. *) +| Top_level_defs of BU.psmap bool (* top-level definition for an unqualified identifier x to be resolved as curmodule.x. *) | Record_or_dc of record_or_dc (* to honor interleavings of "open" and record definitions *) type string_set = RBSet.t string @@ -320,8 +320,8 @@ let try_lookup_id'' | None -> Cont_ignore | Some id -> find_in_module_with_includes eikind find_in_module Cont_ignore env ns id) - | Top_level_def id' - when string_of_id id' = string_of_id id -> + | Top_level_defs ids + when Some? (BU.psmap_try_find ids (string_of_id id)) -> (* indicates a global definition shadowing previous "open"s. If the definition is not actually found by the [lookup_default_id] finder, then it may mean that we are in a @@ -1027,12 +1027,19 @@ let push_sigelt' fail_on_dup env s = let env, lss = match s.sigel with | Sig_bundle {ses} -> env, List.map (fun se -> (lids_of_sigelt se, se)) ses | _ -> env, [lids_of_sigelt s, s] in + let push_top_level_def id stack = + match stack with + | Top_level_defs ids :: rest -> + Top_level_defs (BU.psmap_add ids (string_of_id id) true) :: rest + | _ -> + Top_level_defs (BU.psmap_add (BU.psmap_empty()) (string_of_id id) true) :: stack + in lss |> List.iter (fun (lids, se) -> lids |> List.iter (fun lid -> (* the identifier is added into the list of global declarations, to allow shadowing of definitions that were formerly reachable by previous "open"s. *) - let () = globals := Top_level_def (ident_of_lid lid) :: !globals in + let () = globals := push_top_level_def (ident_of_lid lid) !globals in (* the identifier is added into the list of global identifiers of the corresponding module to shadow any "include" *) let modul = string_of_lid (lid_of_ids (ns_of_lid lid)) in From 95fad8a06a8e51d54cbc4868317a80d8ff130982 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 11:27:18 -0700 Subject: [PATCH 4/5] coalesce local bindings in DsEnv too, for faster resolution of local names --- .../generated/FStarC_Syntax_DsEnv.ml | 71 +++++++++++++++---- src/syntax/FStarC.Syntax.DsEnv.fst | 16 +++-- 2 files changed, 70 insertions(+), 17 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml index 5b1ddf64318..c2f053f03b7 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml @@ -54,18 +54,19 @@ type local_binding = (FStarC_Ident.ident * FStarC_Syntax_Syntax.bv * used_marker) type rec_binding = (FStarC_Ident.ident * FStarC_Ident.lid * used_marker) type scope_mod = - | Local_binding of local_binding + | Local_bindings of local_binding FStarC_Compiler_Util.psmap | Rec_binding of rec_binding | Module_abbrev of FStarC_Syntax_Syntax.module_abbrev | Open_module_or_namespace of FStarC_Syntax_Syntax.open_module_or_namespace | Top_level_defs of Prims.bool FStarC_Compiler_Util.psmap | Record_or_dc of record_or_dc -let (uu___is_Local_binding : scope_mod -> Prims.bool) = +let (uu___is_Local_bindings : scope_mod -> Prims.bool) = fun projectee -> - match projectee with | Local_binding _0 -> true | uu___ -> false -let (__proj__Local_binding__item___0 : scope_mod -> local_binding) = - fun projectee -> match projectee with | Local_binding _0 -> _0 + match projectee with | Local_bindings _0 -> true | uu___ -> false +let (__proj__Local_bindings__item___0 : + scope_mod -> local_binding FStarC_Compiler_Util.psmap) = + fun projectee -> match projectee with | Local_bindings _0 -> _0 let (uu___is_Rec_binding : scope_mod -> Prims.bool) = fun projectee -> match projectee with | Rec_binding _0 -> true | uu___ -> false @@ -858,13 +859,22 @@ let try_lookup_id'' : FStarC_Ident.ids_of_lid uu___ in let proc uu___ = match uu___ with - | Local_binding l when check_local_binding_id l -> - let uu___1 = l in + | Local_bindings lbs when + let uu___1 = + let uu___2 = FStarC_Ident.string_of_id id in + FStarC_Compiler_Util.psmap_try_find lbs uu___2 in + FStar_Pervasives_Native.uu___is_Some uu___1 -> + let uu___1 = + let uu___2 = FStarC_Ident.string_of_id id in + FStarC_Compiler_Util.psmap_try_find lbs uu___2 in (match uu___1 with - | (uu___2, uu___3, used_marker1) -> - (FStarC_Compiler_Effect.op_Colon_Equals - used_marker1 true; - k_local_binding l)) + | FStar_Pervasives_Native.Some l -> + let uu___2 = l in + (match uu___2 with + | (uu___3, uu___4, used_marker1) -> + (FStarC_Compiler_Effect.op_Colon_Equals + used_marker1 true; + k_local_binding l))) | Rec_binding r when check_rec_binding_id r -> let uu___1 = r in (match uu___1 with @@ -2426,8 +2436,43 @@ let (push_bv' : (FStarC_Syntax_Syntax.tun.FStarC_Syntax_Syntax.hash_code) } in let used_marker1 = FStarC_Compiler_Util.mk_ref false in - ((push_scope_mod env1 (Local_binding (x, bv, used_marker1))), bv, - used_marker1) + let scope_mods = + match env1.scope_mods with + | (Local_bindings lbs)::rest -> + let uu___ = + let uu___1 = + let uu___2 = FStarC_Ident.string_of_id x in + FStarC_Compiler_Util.psmap_add lbs uu___2 + (x, bv, used_marker1) in + Local_bindings uu___1 in + uu___ :: rest + | uu___ -> + let uu___1 = + let uu___2 = + let uu___3 = FStarC_Compiler_Util.psmap_empty () in + let uu___4 = FStarC_Ident.string_of_id x in + FStarC_Compiler_Util.psmap_add uu___3 uu___4 + (x, bv, used_marker1) in + Local_bindings uu___2 in + uu___1 :: (env1.scope_mods) in + ({ + curmodule = (env1.curmodule); + curmonad = (env1.curmonad); + modules = (env1.modules); + scope_mods; + exported_ids = (env1.exported_ids); + trans_exported_ids = (env1.trans_exported_ids); + includes = (env1.includes); + sigaccum = (env1.sigaccum); + sigmap = (env1.sigmap); + iface = (env1.iface); + admitted_iface = (env1.admitted_iface); + expect_typ = (env1.expect_typ); + remaining_iface_decls = (env1.remaining_iface_decls); + syntax_only = (env1.syntax_only); + ds_hooks = (env1.ds_hooks); + dep_graph = (env1.dep_graph) + }, bv, used_marker1) let (push_bv : env -> FStarC_Ident.ident -> (env * FStarC_Syntax_Syntax.bv)) = fun env1 -> diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index 531baea74c9..478673ceff8 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -45,7 +45,7 @@ type rec_binding = (ident & lid & (* name bound by recur used_marker) (* this ref marks whether it was used, so we can warn if not *) type scope_mod = -| Local_binding of local_binding +| Local_bindings of BU.psmap local_binding | Rec_binding of rec_binding | Module_abbrev of module_abbrev | Open_module_or_namespace of open_module_or_namespace @@ -303,8 +303,9 @@ let try_lookup_id'' in let curmod_ns = ids_of_lid (current_module env) in let proc = function - | Local_binding l - when check_local_binding_id l -> + | Local_bindings lbs + when Some? (BU.psmap_try_find lbs (string_of_id id)) -> + let Some l = BU.psmap_try_find lbs (string_of_id id) in let (_, _, used_marker) = l in used_marker := true; k_local_binding l @@ -982,7 +983,14 @@ let push_bv' env (x:ident) = let r = range_of_id x in let bv = S.gen_bv (string_of_id x) (Some r) ({ tun with pos = r }) in let used_marker = BU.mk_ref false in - push_scope_mod env (Local_binding (x, bv, used_marker)), bv, used_marker + let scope_mods = + match env.scope_mods with + | Local_bindings lbs :: rest -> + Local_bindings (BU.psmap_add lbs (string_of_id x) (x, bv, used_marker)) :: rest + | _ -> + Local_bindings (BU.psmap_add (BU.psmap_empty()) (string_of_id x) (x, bv, used_marker)) :: env.scope_mods + in + { env with scope_mods }, bv, used_marker let push_bv env x = let (env, bv, _) = push_bv' env x in From 2bf0446bb21540ef8595112b88cc7713324bff81 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 18 Oct 2024 11:50:48 -0700 Subject: [PATCH 5/5] comments --- src/syntax/FStarC.Syntax.DsEnv.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index 478673ceff8..9bb723c7607 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -45,11 +45,11 @@ type rec_binding = (ident & lid & (* name bound by recur used_marker) (* this ref marks whether it was used, so we can warn if not *) type scope_mod = -| Local_bindings of BU.psmap local_binding +| Local_bindings of BU.psmap local_binding (* a map local bindings in a scope; a map to avoid a linear scan *) | Rec_binding of rec_binding | Module_abbrev of module_abbrev | Open_module_or_namespace of open_module_or_namespace -| Top_level_defs of BU.psmap bool (* top-level definition for an unqualified identifier x to be resolved as curmodule.x. *) +| Top_level_defs of BU.psmap bool (* a map (to avoid a linear scan) recording that a top-level definition for an unqualified identifier x is in scope and should be resolved as curmodule.x. *) | Record_or_dc of record_or_dc (* to honor interleavings of "open" and record definitions *) type string_set = RBSet.t string