[Canonical structures] “not_canonical” annotation to field declarations

7 files changed, 36 insertions, 13 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9b8c4efb37..31b0b7e49a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -219,3 +219,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 =
+  bool_attribute ~name:"Canonical projection" ~on:"canonical" ~off:"not_canonical"
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 3cb4d69ca0..2559941354 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 option 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 59d2a66259..cc74121064 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 |> Option.default true 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 9b0fbea148..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, Recordops.mk_proj_kind 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 51ab7487d7..24bb27e107 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,12 +14,17 @@ 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 ->
     Recordops.proj_kind list * Constant.t option list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 279d4f0935..208210217a 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 34a9b9394a..7267def362 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -148,6 +148,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 =