Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/…

…native

Reviewed-by: ppedrot

pretyping/nativenorm.ml

@@ -318,13 +318,12 @@ and nf_atom_type env sigma atom =
   | Avar id ->
       mkVar id, Typeops.type_of_variable env id
   | Acase(ans,accu,p,bs) ->
-      let () = if Typeops.should_invert_case env ans.asw_ci then
-          (* TODO implement case inversion readback (properly reducing
-             it is a problem for the kernel) *)
-          CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.")
-      in
       let a,ta = nf_accu_type env sigma accu in
       let ((mind,_),u as ind),allargs = find_rectype_a env ta in
+      let iv = if Typeops.should_invert_case env ans.asw_ci then
+          CaseInvert {univs=u; args=allargs}
+        else NoInvert
+      in
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
@@ -344,7 +343,7 @@ and nf_atom_type env sigma atom =
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
-      mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase
+      mkCase(ans.asw_ci, p, iv, a, branchs), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in

pretyping/vnorm.ml

@@ -263,12 +263,11 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
   | Zswitch sw :: stk ->
       assert (from = 0) ;
       let ci = sw.sw_annot.Vmvalues.ci in
-      let () = if Typeops.should_invert_case env ci then
-          (* TODO implement case inversion readback (properly reducing
-             it is a problem for the kernel) *)
-          CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.")
-      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
@@ -287,7 +286,7 @@ 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
-      nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk
+      nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
   | Zproj p :: stk ->
      assert (from = 0) ;
      let p' = Projection.make p true in

test-suite/success/sprop_uip.v

@@ -95,6 +95,32 @@ Section funext.
     := eq_refl.
 End funext.
 
+(* test reductions on inverted cases *)
+
+(* first check production of correct blocked cases *)
+Definition lazy_seq_rect := Eval lazy in seq_rect.
+Definition vseq_rect := Eval vm_compute in seq_rect.
+Definition native_seq_rect := Eval native_compute in seq_rect.
+Definition cbv_seq_rect := Eval cbv in seq_rect.
+
+(* check it reduces according to indices *)
+Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end.
+Ltac check := match goal with |- False => idtac end.
+Lemma foo (H:seq 0 0) : False.
+Proof.
+  reset.
+  Fail check. (* check that "reset" and "check" actually do something *)
+
+  lazy; check; reset.
+
+  (* TODO *)
+  vm_compute. Fail check.
+  native_compute. Fail check.
+  cbv. Fail check.
+  cbn. Fail check.
+  simpl. Fail check.
+Abort.
+
 (* check that extraction doesn't fall apart on matches with special reduction *)
 Require Extraction.