Native compiler: refactor code handling pre-computed values.

Fixes #4139 (Not_found exception with Require in modules).

9 files changed, 53 insertions, 40 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f56b6f83e..90c437bbf 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
 
 let symb_tbl = HashtblSymbol.create 211
 
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
 
 let get_value tbl i =
   match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
 
 let symbols_tbl_name = Ginternal "symbols_tbl"
 
-let get_symbols_tbl () =
+let get_symbols () =
   let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
   HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
 
@@ -2058,7 +2062,7 @@ let mk_internal_let s code =
 
 (* ML Code for conversion function *)
 let mk_conv_code env sigma prefix t1 t2 =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2080,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
   let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
   let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_norm_code env sigma prefix t =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2098,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
   let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
   let gl = List.rev (setref :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_library_header dir =
   let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
   [Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_library_native_symbols"),
     [|MLglobal (Ginternal libname)|]))]
 
 let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92dd..5d4c9e1e2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
 
+(* Precomputed values for a compilation unit *)
 type symbol
+type symbols
 
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
 
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
 
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
 
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
 
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
 
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
 
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
 
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
 
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
 
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
 
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
 
 type code_location_update
 type code_location_updates
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff0..443cd8c2a 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
       let prefix = mod_uid_of_dirpath dp ^ "." in
       let t0 = Sys.time () in
       clear_global_tbl ();
-      clear_symb_tbl ();
+      clear_symbols ();
       let mlcode =
         List.fold_left (translate_field prefix mp env) [] struc
       in
       let t1 = Sys.time () in
       let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
       let mlcode = add_header_comment (List.rev mlcode) time_info in
-      mlcode, get_symbols_tbl ()
+      mlcode, get_symbols ()
   | _ -> assert false
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a66fb715d..29368d140 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,4 +14,4 @@ open Nativecode
 compiler *)
 
 val dump_library : module_path -> dir_path -> env -> module_signature ->
-  global list * symbol array
+  global list * symbols
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 } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a57fb108c..1e9cdbda0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,8 @@ type compiled_library
 
 type native_library = Nativecode.global list
 
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+
 val start_library : DirPath.t -> module_path safe_transformer
 
 val export :
@@ -146,7 +148,7 @@ val export :
 
 (* Constraints are non empty iff the file is a vi2vo *)
 val import : compiled_library -> Univ.universe_context_set -> vodigest ->
-  (module_path * Nativecode.symbol array) safe_transformer
+  module_path safe_transformer
 
 (** {6 Safe typing judgments } *)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index a82f5260b..f66656d09 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects
 
 (** For the native compiler, we cache the library values *)
 
-type library_values = Nativecode.symbol array
-let library_values =
-  Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
-
 let register_library dir cenv (objs:library_objects) digest univ =
   let mp = MPfile dir in
   let () =
@@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ =
       ignore(Global.lookup_module mp);
     with Not_found ->
       (* If not, let's do it now ... *)
-      let mp', values = Global.import cenv univ digest in
+      let mp' = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
         anomaly (Pp.str "Unexpected disk module name");
-      library_values := Dirmap.add dir values !library_values
   in
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
 
-let get_library_symbols_tbl dir = Dirmap.find dir !library_values
+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
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c3578ec42..319d168d0 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -75,7 +75,7 @@ val register_library :
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
   Univ.universe_context_set -> unit
 
-val get_library_symbols_tbl : library_name -> Nativecode.symbol array
+val get_library_native_symbols : library_name -> Nativecode.symbols
 
 val start_library : library_name -> unit
 
diff --git a/library/global.mli b/library/global.mli
index 248e1f86d..75a1ebee9 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
-  module_path * Nativecode.symbol array
+  module_path
 
 (** {6 Misc } *)