diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 25 |
1 files changed, 16 insertions, 9 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d9adca0c9..d8473183a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -125,7 +125,8 @@ type safe_environment = type_in_type : bool; required : vodigest DPMap.t; loads : (module_path * module_body) list; - local_retroknowledge : Retroknowledge.action list } + local_retroknowledge : Retroknowledge.action list; + native_symbols : Nativecode.symbols DPMap.t } and modvariant = | NONE @@ -154,7 +155,8 @@ let empty_environment = type_in_type = false; required = DPMap.empty; loads = []; - local_retroknowledge = [] } + local_retroknowledge = []; + native_symbols = DPMap.empty } let is_initial senv = match senv.revstruct, senv.modvariant with @@ -623,7 +625,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv = required = senv.required; loads = senv.loads@oldsenv.loads; local_retroknowledge = - senv.local_retroknowledge@oldsenv.local_retroknowledge } + senv.local_retroknowledge@oldsenv.local_retroknowledge; + native_symbols = senv.native_symbols} let end_module l restype senv = let mp = senv.modpath in @@ -732,11 +735,14 @@ type compiled_library = { comp_mod : module_body; comp_deps : library_info array; comp_enga : engagement option; - comp_natsymbs : Nativecode.symbol array + comp_natsymbs : Nativecode.symbols } type native_library = Nativecode.global list +let get_library_native_symbols senv dir = + DPMap.find dir senv.native_symbols + (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath let current_dirpath senv = Names.ModPath.dp (current_modpath senv) @@ -773,17 +779,17 @@ let export ?except senv dir = mod_retroknowledge = senv.local_retroknowledge } in - let ast, values = + let ast, symbols = if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str - else [], [||] + else [], Nativecode.empty_symbols in let lib = { comp_name = dir; comp_mod = mb; comp_deps = Array.of_list (DPMap.bindings senv.required); comp_enga = Environ.engagement senv.env; - comp_natsymbs = values } + comp_natsymbs = symbols } in mp, lib, ast @@ -796,7 +802,7 @@ let import lib cst vodigest senv = let mb = lib.comp_mod in let env = Environ.add_constraints mb.mod_constraints senv.env in let env = Environ.push_context_set cst env in - (mp, lib.comp_natsymbs), + mp, { senv with env = (let linkinfo = @@ -805,7 +811,8 @@ let import lib cst vodigest senv = Modops.add_linked_module mb linkinfo env); modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; required = DPMap.add lib.comp_name vodigest senv.required; - loads = (mp,mb)::senv.loads } + loads = (mp,mb)::senv.loads; + native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols } (** {6 Safe typing } *) |