From 4513b7735779fb440223e6f22079994528249047 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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 +++++++++++++++++++++++++---------
 1 file changed, 25 insertions(+), 9 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index bc2d2068a2..39c83f47ef 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
-- 
cgit v1.2.3


From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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.
---
 interp/declare.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 39c83f47ef..aa737239ba 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
-- 
cgit v1.2.3