Merge PR coq#17321: Fix coq#16288: wrongly self-referencing extractio…

…n of primitive projections in functors Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
eladrion · Feb 23, 2024 · 6208d8c · 6208d8c
2 parents 28456dd + acb2fb1
commit 6208d8c
Show file tree

Hide file tree

Showing 4 changed files with 110 additions and 93 deletions.
diff --git a/doc/changelog/13-misc/17321-master+fix16288-extraction-prim-field-functor.rst b/doc/changelog/13-misc/17321-master+fix16288-extraction-prim-field-functor.rst
@@ -0,0 +1,7 @@
+- **Fixed:**
+  Wrongly self-referencing extraction of primitive projections to OCaml in functors
+  (`#17321 <https://github.com/coq/coq/pull/17321>`_,
+  fixes `#16288 <https://github.com/coq/coq/issues/16288>`_,
+  by Hugo Herbelin). Note that OCaml wrappers assuming that the
+  applicative syntax of projections is provided may have
+  to use the dot notation instead.
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
@@ -256,6 +256,73 @@ let check_sort_poly sigma gr u =
           ++ str "(instantiation of " ++ Nametab.pr_global_env Id.Set.empty gr
           ++ spc() ++ str "using Prop or SProp).")
 
+let relevance_of_projection_repr mib p =
+  let _mind,i = Names.Projection.Repr.inductive p in
+  match mib.mind_record with
+  | NotRecord | FakeRecord ->
+    CErrors.anomaly ~label:"relevance_of_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,_,rs,_ = infos.(i) in
+    rs.(Names.Projection.Repr.arg p)
+
+(** Because of automatic unboxing the easy way [mk_def c] on the
+   constant body of primitive projections doesn't work. We pretend
+   that they are implemented by matches until someone figures out how
+   to clean it up (test with #4710 when working on this). *)
+let fake_match_projection env p =
+  let ind = Projection.Repr.inductive p in
+  let proj_arg = Projection.Repr.arg p in
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+  let u = UVars.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+  let indu = mkIndU (ind,u) in
+  let ctx, paramslet =
+    let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
+    let (ctx, cty) = mip.mind_nf_lc.(0) in
+    let cty = Term.it_mkProd_or_LetIn cty ctx in
+    let rctx, _ = decompose_prod_decls (Vars.substl subst cty) in
+    List.chop mip.mind_consnrealdecls.(0) rctx
+  in
+  let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+  let ci = {
+    ci_ind = ind;
+    ci_npar = mib.mind_nparams;
+    ci_cstr_ndecls = mip.mind_consnrealdecls;
+    ci_cstr_nargs = mip.mind_consnrealargs;
+    ci_pp_info;
+  }
+  in
+  let relevance = relevance_of_projection_repr mib p in
+  let x = match mib.mind_record with
+    | NotRecord | FakeRecord -> assert false
+    | PrimRecord info ->
+      let x, _, _, _ = info.(snd ind) in
+      make_annot (Name x) mip.mind_relevance
+  in
+  let indty = mkApp (indu, Context.Rel.instance mkRel 0 paramslet) in
+  let rec fold arg j subst = function
+    | [] -> assert false
+    | LocalAssum (na,ty) :: rem ->
+      let ty = Vars.substl subst (liftn 1 j ty) in
+      if arg != proj_arg then
+        let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in
+        let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
+        fold (arg+1) (j+1) (mkProj (Projection.make kn false, na.binder_relevance, mkRel 1)::subst) rem
+      else
+        let p = ([|x|], liftn 1 2 ty) in
+        let branch =
+          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+          (nas, mkRel (List.length ctx - (j - 1)))
+        in
+        let params = Context.Rel.instance mkRel 1 paramslet in
+        let body = mkCase (ci, u, params, (p,relevance), NoInvert, mkRel 1, [|branch|]) in
+        it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
+    | LocalDef (_,c,t) :: rem ->
+      let c = liftn 1 j c in
+      let c1 = Vars.substl subst c in
+      fold arg (j+1) (c1::subst) rem
+  in
+  fold 0 1 [] (List.rev ctx)
+
 (*S Extraction of a type. *)
 
 (* [extract_type env db c args] is used to produce an ML type from the
@@ -660,8 +727,13 @@ let rec extract_term env sg mle mlt c args =
         let () = check_sort_poly sg (ConstructRef cp) u in
         extract_cons_app env sg mle mlt cp args
     | Proj (p, _, c) ->
-        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
-        extract_term env sg mle mlt term args
+        let p = Projection.repr p in
+        let term = fake_match_projection env p in
+        let ind = Inductiveops.find_rectype env sg (Retyping.get_type_of env sg c) in
+        let indf,_ = Inductiveops.dest_ind_type ind in
+        let _,indargs = Inductiveops.dest_ind_family indf in
+        let indargs = List.map EConstr.of_constr indargs in
+        extract_term env sg mle mlt (beta_applist sg (EConstr.of_constr term,indargs@[c])) args
     | Rel n ->
         (* As soon as the expected [mlt] for the head is known, *)
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
@@ -1035,73 +1107,6 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
   current_fixpoints := [];
   Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types)
 
-let relevance_of_projection_repr mib p =
-  let _mind,i = Names.Projection.Repr.inductive p in
-  match mib.mind_record with
-  | NotRecord | FakeRecord ->
-    CErrors.anomaly ~label:"relevance_of_projection" Pp.(str "not a projection")
-  | PrimRecord infos ->
-    let _,_,rs,_ = infos.(i) in
-    rs.(Names.Projection.Repr.arg p)
-
-(** Because of automatic unboxing the easy way [mk_def c] on the
-   constant body of primitive projections doesn't work. We pretend
-   that they are implemented by matches until someone figures out how
-   to clean it up (test with #4710 when working on this). *)
-let fake_match_projection env p =
-  let ind = Projection.Repr.inductive p in
-  let proj_arg = Projection.Repr.arg p in
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  let u = UVars.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-  let indu = mkIndU (ind,u) in
-  let ctx, paramslet =
-    let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
-    let (ctx, cty) = mip.mind_nf_lc.(0) in
-    let cty = Term.it_mkProd_or_LetIn cty ctx in
-    let rctx, _ = decompose_prod_decls (Vars.substl subst cty) in
-    List.chop mip.mind_consnrealdecls.(0) rctx
-  in
-  let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-  let ci = {
-    ci_ind = ind;
-    ci_npar = mib.mind_nparams;
-    ci_cstr_ndecls = mip.mind_consnrealdecls;
-    ci_cstr_nargs = mip.mind_consnrealargs;
-    ci_pp_info;
-  }
-  in
-  let relevance = relevance_of_projection_repr mib p in
-  let x = match mib.mind_record with
-    | NotRecord | FakeRecord -> assert false
-    | PrimRecord info ->
-      let x, _, _, _ = info.(snd ind) in
-      make_annot (Name x) mip.mind_relevance
-  in
-  let indty = mkApp (indu, Context.Rel.instance mkRel 0 paramslet) in
-  let rec fold arg j subst = function
-    | [] -> assert false
-    | LocalAssum (na,ty) :: rem ->
-      let ty = Vars.substl subst (liftn 1 j ty) in
-      if arg != proj_arg then
-        let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in
-        let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
-        fold (arg+1) (j+1) (mkProj (Projection.make kn false, na.binder_relevance, mkRel 1)::subst) rem
-      else
-        let p = ([|x|], liftn 1 2 ty) in
-        let branch =
-          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
-          (nas, mkRel (List.length ctx - (j - 1)))
-        in
-        let params = Context.Rel.instance mkRel 1 paramslet in
-        let body = mkCase (ci, u, params, (p,relevance), NoInvert, mkRel 1, [|branch|]) in
-        it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
-    | LocalDef (_,c,t) :: rem ->
-      let c = liftn 1 j c in
-      let c1 = Vars.substl subst c in
-      fold arg (j+1) (c1::subst) rem
-  in
-  fold 0 1 [] (List.rev ctx)
-
 let extract_constant env kn cb =
   let sg = Evd.from_env env in
   let r = GlobRef.ConstRef kn in

diff --git a/test-suite/bugs/bug_16288.v b/test-suite/bugs/bug_16288.v
@@ -0,0 +1,15 @@
+(* Extraction of primitive projections within a functor were
+   incorrectly referencing themselves *)
+Module Type Nop. End Nop.
+Module Empty. End Empty.
+Module M (N : Nop).
+  Local Set Primitive Projections.
+  Record M_t_NonEmpty elt := { M_m :> list elt }.
+  Record M_t_NonEmpty' X Y := { a : X ; b : Y }.
+End M.
+Module M' := M Empty.
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrOcamlBasic.
+Extraction Language OCaml.
+Recursive Extraction M'.
+Extraction TestCompile M'.
diff --git a/test-suite/output/extraction_projection.out b/test-suite/output/extraction_projection.out
@@ -109,20 +109,10 @@ module A =
   type prim_record_two_fields = { prim_proj1_of_2 : bool;
                                   prim_proj2_of_2 : bool }
 
-  (** val prim_proj1_of_2 : prim_record_two_fields -> bool **)
-
-  let prim_proj1_of_2 p =
-    p.prim_proj1_of_2
-
   type prim_record_one_field =
     bool
     (* singleton inductive, whose constructor was Build_prim_record_one_field *)
 
-  (** val prim_proj1_of_1 : prim_record_one_field -> bool **)
-
-  let prim_proj1_of_1 p =
-    p
-
   (** val d21 : prim_record_two_fields -> bool **)
 
   let d21 x =
@@ -220,51 +210,51 @@ module M =
 
   (** val prim_proj1_of_2 : prim_record_two_fields -> bool **)
 
-  let prim_proj1_of_2 =
-    prim_proj1_of_2
+  let prim_proj1_of_2 p =
+    p.prim_proj1_of_2
 
   (** val prim_proj2_of_2 : prim_record_two_fields -> bool **)
 
-  let prim_proj2_of_2 =
-    prim_proj2_of_2
+  let prim_proj2_of_2 p =
+    p.prim_proj2_of_2
 
   type prim_record_one_field =
     bool
     (* singleton inductive, whose constructor was Build_prim_record_one_field *)
 
   (** val prim_proj1_of_1 : prim_record_one_field -> bool **)
 
-  let prim_proj1_of_1 =
-    prim_proj1_of_1
+  let prim_proj1_of_1 p =
+    p
 
   type prim_record_one_field_unused =
     bool
     (* singleton inductive, whose constructor was Build_prim_record_one_field_unused *)
 
   (** val prim_proj1_of_1_unused : prim_record_one_field_unused -> bool **)
 
-  let prim_proj1_of_1_unused =
-    prim_proj1_of_1_unused
+  let prim_proj1_of_1_unused p =
+    p
 
   (** val d21 : prim_record_two_fields -> bool **)
 
-  let d21 =
-    prim_proj1_of_2
+  let d21 x =
+    x.prim_proj1_of_2
 
   (** val d22 : (unit0 -> prim_record_two_fields) -> bool **)
 
   let d22 x =
-    prim_proj1_of_2 (x Tt)
+    (x Tt).prim_proj1_of_2
 
   (** val e21 : prim_record_one_field -> bool **)
 
-  let e21 =
-    prim_proj1_of_1
+  let e21 x =
+    x
 
   (** val e22 : (unit0 -> prim_record_one_field) -> bool **)
 
   let e22 x =
-    prim_proj1_of_1 (x Tt)
+    x Tt
  end
 
 module N = M(Empty)