Merge PR #7234: Reduce circular dependency constants <-> projections

12 files changed, 37 insertions, 86 deletions

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 8389dd326..b722e4200 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -708,12 +708,10 @@ let rec lambda_of_constr env c =
     Lcofix(init, (names, ltypes, lbodies))
 
   | Proj (p,c) ->
-    let kn = Projection.constant p in
-    let cb = lookup_constant kn env.global_env in
-    let pb = Option.get cb.const_proj in
+    let pb = lookup_projection p env.global_env in
     let n = pb.proj_arg in
     let lc = lambda_of_constr env c in
-    Lproj (n,kn,lc)
+    Lproj (n,Projection.constant p,lc)
 
 and lambda_of_app env f args =
   match Constr.kind f with
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6f4541e95..5783453e6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,7 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : projection_body option;
+  cook_proj : bool;
   cook_universes : constant_universes;
   cook_inline : inline;
   cook_context : Context.Named.t option;
@@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } =
 		  hyps)
       hyps ~init:cb.const_hyps in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
-  let projection pb =
-    let c' = abstract_constant_body (expmod pb.proj_body) hyps in
-    let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
-    let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
-    let ((mind, _), _), n' =
-      try 
-	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
-	  match kind c' with
-	  | App (f,l) -> (destInd f, Array.length l)
-	  | Ind ind -> ind, 0
-	  | _ -> assert false 
-      with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
-    in 
-    let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
-      { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
-	proj_eta = etab, etat;
-	proj_type = ty'; proj_body = c' }
-  in
   {
     cook_body = body;
     cook_type = typ;
-    cook_proj = Option.map projection cb.const_proj;
+    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 7bd0ae566..0d907f3de 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,7 @@ type inline = bool
 type result = {
   cook_body : constant_def;
   cook_type : types;
-  cook_proj : projection_body option;
+  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 b7427d20a..913c13173 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,7 +87,7 @@ type constant_body = {
     const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
-    const_proj : projection_body option;
+    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 832d478b3..75c0e5b4c 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -94,14 +94,13 @@ let subst_const_body sub cb =
   else
     let body' = subst_const_def sub cb.const_body in
     let type' = subst_const_type sub cb.const_type in
-    let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
-      && proj' == cb.const_proj then cb
+    then cb
     else
       { const_hyps = [];
         const_body = body';
         const_type = type';
-        const_proj = proj';
+        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 c3e7cec75..fb89576dd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
+  env_projections : projection_body Cmap_env.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
@@ -108,6 +109,7 @@ let empty_rel_context_val = {
 let empty_env = {
   env_globals = {
     env_constants = Cmap_env.empty;
+    env_projections = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
@@ -485,14 +487,10 @@ let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
 let lookup_projection cst env =
-  match (lookup_constant (Projection.constant cst) env).const_proj with 
-  | Some pb -> pb
-  | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.")
+  Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
 
 let is_projection cst env =
-  match (lookup_constant cst env).const_proj with 
-  | Some _ -> true
-  | None -> false
+  (lookup_constant cst env).const_proj
 
 (* Mutual Inductives *)
 let polymorphic_ind (mind,i) env =
@@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
   
-let add_mind_key kn mind_key env =
+let add_mind_key kn (mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
+  let new_projections = match mind.mind_record with
+    | None | Some None -> env.env_globals.env_projections
+    | Some (Some (id, kns, pbs)) ->
+      Array.fold_left2 (fun projs kn pb ->
+          Cmap_env.add kn pb projs)
+        env.env_globals.env_projections kns pbs
+  in
   let new_globals =
     { env.env_globals with
-	env_inductives = new_inds } in
+        env_inductives = new_inds; env_projections = new_projections; } in
   { env with env_globals = new_globals }
 
 let add_mind kn mib env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index fc45ce0e3..8928b32f1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -48,6 +48,7 @@ type mind_key = mutual_inductive_body * link_info ref
 
 type globals = {
   env_constants : constant_key Cmap_env.t;
+  env_projections : projection_body Cmap_env.t;
   env_inductives : mind_key Mindmap_env.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bed598bb..090acdf16 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -803,9 +803,7 @@ let rec subterm_specif renv stack t =
          (* We take the subterm specs of the constructor of the record *)
          let wf_args = (dest_subterms wf).(0) in
          (* We extract the tree of the projected argument *)
-         let kn = Projection.constant p in
-         let cb = lookup_constant kn renv.env in
-         let pb = Option.get cb.const_proj in
+         let pb = lookup_projection p renv.env in
          let n = pb.proj_arg in
          spec_of_tree (List.nth wf_args n)
        | Dead_code -> Dead_code
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 0cd0ad46c..036cd4847 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id =
 
 let compile_constant env sigma prefix ~interactive con cb =
   match cb.const_proj with
-  | None ->
+  | false ->
      let no_univs =
        match cb.const_universes with
        | Monomorphic_const _ -> true
@@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  if interactive then LinkedInteractive prefix
 	  else Linked prefix
     end
-  | Some pb ->
+  | true ->
+      let pb = lookup_projection (Projection.make con false) env in
       let mind = pb.proj_ind in
       let ind = (mind,0) in
       let mib = lookup_mind mind env in
@@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t =
       else
       let comp_stack, (mind_updates, const_updates) =
 	match cb.const_proj, cb.const_body with
-        | None, Def t ->
+        | false, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
-	| Some pb, _ ->
-	   let mind = pb.proj_ind in
-	   compile_mind_deps env prefix ~interactive init mind
+        | true, _ ->
+          let pb = lookup_projection (Projection.make c false) env in
+          let mind = pb.proj_ind in
+          compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 7352c1882..db1109e75 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = Undef nl;
         cook_type = t;
-        cook_proj = None;
+        cook_proj = false;
         cook_universes = univs;
         cook_inline = false;
         cook_context = ctx;
@@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = None;
+        cook_proj = false;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       {
         Cooking.cook_body = def;
         cook_type = typ;
-        cook_proj = None;
+        cook_proj = false;
         cook_universes = univs;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
@@ -370,7 +370,7 @@ 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 = Some pb;
+      cook_proj = true;
       cook_universes = univs;
       cook_inline = false;
       cook_context = None;
@@ -458,30 +458,8 @@ let build_constant_declaration kn env result =
               check declared inferred) lc) in
   let univs = result.cook_universes in
   let tps = 
-    let res =
-      match result.cook_proj with
-      | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def
-      | Some pb ->
-	(* The compilation of primitive projections is a bit tricky, because
-           they refer to themselves (the body of p looks like fun c =>
-           Proj(p,c)). We break the cycle by building an ad-hoc compilation
-           environment. A cleaner solution would be that kernel projections are
-           simply Proj(i,c) with i an int and c a constr, but we would have to
-           get rid of the compatibility layer. *)
-	let cb =
-	  { const_hyps = hyps;
-	    const_body = def;
-	    const_type = typ;
-	    const_proj = result.cook_proj;
-	    const_body_code = None;
-	    const_universes = univs;
-	    const_inline_code = result.cook_inline;
-	    const_typing_flags = Environ.typing_flags env;
-	    }
-	in
-	let env = add_constant kn cb env in
-        Cbytegen.compile_constant_body ~fail_on_error:false env univs def
-    in Option.map Cemitcodes.from_val res
+    let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
+    Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fd9cefb2c..325d5cecd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj =
   let lf, lft = dest_judgev lfj in
   make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
              (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
-
-let type_of_projection_constant env (p,u) =
-  let cst = Projection.constant p in
-  let cb = lookup_constant cst env in
-  match cb.const_proj with
-  | Some pb ->
-    if Declareops.constant_is_polymorphic cb then
-      Vars.subst_instance_constr u pb.proj_type
-    else pb.proj_type
-  | None -> raise (Invalid_argument "type_of_projection: not a projection")
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 85b2cfffd..546f2d2b4 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -100,8 +100,6 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_projection_constant : env -> Projection.t puniverses -> types
-
 val type_of_constant_in : env -> pconstant -> types
 
 (** Check that hyps are included in env and fails with error otherwise *)