Numerals without int notation in prelude#2
Open
JasonGross wants to merge 26 commits intoletouzey:numeral-notation-2from
Open
Numerals without int notation in prelude#2JasonGross wants to merge 26 commits intoletouzey:numeral-notation-2from
JasonGross wants to merge 26 commits intoletouzey:numeral-notation-2from
Conversation
This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
This is a portion of roglo's PR#156 introducing a Numeral Notation command : we deal here with inductive types via conversion fonctions from/to Z written in Coq. For an example, see plugins/syntax/NatSyntaxViaZ.v This commit does not include the part about printing via some ltac. Using ltac was meant for dealing with real numbers, let's see first what become PR#415 about a compact representation for real literals.
This way, we could fully bypass bigint.ml.
The previous mechanism of parsing/printing Z is kept for now.
Currently, the conversion functions accepted by Numeral Notation foo
may have the following types.
for parsing:
int -> foo
int -> option foo
uint -> foo
uint -> option foo
Z -> foo
Z -> option foo
for printing:
foo -> int
foo -> option int
foo -> uint
foo -> option uint
foo -> Z
foo -> option Z
Notes:
- The Declare ML Module is directly done in Prelude
- When doing a Numeral Notation, having the Z datatype around
isn't mandatory anymore (but the error messages suggest that
it can still be used).
- An option (abstract after ...) allows to keep large numbers in
an abstract form such as (Nat.of_uint 123456) instead of reducing
to (S (S (S ...))) and ending immediately with Stack Overflow.
- After checking with Matthieu, there is now a explicit check
and an error message in case of polymorphic inductive types
Just because it's fun and easy. Not used by the Numeral Notation command.
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.
If it's in the prelude, it conflicts with ssr's int_scope. So we stuff it in Numbers.DecimalNotations.
Author
|
Indeed, all of the cis build, though the test-suite doesn't. |
- Bugs 4527, 4533, 4544 broke because we now need to import [Prelude], not just [Notations], to get nat syntax. I think this is an acceptable change, and it's incidental to the bugs being tracked, so I've updated the test-suite files to not rely on it.
This restores printing compatibility with v8.6.
There is more churn than there should be because SearchPattern uses a non-local sorting algorithm; the comparison function considers many constants equal in priority and leaves it up to the heap structure to break ties, which seems wrong. This has been reported as [bug rocq-prover#5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
In v8.6 and trunk, numerals are parsed up to integer equality (modulo the difference between `-0` and `0`). We restore this by stripping leading zeros from the string before comparison.
``` git grep --name-only 'should goes' | xargs sed s'/should goes/should go/g' -i ```
JasonGross
force-pushed
the
numerals-without-int-notation-in-prelude
branch
from
ab0b9af to
f658ac7
Compare
fiat-crypto was failing to build in time, and I suspect this was the bottleneck.
I'm not actually sure if it's needed here, but this is what gives unit-level compatibility with v8.6 / trunk.
Author
|
Bump. By the way, travis is completely happy with this: https://travis-ci.org/JasonGross/coq/builds/238632055 |
letouzey
force-pushed
the
numeral-notation-2
branch
2 times, most recently
from
45a90cd to
282d54d
Compare
letouzey
force-pushed
the
numeral-notation-2
branch
5 times, most recently
from
16e585c to
7e2c563
Compare
letouzey
force-pushed
the
numeral-notation-2
branch
from
70c23b4 to
a780f25
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I expect this will build on travis (though I haven't tested it all yet).