Merge PR coq#18327: Make projection constants transparent and allowin…

…g projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

checker/values.ml

@@ -227,8 +227,10 @@ let v_oracle =
   v_tuple "oracle" [|
     v_map v_id v_conv_level;
     v_hmap v_cst v_conv_level;
+    v_hmap v_proj_repr v_conv_level;
     v_pred v_id;
     v_pred v_cst;
+    v_pred v_proj_repr;
   |]
 
 let v_template_arity =

dev/ci/user-overlays/18327-rlepigre-brfix-18281.sh

@@ -0,0 +1,13 @@
+overlay elpi https://github.com/rlepigre/coq-elpi br/fix-18281 18327
+
+overlay equations https://github.com/rlepigre/Coq-Equations br/fix-18281 18327
+
+overlay lean_importer https://github.com/rlepigre/coq-lean-import br/fix-18281 18327
+
+overlay mtac2 https://github.com/rlepigre/Mtac2 br/fix-18281 18327
+
+overlay serapi https://github.com/rlepigre/coq-serapi br/fix-18281 18327
+
+overlay tactician https://github.com/rlepigre/coq-tactician br/fix-18281 18327
+
+overlay waterproof https://github.com/rlepigre/coq-waterproof br/fix-18281 18327

dev/top_printers.ml

@@ -50,7 +50,7 @@ let ppdir dir = pp (DirPath.print dir)
 let ppmp mp = pp(str (ModPath.debug_to_string mp))
 let ppcon con = pp(Constant.debug_print con)
 let ppprojrepr con = pp(Constant.debug_print (Projection.Repr.constant con))
-let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppproj p = pp(Projection.debug_print p)
 let ppkn kn = pp(str (KerName.to_string kn))
 let ppmind kn = pp(MutInd.debug_print kn)
 let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
@@ -348,7 +348,7 @@ let constr_display csr =
   | Construct (((sp,i),j),u) ->
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
-  | Proj (p, r, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
+  | Proj (p, r, c) -> "Proj("^(Projection.to_string p)^","^term_display c ^")"
   | Case (ci,u,pms,((_,p),_),iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display (Array.map snd bl))^")"
@@ -457,7 +457,7 @@ let print_pure_constr csr =
       print_string ","; universes_display u;
       print_string ")"
   | Proj (p,_,c') -> print_string "Proj(";
-      sp_con_display (Projection.constant p);
+      sp_prj_display p;
       print_string ",";
       box_display c';
       print_string ")"
@@ -577,7 +577,8 @@ let print_pure_constr csr =
         | l             -> l
     in  List.iter (fun x -> print_string x; print_string ".") ls;*)
       print_string (Constant.debug_to_string sp)
-
+  and sp_prj_display sp =
+      print_string (Projection.debug_to_string sp)
   in
     try
      box_display csr; print_flush()

doc/changelog/04-tactics/18327-br-fix-18281.rst

@@ -0,0 +1,7 @@
+- **Changed:**
+  The opacity/transparency of primitive projections is now attached to the
+  projections themselves, not the compatibility constants, and compatibility
+  constants are always considered transparent
+  (`#18327 <https://github.com/coq/coq/pull/18327>`_,
+  fixes `#18281 <https://github.com/coq/coq/issues/18281>`_,
+  by Jan-Oliver Kaiser and Rodolphe Lepigre).

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -952,7 +952,7 @@ The commands to fine-tune the reduction strategies and the lazy conversion
 algorithm are described in this section.  Also see :ref:`Args_effect_on_unfolding`,
 which supports additional fine-tuning.
 
-.. cmd:: Opaque {+ @reference }
+.. cmd:: Opaque {? ! } {+ @reference }
 
    Marks the specified constants as :term:`opaque` so tactics won't :term:`unfold` them
    with :term:`delta-reduction`.
@@ -968,7 +968,13 @@ which supports additional fine-tuning.
    has to check that two distinct applied constants are convertible.
    See Section :ref:`conversion-rules`.
 
-.. cmd:: Transparent {+ @reference }
+   In the particular case where the constants refer to primitive projections,
+   a :token:`!` can be used to make the compatibility constants opaque, while
+   by default the projection themselves are made opaque and the compatibility
+   constants always remain transparent. This mechanism is only intended for
+   debugging purposes.
+
+.. cmd:: Transparent {? ! } {+ @reference }
 
    The opposite of :cmd:`Opaque`, it marks the specified constants
    as :term:`transparent`
@@ -986,6 +992,10 @@ which supports additional fine-tuning.
    the usual defined constants, whose actual values are of course
    relevant in general.
 
+   In the particular case where the constants refer to primitive projections,
+   a :token:`!` can be used to make the compatibility constants transparent
+   (see :cmd:`Opaque` for more details).
+
    .. exn:: The reference @qualid was not found in the current environment.
 
       There is no constant named :n:`@qualid` in the environment.

doc/tools/docgram/fullGrammar

@@ -1063,8 +1063,8 @@ gallina_ext: [
 | "Export" OPT import_categories LIST1 filtered_import
 | "Include" module_type_inl LIST0 ext_module_expr
 | "Include" "Type" module_type_inl LIST0 ext_module_type
-| "Transparent" LIST1 smart_global
-| "Opaque" LIST1 smart_global
+| "Transparent" OPT "!" LIST1 smart_global
+| "Opaque" OPT "!" LIST1 smart_global
 | "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
 | "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
 | "Canonical" OPT "Structure" by_notation

doc/tools/docgram/orderedGrammar

@@ -923,8 +923,8 @@ command: [
 | "Export" OPT import_categories LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
-| "Transparent" LIST1 reference
-| "Opaque" LIST1 reference
+| "Transparent" OPT "!" LIST1 reference
+| "Opaque" OPT "!" LIST1 reference
 | "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
 | "Canonical" OPT "Structure" ident_decl def_body
 | "Canonical" OPT "Structure" reference

kernel/constr.ml

@@ -1517,8 +1517,7 @@ let rec debug_print c =
   | Construct (((sp,i),j),u) ->
       str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
   | Proj (p,_r,c) ->
-    str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++
-    bool (Projection.unfolded p) ++ str"," ++ debug_print c ++ str")"
+    str"Proj(" ++ Projection.debug_print p ++ str"," ++ debug_print c ++ str")"
   | Case (_ci,_u,pms,(p,_),iv,c,bl) ->
     let pr_ctx (nas, c) =
       hov 2 (hov 0 (prvect (fun na -> Name.print na.binder_name ++ spc ()) nas ++ str "|-") ++ spc () ++

kernel/conv_oracle.ml

@@ -37,29 +37,35 @@ let is_transparent = function
 type oracle = {
   var_opacity : level Id.Map.t;
   cst_opacity : level Cmap.t;
+  prj_opacity : level PRmap.t;
   var_trstate : Id.Pred.t;
   cst_trstate : Cpred.t;
+  prj_trstate : PRpred.t;
 }
 
 let empty = {
   var_opacity = Id.Map.empty;
   cst_opacity = Cmap.empty;
+  prj_opacity = PRmap.empty;
   var_trstate = Id.Pred.full;
   cst_trstate = Cpred.full;
+  prj_trstate = PRpred.full;
 }
 
-let get_strategy { var_opacity; cst_opacity; _ } f = function
-  | VarKey id ->
+let get_strategy { var_opacity; cst_opacity; prj_opacity; _ } = function
+  | Evaluable.EvalVarRef id ->
       (try Id.Map.find id var_opacity
       with Not_found -> default)
-  | ConstKey c ->
-      (try Cmap.find (f c) cst_opacity
+  | Evaluable.EvalConstRef c ->
+      (try Cmap.find c cst_opacity
+      with Not_found -> default)
+  | Evaluable.EvalProjectionRef p ->
+      (try PRmap.find p prj_opacity
       with Not_found -> default)
-  | RelKey _ -> Expand
 
-let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l =
+let set_strategy ({var_opacity; cst_opacity; prj_opacity; _} as oracle) k l =
   match k with
-  | VarKey id ->
+  | Evaluable.EvalVarRef id ->
     let var_opacity =
       if is_default l then Id.Map.remove id var_opacity
       else Id.Map.add id l var_opacity
@@ -69,7 +75,7 @@ let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l =
     | _ -> Id.Pred.add id oracle.var_trstate
     in
     { oracle with var_opacity; var_trstate; }
-  | ConstKey c ->
+  | Evaluable.EvalConstRef c ->
     let cst_opacity =
       if is_default l then Cmap.remove c cst_opacity
       else Cmap.add c l cst_opacity
@@ -79,30 +85,52 @@ let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l =
     | _ -> Cpred.add c oracle.cst_trstate
     in
     { oracle with cst_opacity; cst_trstate; }
-  | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey")
+  | Evaluable.EvalProjectionRef p ->
+    let prj_opacity =
+      if is_default l then PRmap.remove p prj_opacity
+      else PRmap.add p l prj_opacity
+    in
+    let prj_trstate = match l with
+    | Opaque -> PRpred.remove p oracle.prj_trstate
+    | _ -> PRpred.add p oracle.prj_trstate
+    in
+    {oracle with prj_opacity; prj_trstate}
 
-let fold_strategy f { var_opacity; cst_opacity; _ } accu =
-  let fvar id lvl accu = f (VarKey id) lvl accu in
-  let fcst cst lvl accu = f (ConstKey cst) lvl accu in
+let fold_strategy f {var_opacity; cst_opacity; prj_opacity; _} accu =
+  let fvar id lvl accu = f (Evaluable.EvalVarRef id) lvl accu in
+  let fcst cst lvl accu = f (Evaluable.EvalConstRef cst) lvl accu in
+  let fprj p lvl accu = f (Evaluable.EvalProjectionRef p) lvl accu in
   let accu = Id.Map.fold fvar var_opacity accu in
-  Cmap.fold fcst cst_opacity accu
+  let accu = Cmap.fold fcst cst_opacity accu in
+  PRmap.fold fprj prj_opacity accu
 
-let get_transp_state { var_trstate; cst_trstate; _ } =
-  { TransparentState.tr_var = var_trstate; tr_cst = cst_trstate }
+let get_transp_state { var_trstate; cst_trstate; prj_trstate; _ } =
+  let open TransparentState in
+  { tr_var = var_trstate; tr_cst = cst_trstate ; tr_prj = prj_trstate }
 
-let dep_order l2r k1 k2 = match k1, k2 with
-| RelKey _, RelKey _ -> l2r
-| RelKey _, (VarKey _ | ConstKey _) -> true
-| VarKey _, RelKey _ -> false
-| VarKey _, VarKey _ -> l2r
-| VarKey _, ConstKey _ -> true
-| ConstKey _, (RelKey _ | VarKey _) -> false
-| ConstKey _, ConstKey _ -> l2r
+let dep_order l2r k1 k2 =
+  let open Evaluable in
+  match k1, k2 with
+  | None, None -> l2r
+  | None, _    -> true
+  | Some _, None -> false
+  | Some k1, Some k2 ->
+  match k1, k2 with
+  | EvalVarRef _, EvalVarRef _ -> l2r
+  | EvalVarRef _, (EvalConstRef _ | EvalProjectionRef _) -> true
+  | EvalConstRef _, EvalVarRef _ -> false
+  | EvalConstRef _, EvalProjectionRef _ -> l2r
+  | EvalConstRef _, EvalConstRef _ -> l2r
+  | EvalProjectionRef _, EvalVarRef _ -> false
+  | EvalProjectionRef _, EvalConstRef _ -> l2r
+  | EvalProjectionRef _, EvalProjectionRef _ -> l2r
 
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, use the recommended default. *)
-let oracle_order f o l2r k1 k2 =
-  match get_strategy o f k1, get_strategy o f k2 with
+let oracle_order o l2r k1 k2 =
+  let s1 = match k1 with None -> Expand | Some k1 -> get_strategy o k1 in
+  let s2 = match k2 with None -> Expand | Some k2 -> get_strategy o k2 in
+  match s1, s2 with
   | Expand, Expand -> dep_order l2r k1 k2
   | Expand, (Opaque | Level _) -> true
   | (Opaque | Level _), Expand -> false
@@ -112,5 +140,3 @@ let oracle_order f o l2r k1 k2 =
   | Level n1, Level n2 ->
      if Int.equal n1 n2 then dep_order l2r k1 k2
      else n1 < n2
-
-let get_strategy o = get_strategy o (fun x -> x)

kernel/conv_oracle.mli

@@ -18,8 +18,8 @@ val empty : oracle
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : ('a -> Constant.t) -> oracle -> bool ->
-  'a tableKey -> 'a tableKey -> bool
+val oracle_order :
+  oracle -> bool -> Evaluable.t option -> Evaluable.t option -> bool
 
 (** Priority for the expansion of constant in the conversion test.
  * Higher levels means that the expansion is less prioritary.
@@ -33,13 +33,13 @@ val transparent : level
 (** Check whether a level is transparent *)
 val is_transparent : level -> bool
 
-val get_strategy : oracle -> Constant.t tableKey -> level
+val get_strategy : oracle -> Evaluable.t -> level
 
 (** Sets the level of a constant.
  * Level of RelKey constant cannot be set. *)
-val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
+val set_strategy : oracle -> Evaluable.t -> level -> oracle
 
 (** Fold over the non-transparent levels of the oracle. Order unspecified. *)
-val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
+val fold_strategy : (Evaluable.t -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
 
 val get_transp_state : oracle -> TransparentState.t

kernel/conversion.ml

@@ -442,7 +442,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | Some t1, Some t2 ->
           (* else the oracle tells which constant is to be expanded *)
           let oracle = CClosure.oracle_of_infos infos.cnv_inf in
-          if Conv_oracle.oracle_order UVars.out_punivs oracle l2r fl1 fl2 then
+          let to_er fl =
+            match fl with
+            | ConstKey (c, _) -> Some (Evaluable.EvalConstRef c)
+            | VarKey id -> Some (Evaluable.EvalVarRef id)
+            | RelKey _ -> None
+          in
+          if Conv_oracle.oracle_order oracle l2r (to_er fl1) (to_er fl2) then
             eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv
           else
             eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv

kernel/names.ml

@@ -981,8 +981,18 @@ struct
   let to_string p = Constant.to_string (constant p)
   let print p = Constant.print (constant p)
 
+  let debug_to_string p =
+    (if unfolded p then "unfolded(" else "") ^
+    Constant.debug_to_string (constant p) ^
+    (if unfolded p then ")" else "")
+  let debug_print p = str (debug_to_string p)
+
 end
 
+module PRmap = HMap.Make(Projection.Repr.CanOrd)
+module PRset = PRmap.Set
+module PRpred = Predicate.Make(Projection.Repr.CanOrd)
+
 module GlobRefInternal = struct
 
   type t =
@@ -1096,3 +1106,28 @@ type lname = Name.t CAst.t
 type lstring = string CAst.t
 
 let lident_eq = CAst.eq Id.equal
+
+(** Evaluable references (whose transparency can be controlled) *)
+
+module Evaluable = struct
+  type t =
+    | EvalVarRef of Id.t
+    | EvalConstRef of Constant.t
+    | EvalProjectionRef of Projection.Repr.t
+
+  let map fvar fcst fprj = function
+    | EvalVarRef v -> EvalVarRef (fvar v)
+    | EvalConstRef c -> EvalConstRef (fcst c)
+    | EvalProjectionRef p -> EvalProjectionRef (fprj p)
+
+  let equal er1 er2 =
+    er1 == er2 ||
+    match er1, er2 with
+    | EvalVarRef v1, EvalVarRef v2 ->
+        Id.equal v1 v2
+    | EvalConstRef c1, EvalConstRef c2 ->
+        Constant.CanOrd.equal c1 c2
+    | EvalProjectionRef p1, EvalProjectionRef p2 ->
+        Projection.Repr.CanOrd.equal p1 p2
+    | _ -> false
+end

kernel/names.mli

@@ -643,8 +643,20 @@ module Projection : sig
   val print : t -> Pp.t
   (** Print internal representation (not to be used for user-facing messages). *)
 
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs extra information related to debug. *)
+
+  val debug_print : t -> Pp.t
+  (** Same as [print], but outputs extra information related to debug. *)
+
 end
 
+module PRset : CSig.SetS with type elt = Projection.Repr.t
+module PRmap : Map.ExtS with type key = Projection.Repr.t and module Set := PRset
+
+(** Predicate on projection representation (ignoring unfolding state) *)
+module PRpred : Predicate.S with type elt = Projection.Repr.t
+
 (** {6 Global reference is a kernel side type for all references together } *)
 
 module GlobRef : sig
@@ -682,3 +694,17 @@ type lname = Name.t CAst.t
 type lstring = string CAst.t
 
 val lident_eq : lident -> lident -> bool
+
+(** Evaluable references (whose transparency can be controlled) *)
+
+module Evaluable : sig
+  type t =
+    | EvalVarRef of Id.t
+    | EvalConstRef of Constant.t
+    | EvalProjectionRef of Projection.Repr.t
+
+  val map : (Id.t -> Id.t) -> (Constant.t -> Constant.t) ->
+    (Projection.Repr.t -> Projection.Repr.t) -> t -> t
+
+  val equal : t -> t -> bool
+end