Merge PR #11135: Simplifying the code declaring the constants bound to primitive projections

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot

5 files changed, 87 insertions, 94 deletions

diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
index e9c28faf1d..1dd89c9bcd 100644
--- a/test-suite/output/Projections.out
+++ b/test-suite/output/Projections.out
@@ -1,2 +1,17 @@
 fun S : store => S.(store_funcs)
      : store -> host_func
+a = 
+fun A : Type =>
+let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
+     : forall A : Type,
+       let B := A in
+       forall C : Type, U A C -> Type * Type * Type * (B * A * C)
+
+Arguments a (_ _)%type_scope
+b = 
+fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
+     : forall A : Type,
+       let B := A in
+       forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
+
+Arguments b (_ _)%type_scope
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 14d63d39c4..83a581338f 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -10,3 +10,12 @@ Section store.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
+
+Module LocalDefUnfolding.
+
+Unset Printing Projections.
+Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}.
+Print a.
+Print b.
+
+End LocalDefUnfolding.
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 3e6552c8d2..e22d63b811 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -96,38 +96,6 @@ let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj =
 
 let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
 
-let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
-  let name = Label.to_id label in
-  let univs, u = match univs with
-    | Monomorphic_entry _ ->
-      (* Global constraints already defined through the inductive *)
-      Monomorphic_entry Univ.ContextSet.empty, Univ.Instance.empty
-    | Polymorphic_entry (nas, ctx) ->
-      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
-  in
-  let term = Vars.subst_instance_constr u term in
-  let types = Vars.subst_instance_constr u types in
-  let entry = Declare.definition_entry ~types ~univs term in
-  let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) in
-  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  declare_primitive_projection p cst
-
-let declare_projections univs mind =
-  let env = Global.env () in
-  let mib = Environ.lookup_mind mind env in
-  let open Declarations in
-  match mib.mind_record with
-  | PrimRecord info ->
-    let iter_ind i (_, labs, _, _) =
-      let ind = (mind, i) in
-      let projs = Inductiveops.compute_projections env ind in
-      CArray.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
-    in
-    let () = Array.iteri iter_ind info in
-    true
-  | FakeRecord -> false
-  | NotRecord -> false
-
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags () =
@@ -149,7 +117,7 @@ let declare_mind mie =
   let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
   if is_unsafe_typing_flags() then feedback_axiom ();
   let mind = Global.mind_of_delta_kn kn in
-  let isprim = declare_projections mie.mind_entry_universes mind in
+  let isprim = Inductive.is_primitive_record (Inductive.lookup_mind_specif (Global.env()) (mind,0)) in
   Impargs.declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index ae649634a5..05a1617329 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -30,3 +30,6 @@ type inductive_obj
 val objInductive : inductive_obj Libobject.Dyn.tag
 
 end
+
+val declare_primitive_projection :
+  Names.Projection.Repr.t -> Names.Constant.t -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index b9d450044b..0b6e8cd8c1 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -320,67 +320,65 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
       (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
-        let fi = RelDecl.get_name decl in
-        let ti = RelDecl.get_type decl in
-        let (sp_projs,i,subst) =
-          match fi with
-          | Anonymous ->
-              (None::sp_projs,i,NoProjection fi::subst)
-          | Name fid -> try
-            let kn, term =
-              if is_local_assum decl && primitive then
-                let p = Projection.Repr.make indsp
-                    ~proj_npars:mib.mind_nparams
-                    ~proj_arg:i
-                    (Label.of_id fid)
-                in
-                (* Already defined by declare_mind silently *)
-                let kn = Projection.Repr.constant p in
-                Declare.definition_message fid;
-                kn, mkProj (Projection.make p false,mkRel 1)
-              else
-                let ccl = subst_projection fid subst ti in
-                let body = match decl with
-                  | LocalDef (_,ci,_) -> subst_projection fid subst ci
-                  | LocalAssum ({binder_relevance=rci},_) ->
-                    (* [ccl] is defined in context [params;x:rp] *)
-                    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
-                    let ccl' = liftn 1 2 ccl in
-                    let p = mkLambda (x, lift 1 rp, ccl') in
-                    let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-                    let ci = Inductiveops.make_case_info env indsp rci LetStyle in
-                    (* Record projections have no is *)
-                    mkCase (ci, p, mkRel 1, [|branch|])
-                in
-                let proj =
-                  it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
-                let projtyp =
-                  it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
-                try
-                  let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
-                  let kind = Decls.IsDefinition kind in
-                  let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
-                  let constr_fip =
-                    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-                      applist (mkConstU (kn,u),proj_args)
-                  in
-                  Declare.definition_message fid;
-                    kn, constr_fip
-                with Type_errors.TypeError (ctx,te) ->
-                  raise (NotDefinable (BadTypedProj (fid,ctx,te)))
-            in
-            let refi = GlobRef.ConstRef kn in
-            Impargs.maybe_declare_manual_implicits false refi impls;
-            if flags.pf_subclass then begin
-              let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
-                ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
-            end;
-            let i = if is_local_assum decl then i+1 else i in
-              (Some kn::sp_projs, i, Projection term::subst)
-            with NotDefinable why ->
-              warning_or_error flags.pf_subclass indsp why;
-              (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+         let fi = RelDecl.get_name decl in
+         let ti = RelDecl.get_type decl in
+         let (sp_projs,i,subst) =
+           match fi with
+           | Anonymous ->
+             (None::sp_projs,i,NoProjection fi::subst)
+           | Name fid ->
+             try
+               let ccl = subst_projection fid subst ti in
+               let body, p_opt = match decl with
+                 | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
+                 | LocalAssum ({binder_relevance=rci},_) ->
+                   (* [ccl] is defined in context [params;x:rp] *)
+                   (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+                   if primitive then
+                     let p = Projection.Repr.make indsp
+                         ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
+                     mkProj (Projection.make p true, mkRel 1), Some p
+                   else
+                     let ccl' = liftn 1 2 ccl in
+                     let p = mkLambda (x, lift 1 rp, ccl') in
+                     let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+                     let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+                     (* Record projections have no is *)
+                     mkCase (ci, p, mkRel 1, [|branch|]), None
+               in
+               let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+               let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
+               let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
+               let kind = Decls.IsDefinition kind in
+               let kn =
+                 try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
+                 with Type_errors.TypeError (ctx,te) when not primitive ->
+                   raise (NotDefinable (BadTypedProj (fid,ctx,te)))
+               in
+               Declare.definition_message fid;
+               let term = match p_opt with
+                 | Some p ->
+                   let _ = DeclareInd.declare_primitive_projection p kn in
+                   mkProj (Projection.make p false,mkRel 1)
+                 | None ->
+                   let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+                   match decl with
+                   | LocalDef (_,ci,_) when primitive -> body
+                   | _ -> applist (mkConstU (kn,u),proj_args)
+               in
+               let refi = GlobRef.ConstRef kn in
+               Impargs.maybe_declare_manual_implicits false refi impls;
+               if flags.pf_subclass then begin
+                 let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+                 ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+               end;
+               let i = if is_local_assum decl then i+1 else i in
+               (Some kn::sp_projs, i, Projection term::subst)
+             with NotDefinable why ->
+               warning_or_error flags.pf_subclass indsp why;
+               (None::sp_projs,i,NoProjection fi::subst)
+         in
+         (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
       (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)