aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh6
-rw-r--r--doc/changelog/02-specification-language/10076-not-canonical-projection.rst4
-rw-r--r--doc/sphinx/addendum/canonical-structures.rst13
-rw-r--r--doc/sphinx/language/gallina-extensions.rst19
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml2
-rw-r--r--pretyping/recordops.ml54
-rw-r--r--pretyping/recordops.mli10
-rw-r--r--test-suite/success/attribute_syntax.v4
-rw-r--r--vernac/attributes.ml33
-rw-r--r--vernac/attributes.mli1
-rw-r--r--vernac/g_vernac.mlg9
-rw-r--r--vernac/record.ml26
-rw-r--r--vernac/record.mli9
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacexpr.ml1
16 files changed, 145 insertions, 52 deletions
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+ elpi_CI_REF=canonical-disable-hint
+ elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
new file mode 100644
index 0000000000..0a902079b9
--- /dev/null
+++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst
@@ -0,0 +1,4 @@
+- Record fields can be annotated to prevent them from being used as canonical projections;
+ see :ref:`canonicalstructures` for details
+ (`#10076 <https://github.com/coq/coq/pull/10076>`_,
+ by Vincent Laporte).
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index dd21ea09bd..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
LE_class : LE.class T;
extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
- Structure type := _Pack { obj : Type; class_of : class obj }.
+ Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
Arguments Mixin {e le} _.
@@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we
are adding to ``EQ`` and ``LE``. In particular it contains the requirement
that the two relations we are combining are compatible.
+The `class_of` projection of the `type` structure is annotated as *not canonical*;
+it plays no role in the search for instances.
+
Unfortunately there is still an obstacle to developing the algebraic
theory of this new class.
@@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected.
Unfortunately, these declarations are very verbose. In the following
subsection we show how to make them more compact.
-.. FIXME shouldn't warn
-
-.. coqtop:: all warn
+.. coqtop:: all
Module Add_instance_attempt.
@@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`.
The declaration of canonical instances can now be way more compact:
-.. FIXME should not warn
-
-.. coqtop:: all warn
+.. coqtop:: all
Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 5308330820..ba766c8c3d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given.
If a same field occurs in several canonical structures, then
only the structure declared first as canonical is considered.
+ .. note::
+ To prevent a field from being involved in the inference of canonical instances,
+ its declaration can be annotated with the :g:`#[canonical(false)]` attribute.
+
+ .. example::
+
+ For instance, when declaring the :g:`Setoid` structure above, the
+ :g:`Prf_equiv` field declaration could be written as follows.
+
+ .. coqdoc::
+
+ #[canonical(false)] Prf_equiv : equivalence Carrier Equal
+
+ See :ref:`canonicalstructures` for a more realistic example.
+
.. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
This is equivalent to a regular definition of :token:`ident` followed by the
@@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
Print Canonical Projections.
+ .. note::
+
+ The last line would not show up if the corresponding projection (namely
+ :g:`Prf_equiv`) were annotated as not canonical, as described above.
Implicit types of variables
~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e5bf52571c..bb66658a37 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -850,10 +850,10 @@ let rec extern inctx scopes vars r =
| Some c :: q ->
match locs with
| [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
- | (_, false) :: locs' ->
+ | { Recordops.pk_true_proj = false } :: locs' ->
(* we don't want to print locals *)
ip q locs' args acc
- | (_, true) :: locs' ->
+ | { Recordops.pk_true_proj = true } :: locs' ->
match args with
| [] -> raise No_match
(* we give up since the constructor is not complete *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c0801067ce..f06493b374 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer =
let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
- | (_, regular) :: proj_kinds ->
+ | { Recordops.pk_true_proj = regular } :: proj_kinds ->
(* "regular" is false when the field is defined
by a let-in in the record declaration
(its value is fixed from other fields). *)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index d69824a256..a23c58c062 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -27,16 +27,27 @@ open Reductionops
(*s A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
-(* Table des structures: le nom de la structure (un [inductive]) donne
- le nom du constructeur, le nombre de paramètres et pour chaque
- argument réel du constructeur, le nom de la projection
- correspondante, si valide, et un booléen disant si c'est une vraie
- projection ou bien une fonction constante (associée à un LetIn) *)
+(* Table of structures.
+ It maps to each structure name (of type [inductive]):
+ - the name of its constructor;
+ - the number of parameters;
+ - for each true argument, some data about the corresponding projection:
+ * its name (may be anonymous);
+ * whether it is a true projection (as opposed to a constant function, LetIn);
+ * whether it should be used as a canonical hint;
+ * the constant realizing this projection (if any).
+*)
+
+type proj_kind = {
+ pk_name: Name.t;
+ pk_true_proj: bool;
+ pk_canonical: bool;
+}
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : (Name.t * bool) list;
+ s_PROJKIND : proj_kind list;
s_PROJ : Constant.t option list }
let structure_table =
@@ -47,7 +58,7 @@ let projection_table =
(* TODO: could be unify struc_typ and struc_tuple ? *)
type struc_tuple =
- constructor * (Name.t * bool) list * Constant.t option list
+ constructor * proj_kind list * Constant.t option list
let register_structure env (id,kl,projs) =
let open Declarations in
@@ -161,7 +172,7 @@ let canonical_projections () =
!object_table []
let keep_true_projections projs kinds =
- let filter (p, (_, b)) = if b then Some p else None in
+ let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in
List.map_filter filter (List.combine projs kinds)
let rec cs_pattern_of_constr env t =
@@ -206,17 +217,20 @@ let compute_canonical_projections env ~warn (con,ind) =
let o_NPARAMS = List.length o_TPARAMS in
let lpj = keep_true_projections lpj kl in
let nenv = Termops.push_rels_assum sign env in
- List.fold_left2 (fun acc spopt t ->
- Option.cata (fun proji_sp ->
- match cs_pattern_of_constr nenv t with
- | patt, o_INJ, o_TCOMPS ->
- ((ConstRef proji_sp, (patt, t)),
- { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
- :: acc
- | exception Not_found ->
- if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
- acc
- ) acc spopt
+ List.fold_left2 (fun acc (spopt, canonical) t ->
+ if canonical
+ then
+ Option.cata (fun proji_sp ->
+ match cs_pattern_of_constr nenv t with
+ | patt, o_INJ, o_TCOMPS ->
+ ((ConstRef proji_sp, (patt, t)),
+ { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+ :: acc
+ | exception Not_found ->
+ if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+ acc
+ ) acc spopt
+ else acc
) [] lpj projs
let pr_cs_pattern = function
@@ -288,7 +302,7 @@ let check_and_decompose_canonical_structure env sigma ref =
with Not_found ->
error_not_structure ref
(str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
- let ntrue_projs = List.count snd s.s_PROJKIND in
+ let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
(sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f0594d513a..25b6cd0751 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -17,14 +17,20 @@ open Constr
(** A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
+type proj_kind = {
+ pk_name: Name.t;
+ pk_true_proj: bool;
+ pk_canonical: bool;
+}
+
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : (Name.t * bool) list;
+ s_PROJKIND : proj_kind list;
s_PROJ : Constant.t option list }
type struc_tuple =
- constructor * (Name.t * bool) list * Constant.t option list
+ constructor * proj_kind list * Constant.t option list
val register_structure : Environ.env -> struc_tuple -> unit
val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index f4f59a3c16..4717759dec 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -20,6 +20,10 @@ Check ι _ ι.
Fixpoint f (n: nat) {wf lt n} : nat := _.
Reset f.
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
#[deprecated(since="8.9.0")]
Ltac foo := foo.
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:57:08 +0000