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