| Age | Commit message (Collapse) | Author |
|---|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?
This is unfortunately a rather large commit. I suggest reading it in
the following order:
* test-suite/output/ZSyntax.{v,out} new test
* test-suite/output/Int63Syntax.{v,out} ''
* test-suite/output/QArithSyntax.{v,out} ''
* test-suite/output/RealSyntax.{v,out} ''
* test-suite/output/FloatSyntax.{v,out} ''
* interp/numTok.ml{i,} extending numeral tokens
* theories/Init/Hexadecimal.v adaptation of Decimal.v
for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v new interface for Numeral Notation (basically,
a numeral is either a decimal or an hexadecimal)
* theories/Init/Nat.v add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v '' positive
* theories/ZArith/BinIntDef.v '' Z
* theories/NArith/BinNatDef.v '' N
* theories/QArith/QArith_base.v '' Q
* interp/notation.ml{i,} adapting implementation of numeral notations
* plugins/syntax/numeral.ml ''
* plugins/syntax/r_syntax.ml adapt parser for real numbers
* plugins/syntax/float_syntax.ml adapt parser for primitive floats
* theories/Init/Prelude.v register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
had to be permuted)
|
|
"decimal" would no longer be an appropriate name when extending to
hexadecimal for instance.
|
|
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Add headers to a few files which were missing them.
|
|
|
