Merge PR #20605: Cleanup handling of projection flags

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

dev/ci/user-overlays/20605-SkySkimmer-simpl-proj-flags.sh

@@ -0,0 +1,7 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi simpl-proj-flags 20605
+
+overlay metarocq https://github.com/SkySkimmer/metarocq simpl-proj-flags 20605
+
+overlay lean_importer https://github.com/SkySkimmer/rocq-lean-import simpl-proj-flags 20605
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp simpl-proj-flags 20605

vernac/record.ml

@@ -126,12 +126,18 @@ module DataI = struct
 end
 
 module Data = struct
+  (* XXX move coercion_flags to ComCoercion? *)
+  type coercion_flags = {
+    coe_local : bool;
+    coe_reversible : bool;
+  }
+  type instance_flags = {
+    inst_locality : Hints.hint_locality;
+    inst_priority : int option;
+  }
   type projection_flags = {
-    pf_coercion: bool;
-    pf_reversible: bool;
-    pf_instance: bool;
-    pf_priority: int option;
-    pf_locality: Goptions.option_locality;
+    pf_coercion: coercion_flags option;
+    pf_instance: instance_flags option;
     pf_canonical: bool;
   }
   type t =
@@ -473,7 +479,9 @@ let warning_or_error ?loc ~info flags indsp err =
              Himsg.explain_type_error env (Evd.from_env env)
                (Pretype_errors.of_type_error te))
   in
-  if flags.Data.pf_coercion || flags.Data.pf_instance then user_err ?loc ~info st;
+  (* XXX flags.pf_canonical? *)
+  if Option.has_some flags.Data.pf_coercion || Option.has_some flags.Data.pf_instance then
+    user_err ?loc ~info st;
   warn_cannot_define_projection ?loc (hov 0 st)
 
 type field_status =
@@ -523,22 +531,21 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
 (** Declare projection [ref] over [from] a coercion
    or a typeclass instance according to [flags]. *)
 let declare_proj_coercion_instance ~flags ref from =
-  if flags.Data.pf_coercion then begin
-    let cl = ComCoercion.class_of_global from in
-    let local = flags.Data.pf_locality = Goptions.OptLocal in
-    ComCoercion.try_add_new_coercion_with_source ref ~local ~reversible:flags.Data.pf_reversible ~source:cl
-  end;
-  if flags.Data.pf_instance then begin
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let info = Typeclasses.{ hint_priority = flags.Data.pf_priority; hint_pattern = None } in
-    let local =
-      match flags.Data.pf_locality with
-      | Goptions.OptLocal -> Hints.Local
-      | Goptions.(OptDefault | OptExport) -> Hints.Export
-      | Goptions.OptGlobal -> Hints.SuperGlobal in
-    Classes.declare_instance ~warn:true env sigma (Some info) local ref
-  end
+  let () = match flags.Data.pf_coercion with
+    | None -> ()
+    | Some { coe_local=local; coe_reversible=reversible } ->
+      let cl = ComCoercion.class_of_global from in
+      ComCoercion.try_add_new_coercion_with_source ref ~local ~reversible ~source:cl
+  in
+  let () = match flags.Data.pf_instance with
+    | None -> ()
+    | Some { inst_locality; inst_priority } ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      let info = Typeclasses.{ hint_priority = inst_priority; hint_pattern = None } in
+      Classes.declare_instance ~warn:true env sigma (Some info) inst_locality ref
+  in
+  ()
 
 (* TODO: refactor the declaration part here; this requires some
    surgery as Evarutil.finalize is called too early in the path *)
@@ -718,25 +725,25 @@ module Ast = struct
     { name : Names.lident
     ; is_coercion : coercion_flag
     ; binders: local_binder_expr list
-    ; cfs : (local_decl_expr * record_field_attr) list
+    ; cfs : (local_decl_expr * Data.projection_flags * notation_declaration list) list
     ; idbuild : lident
     ; sort : constr_expr option
     ; default_inhabitant_id : Id.t option
     }
 
   let to_datai { name; idbuild; cfs; sort; default_inhabitant_id; } =
-    let fs = List.map fst cfs in
+    let fs = List.map pi1 cfs in
     { DataI.name = name
     ; constructor_name = idbuild.CAst.v
     ; arity = sort
-    ; nots = List.map (fun (_, { rf_notation }) -> List.map Metasyntax.prepare_where_notation rf_notation) cfs
+    ; nots = List.map (fun (_, _, rf_notation) -> List.map Metasyntax.prepare_where_notation rf_notation) cfs
     ; fs
     ; default_inhabitant_id
     }
 end
 
 let check_unique_names ~def records =
-  let extract_name acc (rf_decl, _) = match rf_decl with
+  let extract_name acc (rf_decl, _, _) = match rf_decl with
       Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
     | _ -> acc in
@@ -763,47 +770,10 @@ let kind_class =
   function Class true -> DefClass | Class false -> RecordClass
   | Inductive_kw | CoInductive | Variant | Record | Structure -> NotClass
 
-let check_priorities kind records =
-  let open Vernacexpr in
-  let isnot_class = kind_class kind <> RecordClass in
-  let has_priority { Ast.cfs; _ } =
-    List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
-  in
-  if isnot_class && List.exists has_priority records then
-    user_err Pp.(str "Priorities only allowed for type class substructures.")
-
-let check_proj_flags kind rf =
-  let open Vernacexpr in
-  let pf_coercion, pf_reversible =
-    match rf.rf_coercion with
-    | AddCoercion -> true, Option.default true rf.rf_reversible
-    | NoCoercion ->
-       if rf.rf_reversible <> None then
-         Attributes.(unsupported_attributes
-           [CAst.make ("reversible (without :>)",VernacFlagEmpty)]);
-       false, false in
-  let pf_instance =
-    match rf.rf_instance with NoInstance -> false | BackInstance -> true in
-  let pf_priority = rf.rf_priority in
-  let pf_locality =
-    begin match rf.rf_coercion, rf.rf_instance with
-    | NoCoercion, NoInstance ->
-       if rf.rf_locality <> Goptions.OptDefault then
-         Attributes.(unsupported_attributes
-           [CAst.make ("locality (without :> or ::)",VernacFlagEmpty)])
-    | AddCoercion, NoInstance ->
-       if rf.rf_locality = Goptions.OptExport then
-         Attributes.(unsupported_attributes
-           [CAst.make ("export (without ::)",VernacFlagEmpty)])
-    | _ -> ()
-    end; rf.rf_locality in
-  let pf_canonical = rf.rf_canonical in
-  Data.{ pf_coercion; pf_reversible; pf_instance; pf_priority; pf_locality; pf_canonical }
-
-let extract_record_data kind records =
+let extract_record_data records =
   let data = List.map Ast.to_datai records in
   let decl_data = List.map (fun { Ast.is_coercion; cfs } ->
-      let proj_flags = List.map (fun (_,rf) -> check_proj_flags kind rf) cfs in
+      let proj_flags = List.map (fun (_,rf,_) -> rf) cfs in
       { Data.is_coercion; proj_flags })
       records
   in
@@ -823,8 +793,7 @@ let extract_record_data kind records =
 let pre_process_structure udecl kind ~flags ~primitive_proj (records : Ast.t list) =
   let def = (kind = Vernacexpr.Class true) in
   let indlocs = check_unique_names ~def records in
-  let () = check_priorities kind records in
-  let ps, interp_data, decl_data = extract_record_data kind records in
+  let ps, interp_data, decl_data = extract_record_data records in
   let entry =
     (* In theory we should be able to use
        [Notation.with_notation_protection], due to the call to
@@ -1107,14 +1076,6 @@ let definition_structure ~flags udecl kind ~primitive_proj (records : Ast.t list
   inds
 
 module Internal = struct
-  type nonrec projection_flags = Data.projection_flags = {
-    pf_coercion: bool;
-    pf_reversible: bool;
-    pf_instance: bool;
-    pf_priority: int option;
-    pf_locality: Goptions.option_locality;
-    pf_canonical: bool;
-  }
   let declare_projections = declare_projections
   let declare_structure_entry = declare_structure_entry
 end

vernac/record.mli

@@ -13,12 +13,32 @@ open Vernacexpr
 open Constrexpr
 open Structures
 
+module Data : sig
+  type coercion_flags = {
+    coe_local : bool;
+    coe_reversible : bool;
+  }
+  type instance_flags = {
+    inst_locality : Hints.hint_locality;
+    inst_priority : int option;
+  }
+  type projection_flags = {
+    pf_coercion: coercion_flags option;
+    pf_instance: instance_flags option;
+    pf_canonical: bool;
+  }
+  type t = {
+    is_coercion : Vernacexpr.coercion_flag;
+    proj_flags : projection_flags list;
+  }
+end
+
 module Ast : sig
   type t =
     { name : Names.lident
     ; is_coercion : coercion_flag
     ; binders: local_binder_expr list
-    ; cfs : (local_decl_expr * record_field_attr) list
+    ; cfs : (local_decl_expr * Data.projection_flags * notation_declaration list) list
     ; idbuild : lident
     ; sort : constr_expr option
     ; default_inhabitant_id : Id.t option
@@ -33,21 +53,6 @@ val definition_structure
   -> Ast.t list
   -> GlobRef.t list
 
-module Data : sig
-  type projection_flags = {
-    pf_coercion: bool;
-    pf_reversible: bool;
-    pf_instance: bool;
-    pf_priority: int option;
-    pf_locality: Goptions.option_locality;
-    pf_canonical: bool;
-  }
-  type t =
-    { is_coercion : Vernacexpr.coercion_flag
-    ; proj_flags : projection_flags list
-    }
-end
-
 module RecordEntry : sig
 
   type one_ind_info = {
@@ -96,20 +101,11 @@ val canonical_inhabitant_id : isclass:bool -> Id.t -> Id.t
 (* Implementation internals, consult Rocq developers before using;
    current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *)
 module Internal : sig
-  type projection_flags = {
-    pf_coercion: bool;
-    pf_reversible: bool;
-    pf_instance: bool;
-    pf_priority: int option;
-    pf_locality: Goptions.option_locality;
-    pf_canonical: bool;
-  }
-
   val declare_projections
     : Names.inductive
     -> kind:Decls.definition_object_kind
     -> inhabitant_id:Names.Id.t
-    -> projection_flags list
+    -> Data.projection_flags list
     -> ?fieldlocs:Loc.t option list
     -> Impargs.manual_implicits list
     -> Structure.projection list

vernac/vernacentries.ml

@@ -1076,6 +1076,64 @@ module Preprocessed_Mind_decl = struct
     | Inductive of inductive
 end
 
+(* Intermediate type while parsing record field flags *)
+type record_field_attr = {
+  rf_coercion: coercion_flag; (* the projection is an implicit coercion *)
+  rf_reversible: bool option; (* coercion is reversible, if relevant *)
+  rf_instance: instance_flag; (* the projection is an instance *)
+  rf_priority: int option; (* priority of the instance, if relevant *)
+  rf_locality: Goptions.option_locality; (* locality of coercion and instance *)
+  rf_canonical: bool; (* use this projection in the search for canonical instances *)
+}
+
+let check_proj_flags rf =
+  let open Vernacexpr in
+  let open Record.Data in
+  let () = match rf.rf_coercion, rf.rf_instance with
+    | NoCoercion, NoInstance ->
+      if rf.rf_locality <> Goptions.OptDefault then
+        Attributes.(unsupported_attributes
+                      [CAst.make ("locality (without :> or ::)",VernacFlagEmpty)])
+    | AddCoercion, NoInstance ->
+      if rf.rf_locality = Goptions.OptExport then
+        Attributes.(unsupported_attributes
+                      [CAst.make ("export (without ::)",VernacFlagEmpty)])
+    | _ -> ()
+  in
+  let pf_coercion =
+    match rf.rf_coercion with
+    | AddCoercion ->
+      Some {
+        coe_local = rf.rf_locality = OptLocal;
+        coe_reversible = Option.default true rf.rf_reversible;
+      }
+    | NoCoercion ->
+      if rf.rf_reversible <> None then
+        Attributes.(unsupported_attributes
+                      [CAst.make ("reversible (without :>)",VernacFlagEmpty)]);
+      None
+  in
+  let pf_instance =
+    match rf.rf_instance with
+    | NoInstance ->
+      let () = if Option.has_some rf.rf_priority then
+          CErrors.user_err Pp.(str "Priority not allowed without \"::\".")
+      in
+      None
+    | BackInstance ->
+      let local =
+        match rf.rf_locality with
+        | Goptions.OptLocal -> Hints.Local
+        | Goptions.(OptDefault | OptExport) -> Hints.Export
+        | Goptions.OptGlobal -> Hints.SuperGlobal
+      in
+      Some {
+        inst_locality = local;
+        inst_priority = rf.rf_priority;
+      }
+  in
+  { pf_coercion; pf_instance; pf_canonical = rf.rf_canonical }
+
 let preprocess_defclass ~atts udecl (id, bl, c, l) =
   let poly, mode =
     Attributes.(parse Notations.(polymorphic ++ mode_attr) atts)
@@ -1096,10 +1154,14 @@ let preprocess_defclass ~atts udecl (id, bl, c, l) =
   let ((attr, rf_coercion, rf_instance), (lid, ce)) = l in
   let rf_locality = match rf_coercion, rf_instance with
     | AddCoercion, _ | _, BackInstance -> parse option_locality attr
-    | _ -> let () = unsupported_attributes attr in Goptions.OptDefault in
+    | _ -> let () = unsupported_attributes attr in Goptions.OptDefault
+  in
   let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
-          { rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
-            rf_locality ; rf_notation = [] ; rf_canonical = true } in
+          check_proj_flags
+            { rf_coercion ; rf_reversible = None ; rf_instance ; rf_priority = None ;
+              rf_locality ; rf_canonical = true },
+          []
+  in
   let recordl = [id, bl, c, None, [f], None] in
   let kind = Class true in
   let records = vernac_record recordl in
@@ -1142,14 +1204,17 @@ let preprocess_record ~atts udecl kind indl =
         | _ -> Notations.return Goptions.OptDefault in
       Notations.(rev ++ loc ++ canonical_field) in
     let (rf_reversible, rf_locality), rf_canonical = parse attr f.rfu_attrs in
-    x,
-    { rf_coercion = f.rfu_coercion;
-      rf_reversible;
-      rf_instance = f.rfu_instance;
-      rf_priority = f.rfu_priority;
-      rf_locality;
-      rf_notation = f.rfu_notation;
-      rf_canonical } in
+    let flags = check_proj_flags {
+        rf_coercion = f.rfu_coercion;
+        rf_reversible;
+        rf_instance = f.rfu_instance;
+        rf_priority = f.rfu_priority;
+        rf_locality;
+        rf_canonical;
+      }
+    in
+    x, flags, f.rfu_notation
+  in
   let unpack ((id, bl, c, decl), _) = match decl with
     | RecordDecl (oc, fs, ido) ->
       let bl = match bl with
@@ -1234,7 +1299,7 @@ let dump_inductive indl_for_glob decl =
       indl_for_glob;
     match decl with
     | Record { records } ->
-      let dump_glob_proj (x, _) = match x with
+      let dump_glob_proj (x, _, _) = match x with
         | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
         | _ -> () in

vernac/vernacexpr.mli

@@ -209,16 +209,6 @@ type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
 type 'a with_coercion_instance = (Attributes.vernac_flags * coercion_flag * instance_flag) * 'a
-(* Attributes of a record field declaration *)
-type record_field_attr = {
-  rf_coercion: coercion_flag; (* the projection is an implicit coercion *)
-  rf_reversible: bool option; (* coercion is reversible, if relevant *)
-  rf_instance: instance_flag; (* the projection is an instance *)
-  rf_priority: int option; (* priority of the instance, if relevant *)
-  rf_locality: Goptions.option_locality; (* locality of coercion and instance *)
-  rf_notation: notation_declaration list;
-  rf_canonical: bool; (* use this projection in the search for canonical instances *)
-  }
 (* Same before parsing the attributes *)
 type record_field_attr_unparsed = {
   rfu_attrs: Attributes.vernac_flags;