Skip to content

Commit

Permalink
Fixes coq#16288: wrong extraction of primitive field in functors.
Browse files Browse the repository at this point in the history 
- The code for extracting a primitive projection was referencing the
  constant form of the projection.
- The code for compiling the constant form of the projection was doing
  a call to the global table of projections which is however not fed in
  functors.
- The declaration of constants bound to a projection had a small size
  and were then inlined.

Instead of relying on the table of projections, we use the
"match"-expanded form of the projections which has the advantage of be
valid in all target languages. In particular, in OCaml extraction,
this is anyway reprinted as a field.

Note: we need to move the fake_match_projection function a bit
earlier.
  • Loading branch information
@herbelin @louiseddp
herbelin authored and louiseddp committed Feb 27, 2024
1 parent d5fd270 commit eb19e71
Show file tree
Hide file tree
Showing 3 changed files with 103 additions and 93 deletions.
143 changes: 74 additions & 69 deletions plugins/extraction/extraction.ml
View file
Expand Up @@ -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
Expand Down Expand Up @@ -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]. *)
Expand Down Expand Up @@ -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
Expand Down
15 changes: 15 additions & 0 deletions test-suite/bugs/bug_16288.v
View file
@@ -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'.
38 changes: 14 additions & 24 deletions test-suite/output/extraction_projection.out
View file
Expand Up @@ -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 =
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit eb19e71

Please sign in to comment.