Merge PR #9306: Remove Printing Primitive Projection Compatibility

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot

7 files changed, 63 insertions, 88 deletions

diff --git a/CHANGES.md b/CHANGES.md
index d0774276ad..38c197d8cc 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -194,6 +194,8 @@ Misc
 
 - Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
 
+- Removed option "Printing Primitive Projection Compatibility"
+
 SSReflect
 
 - New intro patterns:
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 933f07674a..d2fd08536a 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -247,11 +247,6 @@ Primitive Projections
    printing time (even though they are absent in the actual AST manipulated
    by the kernel).
 
-.. flag:: Printing Primitive Projection Compatibility
-
-   This compatibility option (on by default) governs the
-   printing of pattern matching over primitive records.
-
 Primitive Record Types
 ++++++++++++++++++++++
 
@@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to
 precisely mimic the usual unfolding rules of constants. Projections
 obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
 There is currently no way to input unfolded primitive projections at the
-user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
-to display unfolded primitive projections as matches and distinguish them from folded ones.
+user-level, and there is no way to display unfolded projections differently
+from folded ones.
 
 
 Compatibility Projections and :g:`match`
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c15486ea10..204f889f90 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1032,6 +1032,55 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
   current_fixpoints := [];
   Dfix (Array.map (fun kn -> 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 rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) 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 x = match mib.mind_record with
+    | NotRecord | FakeRecord -> assert false
+    | PrimRecord info -> Name (pi1 info.(snd ind))
+  in
+  let indty = mkApp (indu, Context.Rel.to_extended_vect 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 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, mkRel 1)::subst) rem
+      else
+        let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
+        let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
+        let body = mkCase (ci, p, 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 = ConstRef kn in
@@ -1069,10 +1118,7 @@ let extract_constant env kn cb =
              (match Recordops.find_primitive_projection kn with
               | None -> mk_typ (get_body c)
               | Some p ->
-                let p = Projection.make p false in
-                let ind = Projection.inductive p in
-                let bodies = Inductiveops.legacy_match_projection env ind in
-                let body = bodies.(Projection.arg p) in
+                let body = fake_match_projection env p in
                 mk_typ (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
@@ -1085,10 +1131,7 @@ let extract_constant env kn cb =
              (match Recordops.find_primitive_projection kn with
               | None -> mk_def (get_body c)
               | Some p ->
-                let p = Projection.make p false in
-                let ind = Projection.inductive p in
-                let bodies = Inductiveops.legacy_match_projection env ind in
-                let body = bodies.(Projection.arg p) in
+                let body = fake_match_projection env p in
                 mk_def (EConstr.of_constr body))
 	  | OpaqueDef c ->
 	    add_opaque r;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6746e4b902..99cd89cc2a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open CErrors
 open Util
@@ -175,16 +173,6 @@ let () = declare_bool_option
 	    optread  = print_primproj_params;
 	    optwrite = (:=) print_primproj_params_value }
 
-let print_primproj_compatibility_value = ref false
-let print_primproj_compatibility () = !print_primproj_compatibility_value
-
-let () = declare_bool_option
-	  { optdepr  = false;
-	    optname  = "backwards-compatible printing of primitive projections";
-	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
-	    optread  = print_primproj_compatibility;
-	    optwrite = (:=) print_primproj_compatibility_value }
-
 	  
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
@@ -702,30 +690,12 @@ and detype_r d flags avoid env sigma t =
 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), 
 		[detype d flags avoid env sigma c])
       else 
-	if print_primproj_compatibility () && Projection.unfolded p then
-          (* Print the compatibility match version *)
-	  let c' = 
-	    try 
-              let ind = Projection.inductive p in
-              let bodies = Inductiveops.legacy_match_projection (snd env) ind in
-              let body = bodies.(Projection.arg p) in
-	      let ty = Retyping.get_type_of (snd env) sigma c in
-	      let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in
-	      let body' = strip_lam_assum body in
-	      let u = EInstance.kind sigma u in
-	      let body' = CVars.subst_instance_constr u body' in
-	      let body' = EConstr.of_constr body' in
-		substl (c :: List.rev args) body'
-	    with Retyping.RetypeError _ | Not_found -> 
-	      anomaly (str"Cannot detype an unfolded primitive projection.")
-	  in DAst.get (detype d flags avoid env sigma c')
-	else
-	  if print_primproj_params () then
-	    try
-	      let c = Retyping.expand_projection (snd env) sigma p c [] in
-              DAst.get (detype d flags avoid env sigma c)
-	    with Retyping.RetypeError _ -> noparams ()
-	  else noparams ()
+        if print_primproj_params () then
+          try
+            let c = Retyping.expand_projection (snd env) sigma p c [] in
+            DAst.get (detype d flags avoid env sigma c)
+          with Retyping.RetypeError _ -> noparams ()
+        else noparams ()
 
     | Evar (evk,cl) ->
         let bound_to_itself_or_letin decl c =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 2c4ca46343..4c02dc0f09 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -475,25 +475,6 @@ let compute_projections env (kn, i as ind) =
     (* [Ind inst] is typed in context [params-wo-let] *)
     ty
   in
-  let ci =
-    let print_info =
-      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
-      { ci_ind     = ind;
-        ci_npar    = nparamargs;
-        ci_cstr_ndecls = pkt.mind_consnrealdecls;
-        ci_cstr_nargs = pkt.mind_consnrealargs;
-        ci_pp_info = print_info }
-  in
-  let len = List.length ctx in
-  let compat_body ccl i =
-    (* [ccl] is defined in context [params;x:indty] *)
-    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
-    let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 indty, ccl') in
-    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
-    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
-  in
   let projections decl (proj_arg, j, pbs, subst) =
     match decl with
     | LocalDef (na,c,t) ->
@@ -523,10 +504,9 @@ let compute_projections env (kn, i as ind) =
         let ty = substl subst t in
         let term = mkProj (Projection.make kn true, mkRel 1) in
         let fterm = mkProj (Projection.make kn false, mkRel 1) in
-        let compat = compat_body ty (j - 1) in
         let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
         let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
-        let body = (etab, etat, compat) in
+        let body = (etab, etat) in
         (proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
       | Anonymous ->
         anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
@@ -536,13 +516,6 @@ let compute_projections env (kn, i as ind) =
   in
   Array.rev_of_list pbs
 
-let legacy_match_projection env ind =
-  Array.map pi3 (compute_projections env ind)
-
-let compute_projections ind mib =
-  let ans = compute_projections ind mib in
-  Array.map (fun (prj, ty, _) -> (prj, ty)) ans
-
 (**************************************************)
 
 let extract_mrectype sigma t =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index b2e205115f..5a4257e175 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -194,14 +194,6 @@ val compute_projections : Environ.env -> inductive -> (constr * types) array
 (** Given a primitive record type, for every field computes the eta-expanded
     projection and its type. *)
 
-val legacy_match_projection : Environ.env -> inductive -> constr array
-(** Given a record type, computes the legacy match-based projection of the
-    projections.
-
-    BEWARE: such terms are ill-typed, and should thus only be used in upper
-    layers. The kernel will probably badly fail if presented with one of
-    those. *)
-
 (********************)
 
 val type_of_inductive_knowing_conclusion :
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
index b67e93d677..0c236e12ad 100644
--- a/test-suite/bugs/closed/bug_5197.v
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Primitive Projections.
-Unset Printing Primitive Projection Compatibility.
+
 Axiom Ω : Type.
 
 Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack {