Removing native_name reference from constant_body.

For now, this reference (renamed to link_info) has been moved to the
environment (for constants and inductive types). But this is only a first step
towards making the native compiler more functional.

17 files changed, 108 insertions, 94 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 146b6a1ec..0111cf74d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -92,7 +92,7 @@ let slot_for_annot key =
     n
 
 let rec slot_for_getglobal env kn =
-  let (cb,rk) = lookup_constant_key kn env in
+  let (cb,(_,rk)) = lookup_constant_key kn env in
   try key rk
   with NotEvaluated ->
 (*    Pp.msgnl(str"not yet evaluated");*)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d74c9a0d5..d92b66707 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -40,14 +40,6 @@ type constant_def =
   | Def of Lazyconstr.constr_substituted
   | OpaqueDef of Lazyconstr.lazy_constr Future.computation
 
-(** Linking information for the native compiler. The boolean flag indicates if
-  the term is protected by a lazy tag *)
-
-type native_name =
-  | Linked of string * bool
-  | LinkedInteractive of string * bool
-  | NotLinked
-
 type constant_constraints = Univ.constraints Future.computation
 
 type constant_body = {
@@ -56,7 +48,6 @@ type constant_body = {
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
     const_constraints : constant_constraints;
-    const_native_name : native_name ref;
     const_inline_code : bool }
 
 type side_effect =
@@ -150,11 +141,6 @@ type mutual_inductive_body = {
 
     mind_constraints : Univ.constraints;  (** Universes constraints enforced by the inductive declaration *)
 
-(** {8 Data for native compilation } *)
-
-    mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
-
-
   }
 
 (** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 724f29092..2e691491a 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -65,7 +65,6 @@ let subst_const_body sub cb = {
   const_type = subst_const_type sub cb.const_type;
   const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
   const_constraints = cb.const_constraints;
-  const_native_name = ref NotLinked;
   const_inline_code = cb.const_inline_code }
 
 (** {7 Hash-consing of constants } *)
@@ -201,8 +200,7 @@ let subst_mind sub mib =
     else
       { mib with
         mind_params_ctxt = params';
-        mind_packets = packets';
-        mind_native_name = ref NotLinked }
+        mind_packets = packets' }
 
 (** {6 Hash-consing of inductive declarations } *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9f1868004..679c807d6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -157,14 +157,19 @@ let fold_named_context_reverse f ~init env =
 
 let lookup_constant = lookup_constant
 
-let add_constant kn cs env =
+let no_link_info () = ref NotLinked
+
+let add_constant_key kn cb linkinfo env =
   let new_constants =
-    Cmap_env.add kn (cs,ref None) env.env_globals.env_constants in
+    Cmap_env.add kn (cb,(linkinfo, ref None)) env.env_globals.env_constants in
   let new_globals =
     { env.env_globals with
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
+let add_constant kn cb env =
+  add_constant_key kn cb (no_link_info ()) env
+
 (* constant_type gives the type of a constant *)
 let constant_type env kn =
   let cb = lookup_constant kn env in
@@ -192,14 +197,17 @@ let evaluable_constant cst env =
 
 (* Mutual Inductives *)
 let lookup_mind = lookup_mind
-  
-let add_mind kn mib env =
-  let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+
+let add_mind_key kn mind_key env =
+  let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
 	env_inductives = new_inds } in
   { env with env_globals = new_globals }
 
+let add_mind kn mib env =
+  let li = no_link_info () in add_mind_key kn (mib, li) env
+
 (* Universe constraints *)
 
 let add_constraints c env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 38a1bf68a..66cb03a1c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -117,6 +117,8 @@ val reset_with_named_context : named_context_val -> env -> env
   {6 Add entries to global environment } *)
 
 val add_constant : constant -> constant_body -> env -> env
+val add_constant_key : constant -> constant_body -> Pre_env.link_info ref ->
+  env -> env
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
@@ -136,7 +138,7 @@ val constant_type      : env -> constant -> constant_type
 val constant_opt_value : env -> constant -> constr option
 
 (** {5 Inductive types } *)
-
+val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env
 val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 
 (** Looks up in the context of global inductive names 
@@ -229,4 +231,5 @@ val unregister : env -> field -> env
 
 val register : env -> field -> Retroknowledge.entry -> env
 
-
+(** Native compiler *)
+val no_link_info : unit -> Pre_env.link_info ref
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 50c052abb..214aac5ec 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -686,8 +686,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
       mind_nparams_rec = nmr;
       mind_params_ctxt = params;
       mind_packets = packets;
-      mind_constraints = cst;
-      mind_native_name = ref NotLinked
+      mind_constraints = cst
     }
 
 (************************************************************************)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6a0a952f7..2942412f0 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -302,28 +302,37 @@ let add_retroknowledge mp =
 
 (** {6 Adding a module in the environment } *)
 
-let rec add_structure mp sign resolver env =
+let rec add_structure mp sign resolver linkinfo env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
       let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
-      Environ.add_constant c cb env
+      Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
       let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in
-      Environ.add_mind mind mib env
-    |SFBmodule mb -> add_module mb env (* adds components as well *)
+      Environ.add_mind_key mind (mib,linkinfo) env
+    |SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
     |SFBmodtype mtb -> Environ.add_modtype mtb env
   in
   List.fold_left add_one env sign
 
-and add_module mb env =
+and add_module mb linkinfo env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mb env in
   match mb.mod_type with
   |NoFunctor struc ->
     add_retroknowledge mp mb.mod_retroknowledge
-      (add_structure mp struc mb.mod_delta env)
+      (add_structure mp struc mb.mod_delta linkinfo env)
   |MoreFunctor _ -> env
 
+let add_linked_module mb linkinfo env =
+  add_module mb linkinfo env
+
+let add_structure mp sign resolver env =
+  add_structure mp sign resolver (no_link_info ()) env
+
+let add_module mb env =
+  add_module mb (no_link_info ()) env
+
 let add_module_type mp mtb env =
   add_module (module_body_of_type mp mtb) env
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 11eb876ad..f50dcfd63 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -49,6 +49,9 @@ val add_structure :
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
 
+(** same as add_module, but for a module whose native code has been linked by
+the native compiler. The linking information is updated. *)
+val add_linked_module : module_body -> Pre_env.link_info ref -> env -> env
 
 (** same, for a module type *)
 val add_module_type : module_path -> module_type_body -> env -> env
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index fd8844e00..219ccd220 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1169,6 +1169,9 @@ let string_of_dirpath s = "N"^string_of_dirpath s
 
 let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)
 
+let link_info_of_dirpath dir =
+  ref (Linked (mod_uid_of_dirpath dir ^ ".", false))
+
 let string_of_name x =
   match x with
     | Anonymous -> "anonymous" (* assert false *)
@@ -1540,15 +1543,10 @@ let compile_mind prefix ~interactive mb mind stack =
     in
     Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl
   in
-  let name =
-    if interactive then LinkedInteractive (prefix, false)
-    else Linked (prefix, false)
-  in
-  let upd = (mb.mind_native_name, name) in
-  Array.fold_left_i f stack mb.mind_packets, upd
+  Array.fold_left_i f stack mb.mind_packets
 
 type code_location_update =
-    Declarations.native_name ref * Declarations.native_name
+    link_info ref * link_info
 type code_location_updates =
   code_location_update Mindmap_env.t * code_location_update Cmap_env.t
 
@@ -1558,12 +1556,19 @@ let empty_updates = Mindmap_env.empty, Cmap_env.empty
 
 let compile_mind_deps env prefix ~interactive
     (comp_stack, (mind_updates, const_updates) as init) mind =
-  let mib = lookup_mind mind env in
-  if is_code_loaded ~interactive mib.mind_native_name
+  let mib,nameref = lookup_mind_key mind env in
+  if is_code_loaded ~interactive nameref
     || Mindmap_env.mem mind mind_updates
   then init
   else
-    let comp_stack, upd = compile_mind prefix ~interactive mib mind comp_stack in
+    let comp_stack =
+      compile_mind prefix ~interactive mib mind comp_stack
+    in
+    let name =
+      if interactive then LinkedInteractive (prefix, false)
+      else Linked (prefix, false)
+    in
+    let upd = (nameref, name) in
     let mind_updates = Mindmap_env.add mind upd mind_updates in
     (comp_stack, (mind_updates, const_updates))
 
@@ -1576,9 +1581,9 @@ let rec compile_deps env prefix ~interactive init t =
   | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
       let c = get_allias env c in
-      let cb = lookup_constant c env in
+      let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
-      if is_code_loaded ~interactive cb.const_native_name
+      if is_code_loaded ~interactive nameref
         || (Cmap_env.mem c const_updates)
       then init
       else
@@ -1588,7 +1593,7 @@ let rec compile_deps env prefix ~interactive init t =
       in
       let code, name = compile_constant env prefix ~interactive c cb.const_body in
       let comp_stack = code@comp_stack in
-      let const_updates = Cmap_env.add c (cb.const_native_name, name) const_updates in
+      let const_updates = Cmap_env.add c (nameref, name) const_updates in
       comp_stack, (mind_updates, const_updates)
   | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind
   | Case (ci, p, c, ac) ->
@@ -1597,31 +1602,15 @@ let rec compile_deps env prefix ~interactive init t =
       fold_constr (compile_deps env prefix ~interactive) init t
   | _ -> fold_constr (compile_deps env prefix ~interactive) init t
 
-let compile_constant_field env prefix con (code, (mupds, cupds)) cb =
-  let acc = (code, (mupds, cupds)) in
-  match cb.const_body with
-  | Def t ->
-    let t = Lazyconstr.force t in
-    let (code, (mupds, cupds)) =
-      compile_deps env prefix ~interactive:false acc t
-    in
-    let (gl, name) =
+let compile_constant_field env prefix con acc cb =
+    let (gl, _) =
       compile_constant ~interactive:false env prefix con cb.const_body
     in
-    let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
-    gl@code, (mupds, cupds)
-  | _ ->
-    let (gl, name) =
-      compile_constant env prefix ~interactive:false con cb.const_body
-    in
-    let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
-    gl@code, (mupds, cupds)
+    gl@acc
 
-let compile_mind_field prefix mp l (code, (mupds, cupds)) mb =
+let compile_mind_field prefix mp l acc mb =
   let mind = MutInd.make2 mp l in
-  let code, upd = compile_mind prefix ~interactive:false mb mind code in
-  let mupds = Mindmap_env.add mind upd mupds in
-  code, (mupds, cupds)
+  compile_mind prefix ~interactive:false mb mind acc
 
 let mk_open s = Gopen s
 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 5d8ae96f0..f6a0c79f4 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -51,14 +51,10 @@ val empty_updates : code_location_updates
 val register_native_file : string -> unit
 
 val compile_constant_field : env -> string -> constant ->
-  global list * code_location_updates ->
-  constant_body ->
-    global list * code_location_updates
+  global list -> constant_body -> global list
 
 val compile_mind_field : string -> module_path -> label ->
-  global list * code_location_updates ->
-  mutual_inductive_body ->
-    global list * code_location_updates
+  global list -> mutual_inductive_body -> global list
 
 val mk_conv_code : env -> string -> constr -> constr -> linkable_code
 val mk_norm_code : env -> string -> constr -> linkable_code
@@ -67,6 +63,8 @@ val mk_library_header : dir_path -> global list
 
 val mod_uid_of_dirpath : dir_path -> string
 
+val link_info_of_dirpath : dir_path -> link_info ref
+
 val update_locations : code_location_updates -> unit
 
 val add_header_comment : global list -> string -> global list
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index cfb128d50..7e46a0550 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -87,15 +87,15 @@ let shift subst = subs_shft (1, subst)
 
 (* Linked code location utilities *)
 let get_mind_prefix env mind =
-   let mib = lookup_mind mind env in
-   match !(mib.mind_native_name) with
+   let _,name = lookup_mind_key mind env in
+   match !name with
    | NotLinked -> ""
    | Linked (s,_) -> s
    | LinkedInteractive (s,_) -> s
 
 let get_const_prefix env c =
-   let cb = lookup_constant c env in
-   match !(cb.const_native_name) with
+   let _,(nameref,_) = lookup_constant_key c env in
+   match !nameref with
    | NotLinked -> ""
    | Linked (s,_) -> s
    | LinkedInteractive (s,_) -> s
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 55d348550..39717c351 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -24,7 +24,7 @@ let rec translate_mod prefix mp env mod_expr acc =
       List.fold_left (translate_field prefix mp env') acc struc
   | MoreFunctor _ -> acc
 
-and translate_field prefix mp env (code, upds as acc) (l,x) =
+and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
       let con = make_con mp empty_dirpath l in
@@ -45,13 +45,13 @@ let dump_library mp dp env mod_expr =
       let t0 = Sys.time () in
       clear_global_tbl ();
       clear_symb_tbl ();
-      let mlcode, upds =
-        List.fold_left (translate_field prefix mp env) ([],empty_updates) struc
+      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 (), upds
+      mlcode, get_symbols_tbl ()
   | _ -> assert false
 
 
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 3f413631c..a45402a43 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,7 +14,7 @@ open Nativecode
 compiler *)
 
 val dump_library : module_path -> dir_path -> env -> module_signature ->
-  global list * symbol array * code_location_updates
+  global list * symbol array
 
 val compile_library :
   dir_path -> global list -> string list -> string -> int
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index e543c4e68..d96492020 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -22,14 +22,26 @@ open Declarations
 
 (* The type of environments. *)
 
-
+(* The key attached to each constant is used by the VM to retrieve previous *)
+(* evaluations of the constant. It is essentially an index in the symbols table *)
+(* used by the VM. *)
 type key = int option ref
 
-type constant_key = constant_body * key
+(** Linking information for the native compiler. The boolean flag indicates if
+  the term is protected by a lazy tag. *)
+
+type link_info =
+  | Linked of string * bool
+  | LinkedInteractive of string * bool
+  | NotLinked
+
+type constant_key = constant_body * (link_info ref * key)
+
+type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
-  env_inductives : mutual_inductive_body Mindmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -139,5 +151,7 @@ let lookup_constant kn env =
 
 (* Mutual Inductives *)
 let lookup_mind kn env =
-  Mindmap_env.find kn env.env_globals.env_inductives
+  fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
+let lookup_mind_key kn env =
+  Mindmap_env.find kn env.env_globals.env_inductives
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f634719f9..b6b6b4828 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -14,14 +14,20 @@ open Declarations
 
 (** The type of environments. *)
 
+type link_info =
+  | Linked of string * bool
+  | LinkedInteractive of string * bool
+  | NotLinked
 
 type key = int option ref
 
-type constant_key = constant_body * key
+type constant_key = constant_body * (link_info ref * key)
+
+type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
-  env_inductives : mutual_inductive_body Mindmap_env.t;
+  env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -77,5 +83,5 @@ val lookup_constant_key : constant -> env -> constant_key
 val lookup_constant : constant -> env -> constant_body
 
 (** Mutual Inductives *)
+val lookup_mind_key : mutual_inductive -> env -> mind_key
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
-
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ac7a5bb93..ebfb99c73 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -679,9 +679,7 @@ let export senv dir =
   let ast, values =
     if !Flags.no_native_compiler then [], [||]
     else
-      let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in
-      Nativecode.update_locations upds;
-      ast, values
+      Nativelibrary.dump_library mp dir senv.env str
   in
   let lib = {
     comp_name = dir;
@@ -700,7 +698,11 @@ let import lib digest senv =
   let env = Environ.add_constraints mb.mod_constraints senv.env in
   (mp, lib.comp_natsymbs),
   { senv with
-    env = Modops.add_module mb env;
+    env =
+      (let linkinfo =
+	 Nativecode.link_info_of_dirpath lib.comp_name
+       in
+       Modops.add_linked_module mb linkinfo env);
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
     imports = (lib.comp_name,digest)::senv.imports;
     loads = (mp,mb)::senv.loads }
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 57d4a287b..b8c32ffe5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -174,7 +174,6 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
     const_type = typ;
     const_body_code = Cemitcodes.from_val (compile_constant_body env def);
     const_constraints = cst;
-    const_native_name = ref NotLinked;
     const_inline_code = inline_code }
 
 (*s Global and local constant declaration. *)