Remove redundant data from VM case switch.

No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.

Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.

6 files changed, 14 insertions, 22 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9921208e04..15cc451ea8 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1187,7 +1187,7 @@ value coq_interprete
             if (sz == 0) accu = Atom(0);
             else {
               Alloc_small(accu, sz, Default_tag);
-              if (Field(*sp, 2) == Val_true) {
+              if (Is_tailrec_switch(*sp)) {
                 for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
               }else{
                 for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 86ae6295fd..a19f9b56c1 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -32,6 +32,7 @@
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
 #define Is_double(v) (Tag_val(v) == Double_tag)
+#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
 
 /* coq array */
 #define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7bff377238..bacc308e1f 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont =
       done;
 
       let annot =
-        {ci = ci; rtbl = rtbl; tailcall = is_tailcall;
+        {rtbl = rtbl; tailcall = is_tailcall;
          max_stack_size = !max_stack_size - sz}
       in
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6b4daabf0c..ed475dca7e 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -13,7 +13,6 @@
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
 open Names
-open Constr
 open Vmvalues
 open Cbytecodes
 open Copcodes
@@ -424,12 +423,11 @@ let subst_strcst s sc =
   | Const_float _ -> sc
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
+let subst_annot _ (a : annot_switch) = a
+
 let subst_reloc s ri =
   match ri with
-  | Reloc_annot a ->
-      let (kn,i) = a.ci.ci_ind in
-      let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
-      Reloc_annot {a with ci = ci}
+  | Reloc_annot a -> Reloc_annot (subst_annot s a)
   | 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_proj_repr s p)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index ec429d5f9e..de604176cb 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 open Names
 open Univ
-open Constr
 
 (********************************************)
 (* Initialization of the abstract machine ***)
@@ -61,8 +60,9 @@ type structured_constant =
 
 type reloc_table = (tag * int) array
 
+(** When changing this, adapt Is_tailrec_switch in coq_values.h accordingly *)
 type annot_switch =
-   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+   { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
 
 let rec eq_structured_values v1 v2 =
   v1 == v2 ||
@@ -123,22 +123,16 @@ let hash_structured_constant c =
   | Const_float f -> combinesmall 7 (Float64.hash f)
 
 let eq_annot_switch asw1 asw2 =
-  let eq_ci ci1 ci2 =
-    eq_ind ci1.ci_ind ci2.ci_ind &&
-    Int.equal ci1.ci_npar ci2.ci_npar &&
-    CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
-  in
   let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
-  eq_ci asw1.ci asw2.ci &&
   CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
-  (asw1.tailcall : bool) == asw2.tailcall
+  (asw1.tailcall : bool) == asw2.tailcall &&
+  Int.equal asw1.max_stack_size asw2.max_stack_size
 
 let hash_annot_switch asw =
   let open Hashset.Combine in
-  let h1 = Constr.case_info_hash asw.ci in
-  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
-  let h3 = if asw.tailcall then 1 else 0 in
-  combine3 h1 h2 h3
+  let h1 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+  let h2 = if asw.tailcall then 1 else 0 in
+  combine3 h1 h2 asw.max_stack_size
 
 let pp_sort s =
   let open Sorts in
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f4070a02a3..f6efd49cfc 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 
 (** Values *)
 
@@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t
 type reloc_table = (tag * int) array
 
 type annot_switch =
-   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
+   { rtbl : reloc_table; tailcall : bool; max_stack_size : int }
 
 val eq_structured_constant : structured_constant -> structured_constant -> bool
 val hash_structured_constant : structured_constant -> int