From df2a8661fb946f21f8d9f0c55928f8c957cf6ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 3 Mar 2023 09:06:56 +0100
Subject: [PATCH] Extraction to OCaml: use dot notation for non-primitive
 projections in functors.

Previously, it was relying on the table of projections in structure.ml
but this is not valid in functors. We craft instead the kernel name of
projections from the data in the declaration of the inductive type.
---
 plugins/extraction/extraction.ml            | 18 ++++--------------
 test-suite/output/extraction_projection.out |  6 +++---
 2 files changed, 7 insertions(+), 17 deletions(-)

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 7387717278d5..89ea8e34fd2c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -492,9 +492,10 @@ and extract_really_ind env kn mib =
         let field_names =
           List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
         assert (Int.equal (List.length field_names) (List.length typ));
-        let projs = ref Cset.empty in
         let mp = MutInd.modpath kn in
         let implicits = implicits_of_global (GlobRef.ConstructRef (ip,1)) in
+        let ty = Inductive.type_of_inductive ((mib,mip0),u) in
+        let nparams = nb_default_params env sg (EConstr.of_constr ty) in
         let rec select_fields i l typs = match l,typs with
           | [],[] -> []
           | _::l, typ::typs when isTdummy (expand env typ) || Int.Set.mem i implicits ->
@@ -505,22 +506,11 @@ and extract_really_ind env kn mib =
               let knp = Constant.make2 mp (Label.of_id id) in
               (* Is it safe to use [id] for projections [foo.id] ? *)
               if List.for_all ((==) Keep) (type2signature env typ)
-              then projs := Cset.add knp !projs;
+              then add_projection nparams knp ip;
               Some (GlobRef.ConstRef knp) :: (select_fields (i+1) l typs)
           | _ -> assert false
         in
-        let field_glob = select_fields (1+npar) field_names typ
-        in
-        (* Is this record officially declared with its projections ? *)
-        (* If so, we use this information. *)
-        begin try
-          let ty = Inductive.type_of_inductive ((mib,mip0),u) in
-          let n = nb_default_params env sg (EConstr.of_constr ty) in
-          let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
-          in
-          List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip)
-        with Not_found -> ()
-        end;
+        let field_glob = select_fields (1+npar) field_names typ in
         Record field_glob
       with (I info) -> info
     in
diff --git a/test-suite/output/extraction_projection.out b/test-suite/output/extraction_projection.out
index b625f877d90a..b8ad88b5ff23 100644
--- a/test-suite/output/extraction_projection.out
+++ b/test-suite/output/extraction_projection.out
@@ -207,13 +207,13 @@ module M =
 
   (** val d11 : non_prim_record_two_fields -> bool **)
 
-  let d11 =
-    non_prim_proj1_of_2
+  let d11 x =
+    x.non_prim_proj1_of_2
 
   (** val d12 : (unit0 -> non_prim_record_two_fields) -> bool **)
 
   let d12 x =
-    non_prim_proj1_of_2 (x Tt)
+    (x Tt).non_prim_proj1_of_2
 
   (** val e11 : non_prim_record_one_field -> bool **)