From 24ccc118ccfb4c1223cd37bd43c9d26a77851176 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 15 Mar 2017 03:11:23 +0100 Subject: Numeral Notation for nat This parsing/printing method for nat should be just as fast as the previous dedicated code. Moreover, we could now parse large literals as nat numbers, by leaving them in a half-abstract form such as (Nat.of_uint 123456). This form is convertible to the closed (S (S (S ...))) form, so it shouldn't be a big deal for compatibility, except for if some Ltac stuff relies on (S ...) to be present after parsing. Of course, forcing the computation of a (Nat.of_uint ....) may take a while or raise a Stack Overflow. --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f448248468..0fa42cadad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -226,6 +226,7 @@ through the Require Import command.

theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v -- cgit v1.2.3 From 1e49dad4c4ea721a0844d9553e84aed90777f46d Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Mar 2017 18:56:18 +0100 Subject: Numeral Notation: some documentation in the refman --- doc/sphinx/user-extensions/syntax-extensions.rst | 44 ++++++++++++++++++++++++ 1 file changed, 44 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5089a1b3e3..0293a92fbb 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1372,6 +1372,50 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + +Numeral notations +----------------- + +Starting with version 8.9, the following command allows to customize +the way numeral literals are parsed and printed: + +.. cmd:: Numeral Notation @ty @pa @pr : @scope. + +In the previous line, `ty` should be the name of an inductive type, +while `pa` and `pr` should be the names of two parsing and printing +functions. +The parsing function `pa` should have one of the following types: + + * :g:`Decimal.int -> ty` + * :g:`Decimal.int -> option ty` + * :g:`Decimal.uint -> ty` + * :g:`Decimal.uint -> option ty` + * :g:`Z -> ty` + * :g:`Z -> option ty` + +And the printing function `pr` should have one of the following types: + + * :g:`ty -> Decimal.int` + * :g:`ty -> option Decimal.int` + * :g:`ty -> Decimal.uint` + * :g:`ty -> option Decimal.uint` + * :g:`ty -> Z` + * :g:`ty -> option Z` + +.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). + +When a literal larger than `n` is parsed, a warning message about +possible stack overflow will be displayed. + +.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). + +When a literal `m` larger than `n` is parsed, the result will be +:g:`(pa m)`, without reduction of this application to a normal form. +Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, +depending on the type of the parsing function `pa`. This allows a more +compact representation of literals in types such as ``nat``, and +limits parse failures due to stack overflow. + .. _TacticNotation: Tactic Notations -- cgit v1.2.3 From e539db48ab064dc0c10c5ebeb043372c840497c2 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 9 Mar 2018 15:23:17 +0100 Subject: Numeral Notation: minor text improvements suggested by J. Gross --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0293a92fbb..e947fd891b 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,7 +1376,7 @@ Abbreviations Numeral notations ----------------- -Starting with version 8.9, the following command allows to customize +Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: .. cmd:: Numeral Notation @ty @pa @pr : @scope. -- cgit v1.2.3 From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 Jul 2018 06:25:22 -0400 Subject: Fix numeral notation for a rebase on top of master Some of this code is cargo-culted or kludged to work. As I understand it, the situation is as follows: There are two sorts of use-cases that need to be supported: 1. A plugin registers an OCaml function as a numeral interpreter. In this case, the function registration must be synchronized with the document state, but the functions should not be marshelled / stored in the .vo. 2. A vernacular registers a Gallina function as a numeral interpreter. In this case, the registration must be synchronized, and the function should be marshelled / stored in the .vo. In case (1), we can compare functions by pointer equality, and we should be able to rely on globally unique keys, even across backtracking. In case (2), we cannot compare functions by pointer equality (because they must be regenerated on unmarshelling when `Require`ing a .vo file), and we also cannot rely on any sort of unique key being both unique and persistent across files. The solution we use here is that we ask clients to provide "unique" keys, and that clients tell us whether or not to overwrite existing registered functions, i.e., to tell us whether or not we should expect interpreter functions to be globally unique under pointer equality. For plugins, a simple string suffices, as long as the string does not clash between different plugins. In the case of vernacular-registered functions, use marshell a description of all of the data used to generate the function, and use that string as a unique key which is expected to persist across files. Because we cannot rely on function-pointer uniqueness here, we tell the interpretation-registration to allow overwriting. ---- Some of this code is response to comments on the PR ---- Some code is to fix an issue that bignums revealed: Both Int31 and bignums registered numeral notations in int31_scope. We now prepend a globally unique identifier when registering numeral notations from OCaml plugins. This is permissible because we don't store the uid information for such notations in .vo files (assuming I'm understanding the code correctly). --- doc/sphinx/user-extensions/syntax-extensions.rst | 160 ++++++++++++++++++----- 1 file changed, 124 insertions(+), 36 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e947fd891b..ca588acf29 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1379,42 +1379,130 @@ Numeral notations Starting with version 8.9, the following command allows the user to customize the way numeral literals are parsed and printed: -.. cmd:: Numeral Notation @ty @pa @pr : @scope. - -In the previous line, `ty` should be the name of an inductive type, -while `pa` and `pr` should be the names of two parsing and printing -functions. -The parsing function `pa` should have one of the following types: - - * :g:`Decimal.int -> ty` - * :g:`Decimal.int -> option ty` - * :g:`Decimal.uint -> ty` - * :g:`Decimal.uint -> option ty` - * :g:`Z -> ty` - * :g:`Z -> option ty` - -And the printing function `pr` should have one of the following types: - - * :g:`ty -> Decimal.int` - * :g:`ty -> option Decimal.int` - * :g:`ty -> Decimal.uint` - * :g:`ty -> option Decimal.uint` - * :g:`ty -> Z` - * :g:`ty -> option Z` - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (warning after @n). - -When a literal larger than `n` is parsed, a warning message about -possible stack overflow will be displayed. - -.. cmdv:: Numeral Notation @ty @pa @pr : @scope (abstract after @n). - -When a literal `m` larger than `n` is parsed, the result will be -:g:`(pa m)`, without reduction of this application to a normal form. -Here `m` will be a ``Decimal.int`` or ``Decimal.uint`` or ``Z``, -depending on the type of the parsing function `pa`. This allows a more -compact representation of literals in types such as ``nat``, and -limits parse failures due to stack overflow. +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + In the previous line, :n:`@ident__1` should be the name of an + inductive type, while :n:`@ident__2` and :n:`@ident__3` should be + the names of the parsing and printing functions, respectively. The + parsing function :n:`@ident__2` should have one of the following + types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. 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 + warning will be emitted when an integer larger than :token:`num` + is parsed. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :g:`ty` does not support the + given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. + + Numeral notations do not currently support polymorphic inductive + types. Ensure that all types involved in numeral notations are + declared with :g:`Unset Universe Polymorphism`, or with the + :g:`Monomorphic` attribute. + + .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. + + Numeral notations do not currently support polymorphic functions + for printing and parsing. Ensure that both functions passed to + :cmd:`Numeral Notation` are defined with :g:`Unset Universe + Polymorphism`, or with the :g:`Monomorphic` attribute. + + .. exn:: Unexpected term while parsing a numeral notation + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term while parsing a numeral notation + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + .. _TacticNotation: -- cgit v1.2.3 From ebf453d4ae4e4f0312f3fd696da26c03671bc906 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 Jul 2018 13:06:03 -0400 Subject: Update doc and test-suite after supporting univ poly Also make `Check S` no longer anomaly Add a couple more test cases for numeral notations Also add another possibly-confusing error message to the doc. Respond to Hugo's doc request with Zimmi48's suggestion From https://github.com/coq/coq/pull/8064/files#r204191608 --- doc/sphinx/user-extensions/syntax-extensions.rst | 48 +++++++++++------------- 1 file changed, 22 insertions(+), 26 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ca588acf29..50425c8a5d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1376,16 +1376,15 @@ Abbreviations Numeral notations ----------------- -Starting with version 8.9, the following command allows the user to customize -the way numeral literals are parsed and printed: - .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. - In the previous line, :n:`@ident__1` should be the name of an - inductive type, while :n:`@ident__2` and :n:`@ident__3` should be - the names of the parsing and printing functions, respectively. The - parsing function :n:`@ident__2` should have one of the following - types: + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: * :n:`Decimal.int -> @ident__1` * :n:`Decimal.int -> option @ident__1` @@ -1404,6 +1403,10 @@ the way numeral literals are parsed and printed: * :n:`@ident__1 -> Z` * :n:`@ident__1 -> option Z` + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1420,12 +1423,13 @@ the way numeral literals are parsed and printed: more compact representation of literals in types such as :g:`nat`, and limits parse failures due to stack overflow. Note that a warning will be emitted when an integer larger than :token:`num` - is parsed. + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. .. exn:: Cannot interpret this number as a value of type @type - The numeral notation registered for :g:`ty` does not support the - given numeral. This error is given when the interpretation + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation function returns :g:`None`, or if the interpretation is registered for only non-negative integers, and the given numeral is negative. @@ -1434,7 +1438,7 @@ the way numeral literals are parsed and printed: The parsing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the the types Decimal.uint or Z could be used{? (require BinNums first)}. + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. @@ -1444,20 +1448,6 @@ the way numeral literals are parsed and printed: Numeral notations can only be declared for inductive types with no arguments. - .. exn:: The inductive type @type cannot be used in numeral notations because support for polymorphic inductive types is not yet implemented. - - Numeral notations do not currently support polymorphic inductive - types. Ensure that all types involved in numeral notations are - declared with :g:`Unset Universe Polymorphism`, or with the - :g:`Monomorphic` attribute. - - .. exn:: The function @ident cannot be used in numeral notations because support for polymorphic printing and parsing functions is not yet implemented. - - Numeral notations do not currently support polymorphic functions - for printing and parsing. Ensure that both functions passed to - :cmd:`Numeral Notation` are defined with :g:`Unset Universe - Polymorphism`, or with the :g:`Monomorphic` attribute. - .. exn:: Unexpected term while parsing a numeral notation Parsing functions must always return ground terms, made up of @@ -1482,6 +1472,12 @@ the way numeral literals are parsed and printed: Both functions passed to :cmd:`Numeral Notation` must be single identifiers. + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must be global + definitions, not notations, section variables, section-local + :g:`Let` bound identifiers, etc. + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). When a :cmd:`Numeral Notation` is registered in the current scope -- cgit v1.2.3 From 296ac045fdfe6d6ae4875d7a6c89cad0c64c2e97 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 11:25:19 -0400 Subject: Add a warning about abstract after being a no-op As per https://github.com/coq/coq/pull/8064#discussion_r209875616 I decided to make it a warning because it seems more flexible that way; users to are flipping back and forth between option types and not option types while designing won't have to update their `abstract after` directives to do so, and users who don't want to allow this can make it an actual error message. --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 50425c8a5d..2f7a7d42c1 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1499,6 +1499,10 @@ Numeral notations Check 90000. + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. .. _TacticNotation: -- cgit v1.2.3 From 581bbbb23fcb488d5c1a10f360a6705a6792b2b1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Aug 2018 20:19:07 -0400 Subject: Add periods in response to PR comments --- doc/sphinx/user-extensions/syntax-extensions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2f7a7d42c1..6f655340da 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1443,19 +1443,19 @@ Numeral notations The printing function given to the :cmd:`Numeral Notation` vernacular is not of the right type. - .. exn:: @type is not an inductive type + .. exn:: @type is not an inductive type. Numeral notations can only be declared for inductive types with no arguments. - .. exn:: Unexpected term while parsing a numeral notation + .. exn:: Unexpected term @term while parsing a numeral notation. Parsing functions must always return ground terms, made up of applications of constructors and inductive types. Parsing functions may not return terms containing axioms, bare (co)fixpoints, lambdas, etc. - .. exn:: Unexpected non-option term while parsing a numeral notation + .. exn:: Unexpected non-option term @term while parsing a numeral notation. Parsing functions expected to return an :g:`option` must always return a concrete :g:`Some` or :g:`None` when applied to a -- cgit v1.2.3 From 548976ac825298f27e6be00bbbb1be0752568f6f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 16 Aug 2018 10:35:11 -0400 Subject: [numeral notations] support aliases Aliases of global references can now be used in numeral notations --- doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++++-- 1 file changed, 6 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 6f655340da..886ca0472a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1474,9 +1474,13 @@ Numeral notations .. exn:: The reference @ident was not found in the current environment. + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + Identifiers passed to :cmd:`Numeral Notation` must be global - definitions, not notations, section variables, section-local - :g:`Let` bound identifiers, etc. + references, or notations which denote to single identifiers. .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). -- cgit v1.2.3 From 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Aug 2018 17:01:43 -0400 Subject: Give a proper error message on num-not in functor Numeral Notations are not well-supported inside functors. We now give a proper error message rather than an anomaly when this occurs. --- doc/sphinx/user-extensions/syntax-extensions.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 886ca0472a..b46382dbbf 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1462,6 +1462,18 @@ Numeral notations concrete numeral expressed as a decimal. They may not return opaque constants. + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). The type passed to :cmd:`Numeral Notation` must be a single -- cgit v1.2.3