From 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:10:26 +0200 Subject: Renaming Numeral.v into Number.v --- doc/sphinx/language/core/basic.rst | 2 +- doc/sphinx/user-extensions/syntax-extensions.rst | 50 ++++++++++++------------ doc/stdlib/hidden-files | 1 + doc/stdlib/index-list.html.template | 2 +- 4 files changed, 28 insertions(+), 27 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 29a2b40162..dfa2aaf8ff 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -113,7 +113,7 @@ Identifiers Numbers Numbers are sequences of digits with an optional fractional part - and exponent, optionally preceded by a minus sign. Hexadecimal numerals + and exponent, optionally preceded by a minus sign. Hexadecimal numbers 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 diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 06018304ab..f982898335 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1571,32 +1571,32 @@ Number notations parsing and printing functions, respectively. The parsing function :n:`@qualid__parse` should have one of the following types: - * :n:`Numeral.int -> @qualid__type` - * :n:`Numeral.int -> option @qualid__type` - * :n:`Numeral.uint -> @qualid__type` - * :n:`Numeral.uint -> option @qualid__type` + * :n:`Number.int -> @qualid__type` + * :n:`Number.int -> option @qualid__type` + * :n:`Number.uint -> @qualid__type` + * :n:`Number.uint -> option @qualid__type` * :n:`Z -> @qualid__type` * :n:`Z -> option @qualid__type` - * :n:`Numeral.numeral -> @qualid__type` - * :n:`Numeral.numeral -> option @qualid__type` + * :n:`Number.number -> @qualid__type` + * :n:`Number.number -> option @qualid__type` And the printing function :n:`@qualid__print` should have one of the following types: - * :n:`@qualid__type -> Numeral.int` - * :n:`@qualid__type -> option Numeral.int` - * :n:`@qualid__type -> Numeral.uint` - * :n:`@qualid__type -> option Numeral.uint` + * :n:`@qualid__type -> Number.int` + * :n:`@qualid__type -> option Number.int` + * :n:`@qualid__type -> Number.uint` + * :n:`@qualid__type -> option Number.uint` * :n:`@qualid__type -> Z` * :n:`@qualid__type -> option Z` - * :n:`@qualid__type -> Numeral.numeral` - * :n:`@qualid__type -> option Numeral.numeral` + * :n:`@qualid__type -> Number.number` + * :n:`@qualid__type -> option Number.number` .. deprecated:: 8.12 - Numeral notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by numeral - notations on :g:`Numeral.uint`, :g:`Numeral.int` and - :g:`Numeral.numeral`. + Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and + :g:`Decimal.decimal` are replaced respectively by number + notations on :g:`Number.uint`, :g:`Number.int` and + :g:`Number.number`. When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes @@ -1620,7 +1620,7 @@ Number notations returns :n:`(@qualid__parse m)` when parsing a literal :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a - :g:`Numeral.int`, :g:`Numeral.uint`, :g:`Z` or :g:`Numeral.numeral`, depending on the + :g:`Number.int`, :g:`Number.uint`, :g:`Z` or :g:`Number.number`, depending on the type of the parsing function :n:`@qualid__parse`. This allows for a more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a @@ -1644,31 +1644,31 @@ Number notations .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :token:`type` does not support + The number notation registered for :token:`type` does not support the given number. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. - .. exn:: @qualid__parse should go from Numeral.int to @type or (option @type). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The parsing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: @qualid__print should go from @type to Numeral.int or (option Numeral.int). Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first). + .. exn:: @qualid__print should go from @type to Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The printing function given to the :cmd:`Number Notation` vernacular is not of the right type. - .. exn:: Unexpected term @term while parsing a numeral notation. + .. exn:: Unexpected term @term while parsing a number notation. Parsing functions must always return ground terms, made up of applications of constructors, inductive types, and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term @term while parsing a numeral notation. + .. exn:: Unexpected non-option term @term while parsing a number notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a @@ -1741,16 +1741,16 @@ String notations concrete string expressed as a decimal. They may not return opaque constants. -The following errors apply to both string and numeral notations: +The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. - String and numeral notations can only be declared for inductive types with no + String and number notations can only be declared for inductive types with no arguments. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. - The inductive type used to register the string or numeral notation is no + The inductive type used to register the string or number notation is no longer available in the environment. Most likely, this is because the notation was declared inside a functor for an inductive type inside the functor. This use case is not currently diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 4d2972ef8f..e4f0967794 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,3 +1,4 @@ +theories/Init/Numeral.v theories/btauto/Algebra.v theories/btauto/Btauto.v theories/btauto/Reflect.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7c1328916b..e42066d2ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -22,7 +22,7 @@ through the Require Import command.

theories/Init/Nat.v theories/Init/Decimal.v theories/Init/Hexadecimal.v - theories/Init/Numeral.v + theories/Init/Number.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v -- cgit v1.2.3 From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:13:44 +0200 Subject: Renaming numnotoption into number_modifier --- doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++---- doc/tools/docgram/common.edit_mlg | 10 +++++----- doc/tools/docgram/fullGrammar | 6 +++--- doc/tools/docgram/orderedGrammar | 7 ++++--- 4 files changed, 16 insertions(+), 15 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index f982898335..a36772b2d7 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1553,16 +1553,16 @@ numbers (see :ref:`datatypes`). Number notations ~~~~~~~~~~~~~~~~ -.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @numeral_modifier } +.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @number_modifier } :name: Number Notation - .. insertprodn numeral_modifier numeral_modifier + .. insertprodn number_modifier number_modifier .. prodn:: - numeral_modifier ::= ( warning after @bignat ) + number_modifier ::= ( warning after @bignat ) | ( abstract after @bignat ) - This command allows the user to customize the way numeral literals + This command allows the user to customize the way number literals are parsed and printed. :n:`@qualid__type` diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f6a684bbd7..5d0f9208fc 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier +| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier +| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,7 +1358,7 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -numeral_modifier: [ +number_modifier: [ | OPTINREF ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c764cb6f37..914347b4cf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numeral_modifier -| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier +| "Number" "Notation" reference reference reference ":" ident number_modifier +| "Numeral" "Notation" reference reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,7 +2549,7 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 12a7bc684d..a972ad4719 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,6 +910,7 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1269,7 +1270,7 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -- cgit v1.2.3 From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:12:00 +0200 Subject: [numeral notation] Adding the via ... using ... option This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R. --- doc/tools/docgram/common.edit_mlg | 8 ++++---- doc/tools/docgram/fullGrammar | 12 ++++++++++-- doc/tools/docgram/orderedGrammar | 14 +++++++++++--- 3 files changed, 25 insertions(+), 9 deletions(-) (limited to 'doc') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5d0f9208fc..4d615a130a 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 914347b4cf..8a0feb0e2f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident number_modifier -| "Numeral" "Notation" reference reference reference ":" ident number_modifier +| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2555,6 +2555,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| reference reference +] + +number_via: [ +| "via" reference "using" "(" LIST1 number_using SEP "," ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a972ad4719..d12b3bf6cd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +910,7 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1275,6 +1275,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| qualid qualid +] + +number_via: [ +| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" -- cgit v1.2.3 From c217bbe80e18255ee3e67fa6266736529d80636d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:14:00 +0200 Subject: [numeral notation] Document the via ... using ... option --- doc/sphinx/user-extensions/syntax-extensions.rst | 116 +++++++++++++++++++++-- doc/tools/docgram/common.edit_mlg | 14 ++- doc/tools/docgram/fullGrammar | 22 +++-- doc/tools/docgram/orderedGrammar | 16 ++-- 4 files changed, 139 insertions(+), 29 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a36772b2d7..f07eb02946 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1553,14 +1553,16 @@ numbers (see :ref:`datatypes`). Number notations ~~~~~~~~~~~~~~~~ -.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @number_modifier } +.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name :name: Number Notation - .. insertprodn number_modifier number_modifier + .. insertprodn number_modifier number_via .. prodn:: - number_modifier ::= ( warning after @bignat ) - | ( abstract after @bignat ) + number_modifier ::= warning after @bignat + | abstract after @bignat + | @number_via + number_via ::= via @qualid mapping [ {+, @qualid => @qualid } ] This command allows the user to customize the way number literals are parsed and printed. @@ -1606,7 +1608,38 @@ Number notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. - :n:`( warning after @bignat )` + :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` + When using this option, :n:`@qualid__type` no + longer needs to be an inductive type and is instead mapped to the + inductive type :n:`@qualid__ind` according to the provided + list of pairs, whose first component :n:`@qualid__constant` is a + constant of type :n:`@qualid__type` + (or a function of type :n:`{* _ -> } @qualid__type`) and the second a + constructor of type :n:`@qualid__ind`. The type + :n:`@qualid__type` is then replaced by :n:`@qualid__ind` in the + above parser and printer types. + + .. note:: + To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation ` + as in the :ref:`example below `. + + .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid + + Duplicates are not allowed in the :n:`mapping` list. + + .. exn:: Missing mapping for constructor @qualid + + A mapping should be provided for :n:`@qualid` in the :n:`mapping` list. + + .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation. + + Two pairs in the :n:`mapping` list associate types that might be incompatible. + + .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation. + + A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor. + + :n:`warning after @bignat` displays a warning message about a possible stack overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`. @@ -1616,7 +1649,7 @@ Number notations with :n:`(warning after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. - :n:`( abstract after @bignat )` + :n:`abstract after @bignat` returns :n:`(@qualid__parse m)` when parsing a literal :n:`m` that's greater than :n:`@bignat` rather than reducing it to a normal form. Here :g:`m` will be a @@ -1642,6 +1675,12 @@ Number notations As noted above, the :n:`(abstract after @natural)` directive has no effect when :n:`@qualid__parse` lands in an :g:`option` type. + .. exn:: 'via' and 'abstract' cannot be used together. + + With the :n:`abstract after` option, the parser function + :n:`@qualid__parse` does not reduce large numbers to a normal form, + which prevents doing the translation given in the :n:`mapping` list. + .. exn:: Cannot interpret this number as a value of type @type The number notation registered for :token:`type` does not support @@ -1664,7 +1703,7 @@ Number notations .. exn:: Unexpected term @term while parsing a number notation. Parsing functions must always return ground terms, made up of - applications of constructors, inductive types, and primitive + function application, constructors, inductive type families, sorts and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. @@ -1675,6 +1714,67 @@ Number notations concrete number expressed as a (hexa)decimal. They may not return opaque constants. + .. exn:: Multiple 'via' options. + + At most one :g:`via` option can be given. + + .. exn:: Multiple 'warning after' or 'abstract after' options. + + At most one :g:`warning after` or :g:`abstract after` option can be given. + + .. _example-number-notation-non-inductive: + + .. example:: Number Notation for a non inductive type + + The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )` + as the number of units in the term. For instance :g:`sum unit (sum unit unit)` + is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. + The inductive :g:`I` will be used as :n:`@qualid__ind`. + + .. coqtop:: in + + Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. + + We then define :n:`@qualid__parse` and :n:`@qualid__print` + + .. coqtop:: in + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with + | O => Iempty | S O => Iunit + | S n => Isum Iunit (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with + | Iempty => O | Iunit => 1 + | Isum i1 i2 => f i1 + f i2 end in + Nat.to_num_uint (f x). + + Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. + + the number notation itself + + .. coqtop:: in + + Notation nSet := Set (only parsing). + Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope. + + and check the printer + + .. coqtop:: all + + Local Open Scope type_scope. + Check sum unit (sum unit unit). + + and the parser + + .. coqtop:: all + + Set Printing All. + Check 3. + .. _string-notations: String notations @@ -1746,7 +1846,7 @@ The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. String and number notations can only be declared for inductive types with no - arguments. + arguments. Declare numeral notations for non-inductive types using :n:`@number_via`. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4d615a130a..e43583de09 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier -| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident +| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name +| REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -number_modifier: [ -| OPTINREF -] - binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 @@ -2464,6 +2460,8 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_mapping +| number_options ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 8a0feb0e2f..17fc220f6c 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Number" "Notation" reference reference reference OPT number_options ":" ident +| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,18 +2549,28 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| reference reference +number_mapping: [ +| reference "=>" reference ] number_via: [ -| "via" reference "using" "(" LIST1 number_using SEP "," ")" +| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +] + +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via +] + +number_options: [ +| "(" LIST1 number_modifier SEP "," ")" ] tac2pat1: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d12b3bf6cd..3d1041e592 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,6 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +908,8 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier +| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name +| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1270,17 +1269,20 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ +| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| qualid qualid +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via ] number_via: [ -| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" ] hints_path: [ -- cgit v1.2.3 From edea770457aea05a7e6a64c1217f66dfc6930419 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:20:00 +0200 Subject: [numeral notation] Specify R --- doc/stdlib/index-list.html.template | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e42066d2ce..b08d7e9d2c 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -238,6 +238,7 @@ through the Require Import command.

theories/Numbers/DecimalN.v theories/Numbers/DecimalZ.v theories/Numbers/DecimalQ.v + theories/Numbers/DecimalR.v theories/Numbers/DecimalString.v theories/Numbers/HexadecimalFacts.v theories/Numbers/HexadecimalNat.v @@ -245,6 +246,7 @@ through the Require Import command.

theories/Numbers/HexadecimalN.v theories/Numbers/HexadecimalZ.v theories/Numbers/HexadecimalQ.v + theories/Numbers/HexadecimalR.v theories/Numbers/HexadecimalString.v -- cgit v1.2.3 From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:23:00 +0200 Subject: [numeral notation] Handle implicit arguments --- doc/sphinx/user-extensions/syntax-extensions.rst | 74 +++++++++++++++++++++++- doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 2 +- 3 files changed, 75 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index f07eb02946..4c6d300b13 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1562,7 +1562,7 @@ Number notations number_modifier ::= warning after @bignat | abstract after @bignat | @number_via - number_via ::= via @qualid mapping [ {+, @qualid => @qualid } ] + number_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ] This command allows the user to customize the way number literals are parsed and printed. @@ -1619,6 +1619,26 @@ Number notations :n:`@qualid__type` is then replaced by :n:`@qualid__ind` in the above parser and printer types. + When :n:`@qualid__constant` is surrounded by square brackets, + all the implicit arguments of :n:`@qualid__constant` (whether maximally inserted or not) are ignored + when translating to :n:`@qualid__constructor` (i.e., before + applying :n:`@qualid__print`) and replaced with implicit + argument holes :g:`_` when translating from + :n:`@qualid__constructor` to :n:`@qualid__constant` (after + :n:`@qualid__parse`). See below for an :ref:`example `. + + .. note:: + The implicit status of the arguments is considered + only at notation declaration time, any further + modification of this status has no impact + on the previously declared notations. + + .. note:: + In case of multiple implicit options (for instance + :g:`Arguments eq_refl {A}%type_scope {x}, [_] _`), an + argument is considered implicit when it is implicit in any of the + options. + .. note:: To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation ` as in the :ref:`example below `. @@ -1775,6 +1795,58 @@ Number notations Set Printing All. Check 3. + .. _example-number-notation-implicit-args: + + .. example:: Number Notation with implicit arguments + + The following example parses and prints natural numbers between + :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. + + .. coqtop:: all reset + + Require Import Vector. + Print Fin.t. + + Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`, + which won't appear in the corresponding inductive type. + + .. coqtop:: in + + Inductive I := I1 : I | IS : I -> I. + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with O => I1 | S n => IS (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with I1 => O | IS n => S (f n) end in + Nat.to_num_uint (f x). + + Declare Scope fin_scope. + Delimit Scope fin_scope with fin. + Local Open Scope fin_scope. + Number Notation Fin.t of_uint to_uint (via I + mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope. + + Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is + :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`. + + .. coqtop:: all + + Check 2. + + which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`) + + .. coqtop:: all + + Check 2 : Fin.t 3. + + but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`) + + .. coqtop:: all fail + + Check 2 : Fin.t 2. + .. _string-notations: String notations diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 17fc220f6c..3a0c3a8bc7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2557,6 +2557,7 @@ deprecated_number_modifier: [ number_mapping: [ | reference "=>" reference +| "[" reference "]" "=>" reference ] number_via: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3d1041e592..13d8979208 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1282,7 +1282,7 @@ number_modifier: [ ] number_via: [ -| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] hints_path: [ -- cgit v1.2.3 From e728a1ef0f8b5fdc4b1815a7d0349c67db15f9b4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:25:00 +0200 Subject: [numeral notation] Add support for parameterized inductives --- doc/sphinx/user-extensions/syntax-extensions.rst | 28 ++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c6d300b13..60fbd68687 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1608,6 +1608,12 @@ Number notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. + .. note:: + Number notations for parameterized inductive types can be + added by declaring an :ref:`abbreviation ` + for the inductive which instantiates all parameters. See + example below. + :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` When using this option, :n:`@qualid__type` no longer needs to be an inductive type and is instead mapped to the @@ -1847,6 +1853,24 @@ Number notations Check 2 : Fin.t 2. + .. example:: Number Notation with a parameterized inductive type + + .. coqtop:: in reset + + Definition of_uint u : list unit := + let fix f n := match n with O => nil | S n => cons tt (f n) end in + f (Nat.of_num_uint u). + Definition to_uint (l : list unit) := Nat.to_num_uint (length l). + + The parameter :g:`unit` for the parameterized inductive type + :g:`list` is given through an :ref:`abbreviation + `. + + .. coqtop:: in + + Notation list_unit := (list unit) (only parsing). + Number Notation list_unit of_uint to_uint : nat_scope. + .. _string-notations: String notations @@ -1917,8 +1941,8 @@ The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. - String and number notations can only be declared for inductive types with no - arguments. Declare numeral notations for non-inductive types using :n:`@number_via`. + String and number notations can only be declared for inductive types. + Declare number notations for non-inductive types using :n:`@number_via`. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. -- cgit v1.2.3 From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:26:00 +0200 Subject: Merge numeral and string notation plugins --- doc/tools/docgram/doc_grammar.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index b7f1e18d2b..92bcd51528 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) "plugins/ltac/g_eqdecide.mlg"; "plugins/ltac/g_tactic.mlg"; "plugins/ltac/g_ltac.mlg"; - "plugins/syntax/g_string.mlg"; "plugins/btauto/g_btauto.mlg"; "plugins/rtauto/g_rtauto.mlg"; "plugins/cc/g_congruence.mlg"; "plugins/firstorder/g_ground.mlg"; - "plugins/syntax/g_numeral.mlg"; + "plugins/syntax/g_number_string.mlg"; ] -- cgit v1.2.3 From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- doc/sphinx/user-extensions/syntax-extensions.rst | 349 ++++++++++++----------- doc/tools/docgram/common.edit_mlg | 7 +- doc/tools/docgram/fullGrammar | 14 +- doc/tools/docgram/orderedGrammar | 6 +- 4 files changed, 193 insertions(+), 183 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 60fbd68687..a52d7f08f0 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1386,7 +1386,7 @@ Scopes` or :cmd:`Print Scope`. ``char_scope`` This scope includes interpretation for all strings of the form ``"c"`` where :g:`c` is an ASCII character, or of the form ``"nnn"`` where nnn is - a three-digits number (possibly with leading 0's), or of the form + a three-digit number (possibly with leading 0s), or of the form ``""""``. Their respective denotations are the ASCII code of :g:`c`, the decimal ASCII code ``nnn``, or the ascii code of the character ``"`` (i.e. the ASCII code 34), all of them being represented in the type :g:`ascii`. @@ -1556,13 +1556,13 @@ Number notations .. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name :name: Number Notation - .. insertprodn number_modifier number_via + .. insertprodn number_modifier number_string_via .. prodn:: number_modifier ::= warning after @bignat | abstract after @bignat - | @number_via - number_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ] + | @number_string_via + number_string_via ::= via @qualid mapping [ {+, {| @qualid => @qualid | [ @qualid ] => @qualid } } ] This command allows the user to customize the way number literals are parsed and printed. @@ -1608,11 +1608,7 @@ Number notations function application, constructors, inductive type families, sorts, and primitive integers) will be considered for printing. - .. note:: - Number notations for parameterized inductive types can be - added by declaring an :ref:`abbreviation ` - for the inductive which instantiates all parameters. See - example below. + .. _number-string-via: :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` When using this option, :n:`@qualid__type` no @@ -1649,22 +1645,6 @@ Number notations To use a :token:`sort` as the target type :n:`@qualid__type`, use an :ref:`abbreviation ` as in the :ref:`example below `. - .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid - - Duplicates are not allowed in the :n:`mapping` list. - - .. exn:: Missing mapping for constructor @qualid - - A mapping should be provided for :n:`@qualid` in the :n:`mapping` list. - - .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation. - - Two pairs in the :n:`mapping` list associate types that might be incompatible. - - .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation. - - A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor. - :n:`warning after @bignat` displays a warning message about a possible stack overflow when calling :n:`@qualid__parse` to parse a literal larger than :n:`@bignat`. @@ -1748,166 +1728,47 @@ Number notations At most one :g:`warning after` or :g:`abstract after` option can be given. - .. _example-number-notation-non-inductive: - - .. example:: Number Notation for a non inductive type - - The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )` - as the number of units in the term. For instance :g:`sum unit (sum unit unit)` - is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. - The inductive :g:`I` will be used as :n:`@qualid__ind`. - - .. coqtop:: in - - Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. - - We then define :n:`@qualid__parse` and :n:`@qualid__print` - - .. coqtop:: in - - Definition of_uint (x : Number.uint) : I := - let fix f n := match n with - | O => Iempty | S O => Iunit - | S n => Isum Iunit (f n) end in - f (Nat.of_num_uint x). - - Definition to_uint (x : I) : Number.uint := - let fix f i := match i with - | Iempty => O | Iunit => 1 - | Isum i1 i2 => f i1 + f i2 end in - Nat.to_num_uint (f x). - - Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. - - the number notation itself - - .. coqtop:: in - - Notation nSet := Set (only parsing). - Number Notation nSet of_uint to_uint (via I - mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope. - - and check the printer - - .. coqtop:: all - - Local Open Scope type_scope. - Check sum unit (sum unit unit). - - and the parser - - .. coqtop:: all - - Set Printing All. - Check 3. - - .. _example-number-notation-implicit-args: - - .. example:: Number Notation with implicit arguments - - The following example parses and prints natural numbers between - :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. - - .. coqtop:: all reset - - Require Import Vector. - Print Fin.t. - - Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`, - which won't appear in the corresponding inductive type. - - .. coqtop:: in - - Inductive I := I1 : I | IS : I -> I. - - Definition of_uint (x : Number.uint) : I := - let fix f n := match n with O => I1 | S n => IS (f n) end in - f (Nat.of_num_uint x). - - Definition to_uint (x : I) : Number.uint := - let fix f i := match i with I1 => O | IS n => S (f n) end in - Nat.to_num_uint (f x). - - Declare Scope fin_scope. - Delimit Scope fin_scope with fin. - Local Open Scope fin_scope. - Number Notation Fin.t of_uint to_uint (via I - mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope. - - Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is - :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`. - - .. coqtop:: all - - Check 2. - - which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`) - - .. coqtop:: all - - Check 2 : Fin.t 3. - - but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`) - - .. coqtop:: all fail - - Check 2 : Fin.t 2. - - .. example:: Number Notation with a parameterized inductive type - - .. coqtop:: in reset - - Definition of_uint u : list unit := - let fix f n := match n with O => nil | S n => cons tt (f n) end in - f (Nat.of_num_uint u). - Definition to_uint (l : list unit) := Nat.to_num_uint (length l). - - The parameter :g:`unit` for the parameterized inductive type - :g:`list` is given through an :ref:`abbreviation - `. - - .. coqtop:: in - - Notation list_unit := (list unit) (only parsing). - Number Notation list_unit of_uint to_uint : nat_scope. - .. _string-notations: String notations ~~~~~~~~~~~~~~~~ -.. cmd:: String Notation @qualid @qualid__parse @qualid__print : @scope_name +.. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name :name: String Notation Allows the user to customize how strings are parsed and printed. - The token :n:`@qualid` should be the name of an inductive type, - while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the - parsing and printing functions, respectively. The parsing function - :n:`@qualid__parse` should have one of the following types: + :n:`@qualid__type` + the name of an inductive type, + while :n:`@qualid__parse` and :n:`@qualid__print` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@qualid__parse` should have one of the following types: - * :n:`Byte.byte -> @qualid` - * :n:`Byte.byte -> option @qualid` - * :n:`list Byte.byte -> @qualid` - * :n:`list Byte.byte -> option @qualid` + * :n:`Byte.byte -> @qualid__type` + * :n:`Byte.byte -> option @qualid__type` + * :n:`list Byte.byte -> @qualid__type` + * :n:`list Byte.byte -> option @qualid__type` - The printing function :n:`@qualid__print` should have one of the - following types: + The printing function :n:`@qualid__print` should have one of the + following types: - * :n:`@qualid -> Byte.byte` - * :n:`@qualid -> option Byte.byte` - * :n:`@qualid -> list Byte.byte` - * :n:`@qualid -> option (list Byte.byte)` + * :n:`@qualid__type -> Byte.byte` + * :n:`@qualid__type -> option Byte.byte` + * :n:`@qualid__type -> list Byte.byte` + * :n:`@qualid__type -> option (list Byte.byte)` - When parsing, the application of the parsing function - :n:`@qualid__parse` to the string will be fully reduced, and universes - of the resulting term will be refreshed. + When parsing, the application of the parsing function + :n:`@qualid__parse` to the string will be fully reduced, and universes + of the resulting term will be refreshed. + + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. - Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` + works as for :ref:`number notations above `. - .. exn:: Cannot interpret this string as a value of type @type + .. exn:: Cannot interpret this string as a value of type @type The string notation registered for :token:`type` does not support the given string. This error is given when the interpretation @@ -1926,7 +1787,7 @@ String notations .. exn:: Unexpected term @term while parsing a string notation. Parsing functions must always return ground terms, made up of - applications of constructors, inductive types, and primitive + function application, constructors, inductive type families, sorts and primitive integers. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. @@ -1937,12 +1798,33 @@ String notations concrete string expressed as a decimal. They may not return opaque constants. +.. note:: + Number or string notations for parameterized inductive types can be + added by declaring an :ref:`abbreviation ` for the + inductive which instantiates all parameters. See :ref:`example below `. + The following errors apply to both string and number notations: .. exn:: @type is not an inductive type. String and number notations can only be declared for inductive types. - Declare number notations for non-inductive types using :n:`@number_via`. + Declare string or numeral notations for non-inductive types using :n:`@number_string_via`. + + .. exn:: @qualid was already mapped to @qualid and cannot be remapped to @qualid + + Duplicates are not allowed in the :n:`mapping` list. + + .. exn:: Missing mapping for constructor @qualid + + A mapping should be provided for :n:`@qualid` in the :n:`mapping` list. + + .. warn:: @type was already mapped to @type, mapping it also to @type might yield ill typed terms when using the notation. + + Two pairs in the :n:`mapping` list associate types that might be incompatible. + + .. warn:: Type of @qualid seems incompatible with the type of @qualid. Expected type is: @type instead of @type. This might yield ill typed terms when using the notation. + + A mapping given in the :n:`mapping` list associates a constant with a seemingly incompatible constructor. .. exn:: Cannot interpret in @scope_name because @qualid could not be found in the current environment. @@ -1975,6 +1857,129 @@ The following errors apply to both string and number notations: .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703 +.. _example-number-notation-non-inductive: + +.. example:: Number Notation for a non inductive type + + The following example encodes the terms in the form :g:`sum unit ( ... (sum unit unit) ... )` + as the number of units in the term. For instance :g:`sum unit (sum unit unit)` + is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. + The inductive :g:`I` will be used as :n:`@qualid__ind`. + + .. coqtop:: in + + Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. + + We then define :n:`@qualid__parse` and :n:`@qualid__print` + + .. coqtop:: in + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with + | O => Iempty | S O => Iunit + | S n => Isum Iunit (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with + | Iempty => O | Iunit => 1 + | Isum i1 i2 => f i1 + f i2 end in + Nat.to_num_uint (f x). + + Inductive sum (A : Set) (B : Set) : Set := pair : A -> B -> sum A B. + + the number notation itself + + .. coqtop:: in + + Notation nSet := Set (only parsing). + Number Notation nSet of_uint to_uint (via I + mapping [Empty_set => Iempty, unit => Iunit, sum => Isum]) : type_scope. + + and check the printer + + .. coqtop:: all + + Local Open Scope type_scope. + Check sum unit (sum unit unit). + + and the parser + + .. coqtop:: all + + Set Printing All. + Check 3. + +.. _example-number-notation-implicit-args: + +.. example:: Number Notation with implicit arguments + + The following example parses and prints natural numbers between + :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. + + .. coqtop:: all reset + + Require Import Vector. + Print Fin.t. + + Note the implicit arguments of :g:`Fin.F1` and :g:`Fin.FS`, + which won't appear in the corresponding inductive type. + + .. coqtop:: in + + Inductive I := I1 : I | IS : I -> I. + + Definition of_uint (x : Number.uint) : I := + let fix f n := match n with O => I1 | S n => IS (f n) end in + f (Nat.of_num_uint x). + + Definition to_uint (x : I) : Number.uint := + let fix f i := match i with I1 => O | IS n => S (f n) end in + Nat.to_num_uint (f x). + + Declare Scope fin_scope. + Delimit Scope fin_scope with fin. + Local Open Scope fin_scope. + Number Notation Fin.t of_uint to_uint (via I + mapping [[Fin.F1] => I1, [Fin.FS] => IS]) : fin_scope. + + Now :g:`2` is parsed as :g:`Fin.FS (Fin.FS Fin.F1)`, that is + :g:`@Fin.FS _ (@Fin.FS _ (@Fin.F1 _))`. + + .. coqtop:: all + + Check 2. + + which can be of type :g:`Fin.t 3` (numbers :g:`0`, :g:`1` and :g:`2`) + + .. coqtop:: all + + Check 2 : Fin.t 3. + + but cannot be of type :g:`Fin.t 2` (only :g:`0` and :g:`1`) + + .. coqtop:: all fail + + Check 2 : Fin.t 2. + +.. _example-string-notation-parameterized-inductive: + +.. example:: String Notation with a parameterized inductive type + + The parameter :g:`Byte.byte` for the parameterized inductive type + :g:`list` is given through an :ref:`abbreviation `. + + .. coqtop:: in reset + + Notation string := (list Byte.byte) (only parsing). + Definition id_string := @id string. + + String Notation string id_string id_string : list_scope. + + .. coqtop:: all + + Check "abc"%list. + .. _TacticNotation: Tactic Notations diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index e43583de09..5de1f09c53 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1289,8 +1289,8 @@ command: [ | WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name | REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier -| REPLACE "String" "Notation" reference reference reference ":" ident -| WITH "String" "Notation" reference reference reference ":" scope_name +| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident +| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) | DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) @@ -2460,8 +2460,9 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) -| number_mapping +| number_string_mapping | number_options +| string_option ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3a0c3a8bc7..826a0b6f36 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -688,7 +688,7 @@ command: [ | "Print" "Fields" (* ring plugin *) | "Number" "Notation" reference reference reference OPT number_options ":" ident | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier -| "String" "Notation" reference reference reference ":" ident +| "String" "Notation" reference reference reference OPT string_option ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) @@ -2555,25 +2555,29 @@ deprecated_number_modifier: [ | "(" "abstract" "after" bignat ")" ] -number_mapping: [ +number_string_mapping: [ | reference "=>" reference | "[" reference "]" "=>" reference ] -number_via: [ -| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +number_string_via: [ +| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]" ] number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] number_options: [ | "(" LIST1 number_modifier SEP "," ")" ] +string_option: [ +| "(" number_string_via ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 13d8979208..151438bbbd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -910,7 +910,7 @@ command: [ | "Declare" "Right" "Step" one_term | "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name | "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier -| "String" "Notation" qualid qualid qualid ":" scope_name +| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] @@ -1278,10 +1278,10 @@ deprecated_number_modifier: [ number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] -number_via: [ +number_string_via: [ | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] -- cgit v1.2.3 From e3593abd322acb59c512b5f2f776091546b38887 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 30 Sep 2020 13:13:25 +0200 Subject: [refman] Add an example for number notations As suggested by Jim Fehrle while reviewing #12218 --- doc/sphinx/user-extensions/syntax-extensions.rst | 71 +++++++++++++++++++++++- 1 file changed, 70 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a52d7f08f0..2af40792df 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1857,6 +1857,75 @@ The following errors apply to both string and number notations: .. todo note on "single qualified identifiers" https://github.com/coq/coq/pull/11718#discussion_r415076703 +.. example:: Number Notation for radix 3 + + The following example parses and prints natural numbers + whose digits are :g:`0`, :g:`1` or :g:`2` as terms of the following + inductive type encoding radix 3 numbers. + + .. coqtop:: in reset + + Inductive radix3 : Set := + | x0 : radix3 + | x3 : radix3 -> radix3 + | x3p1 : radix3 -> radix3 + | x3p2 : radix3 -> radix3. + + We first define a parsing function + + .. coqtop:: in + + Definition of_uint_dec (u : Decimal.uint) : option radix3 := + let fix f u := match u with + | Decimal.Nil => Some x0 + | Decimal.D0 u => match f u with Some u => Some (x3 u) | None => None end + | Decimal.D1 u => match f u with Some u => Some (x3p1 u) | None => None end + | Decimal.D2 u => match f u with Some u => Some (x3p2 u) | None => None end + | _ => None end in + f (Decimal.rev u). + Definition of_uint (u : Number.uint) : option radix3 := + match u with Number.UIntDec u => of_uint_dec u | Number.UIntHex _ => None end. + + and a printing function + + .. coqtop:: in + + Definition to_uint_dec (x : radix3) : Decimal.uint := + let fix f x := match x with + | x0 => Decimal.Nil + | x3 x => Decimal.D0 (f x) + | x3p1 x => Decimal.D1 (f x) + | x3p2 x => Decimal.D2 (f x) end in + Decimal.rev (f x). + Definition to_uint (x : radix3) : Number.uint := Number.UIntDec (to_uint_dec x). + + before declaring the notation + + .. coqtop:: in + + Declare Scope radix3_scope. + Open Scope radix3_scope. + Number Notation radix3 of_uint to_uint : radix3_scope. + + We can check the printer + + .. coqtop:: all + + Check x3p2 (x3p1 x0). + + and the parser + + .. coqtop:: all + + Set Printing All. + Check 120. + + Digits other than :g:`0`, :g:`1` and :g:`2` are rejected. + + .. coqtop:: all fail + + Check 3. + .. _example-number-notation-non-inductive: .. example:: Number Notation for a non inductive type @@ -1866,7 +1935,7 @@ The following errors apply to both string and number notations: is encoded as :g:`3` while :g:`unit` is :g:`1` and :g:`0` stands for :g:`Empty_set`. The inductive :g:`I` will be used as :n:`@qualid__ind`. - .. coqtop:: in + .. coqtop:: in reset Inductive I := Iempty : I | Iunit : I | Isum : I -> I -> I. -- cgit v1.2.3 From 36ac26532028bfc6f84e4dfc849b51f42a3d8286 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 28 Oct 2020 10:32:58 +0100 Subject: Rename Dec and HexDec to Decimal and Hexadecimal As noted by Hugo Herbelin, Dec is rather used for "decidable". --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2af40792df..9d1fcc160d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1884,7 +1884,7 @@ The following errors apply to both string and number notations: | _ => None end in f (Decimal.rev u). Definition of_uint (u : Number.uint) : option radix3 := - match u with Number.UIntDec u => of_uint_dec u | Number.UIntHex _ => None end. + match u with Number.UIntDecimal u => of_uint_dec u | Number.UIntHexadecimal _ => None end. and a printing function @@ -1897,7 +1897,7 @@ The following errors apply to both string and number notations: | x3p1 x => Decimal.D1 (f x) | x3p2 x => Decimal.D2 (f x) end in Decimal.rev (f x). - Definition to_uint (x : radix3) : Number.uint := Number.UIntDec (to_uint_dec x). + Definition to_uint (x : radix3) : Number.uint := Number.UIntDecimal (to_uint_dec x). before declaring the notation -- cgit v1.2.3 From 94132f40eb81ed3249c4d5f32f6d7aa356d38847 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 08:54:17 +0200 Subject: Add changelog --- .../12218-numeral-notations-non-inductive.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst new file mode 100644 index 0000000000..5ea37e7494 --- /dev/null +++ b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst @@ -0,0 +1,19 @@ +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. +- **Added:** + :ref:`Number Notation ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#12035 `_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). -- cgit v1.2.3