diff options
| author | Pierre Roux | 2020-03-26 08:20:09 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-05-09 17:59:00 +0200 |
| commit | 692c642672f863546b423d72c714c1417164e506 (patch) | |
| tree | 56ac54d810735fefb5fa7d91b2b5392f1f432578 /plugins/syntax/float_syntax.ml | |
| parent | deb2607027c158d313b82846c67594067194c8b7 (diff) | |
Add hexadecimal numerals
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)
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
| -rw-r--r-- | plugins/syntax/float_syntax.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 0a5825dfc1..9861a060ab 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -70,7 +70,8 @@ let interp_float ?loc n = else (* e < 0 *) if e' <= e then check m' (-e) m (e - e') else check' m' (-e) (e' - e) m in - if inexact () then warn_inexact_float ?loc (sn, f); + if NumTok.(Signed.classify n = CDec) && inexact () then + warn_inexact_float ?loc (sn, f); DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) |