From 4c642b5c27d4f9c355044cb585a645b50dd844f2 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 6 May 2019 17:38:39 +0000 Subject: [User manual] Fix two warnings related to canonical structures --- doc/sphinx/addendum/canonical-structures.rst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index dd21ea09bd..d81dafa4db 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; #[not_canonical] 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. -- cgit v1.2.3 From e73c09a35c1aa5bc36b73ce555194752b9e6e25d Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 9 May 2019 06:57:09 +0000 Subject: Changelog for PR #10076 --- .../02-specification-language/10076-not-canonical-projection.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/02-specification-language/10076-not-canonical-projection.rst (limited to 'doc') 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 `_, + by Vincent Laporte). -- cgit v1.2.3 From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 9 May 2019 13:39:25 +0000 Subject: [Attributes] Allow explicit value for two-valued attributes Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean? --- doc/sphinx/addendum/canonical-structures.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index d81dafa4db..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; #[not_canonical] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. Arguments Mixin {e le} _. -- cgit v1.2.3 From 4895bf8bb5d0acfaee499991973fc6537657427d Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 10 May 2019 08:48:54 +0000 Subject: [refman] Mention the `#[canonical(false)]` attribute --- doc/sphinx/language/gallina-extensions.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'doc') 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3