[VM] Remove projection names from structured constants.

It was actually a hack since those names are never used to represent
values, only to be passed as arguments to bytecode instructions. So
instead of reusing the structured_constant type, we follow the same
pattern as switch annotations.

7 files changed, 31 insertions, 12 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 599856b64..521f540d2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -36,7 +36,6 @@ let last_variant_tag = 245
 type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive
-  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
   | Const_univ_level of Univ.Level.t
@@ -51,8 +50,6 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sort _, _ -> false
 | Const_ind i1, Const_ind i2 -> eq_ind i1 i2
 | Const_ind _, _ -> false
-| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
-| Const_proj _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
@@ -66,13 +63,12 @@ let rec hash_structured_constant c =
   match c with
   | Const_sort s -> combinesmall 1 (Sorts.hash s)
   | Const_ind i -> combinesmall 2 (ind_hash i)
-  | Const_proj p -> combinesmall 3 (Constant.hash p)
-  | Const_b0 t -> combinesmall 4 (Int.hash t)
+  | Const_b0 t -> combinesmall 3 (Int.hash t)
   | Const_bn (t, a) ->
     let fold h c = combine h (hash_structured_constant c) in
     let h = Array.fold_left fold 0 a in
-    combinesmall 5 (combine (Int.hash t) h)
-  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+    combinesmall 4 (combine (Int.hash t) h)
+  | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l)
 
 let eq_annot_switch asw1 asw2 =
   let eq_ci ci1 ci2 =
@@ -246,7 +242,6 @@ let pp_sort s =
 let rec pp_struct_const = function
   | Const_sort s -> pp_sort s
   | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
-  | Const_proj p -> Constant.print p
   | Const_b0 i -> int i
   | Const_bn (i,t) ->
      int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03b6bc619..238edc0af 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -30,7 +30,6 @@ val last_variant_tag : tag
 type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive
-  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
   | Const_univ_level of Univ.Level.t
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index f4e6d45c2..2426255e4 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -27,6 +27,7 @@ type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
   | Reloc_getglobal of Names.Constant.t
+  | Reloc_proj_name of Constant.t
 
 let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
@@ -35,6 +36,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_const _, _ -> false
 | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
 | Reloc_getglobal _, _ -> false
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Constant.equal p1 p2
+| Reloc_proj_name _, _ -> false
 
 let hash_reloc_info r =
   let open Hashset.Combine in
@@ -42,6 +45,7 @@ let hash_reloc_info r =
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+  | Reloc_proj_name p -> combinesmall 4 (Constant.hash p)
 
 module RelocTable = Hashtbl.Make(struct
   type t = reloc_info
@@ -187,6 +191,9 @@ let slot_for_getglobal env p =
   enter env (Reloc_getglobal p);
   out_int env 0
 
+let slot_for_proj_name env p =
+  enter env (Reloc_proj_name p);
+  out_int env 0
 
 (* Emission of one instruction *)
 
@@ -277,7 +284,7 @@ let emit_instr env = function
       if n <= 1 then out env (opSETFIELD0+n)
       else (out env opSETFIELD;out_int env n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
-  | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p)
+  | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
   (* spiwack *)
   | Kbranch lbl -> out env opBRANCH; out_label env lbl
@@ -353,7 +360,6 @@ type to_patch = emitcodes * patches * fv
 let rec subst_strcst s sc =
   match sc with
   | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
-  | Const_proj p -> Const_proj (subst_constant s p)
   | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
@@ -365,6 +371,7 @@ let subst_reloc s ri =
       Reloc_annot {a with ci = ci}
   | Reloc_const sc -> Reloc_const (subst_strcst s sc)
   | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
+  | Reloc_proj_name p -> Reloc_proj_name (subst_constant s p)
 
 let subst_patches subst p =
   let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 03920dc1a..696721c37 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -5,6 +5,7 @@ type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
   | Reloc_getglobal of Constant.t
+  | Reloc_proj_name of Constant.t
 
 type patches
 type emitcodes
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 9bacdb65f..bbe093782 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -77,11 +77,19 @@ module AnnotTable = Hashtbl.Make (struct
   let hash = hash_annot_switch
 end)
 
+module ProjNameTable = Hashtbl.Make (struct
+  type t = Constant.t
+  let equal = Constant.equal
+  let hash = Constant.hash
+end)
+
 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 *)
 (*************************************************************)
@@ -115,6 +123,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
@@ -170,6 +185,7 @@ 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
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 7a703e653..8524c44d2 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -297,7 +297,6 @@ let rec obj_of_str_const str =
   match str with
   | Const_sort s -> obj_of_atom (Asort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
-  | Const_proj p -> Obj.repr p
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
@@ -355,6 +354,7 @@ let val_of_constant c = val_of_idkey (ConstKey c)
 let val_of_evar evk = val_of_idkey (EvarKey evk)
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Constant.t -> values = "%identity"
 
 (*************************************************)
 (** Operations manipulating data types ***********)
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 550791b2c..08d05a038 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -112,6 +112,7 @@ val val_of_proj : Constant.t -> values -> values
 val val_of_atom : atom -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
+external val_of_proj_name : Constant.t -> values = "%identity"
 
 (** Destructors *)