From 74d700e9f7fcb14e7136e87b5efab25d5adb194b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 1 Jun 2018 16:23:29 +0200
Subject: Getting rid of the const_proj field in the kernel.

This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
---
 checker/cic.mli                  | 1 -
 checker/environ.ml               | 3 ---
 checker/environ.mli              | 1 -
 checker/values.ml                | 3 +--
 kernel/cooking.ml                | 2 --
 kernel/cooking.mli               | 1 -
 kernel/declarations.ml           | 1 -
 kernel/declareops.ml             | 1 -
 kernel/environ.ml                | 2 +-
 kernel/term_typing.ml            | 5 -----
 library/heads.ml                 | 2 +-
 plugins/extraction/extraction.ml | 4 ++--
 12 files changed, 5 insertions(+), 21 deletions(-)

diff --git a/checker/cic.mli b/checker/cic.mli
index 7ec345768..5543e5720 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -241,7 +241,6 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
diff --git a/checker/environ.ml b/checker/environ.ml
index 809150cea..3d5fac806 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -166,9 +166,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let is_projection cst env = 
-  (lookup_constant cst env).const_proj
-
 let lookup_projection p env =
   Cmap_env.find (Projection.constant p) env.env_globals.env_projections
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 4a7597249..acb29d7d2 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val is_projection : Constant.t -> env -> bool
 val lookup_projection : Projection.t -> env -> projection_body
 
 (* Inductives *)
diff --git a/checker/values.ml b/checker/values.ml
index 67032bd1b..f1c4fd470 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
+MD5 3d9612f0adc70404fddb093b85c7d168 checker/cic.mli
 
 *)
 
@@ -241,7 +241,6 @@ let v_cb = v_tuple "constant_body"
     Any;
     v_const_univs;
     v_bool;
-    v_bool;
     v_typing_flags|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5783453e6..68057b389 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,6 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : bool;
   cook_universes : constant_universes;
   cook_inline : inline;
   cook_context : Context.Named.t option;
@@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } =
   {
     cook_body = body;
     cook_type = typ;
-    cook_proj = cb.const_proj;
     cook_universes = univs;
     cook_inline = cb.const_inline_code;
     cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0d907f3de..76c79335f 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,6 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : bool;
   cook_universes : constant_universes;
   cook_inline : inline;
   cook_context : Context.Named.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..02871153b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,7 +87,6 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
-    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
                                            were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 75c0e5b4c..fc6dc8b9e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -100,7 +100,6 @@ let subst_const_body sub cb =
       { const_hyps = [];
         const_body = body';
         const_type = type';
-        const_proj = cb.const_proj;
         const_body_code =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index fb89576dd..2d6c9117b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -490,7 +490,7 @@ let lookup_projection cst env =
   Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
 
 let is_projection cst env =
-  (lookup_constant cst env).const_proj
+  Cmap_env.mem cst env.env_globals.env_projections
 
 (* Mutual Inductives *)
 let polymorphic_ind (mind,i) env =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index db1109e75..d29f2ca82 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
-        cook_proj = false;
         cook_universes = univs;
         cook_inline = false;
         cook_context = ctx;
@@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = false;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -343,7 +341,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = false;
         cook_universes = univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -370,7 +367,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
     {
       Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
       cook_type = typ;
-      cook_proj = true;
       cook_universes = univs;
       cook_inline = false;
       cook_context = None;
@@ -464,7 +460,6 @@ let build_constant_declaration kn env result =
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_proj = result.cook_proj;
     const_body_code = tps;
     const_universes = univs;
     const_inline_code = result.cook_inline;
diff --git a/library/heads.ml b/library/heads.ml
index 3d5f6a6ff..d9d650ac0 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -129,7 +129,7 @@ let compute_head = function
    let cb = Environ.lookup_constant cst env in
    let is_Def = function Declarations.Def _ -> true | _ -> false in
    let body = 
-     if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body
+     if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body
      then Global.body_of_constant cst else None
    in
      (match body with
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 5aee70194..b1ee21536 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1065,7 +1065,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
@@ -1078,7 +1078,7 @@ let extract_constant env kn cb =
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
-	     (match cb.const_proj with
+             (match Environ.is_projection kn env with
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-- 
cgit v1.2.3


From 4513b7735779fb440223e6f22079994528249047 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 2 Jun 2018 15:11:09 +0200
Subject: Remove special declaration of primitive projections in the kernel.

This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.
---
 interp/declare.ml     | 34 +++++++++++++++++++++++++---------
 kernel/entries.ml     |  5 -----
 kernel/term_typing.ml | 26 --------------------------
 3 files changed, 25 insertions(+), 40 deletions(-)

diff --git a/interp/declare.ml b/interp/declare.ml
index bc2d2068a..39c83f47e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -382,17 +382,33 @@ let inInductive : inductive_obj -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = infer_inductive_subtyping }
 
-let declare_projections mind =
+let declare_projections univs mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) ->
-      Array.iteri (fun i kn ->
+    | Some (Some (_, kns, pbs)) ->
+      Array.iter2 (fun kn pb ->
 	let id = Label.to_id (Constant.label kn) in
-	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent)
-	in
-	  assert(Constant.equal kn kn')) kns; true,true
+        let univs = match univs with
+        | Monomorphic_ind_entry _ ->
+          (** Global constraints already defined through the inductive *)
+          Monomorphic_const_entry Univ.ContextSet.empty
+        | Polymorphic_ind_entry ctx ->
+          Polymorphic_const_entry ctx
+        | Cumulative_ind_entry ctx ->
+          Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
+        in
+        let term, types = match univs with
+        | Monomorphic_const_entry _ -> pb.proj_eta
+        | Polymorphic_const_entry ctx ->
+          let u = Univ.UContext.instance ctx in
+          let term, types = pb.proj_eta in
+          Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+        in
+        let entry = definition_entry ~types ~univs term in
+        let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+        assert (Constant.equal kn kn')
+      ) kns pbs;
+      true, true
     | Some None -> true,false
     | None -> false,false
 
@@ -403,7 +419,7 @@ let declare_mind mie =
     | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
-  let isrecord,isprim = declare_projections mind in
+  let isrecord,isprim = declare_projections mie.mind_entry_universes mind in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94da00c7e..3c555f8c7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *)
 type parameter_entry = 
     Context.Named.t option * types in_constant_universes_entry * inline
 
-type projection_entry = {
-  proj_entry_ind : MutInd.t;
-  proj_entry_arg : int }
-
 type 'a constant_entry =
   | DefinitionEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
-  | ProjectionEntry of projection_entry
 
 (** {6 Modules } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d29f2ca82..37bf679c5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -346,32 +346,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
-  | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
-    let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
-    let kn, pb = 
-      match mib.mind_record with
-      | Some (Some (id, kns, pbs)) -> 
-	if i < Array.length pbs then
-	  kns.(i), pbs.(i)
-	else assert false
-      | _ -> assert false
-    in
-    let univs =
-      match mib.mind_universes with
-      | Monomorphic_ind ctx -> Monomorphic_const ctx
-      | Polymorphic_ind auctx -> Polymorphic_const auctx
-      | Cumulative_ind acumi ->
-        Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
-    in
-    let term, typ = pb.proj_eta in
-    {
-      Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
-      cook_type = typ;
-      cook_universes = univs;
-      cook_inline = false;
-      cook_context = None;
-    }
-
 let record_aux env s_ty s_bo =
   let in_ty = keep_hyps env s_ty in
   let v =
-- 
cgit v1.2.3


From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 4 Jun 2018 13:32:35 +0200
Subject: Remove the proj_eta field of the kernel.

This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
---
 checker/cic.mli            |   1 -
 checker/subtyping.ml       |   2 -
 checker/values.ml          |   6 +--
 interp/declare.ml          |  13 +++---
 kernel/declarations.ml     |   1 -
 kernel/indtypes.ml         |   6 +--
 pretyping/inductiveops.ml  | 101 +++++++++++++++++++++++++++++++++++++++++++++
 pretyping/inductiveops.mli |   4 ++
 8 files changed, 115 insertions(+), 19 deletions(-)

diff --git a/checker/cic.mli b/checker/cic.mli
index 5543e5720..94958447e 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -211,7 +211,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
-  proj_eta : constr * constr; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility, the match version *)
 }
 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5c672d04a..6f9bf8fce 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -130,8 +130,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> fst x.proj_eta);
-    check (eq_constr) (fun x -> snd x.proj_eta);
     check (eq_constr) (fun x -> x.proj_body); true
   in
   let check_inductive_type t1 t2 =
diff --git a/checker/values.ml b/checker/values.ml
index f1c4fd470..12fbf1ff0 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 3d9612f0adc70404fddb093b85c7d168 checker/cic.mli
+MD5 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli
 
 *)
 
@@ -225,9 +225,7 @@ let v_cst_def =
 
 let v_projbody =
   v_tuple "projection_body"
-	  [|v_cst;Int;Int;v_constr;
-	    v_tuple "proj_eta" [|v_constr;v_constr|];
-	    v_constr|]
+    [|v_cst;Int;Int;v_constr;v_constr|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
diff --git a/interp/declare.ml b/interp/declare.ml
index 39c83f47e..aa737239b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -383,10 +383,12 @@ let inInductive : inductive_obj -> obj =
     rebuild_function = infer_inductive_subtyping }
 
 let declare_projections univs mind =
-  let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
+  let env = Global.env () in
+  let spec,_ = Inductive.lookup_mind_specif env (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pbs)) ->
-      Array.iter2 (fun kn pb ->
+    | Some (Some (_, kns, _)) ->
+      let projs = Inductiveops.compute_projections env (mind, 0) in
+      Array.iter2 (fun kn (term, types) ->
 	let id = Label.to_id (Constant.label kn) in
         let univs = match univs with
         | Monomorphic_ind_entry _ ->
@@ -398,16 +400,15 @@ let declare_projections univs mind =
           Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx)
         in
         let term, types = match univs with
-        | Monomorphic_const_entry _ -> pb.proj_eta
+        | Monomorphic_const_entry _ -> term, types
         | Polymorphic_const_entry ctx ->
           let u = Univ.UContext.instance ctx in
-          let term, types = pb.proj_eta in
           Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
         in
         let entry = definition_entry ~types ~univs term in
         let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
         assert (Constant.equal kn kn')
-      ) kns pbs;
+      ) kns projs;
       true, true
     | Some None -> true,false
     | None -> false,false
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 02871153b..abebec156 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,7 +54,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
-  proj_eta : constr * types; (* Eta-expanded term and type *)
   proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 439acd15b..4bc7ea198 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -869,14 +869,10 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let ty = substl subst t in
-	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
-	let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
-	let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-		     proj_arg = i; proj_type = projty; proj_eta = etab, etat; 
-		     proj_body = compat } in
+                      proj_arg = i; proj_type = projty; proj_body = compat } in
 	  (i + 1, j + 1, kn :: kns, body :: pbs,
 	   fterm :: subst, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b1ab2d2b7..4ad32fc66 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -454,6 +454,107 @@ let build_branch_type env sigma dep p cs =
 
 (**************************************************)
 
+(** From a rel context describing the constructor arguments,
+    build an expansion function.
+    The term built is expecting to be substituted first by
+    a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, _ as ind) =
+  let open Term in
+  let mib = Environ.lookup_mind kn env in
+  let indu = match mib.mind_universes with
+  | Monomorphic_ind _ -> mkInd ind
+  | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
+  | Cumulative_ind ctx ->
+    mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+  in
+  let x = match mib.mind_record with
+  | None | Some None ->
+    anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  | Some (Some (id, _, _)) -> Name id
+  in
+  (** FIXME: handle mutual records *)
+  let pkt = mib.mind_packets.(0) in
+  let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+  let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+  let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+  let mp, dp, l = MutInd.repr3 kn in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty =
+    (* [ty] = [Ind inst] is typed in context [params] *)
+    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+    let ty = mkApp (indu, inst) in
+    (* [Ind inst] is typed in context [params-wo-let] *)
+    ty
+  in
+  let ci =
+    let print_info =
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+      { ci_ind     = ind;
+        ci_npar    = nparamargs;
+        ci_cstr_ndecls = mind_consnrealdecls;
+        ci_cstr_nargs = mind_consnrealargs;
+        ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let compat_body ccl i =
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 indty, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+  in
+  let projections decl (j, pbs, subst) =
+    match decl with
+    | LocalDef (na,c,t) ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (j+1, pbs, subst)
+    | LocalAssum (na,t) ->
+      match na with
+      | Name id ->
+        let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+        let ty = substl subst t in
+        let term = mkProj (Projection.make kn true, mkRel 1) in
+        let fterm = mkProj (Projection.make kn false, mkRel 1) in
+        let compat = compat_body ty (j - 1) in
+        let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+        let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+        let body = (etab, etat, compat) in
+        (j + 1, body :: pbs, fterm :: subst)
+      | Anonymous ->
+        anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  in
+  let (_, pbs, subst) =
+    List.fold_right projections ctx (1, [], [])
+  in
+  Array.rev_of_list pbs
+
+let compute_projections ind mib =
+  let ans = compute_projections ind mib in
+  Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
 let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b0d714b03..506cdd8c9 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,6 +194,10 @@ val make_case_or_project :
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
 
+val compute_projections : Environ.env -> inductive -> (constr * types) array
+(** Given a primitive record type, for every field computes the eta-expanded
+    projection and its type. *)
+
 (********************)
 
 val type_of_inductive_knowing_conclusion :
-- 
cgit v1.2.3


From e43710b391c278ac7fcb808ec28d720b4317660c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 4 Jun 2018 15:26:20 +0200
Subject: Remove the proj_body field from the kernel.

This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.

Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.

Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
---
 checker/cic.mli                  |  1 -
 checker/subtyping.ml             |  2 +-
 checker/values.ml                |  4 +--
 kernel/declarations.ml           |  1 -
 kernel/declareops.ml             |  2 +-
 kernel/indtypes.ml               | 53 ++++++++--------------------------------
 kernel/indtypes.mli              |  2 +-
 plugins/extraction/extraction.ml | 12 +++++++--
 pretyping/detyping.ml            |  5 +++-
 pretyping/inductiveops.ml        |  3 +++
 pretyping/inductiveops.mli       |  8 ++++++
 11 files changed, 40 insertions(+), 53 deletions(-)

diff --git a/checker/cic.mli b/checker/cic.mli
index 94958447e..3304b032e 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -211,7 +211,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
-  proj_body : constr; (* For compatibility, the match version *)
 }
 
 type constant_def =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6f9bf8fce..f4ae02084 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -130,7 +130,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> x.proj_body); true
+    true
   in
   let check_inductive_type t1 t2 =
 
diff --git a/checker/values.ml b/checker/values.ml
index 12fbf1ff0..45f04f88d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli
+MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
 
 *)
 
@@ -225,7 +225,7 @@ let v_cst_def =
 
 let v_projbody =
   v_tuple "projection_body"
-    [|v_cst;Int;Int;v_constr;v_constr|]
+    [|v_cst;Int;Int;v_constr|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index abebec156..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,7 +54,6 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int; (** Projection index, starting from 0 *)
   proj_type : types; (* Type under params *)
-  proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
 (* Global declarations (i.e. constants) can be either: *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index fc6dc8b9e..1b73096f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -86,7 +86,7 @@ let subst_const_def sub def = match def with
 let subst_const_proj sub pb =
   { pb with proj_ind = subst_mind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
-    proj_body = subst_const_type sub pb.proj_body }
+  }
 
 let subst_const_body sub cb =
   assert (List.is_empty cb.const_hyps); (* we're outside sections *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4bc7ea198..14f2a3d8f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,16 +797,13 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+let compute_projections ((kn, _ as ind), u) nparamargs params
     mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
-  let indty, paramsletsubst =
-    (* [ty] = [Ind inst] is typed in context [params] *)
-    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
-    let ty = mkApp (mkIndU indu, inst) in
+  let paramsletsubst =
     (* [Ind inst] is typed in context [params-wo-let] *)
     let inst' = rel_list 0 nparamargs in
     (* {params-wo-let |- subst:params] *)
@@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
     let subst = (* For the record parameter: *)
       mkRel 1 :: List.map (lift 1) subst in
-      ty, subst
+    subst
   in
-  let ci = 
-    let print_info =
-      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-      { ci_ind     = ind;
-	ci_npar    = nparamargs;
-	ci_cstr_ndecls = mind_consnrealdecls;
-	ci_cstr_nargs = mind_consnrealargs;
-	ci_pp_info = print_info }
-  in
-  let len = List.length ctx in
-  let x = Name x in
-  let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:indty] *)
-    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
-    let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 indty, ccl') in
-    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
-    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
-  in
-  let projections decl (i, j, kns, pbs, subst, letsubst) =
+  let projections decl (i, j, kns, pbs, letsubst) =
     match decl with
     | LocalDef (na,c,t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
         let c = liftn 1 j c in
-        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
-           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
-        let c1 = substl subst c in
-        (* From [params, x:I |- subst:field1,..,fieldj]
-           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
-           is represented with instance of field1 last *)
-        let subst = c1 :: subst in
         (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
         let c2 = substl letsubst c in
         (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
            to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
         let letsubst = c2 :: letsubst in
-        (i, j+1, kns, pbs, subst, letsubst)
+        (i, j+1, kns, pbs, letsubst)
     | LocalAssum (na,t) ->
       match na with
       | Name id ->
@@ -868,17 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
 	let projty = substl letsubst t in
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
-	let ty = substl subst t in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let compat = compat_body ty (j - 1) in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-                      proj_arg = i; proj_type = projty; proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs,
-	   fterm :: subst, fterm :: letsubst)
+                      proj_arg = i; proj_type = projty; } in
+        (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst, letsubst) =
-    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  let (_, _, kns, pbs, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
   in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
@@ -983,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
+             compute_projections indsp nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a38172c2..45228e35e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_projections : pinductive -> Id.t -> Id.t ->
+val compute_projections : pinductive ->
   int -> Context.Rel.t -> int array -> int array -> 
   Context.Rel.t -> Context.Rel.t -> 
   (Constant.t array * projection_body array)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b1ee21536..3a61c7747 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1069,7 +1069,11 @@ let extract_constant env kn cb =
               | false -> mk_typ (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_typ (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_typ (get_opaque env c)
@@ -1082,7 +1086,11 @@ let extract_constant env kn cb =
               | false -> mk_def (get_body c)
               | true ->
                 let pb = lookup_projection (Projection.make kn false) env in
-                mk_def (EConstr.of_constr pb.proj_body))
+                (** FIXME: handle mutual records *)
+                let ind = (pb.Declarations.proj_ind, 0) in
+                let bodies = Inductiveops.legacy_match_projection env ind in
+                let body = bodies.(pb.Declarations.proj_arg) in
+                mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
             if access_opaque () then mk_def (get_opaque env c)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df89d9eac..5a54c6f05 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t =
 	  let c' = 
 	    try 
 	      let pb = Environ.lookup_projection p (snd env) in
-	      let body = pb.Declarations.proj_body in
+              (** FIXME: handle mutual records *)
+              let ind = (pb.Declarations.proj_ind, 0) in
+              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
+              let body = bodies.(pb.Declarations.proj_arg) in
 	      let ty = Retyping.get_type_of (snd env) sigma c in
 	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
 	      let body' = strip_lam_assum body in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4ad32fc66..1a790be64 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -549,6 +549,9 @@ let compute_projections env (kn, _ as ind) =
   in
   Array.rev_of_list pbs
 
+let legacy_match_projection env ind =
+  Array.map pi3 (compute_projections env ind)
+
 let compute_projections ind mib =
   let ans = compute_projections ind mib in
   Array.map (fun (prj, ty, _) -> (prj, ty)) ans
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 506cdd8c9..aa53f7e67 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -198,6 +198,14 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
 (** Given a primitive record type, for every field computes the eta-expanded
     projection and its type. *)
 
+val legacy_match_projection : Environ.env -> inductive -> constr array
+(** Given a record type, computes the legacy match-based projection of the
+    projections.
+
+    BEWARE: such terms are ill-typed, and should thus only be used in upper
+    layers. The kernel will probably badly fail if presented with one of
+    those. *)
+
 (********************)
 
 val type_of_inductive_knowing_conclusion :
-- 
cgit v1.2.3