|
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)
|
