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.

9 files changed, 33 insertions, 38 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index aa650fbdc8..ac4972ed0d 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,6 +1,5 @@
 open Format
 open Term
-open Constr
 open Names
 open Cemitcodes
 open Vmvalues
@@ -8,9 +7,7 @@ open Vmvalues
 let ppripos (ri,pos) =
   (match ri with
   | Reloc_annot a ->
-      let sp,i = a.ci.ci_ind in
-      print_string
-        ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+      print_string "switch\n"
   | Reloc_const _ ->
       print_string "structured constant\n"
   | Reloc_getglobal kn ->
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
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 854a5ff63d..e5fa9bada1 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -262,19 +262,14 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       assert (from = 0) ;
-      let ci = sw.sw_annot.Vmvalues.ci in
       let ((mind,_ as ind), u), allargs = find_rectype_a env t in
-      let iv = if Typeops.should_invert_case env ci then
-          CaseInvert {univs=u; args=allargs}
-        else NoInvert
-      in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
       let params,realargs = Util.Array.chop nparams allargs in
       let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
         hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
-      let p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
+      let p, relevance = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env sigma ind mib mip u params p in
       (* calcul des branches *)
@@ -286,6 +281,11 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs c in
+      let ci = Inductiveops.make_case_info env ind relevance RegularStyle in
+      let iv = if Typeops.should_invert_case env ci then
+          CaseInvert {univs=u; args=allargs}
+        else NoInvert
+      in
       nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
@@ -296,17 +296,17 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
 and nf_predicate env sigma ind mip params v pT =
   match kind (whd_allnolet env pT) with
   | LetIn (name,b,t,pT) ->
-      let body =
+      let body, rel =
         nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
-      mkLetIn (name,b,t,body)
+      mkLetIn (name,b,t,body), rel
   | Prod (name,dom,codom) -> begin
     match whd_val v with
     | Vfun f ->
       let k = nb_rel env in
       let vb = reduce_fun k f in
-      let body =
+      let body, rel =
         nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
-      mkLambda(name,dom,body)
+      mkLambda(name,dom,body), rel
     | _ -> assert false
     end
   | _ ->
@@ -321,8 +321,10 @@ and nf_predicate env sigma ind mip params v pT =
       let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let r = Inductive.relevance_of_inductive env (fst ind) in
       let name = make_annot name r in
-      let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
-      mkLambda(name,dom,body)
+      let env = push_rel (LocalAssum (name,dom)) env in
+      let body = nf_vtype env sigma vb in
+      let rel = Retyping.relevance_of_type env sigma (EConstr.of_constr body) in
+      mkLambda(name,dom,body), rel
     | _ -> assert false
 
 and nf_args env sigma vargs ?from:(f=0) t =
diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index d3e2749088..3a6dfb1e11 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -171,6 +171,10 @@ End sFix.
 
 Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
 
+(* Check that VM/native properly keep the relevance of the predicate in the case info
+   (bad-relevance warning as error otherwise) *)
+Definition vm_rebuild_case := Eval vm_compute in eq_sind.
+
 Require Import ssreflect.
 
 Goal forall T : SProp, T -> True.