Merge PR #10076: [Canonical structures] Annotation to field declarations to prevent them from being “canonical”

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: robbertkrebbers
Ack-by: vbgl

7 files changed, 61 insertions, 20 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9b8c4efb37..1ad5862d5d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -82,9 +82,12 @@ let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
+let error_twice ~name : 'a =
+  user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
 let assert_once ~name prev =
   if Option.has_some prev then
-    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+    error_twice ~name
 
 let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
   let rec p extra v = function
@@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute =
   attribute_of_list [(on, single_key_parser ~name ~key:on true);
                (off, single_key_parser ~name ~key:off false)]
 
+(* Variant of the [bool] attribute with only two values (bool has three). *)
+let get_bool_value ~key ~default =
+  function
+  | VernacFlagEmpty -> default
+  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
+  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
+
+let enable_attribute ~key ~default : bool attribute =
+  fun atts ->
+  let default = default () in
+  let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in
+  extra,
+  match this with
+  | [] -> default
+  | [ _, value ] -> get_bool_value ~key ~default:true value
+  | _ -> error_twice ~name:key
+
 let qualify_attribute qual (parser:'a attribute) : 'a attribute =
   fun atts ->
     let rec extract extra qualified = function
@@ -139,11 +160,8 @@ let () = let open Goptions in
       optread  = (fun () -> !program_mode);
       optwrite = (fun b -> program_mode:=b) }
 
-let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
-
-let program = program_opt >>= function
-  | Some b -> return b
-  | None -> return (!program_mode)
+let program =
+  enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
@@ -219,3 +237,6 @@ let only_polymorphism atts = parse polymorphic atts
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
 let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+
+let canonical =
+  enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 3cb4d69ca0..44688ddafc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -52,6 +52,7 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
+val canonical : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 94d4ed80d1..6438b48e32 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command"
 
 let subprf = Entry.create "vernac:subprf"
 
+let quoted_attributes = Entry.create "vernac:quoted_attributes"
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
 let def_body = Entry.create "vernac:def_body"
@@ -75,7 +76,7 @@ let parse_compat_version = let open Flags in function
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: vernac_control gallina_ext noedit_mode subprf;
+  GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
   vernac_control: FIRST
     [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
       | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
@@ -447,10 +448,12 @@ GRAMMAR EXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-  [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+  [ [ attr = LIST0 quoted_attributes ;
+      bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
       rf_notation = decl_notation -> {
+      let rf_canonical = attr |> List.flatten |> parse canonical in
       let rf_subclass, rf_decl = bd in
-      rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ]
+      rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;
   record_fields:
     [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
diff --git a/vernac/record.ml b/vernac/record.ml
index f489707eb3..f737a8c524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
   let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
   Termops.substl_rel_context (subst @ subst') fields
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+      (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
         let fi = RelDecl.get_name decl in
         let ti = RelDecl.get_type decl in
 	let (sp_projs,i,subst) =
@@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 	    in
 	    let refi = ConstRef kn in
 	    Impargs.maybe_declare_manual_implicits false refi impls;
-	    if coe then begin
+            if flags.pf_subclass then begin
 	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
 	    end;
 	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
-	      warning_or_error coe indsp why;
+              warning_or_error flags.pf_subclass indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
-      (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+      (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+      (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 open Typeclasses
@@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-      let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
+      let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+                         List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Method ~name:[|binder_name|] record_data
       in
@@ -699,7 +705,11 @@ let definition_structure udecl kind ~template cum poly finite records =
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
-      let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in
+      let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+          { pf_subclass = not (Option.is_empty rf_subclass);
+            pf_canonical = rf_canonical })
+          cfs
+      in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index d6e63901cd..24bb27e107 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,15 +14,20 @@ open Constrexpr
 
 val primitive_flag : bool ref
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 val declare_projections :
   inductive ->
   Entries.universes_entry ->
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
-  bool list ->
+  projection_flags list ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
-    (Name.t * bool) list * Constant.t option list
+    Recordops.proj_kind list * Constant.t option list
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c7795602aa..e1d134f3a9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -744,7 +744,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
-            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a51fdfe59..23633e39ab 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -149,6 +149,7 @@ type record_field_attr = {
   rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
   rf_priority: int option; (* priority of the instance, if relevant *)
   rf_notation: decl_notation list;
+  rf_canonical: bool; (* use this projection in the search for canonical instances *)
   }
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =