From aacfda0817557e0e3530966282a7ba1b303590b2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Jul 2020 13:19:06 +0200
Subject: Correctly readback blocked CaseInvert matches in VM/native

---
 pretyping/nativenorm.ml        | 11 +++++------
 pretyping/vnorm.ml             | 11 +++++------
 test-suite/success/sprop_uip.v | 26 ++++++++++++++++++++++++++
 3 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 89bd7e196f..e99f6ad0d3 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -317,13 +317,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
@@ -343,7 +342,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
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index efe1efd74e..bad718860a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -262,12 +262,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
@@ -286,7 +285,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
diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v
index 508cc2be7d..eae1b75689 100644
--- a/test-suite/success/sprop_uip.v
+++ b/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.
 
-- 
cgit v1.2.3