From a947a60c334506b936312fb56cfd2c1d25145cc6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 20 Jul 2020 14:08:26 +0200 Subject: Doc for variance syntax --- .../12653-cumul-syntax.rst | 4 ++++ doc/sphinx/addendum/universe-polymorphism.rst | 25 +++++++++++++++++++++- doc/sphinx/language/core/inductive.rst | 3 ++- 3 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 doc/changelog/02-specification-language/12653-cumul-syntax.rst (limited to 'doc') diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst new file mode 100644 index 0000000000..b6c87ed4b6 --- /dev/null +++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst @@ -0,0 +1,4 @@ +- **Added:** Syntax for specifying the variance of cumulative + polymorphic inductives (:ref:`cumulative`) instead of letting it be + inferred (`#12653 `_, by + Gaëtan Gilbert). diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1fb337b30a..064107d088 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation: .. coqtop:: all Polymorphic Cumulative Record packType := {pk : Type}. + About packType. :g:`packType` binds a covariant universe, i.e. @@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j +Specifying cumulativity +~~~~~~~~~~~~~~~~~~~~~~~ + +The variance of the universe parameters for a cumulative inductive may be specified by the user. + +For the following type, universe ``a`` has its variance automatically +inferred (it is irrelevant), ``b`` is required to be irrelevant, +``c`` is covariant and ``d`` is invariant. With these annotations +``c`` and ``d`` have less general variances than would be inferred. + +.. coqtop:: all + + Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy. + About Dummy. + +Insufficiently restrictive variance annotations lead to errors: + +.. coqtop:: all + + Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}. + An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -280,7 +302,7 @@ An example of a proof using cumulativity End down. Cumulativity Weak Constraints ------------------------------ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. flag:: Cumulativity Weak Constraints @@ -383,6 +405,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index d3bd787587..7bb03d7d85 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -11,10 +11,11 @@ Inductive types .. insertprodn inductive_definition constructor .. prodn:: - inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } + cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors -- cgit v1.2.3 From e511ef1aff7d2103ad6189f3fa79c456c2a42392 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 1 Sep 2020 12:20:37 +0200 Subject: Changelog for variance syntax --- doc/changelog/02-specification-language/12653-cumul-syntax.rst | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst index b6c87ed4b6..ba97f7c796 100644 --- a/doc/changelog/02-specification-language/12653-cumul-syntax.rst +++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst @@ -1,4 +1,5 @@ -- **Added:** Syntax for specifying the variance of cumulative - polymorphic inductives (:ref:`cumulative`) instead of letting it be - inferred (`#12653 `_, by - Gaëtan Gilbert). +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative ` + mode) (`#12653 `_, by Gaëtan + Gilbert). -- cgit v1.2.3 From 19f7d82edd68fb8940c7bcd73a229e957dee260c Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Tue, 21 Jul 2020 13:41:25 -0700 Subject: Update grammar in doc --- doc/sphinx/language/core/inductive.rst | 4 ++-- doc/tools/docgram/orderedGrammar | 10 +++++++++- 2 files changed, 11 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 7bb03d7d85..ad7d6f3963 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -8,14 +8,14 @@ Inductive types .. cmd:: Inductive @inductive_definition {* with @inductive_definition } - .. insertprodn inductive_definition constructor + .. insertprodn inductive_definition cumul_ident_decl .. prodn:: inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } - cumul_ident_decl ::= @ident {? @cumul_univ_decl } + cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 26474d950a..3e45240e5e 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -434,6 +434,10 @@ univ_decl: [ | "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] +cumul_univ_decl: [ +| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +] + univ_constraint: [ | universe_name [ "<" | "=" | "<=" ] universe_name ] @@ -695,7 +699,7 @@ field_def: [ ] inductive_definition: [ -| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations +| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations ] constructors_or_record: [ @@ -707,6 +711,10 @@ constructor: [ | ident LIST0 binder OPT of_type ] +cumul_ident_decl: [ +| ident OPT cumul_univ_decl +] + filtered_import: [ | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ] ] -- cgit v1.2.3