Merge PR #6754: Better elaboration of pattern-matchings on primitive projections

4 files changed, 35 insertions, 10 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0dd3c5944..93ca9dc5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) =
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
           let pred = nf_betaiota pb.env !(pb.evdref) pred in
 	  let case =
-	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
+            make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
           let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1a790be64..1003f86c5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -356,8 +356,8 @@ let make_case_or_project env sigma indf ci pred c branches =
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
      assert(Array.length branches == 1);
+     let na, ty, t = destLambda sigma pred in
      let () =
-       let _, _, t = destLambda sigma pred in
        let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (Vars.noccurn sigma 1 t) &&
@@ -368,16 +368,18 @@ let make_case_or_project env sigma indf ci pred c branches =
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
-     let n, subst =
+     let n, len, ctx =
        List.fold_right
-         (fun decl (i, subst) ->
+         (fun decl (i, j, ctx) ->
           match decl with
-          | LocalAssum (na, t) ->
-             let t = mkProj (Projection.make ps.(i) true, c) in
-             (i + 1, t :: subst)
-          | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
-         ctx (0, [])
-     in Vars.substl subst br
+          | LocalAssum (na, ty) ->
+             let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+             (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+          | LocalDef (na, b, ty) ->
+             (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+         ctx (0, 1, [])
+     in
+     mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
 
 (* substitution in a signature *)
 
diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
index de2857b43..2f0d8bf8c 100644
--- a/test-suite/success/letproj.v
+++ b/test-suite/success/letproj.v
@@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) :=
 
 Scheme foo_case := Case for Foo Sort Type.
 
+Definition test' (A : Type) (f : Foo A) :=
+  let 'Build_Foo _ x y := f in x.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 31a1608c4..7ca2767a5 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -199,3 +199,24 @@ split.
 reflexivity.
 Qed.
 *)
+
+(* Primitive projection match compilation *)
+Require Import List.
+Set Primitive Projections.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {_ _} _ _.
+
+Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) :=
+  match n with
+  | 0 => pair nil l
+  | S n =>
+    match l with
+    | nil => pair nil nil
+    | x :: l => let 'pair l1 l2 := split_at l n in pair (x :: l1) l2
+    end
+  end.
+
+Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *)
+Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *)
+Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *)