From a0080f11d2d1702f5edb850a096b740fa2f905f7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 17:20:19 +0100
Subject: Statically ensure that native update locations are of form Linked*.

---
 kernel/nativecode.ml | 52 ++++++++++++++++++++++++++--------------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 911a879394..da984a7cfe 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1933,7 +1933,7 @@ and compile_named env sigma univ auxdefs id =
   | LocalAssum _ ->
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
-let compile_constant env sigma prefix ~interactive con cb =
+let compile_constant env sigma con cb =
     let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
     begin match cb.const_body with
     | Def t ->
@@ -1942,10 +1942,6 @@ let compile_constant env sigma prefix ~interactive con cb =
       if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
-      let name =
-        if interactive then LinkedInteractive prefix
-        else Linked prefix
-      in
       let l = Constant.label con in
       let auxdefs,code =
         if no_univs then compile_with_fv env sigma None [] (Some l) code
@@ -1959,7 +1955,7 @@ let compile_constant env sigma prefix ~interactive con cb =
         optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
       in
       if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
-      code, name
+      code
     | _ ->
         let i = push_symbol (SymbConst con) in
         let args =
@@ -1969,9 +1965,7 @@ let compile_constant env sigma prefix ~interactive con cb =
         (*
         let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
          *)
-        [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)],
-          if interactive then LinkedInteractive prefix
-          else Linked prefix
+        [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)]
     end
 
 module StringOrd = struct type t = string let compare = String.compare end
@@ -2049,8 +2043,12 @@ let compile_mind mb mind stack =
   in
   Array.fold_left_i f stack mb.mind_packets
 
-type code_location_update =
-    link_info ref * link_info
+type code_location_update = {
+  upd_info : link_info ref;
+  upd_interactive : bool;
+  upd_prefix : string;
+}
+
 type code_location_updates =
   code_location_update Mindmap_env.t * code_location_update Cmap_env.t
 
@@ -2068,11 +2066,11 @@ let compile_mind_deps env prefix ~interactive
     let comp_stack =
       compile_mind mib mind comp_stack
     in
-    let name =
-      if interactive then LinkedInteractive prefix
-      else Linked prefix
-    in
-    let upd = (nameref, name) in
+    let upd = {
+      upd_info = nameref;
+      upd_interactive = interactive;
+      upd_prefix = prefix;
+    } in
     let mind_updates = Mindmap_env.add mind upd mind_updates in
     (comp_stack, (mind_updates, const_updates))
 
@@ -2096,11 +2094,14 @@ let compile_deps env sigma prefix ~interactive init t =
            aux env lvl init (Mod_subst.force_constr t)
         | _ -> init
       in
-      let code, name =
-        compile_constant env sigma prefix ~interactive c cb
-      in
+      let code = compile_constant env sigma c cb in
+      let upd = {
+        upd_info = nameref;
+        upd_interactive = interactive;
+        upd_prefix = prefix;
+      } in
       let comp_stack = code@comp_stack in
-      let const_updates = Cmap_env.add c (nameref, name) const_updates in
+      let const_updates = Cmap_env.add c upd const_updates in
       comp_stack, (mind_updates, const_updates)
   | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
@@ -2130,11 +2131,8 @@ let compile_deps env sigma prefix ~interactive init t =
   in
   aux env 0 init t
 
-let compile_constant_field env prefix con acc cb =
-    let (gl, _) =
-      compile_constant ~interactive:false env empty_evars prefix
-        con cb
-    in
+let compile_constant_field env _prefix con acc cb =
+    let gl = compile_constant env empty_evars con cb in
     gl@acc
 
 let compile_mind_field mp l acc mb =
@@ -2196,7 +2194,9 @@ let mk_library_header (symbols : Nativevalues.symbols) =
   let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in
   [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
 
-let update_location (r,v) = r := v
+let update_location r =
+  let v = if r.upd_interactive then LinkedInteractive r.upd_prefix else Linked r.upd_prefix in
+  r.upd_info := v
 
 let update_locations (ind_updates,const_updates) =
   Mindmap_env.iter (fun _ -> update_location) ind_updates;
-- 
cgit v1.2.3


From c12471f1c5192ba1f18adac2109913c7b55ae50b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 18:22:12 +0100
Subject: Statically ensure that the native interactive flag is always set to
 true.

It was a hidden invariant of the code.
---
 kernel/nativecode.ml | 31 ++++++++++++++-----------------
 1 file changed, 14 insertions(+), 17 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index da984a7cfe..1b9a110379 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1978,11 +1978,11 @@ let is_loaded_native_file s = StringSet.mem s !loaded_native_files
 let register_native_file s =
   loaded_native_files := StringSet.add s !loaded_native_files
 
-let is_code_loaded ~interactive name =
+let is_code_loaded name =
   match !name with
   | NotLinked -> false
   | LinkedInteractive s ->
-      if (interactive && is_loaded_native_file s) then true
+      if (is_loaded_native_file s) then true
       else (name := NotLinked; false)
   | Linked s ->
       if is_loaded_native_file s then true
@@ -2045,7 +2045,6 @@ let compile_mind mb mind stack =
 
 type code_location_update = {
   upd_info : link_info ref;
-  upd_interactive : bool;
   upd_prefix : string;
 }
 
@@ -2056,10 +2055,10 @@ type linkable_code = global list * code_location_updates
 
 let empty_updates = Mindmap_env.empty, Cmap_env.empty
 
-let compile_mind_deps env prefix ~interactive
+let compile_mind_deps env prefix
     (comp_stack, (mind_updates, const_updates) as init) mind =
   let mib,nameref = lookup_mind_key mind env in
-  if is_code_loaded ~interactive nameref
+  if is_code_loaded nameref
     || Mindmap_env.mem mind mind_updates
   then init
   else
@@ -2068,7 +2067,6 @@ let compile_mind_deps env prefix ~interactive
     in
     let upd = {
       upd_info = nameref;
-      upd_interactive = interactive;
       upd_prefix = prefix;
     } in
     let mind_updates = Mindmap_env.add mind upd mind_updates in
@@ -2076,15 +2074,15 @@ let compile_mind_deps env prefix ~interactive
 
 (* This function compiles all necessary dependencies of t, and generates code in
    reverse order, as well as linking information updates *)
-let compile_deps env sigma prefix ~interactive init t =
+let compile_deps env sigma prefix init t =
   let rec aux env lvl init t =
   match kind t with
-  | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind
+  | Ind ((mind,_),_u) -> compile_mind_deps env prefix init mind
   | Const c ->
     let c,_u = get_alias env c in
     let cb,(nameref,_) = lookup_constant_key c env in
     let (_, (_, const_updates)) = init in
-    if is_code_loaded ~interactive nameref
+    if is_code_loaded nameref
     || (Cmap_env.mem c const_updates)
     then init
     else
@@ -2097,19 +2095,18 @@ let compile_deps env sigma prefix ~interactive init t =
       let code = compile_constant env sigma c cb in
       let upd = {
         upd_info = nameref;
-        upd_interactive = interactive;
         upd_prefix = prefix;
       } in
       let comp_stack = code@comp_stack in
       let const_updates = Cmap_env.add c upd const_updates in
       comp_stack, (mind_updates, const_updates)
-  | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind
+  | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix init mind
   | Proj (p,c) ->
-    let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
+    let init = compile_mind_deps env prefix init (Projection.mind p) in
     aux env lvl init c
   | Case (ci, _p, _iv, _c, _ac) ->
       let mind = fst ci.ci_ind in
-      let init = compile_mind_deps env prefix ~interactive init mind in
+      let init = compile_mind_deps env prefix init mind in
       fold_constr_with_binders succ (aux env) lvl init t
   | Var id ->
     let open Context.Named.Declaration in
@@ -2150,11 +2147,11 @@ let mk_conv_code env sigma prefix t1 t2 =
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
-    compile_deps env sigma prefix ~interactive:true init t1
+    compile_deps env sigma prefix init t1
   in
   let gl, (mind_updates, const_updates) =
     let init = (gl, (mind_updates, const_updates)) in
-    compile_deps env sigma prefix ~interactive:true init t2
+    compile_deps env sigma prefix init t2
   in
   let code1 = lambda_of_constr env sigma t1 in
   let code2 = lambda_of_constr env sigma t2 in
@@ -2177,7 +2174,7 @@ let mk_norm_code env sigma prefix t =
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
-    compile_deps env sigma prefix ~interactive:true init t
+    compile_deps env sigma prefix init t
   in
   let code = lambda_of_constr env sigma t in
   let (gl,code) = compile_with_fv env sigma None gl None code in
@@ -2195,7 +2192,7 @@ let mk_library_header (symbols : Nativevalues.symbols) =
   [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
 
 let update_location r =
-  let v = if r.upd_interactive then LinkedInteractive r.upd_prefix else Linked r.upd_prefix in
+  let v = LinkedInteractive r.upd_prefix in
   r.upd_info := v
 
 let update_locations (ind_updates,const_updates) =
-- 
cgit v1.2.3


From 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 18:26:21 +0100
Subject: Merge the Linked and LinkedInteractive constructors.

There was not any difference between those after the cleanup patches that
come before.
---
 kernel/nativecode.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1b9a110379..09db29d222 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1981,9 +1981,6 @@ let register_native_file s =
 let is_code_loaded name =
   match !name with
   | NotLinked -> false
-  | LinkedInteractive s ->
-      if (is_loaded_native_file s) then true
-      else (name := NotLinked; false)
   | Linked s ->
       if is_loaded_native_file s then true
       else (name := NotLinked; false)
@@ -2192,8 +2189,7 @@ let mk_library_header (symbols : Nativevalues.symbols) =
   [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
 
 let update_location r =
-  let v = LinkedInteractive r.upd_prefix in
-  r.upd_info := v
+  r.upd_info := Linked r.upd_prefix
 
 let update_locations (ind_updates,const_updates) =
   Mindmap_env.iter (fun _ -> update_location) ind_updates;
-- 
cgit v1.2.3