diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml index f78b51f4af0..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_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) = +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 @@ -85,11 +86,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 @@ -857,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 @@ -882,10 +893,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 @@ -2423,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 -> @@ -2566,6 +2614,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 +2638,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..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_binding of 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_def of ident (* 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 @@ -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 @@ -320,8 +321,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 @@ -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 @@ -1027,12 +1035,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