From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 kernel/csymtable.ml | 55 ++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 38 insertions(+), 17 deletions(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 01294895..bb9231d0 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -20,13 +20,15 @@ open Vmvalues
 open Cemitcodes
 open Cbytecodes
 open Declarations
-open Pre_env
+open Environ
 open Cbytegen
 
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
-external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode"
+
+type global_data = { mutable glob_len : int; mutable glob_val : values array }
 
 (*******************)
 (* Linkage du code *)
@@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 (* [global_data] contient les valeurs des constantes globales
    (axiomes,definitions), les annotations des switch et les structured
    constant *)
-external global_data : unit -> values array = "get_coq_global_data"
+let global_data = {
+  glob_len = 0;
+  glob_val = Array.make 4096 crazy_val;
+}
 
-(* [realloc_global_data n] augmente de n la taille de [global_data] *)
-external realloc_global_data : int -> unit = "realloc_coq_global_data"
+let get_global_data () = Vmvalues.vm_global global_data.glob_val
 
-let check_global_data n =
-  if n >= Array.length (global_data()) then realloc_global_data n
+let realloc_global_data n =
+  let n = min (2 * n + 0x100) Sys.max_array_length in
+  let ans = Array.make n crazy_val in
+  let src = global_data.glob_val in
+  let () = Array.blit src 0 ans 0 (Array.length src) in
+  global_data.glob_val <- ans
 
-let num_global = ref 0
+let check_global_data n =
+  if n >= Array.length global_data.glob_val then realloc_global_data n
 
 let set_global v =
-  let n = !num_global in
+  let n = global_data.glob_len in
   check_global_data n;
-  (global_data()).(n) <- v;
-  incr num_global;
+  global_data.glob_val.(n) <- v;
+  global_data.glob_len <- global_data.glob_len + 1;
   n
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -68,11 +77,15 @@ module AnnotTable = Hashtbl.Make (struct
   let hash = hash_annot_switch
 end)
 
+module ProjNameTable = Hashtbl.Make (Projection.Repr)
+
 let str_cst_tbl : int SConstTable.t = SConstTable.create 31
 
 let annot_tbl : int AnnotTable.t = AnnotTable.create 31
     (* (annot_switch * int) Hashtbl.t  *)
 
+let proj_name_tbl : int ProjNameTable.t = ProjNameTable.create 31
+
 (*************************************************************)
 (*** Mise a jour des valeurs des variables et des constantes *)
 (*************************************************************)
@@ -106,6 +119,13 @@ let slot_for_annot key =
     AnnotTable.add annot_tbl key n;
     n
 
+let slot_for_proj_name key =
+  try ProjNameTable.find proj_name_tbl key
+  with Not_found ->
+    let n =  set_global (val_of_proj_name key) in
+    ProjNameTable.add proj_name_tbl key n;
+    n
+
 let rec slot_for_getglobal env kn =
   let (cb,(_,rk)) = lookup_constant_key kn env in
   try key rk
@@ -133,23 +153,23 @@ and slot_for_fv env fv =
       | None -> v_of_id id, Id.Set.empty
       | Some c ->
           val_of_constr (env_of_id id env) c,
-          Environ.global_vars_set (Environ.env_of_pre_env env) c in
+          Environ.global_vars_set env c in
     build_lazy_val cache (v, d); v in
   let val_of_rel i = val_of_rel (nb_rel env - i) in
   let idfun _ x = x in
   match fv with
   | FVnamed id ->
-      let nv = Pre_env.lookup_named_val id env in
+      let nv = lookup_named_val id env in
       begin match force_lazy_val nv with
       | None ->
-	 env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
+         env |> lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
-      let rv = Pre_env.lookup_rel_val i env in
+      let rv = lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-        env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
+        env |> lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVevar evk -> val_of_evar evk
@@ -161,10 +181,11 @@ and eval_to_patch env (buff,pl,fv) =
     | Reloc_annot a -> slot_for_annot a
     | Reloc_const sc -> slot_for_str_cst sc
     | Reloc_getglobal kn -> slot_for_getglobal env kn
+    | Reloc_proj_name p -> slot_for_proj_name p
   in
   let tc = patch buff pl slots in
   let vm_env = Array.map (slot_for_fv env) fv in
-  eval_tcode tc vm_env
+  eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
   match compile ~fail_on_error:true env c with
-- 
cgit v1.2.3