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
herbelin committed Mar 1, 2023
1 parent 61ed5bf commit b226400
Show file tree
Hide file tree
Showing 2 changed files with 83 additions and 65 deletions.
135 changes: 70 additions & 65 deletions plugins/extraction/extraction.ml
View file
Expand Up @@ -244,6 +244,69 @@ let parse_ind_args si args relmax =
| _ -> parse (i+1) (j+1) s)
in parse 1 1 si

(** 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 = Univ.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_relevance = Declareops.relevance_of_projection_repr mib p;
ci_pp_info;
}
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 proj_relevant = match na.binder_relevance with
| Sorts.Irrelevant -> false
| Sorts.Relevant -> true
| Sorts.RelevanceVar _ -> assert false
in
let kn = Projection.Repr.make ind ~proj_relevant ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
fold (arg+1) (j+1) (mkProj (Projection.make kn false, 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, 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 @@ -652,8 +715,13 @@ let rec extract_term env sg mle mlt c args =
| Construct (cp,_) ->
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 (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 @@ -1024,69 +1092,6 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
current_fixpoints := [];
Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types)

(** 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 = Univ.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_relevance = Declareops.relevance_of_projection_repr mib p;
ci_pp_info;
}
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 proj_relevant = match na.binder_relevance with
| Sorts.Irrelevant -> false
| Sorts.Relevant -> true
| Sorts.RelevanceVar _ -> assert false
in
let kn = Projection.Repr.make ind ~proj_relevant ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
fold (arg+1) (j+1) (mkProj (Projection.make kn false, 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, 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
13 changes: 13 additions & 0 deletions test-suite/bugs/bug_16288.v
View file
@@ -0,0 +1,13 @@
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'.

0 comments on commit b226400

Please sign in to comment.