coalesce top-level definitions into a map for faster lookup during de…

…sugaring (avoiding linear scan)

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