Remove dependency of native_compile on global env for symbols

Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.

13 files changed, 70 insertions, 43 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index c47bde0864..be3d42bbc9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -95,6 +95,7 @@ type env = {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
+  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 let empty_named_context_val = {
@@ -123,7 +124,9 @@ let empty_env = {
   };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
-  indirect_pterms = Opaqueproof.empty_opaquetab }
+  indirect_pterms = Opaqueproof.empty_opaquetab;
+  native_symbols = DPmap.empty;
+}
 
 
 (* Rel context *)
@@ -763,3 +766,7 @@ let is_type_in_type env r =
   | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
 
 let set_retroknowledge env r = { env with retroknowledge = r }
+
+let set_native_symbols env native_symbols = { env with native_symbols }
+let add_native_symbols dir syms env =
+  { env with native_symbols = DPmap.add dir syms env.native_symbols }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2abcea148a..e46d1ee5ea 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -74,6 +74,7 @@ type env = private {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
+  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 val oracle : env -> Conv_oracle.oracle
@@ -351,3 +352,6 @@ val no_link_info : link_info
 
 (** Primitives *)
 val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env
+
+val set_native_symbols : env -> Nativevalues.symbols DPmap.t -> env
+val add_native_symbols : DirPath.t -> Nativevalues.symbols -> env -> env
diff --git a/kernel/names.ml b/kernel/names.ml
index 047a1d6525..af64299424 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -356,6 +356,9 @@ module ModPath = struct
 
 end
 
+module DPset = Set.Make(DirPath)
+module DPmap = Map.Make(DirPath)
+
 module MPset = Set.Make(ModPath)
 module MPmap = CMap.Make(ModPath)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 2238e932b0..b150d9bf4d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -161,6 +161,9 @@ sig
   val print : t -> Pp.t
 end
 
+module DPset : Set.S with type elt = DirPath.t
+module DPmap : Map.ExtS with type key = DirPath.t and module Set := DPset
+
 (** {6 Names of structure elements } *)
 
 module Label :
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index d153f84e9c..1c76db01de 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -154,7 +154,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
   let fn = compile ml_filename code ~profile:false in
   if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
   let t0 = Sys.time () in
-  call_linker ~fatal:true prefix fn (Some upds);
+  call_linker env ~fatal:true ~prefix fn (Some upds);
   let t1 = Sys.time () in
   let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
   if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 43c9676f05..8722a336dd 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -21,8 +21,7 @@ let get_load_paths =
 let open_header = ["Nativevalues";
                    "Nativecode";
                    "Nativelib";
-		   "Nativeconv";
-                   "Declaremods"]
+                   "Nativeconv"]
 let open_header = List.map mk_open open_header
 
 (* Directory where compiled files are stored *)
@@ -129,9 +128,19 @@ let compile_library dir code fn =
   let _ = call_compiler fn in
   if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
 
+let native_symbols = ref Names.DPmap.empty
+
+let get_library_native_symbols dir =
+  try Names.DPmap.find dir !native_symbols
+  with Not_found ->
+    CErrors.user_err ~hdr:"get_library_native_symbols"
+      Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
+          (str "This use case is not supported, but disabling the native compiler may help."))
+
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
-let call_linker ?(fatal=true) prefix f upds =
+let call_linker ?(fatal=true) env ~prefix f upds =
+  native_symbols := env.Environ.native_symbols;
   rt1 := dummy_value ();
   rt2 := dummy_value ();
   if not (Sys.file_exists f) then
@@ -150,6 +159,6 @@ let call_linker ?(fatal=true) prefix f upds =
      else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
   match upds with Some upds -> update_locations upds | _ -> ()
 
-let link_library ~prefix ~dirname ~basename =
+let link_library env ~prefix ~dirname ~basename =
   let f = dirname / output_dir / basename in
-  call_linker ~fatal:false prefix f None
+  call_linker env ~fatal:false ~prefix f None
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index e113350368..489f443566 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -30,10 +30,23 @@ val compile : string -> global list -> profile:bool -> string
    but will perform some extra tweaks to handle [code] as a Coq lib. *)
 val compile_library : Names.DirPath.t -> global list -> string -> unit
 
-val call_linker :
-  ?fatal:bool -> string -> string -> code_location_updates option -> unit
-
-val link_library : prefix:string -> dirname:string -> basename:string -> unit
+val call_linker
+  : ?fatal:bool
+  -> Environ.env
+  -> prefix:string
+  -> string
+  -> code_location_updates option
+  -> unit
+
+val link_library
+  : Environ.env
+  -> prefix:string
+  -> dirname:string
+  -> basename:string
+  -> unit
 
 val rt1 : Nativevalues.t ref
 val rt2 : Nativevalues.t ref
+
+val get_library_native_symbols : Names.DirPath.t -> Nativevalues.symbols
+(** Strictly for usage by code produced by native compute. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2284196efe..71ecb02298 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,8 +113,6 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
-module DPMap = Map.Make(DirPath)
-
 type safe_environment =
   { env : Environ.env;
     modpath : ModPath.t;
@@ -127,10 +125,10 @@ type safe_environment =
     univ : Univ.ContextSet.t;
     future_cst : Univ.ContextSet.t Future.computation list;
     engagement : engagement option;
-    required : vodigest DPMap.t;
+    required : vodigest DPmap.t;
     loads : (ModPath.t * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
-    native_symbols : Nativevalues.symbols DPMap.t }
+}
 
 and modvariant =
   | NONE
@@ -156,10 +154,10 @@ let empty_environment =
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
-    required = DPMap.empty;
+    required = DPmap.empty;
     loads = [];
     local_retroknowledge = [];
-    native_symbols = DPMap.empty }
+}
 
 let is_initial senv =
   match senv.revstruct, senv.modvariant with
@@ -396,7 +394,7 @@ let check_initial senv = assert (is_initial senv)
 let check_required current_libs needed =
   let check (id,required) =
     try
-      let actual = DPMap.find id current_libs in
+      let actual = DPmap.find id current_libs in
       if not(digest_match ~actual ~required) then
         CErrors.user_err Pp.(pr_sequence str
           ["Inconsistent assumptions over module"; DirPath.to_string id; "."])
@@ -972,8 +970,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;
-    native_symbols = senv.native_symbols}
+      senv.local_retroknowledge@oldsenv.local_retroknowledge;
+  }
 
 let end_module l restype senv =
   let mp = senv.modpath in
@@ -983,6 +981,7 @@ let end_module l restype senv =
   let mbids = List.rev_map fst params in
   let mb = build_module_body params restype senv in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
+  let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv'=
     propagate_loads { senv with
@@ -1013,6 +1012,7 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
+  let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
   let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = propagate_loads {senv with env=newenv} in
@@ -1083,12 +1083,6 @@ let module_of_library lib = lib.comp_mod
 
 type native_library = Nativecode.global list
 
-let get_library_native_symbols senv dir =
-  try DPMap.find dir senv.native_symbols
-  with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols"
-                      Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
-                          (str "This use case is not supported, but disabling the native compiler may help."))
-
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
 let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -1133,7 +1127,7 @@ let export ?except ~output_native_objects senv dir =
   let lib = {
     comp_name = dir;
     comp_mod = mb;
-    comp_deps = Array.of_list (DPMap.bindings senv.required);
+    comp_deps = Array.of_list (DPmap.bindings senv.required);
     comp_enga = Environ.engagement senv.env;
     comp_natsymbs = symbols }
   in
@@ -1153,17 +1147,18 @@ let import lib cst vodigest senv =
 				     (Univ.ContextSet.union mb.mod_constraints cst)
 				     senv.env
   in
+  let env =
+    let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
+    Modops.add_linked_module mb linkinfo env
+  in
+  let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in
   mp,
   { senv with
-    env =
-      (let linkinfo =
-	 Nativecode.link_info_of_dirpath lib.comp_name
-       in
-       Modops.add_linked_module mb linkinfo env);
+    env;
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
-    required = DPMap.add lib.comp_name vodigest senv.required;
+    required = DPmap.add lib.comp_name vodigest senv.required;
     loads = (mp,mb)::senv.loads;
-    native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols }
+  }
 
 (** {6 Safe typing } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d8f7f0cc40..f2920a90ee 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -179,8 +179,6 @@ type native_library = Nativecode.global list
 
 val module_of_library : compiled_library -> Declarations.module_body
 
-val get_library_native_symbols : safe_environment -> DirPath.t -> Nativevalues.symbols
-
 val start_library : DirPath.t -> ModPath.t safe_transformer
 
 val export :
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d74bdd484c..a922e84540 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -915,9 +915,6 @@ let register_library dir cenv (objs:library_objects) digest univ =
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
 
-let get_library_native_symbols dir =
-  Safe_typing.get_library_native_symbols (Global.safe_env ()) dir
-
 let start_library dir =
   let mp = Global.start_library dir in
   openmod_info := default_module_info;
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c35abae155..15191e3d72 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -94,8 +94,6 @@ val register_library :
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
   Univ.ContextSet.t -> unit
 
-val get_library_native_symbols : library_name -> Nativevalues.symbols
-
 val start_library : library_name -> unit
 
 val end_library :
diff --git a/library/library.ml b/library/library.ml
index 1ac75d2fdc..b62164d8fa 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -173,7 +173,7 @@ let register_loaded_library m =
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
     if Coq_config.native_compiler then
-      Nativelib.link_library ~prefix ~dirname ~basename:f
+      Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link (); [libname]
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0fcd6a9e9d..909b0faf2f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -499,7 +499,7 @@ let native_norm env sigma c ty =
     if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
     let profiler_pid = if profile then start_profiler () else None in
     let t0 = Sys.time () in
-    Nativelib.call_linker ~fatal:true prefix fn (Some upd);
+    Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd);
     let t1 = Sys.time () in
     if profile then stop_profiler profiler_pid;
     let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in