From 46b9480a717d5ca78e354fa843f39eed87cb7b15 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:08:00 +0200 Subject: [refman] Rename num to natural --- doc/sphinx/language/core/assumptions.rst | 2 +- doc/sphinx/language/core/basic.rst | 16 ++++++++-------- doc/sphinx/language/core/modules.rst | 2 +- doc/sphinx/language/core/records.rst | 2 +- doc/sphinx/language/core/sorts.rst | 2 +- doc/sphinx/language/core/variants.rst | 2 +- doc/sphinx/language/extensions/match.rst | 6 +++--- 7 files changed, 16 insertions(+), 16 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 955f48b772..fe10e345cd 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -125,7 +125,7 @@ has type :n:`@type`. .. _Axiom: -.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt } +.. cmd:: @assumption_token {? Inline {? ( @natural ) } } {| {+ ( @assumpt ) } | @assumpt } :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables .. insertprodn assumption_token of_type diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 1f0d696d99..63c4243921 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -115,20 +115,20 @@ Numerals Numerals are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@num` is a non-negative + a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn numeral hexdigit .. prodn:: - numeral ::= {? - } @decnum {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnum } - | {? - } @hexnum {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnum } - int ::= {? - } @num - num ::= {| @decnum | @hexnum } - decnum ::= @digit {* {| @digit | _ } } + numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } + int ::= {? - } @natural + natural ::= {| @decnat | @hexnat } + decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 - hexnum ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } + hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } .. todo PR need some code fixes for hex, see PR 11948 @@ -292,7 +292,7 @@ rest of the |Coq| manual: :term:`terms ` and :term:`types .. prodn:: document ::= {* @sentence } sentence ::= {? @attributes } @command . - | {? @attributes } {? @num : } @query_command . + | {? @attributes } {? @natural : } @query_command . | {? @attributes } {? @toplevel_selector : } @ltac_expr {| . | ... } | @control_command diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 29e703c223..866104d5d1 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -67,7 +67,7 @@ together, as well as a means of massive abstraction. module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) module_type_inl ::= ! @module_type | @module_type {? @functor_app_annot } - functor_app_annot ::= [ inline at level @num ] + functor_app_annot ::= [ inline at level @natural ] | [ no inline ] module_type ::= @qualid | ( @module_type ) diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 0080f1d052..cd44d06e67 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -19,7 +19,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. prodn:: record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } - record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @num } {? @decl_notations } + record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term | {* @binder } := @term diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 3517d70005..98dd9a5426 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -20,7 +20,7 @@ Sorts | Type @%{ @universe %} universe ::= max ( {+, @universe_expr } ) | @universe_expr - universe_expr ::= @universe_name {? + @num } + universe_expr ::= @universe_name {? + @natural } The types of types are called :gdef:`sorts `. diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 8e2bf32dd6..ec8e93751c 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -22,7 +22,7 @@ Variants :attr:`universes(noncumulative)` and :attr:`private(matching)` attributes. - .. exn:: The @num th argument of @ident must be @ident in @type. + .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: Private (matching) inductive types diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 182f599a29..c36b9deef3 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -879,7 +879,7 @@ generated expression and the original. Here is a summary of the error messages corresponding to each situation: -.. exn:: The constructor @ident expects @num arguments. +.. exn:: The constructor @ident expects @natural arguments. The variable ident is bound several times in pattern term Found a constructor of inductive type term while a constructor of term is expected @@ -890,8 +890,8 @@ situation: The pattern matching is not exhaustive. -.. exn:: The elimination predicate term should be of arity @num (for non \ - dependent case) or @num (for dependent case). +.. exn:: The elimination predicate term should be of arity @natural (for non \ + dependent case) or @natural (for dependent case). The elimination predicate provided to match has not the expected arity. -- cgit v1.2.3 From 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 4 Sep 2020 15:09:00 +0200 Subject: [refman] Rename numeral to number --- doc/sphinx/language/coq-library.rst | 2 +- doc/sphinx/language/core/basic.rst | 4 ++-- doc/sphinx/language/core/variants.rst | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c27eb216e8..765373619f 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,7 +1062,7 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. -.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing] +.. warn:: The constant @number is not a binary64 floating-point value. A closest value @number will be used and unambiguously printed @number. [inexact-float,parsing] Not all decimal constants are floating-point values. This warning is generated when parsing such a constant (for instance ``0.1``). diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 63c4243921..be513833ad 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -119,10 +119,10 @@ Numerals integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. - .. insertprodn numeral hexdigit + .. insertprodn number hexdigit .. prodn:: - numeral ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } + number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } int ::= {? - } @natural natural ::= {| @decnat | @hexnat } diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index ec8e93751c..2904250e41 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -79,7 +79,7 @@ to apply specific treatments accordingly. | %{%| {* @qualid := @pattern } %|%} | _ | ( {+| @pattern } ) - | @numeral + | @number | @string Note that the :n:`@pattern ::= @pattern10 : @term` production -- cgit v1.2.3 From 724966f56caa66a5ddc9a992cf870ebc2efae004 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 11:53:49 +0200 Subject: [refman] Rename int to integer --- doc/sphinx/language/core/basic.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index be513833ad..d248839fa0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -111,11 +111,11 @@ Identifiers symbols and non-breaking space. :production:`unicode_id_part` non-exhaustively includes symbols for prime letters and subscripts. -Numerals - Numerals are sequences of digits with an optional fractional part +Numbers + Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals start with ``0x`` or ``0X``. :n:`@int` is an integer; - a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative + a number without fractional nor exponent parts. :n:`@natural` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. @@ -124,7 +124,7 @@ Numerals .. prodn:: number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } - int ::= {? - } @natural + integer ::= {? - } @natural natural ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 @@ -434,7 +434,7 @@ gray boxes after the labels "Flag", "Option" and "Table". In the pdf, they appear after a boldface label. They are listed in the :ref:`options_index`. -.. cmd:: Set @setting_name {? {| @int | @string } } +.. cmd:: Set @setting_name {? {| @integer | @string } } :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag -- cgit v1.2.3 From 031cc2ba1a19a06766df85b8693c72f16fa62de6 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 7 Sep 2020 12:07:23 +0200 Subject: [refman] Explicit integer and natural As respectively bigint and bignat that fit into an OCaml int. --- doc/sphinx/language/core/basic.rst | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index d248839fa0..9308da6d27 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -114,9 +114,9 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numerals - start with ``0x`` or ``0X``. :n:`@int` is an integer; - a number without fractional nor exponent parts. :n:`@natural` is a non-negative - integer. Underscores embedded in the digits are ignored, for example + start with ``0x`` or ``0X``. :n:`@bigint` are integers; + numbers without fractional nor exponent parts. :n:`@bignat` are non-negative + integers. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. .. insertprodn number hexdigit @@ -125,13 +125,17 @@ Numbers number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat } | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat } integer ::= {? - } @natural - natural ::= {| @decnat | @hexnat } + natural ::= @bignat + bigint ::= {? - } @bignat + bignat ::= {| @decnat | @hexnat } decnat ::= @digit {* {| @digit | _ } } digit ::= 0 .. 9 hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } } hexdigit ::= {| 0 .. 9 | a .. f | A .. F } - .. todo PR need some code fixes for hex, see PR 11948 + :n:`@integer` and :n:`@natural` are limited to the range that fits + into an OCaml integer (63-bit integers on most architectures). + :n:`@bigint` and :n:`@bignat` have no range limitation. Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent -- cgit v1.2.3 From ad7140a7127b147caf20d7c3803b918e3c6776f5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:29:00 +0200 Subject: [numeral notation] Improve documentation Following reviews from Jim Fehrle on #12218 and #12979 --- doc/sphinx/language/core/basic.rst | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9308da6d27..45bdc019ac 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -137,11 +137,20 @@ Numbers into an OCaml integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. + The :ref:`standard library ` provides some + :ref:`interpretations ` for :n:`@number`. The + :cmd:`Number Notation` mechanism offers the user + a way to define custom parsers and printers for :n:`@number`. + Strings Strings begin and end with ``"`` (double quote). Use ``""`` to represent a double quote character within a string. In the grammar, strings are identified with :production:`string`. + The :cmd:`String Notation` mechanism offers the + user a way to define custom parsers and printers for + :token:`string`. + Keywords The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the `-noinit` -- cgit v1.2.3