Merge PR #10359: Remove dependency of native_compile on global env for symbols

Reviewed-by: maximedenes
Reviewed-by: ppedrot

14 files changed, 105 insertions, 60 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 32f9069747..9a75f0b682 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 a4cd576bcc..6cd4f96645 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 85dc8267bb..9802d4f531 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 65c5d6c139..78eb9295d4 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/nativecode.ml b/kernel/nativecode.ml
index fc9e69d9e3..a6b5fc9a41 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -141,18 +141,6 @@ let fresh_gnormtbl l =
 
 (** Symbols (pre-computed values) **)
 
-type symbol =
-  | SymbValue of Nativevalues.t
-  | SymbSort of Sorts.t
-  | SymbName of Name.t
-  | SymbConst of Constant.t
-  | SymbMatch of annot_sw
-  | SymbInd of inductive
-  | SymbMeta of metavariable
-  | SymbEvar of Evar.t
-  | SymbLevel of Univ.Level.t
-  | SymbProj of (inductive * int)
-
 let dummy_symb = SymbValue (dummy_value ())
 
 let eq_symbol sy1 sy2 =
@@ -194,10 +182,6 @@ let symb_tbl = HashtblSymbol.create 211
 
 let clear_symbols () = HashtblSymbol.clear symb_tbl
 
-type symbols = symbol array
-
-let empty_symbols = [||]
-
 let get_value tbl i =
   match tbl.(i) with
     | SymbValue v -> v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 955c4ad899..ed395368b2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -12,6 +12,7 @@ open Constr
 open Declarations
 open Environ
 open Nativelambda
+open Nativevalues
 
 (** This file defines the mllambda code generation phase of the native
 compiler. mllambda represents a fragment of ML, and can easily be printed
@@ -25,11 +26,6 @@ val pp_global : Format.formatter -> global -> unit
 val mk_open : string -> global
 
 (* Precomputed values for a compilation unit *)
-type symbol
-type symbols
-
-val empty_symbols : symbols
-
 val clear_symbols : unit -> unit
 
 val get_value : symbols -> int -> Nativevalues.t
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index a98523ba66..dd010e5cad 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 94a8b1310a..1cef729916 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 194efecd9a..52d18acca6 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/nativelibrary.mli b/kernel/nativelibrary.mli
index 168bf646af..c53a626528 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -16,4 +16,4 @@ open Nativecode
 compiler *)
 
 val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
-  global list * symbols
+  global list * Nativevalues.symbols
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index b3ad3949dc..e54118c775 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -66,6 +66,23 @@ type atom =
   | Aevar of Evar.t * t array
   | Aproj of (inductive * int) * accumulator
 
+type symbol =
+  | SymbValue of t
+  | SymbSort of Sorts.t
+  | SymbName of Name.t
+  | SymbConst of Constant.t
+  | SymbMatch of annot_sw
+  | SymbInd of inductive
+  | SymbMeta of metavariable
+  | SymbEvar of Evar.t
+  | SymbLevel of Univ.Level.t
+  | SymbProj of (inductive * int)
+
+type symbols = symbol array
+
+let empty_symbols = [| |]
+
+
 let accumulate_tag = 0
 
 (** Unique pointer used to drive the accumulator function *)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b5b4569a24..b54f437e73 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -56,6 +56,22 @@ type atom =
   | Aevar of Evar.t * t array (* arguments *)
   | Aproj of (inductive * int) * accumulator
 
+type symbol =
+  | SymbValue of t
+  | SymbSort of Sorts.t
+  | SymbName of Name.t
+  | SymbConst of Constant.t
+  | SymbMatch of annot_sw
+  | SymbInd of inductive
+  | SymbMeta of metavariable
+  | SymbEvar of Evar.t
+  | SymbLevel of Univ.Level.t
+  | SymbProj of (inductive * int)
+
+type symbols = symbol array
+
+val empty_symbols : symbols
+
 (* Constructors *)
 
 val mk_accu : atom -> t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2c434d4edf..445e359dee 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 : Nativecode.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; "."])
@@ -987,8 +985,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
@@ -998,6 +996,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
@@ -1028,6 +1027,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
@@ -1091,19 +1091,13 @@ type compiled_library = {
   comp_mod : module_body;
   comp_deps : library_info array;
   comp_enga : engagement;
-  comp_natsymbs : Nativecode.symbols
+  comp_natsymbs : Nativevalues.symbols
 }
 
 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)
@@ -1143,12 +1137,12 @@ let export ?except ~output_native_objects senv dir =
   let ast, symbols =
     if output_native_objects then
       Nativelibrary.dump_library mp dir senv.env str
-    else [], Nativecode.empty_symbols
+    else [], Nativevalues.empty_symbols
   in
   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
@@ -1168,17 +1162,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 885becc40a..50f6832ffa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -177,8 +177,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 -> Nativecode.symbols
-
 val start_library : DirPath.t -> ModPath.t safe_transformer
 
 val export :