From e82e8e216c4955db58255062fb5c61c7b2aa3c2a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 13 Feb 2018 18:18:44 +0100
Subject: Better elaboration of pattern-matchings on primitive projections

This ensures that computations are shared as much as possible, mimicking
the "positive" records computational behavior if possible.
---
 pretyping/cases.ml        |  2 +-
 pretyping/inductiveops.ml | 20 +++++++++++---------
 2 files changed, 12 insertions(+), 10 deletions(-)

(limited to 'pretyping')

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 b1ab2d2b7..f839d5b98 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 *)
 
-- 
cgit v1.2.3