From 692c642672f863546b423d72c714c1417164e506 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 26 Mar 2020 08:20:09 +0100
Subject: 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)
---
 test-suite/output/FloatSyntax.out | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'test-suite/output/FloatSyntax.out')

diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 7941d2e647..4a5a700879 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -42,13 +42,25 @@ closest value will be used and unambiguously printed
      : float
 2.5 + 2.5
      : float
-File "stdin", line 24, characters 6-11:
+-26
+     : float
+11.171875
+     : float
+-6882
+     : float
+44.6875
+     : float
+2860
+     : float
+-2.79296875
+     : float
+File "stdin", line 30, characters 6-11:
 Warning: The constant 1e309 is not a binary64 floating-point value. A closest
 value will be used and unambiguously printed infinity.
 [inexact-float,parsing]
 infinity
      : float
-File "stdin", line 25, characters 6-12:
+File "stdin", line 31, characters 6-12:
 Warning: The constant -1e309 is not a binary64 floating-point value. A
 closest value will be used and unambiguously printed neg_infinity.
 [inexact-float,parsing]
-- 
cgit v1.2.3