Merge PR #12679: Remove redundant data from VM case switch.

Reviewed-by: SkySkimmer
Ack-by: silene

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.