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.

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 :