[numeral notation] R

Previously real constants were parsed by an unproved OCaml code. The
parser and printer are now implemented in Coq, which will enable a
proof and hopefully make it easier to maintain / make evolve.

Previously reals were all parsed as an integer, an integer multiplied
by a power of ten or an integer divided by a power of ten. This means
1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell
apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.

Now, decimal dot is parsed as a rational and exponents are parsed as a
product or division by a power of ten. For instance, 1.02 is parsed as
Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos
10 2).

1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R
(102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.

2 files changed, 111 insertions, 34 deletions

diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index a9386b2781..a7b7dabb20 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -4,34 +4,81 @@
      : R
 1.5%R
      : R
-15%R
-     : R
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 102e1 = 102e1
-     : 102e1 = 102e1
-eq_refl : 102 = 102
-     : 102 = 102
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : -1e-4 = -1e-4
-     : -1e-4 = -1e-4
-eq_refl : -0.50 = -0.50
-     : -0.50 = -0.50
+1.5e1%R
+     : R
+eq_refl : 1.02 = 102e-2
+     : 1.02 = 102e-2
+1.02e1
+     : R
+102e-1
+     : R
+1.02e3
+     : R
+102e1
+     : R
+1.02e2
+     : R
+102
+     : R
+10.2e-1
+     : R
+1.02
+     : R
+eq_refl : -0.0001 = -1e-4
+     : -0.0001 = -1e-4
+eq_refl : -0.50 = -50e-2
+     : -0.50 = -50e-2
 eq_refl : -26 = -26
      : -26 = -26
-eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
-     : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
+eq_refl : 0xb.2c%xR = 0xb2cp-8%xR
+     : 0xb.2c%xR = 0xb2cp-8%xR
 eq_refl : -6882 = -6882
      : -6882 = -6882
-eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
-     : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
-eq_refl : 2860 = 2860
-     : 2860 = 2860
-eq_refl
-:
--2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10)
-     : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) =
-       - (2860) / IZR (Z.pow_pos 2 10)
+0xb.2cp2%xR
+     : R
+0xb2cp-6%xR
+     : R
+0xb.2cp8%xR
+     : R
+2860
+     : R
+(-0xb.2cp-2)%xR
+     : R
+- 0xb2cp-10%xR
+     : R
+0
+     : R
+0
+     : R
+42
+     : R
+42
+     : R
+1.23
+     : R
+0x1.23%xR
+     : R
+0.0012
+     : R
+42e3
+     : R
+42e-3
+     : R
+0x0
+     : R
+0x0
+     : R
+0x2a
+     : R
+0x2a
+     : R
+1.23%R
+     : R
+0x1.23
+     : R
+0x0.0012
+     : R
+0x2ap3
+     : R
+0x2ap-3
+     : R
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 69ce3ef5f9..790d5c654f 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -8,18 +8,48 @@ Check 1_.5_e1_%R.
 Open Scope R_scope.
 
 Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
-Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+02 = IZR 102).
-Check (eq_refl : 10.2e-1 = 1.02).
+Check 1.02e1.
+Check IZR 102 / IZR (Z.pow_pos 10 1).
+Check 1.02e+03.
+Check IZR 102 * IZR (Z.pow_pos 10 1).
+Check 1.02e+02.
+Check IZR 102.
+Check 10.2e-1.
+Check 1.02.
 Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
 Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)).
 Check (eq_refl : -0x1a = - 26).
 Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)).
 Check (eq_refl : -0x1ae2 = -6882).
-Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)).
-Check (eq_refl : 0xb.2cp8 = 2860).
-Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)).
+Check 0xb.2cp2.
+Check IZR 2860 / IZR (Z.pow_pos 2 6).
+Check 0xb.2cp8.
+Check 2860.
+Check -0xb.2cp-2.
+Check - (IZR 2860 / IZR (Z.pow_pos 2 10)).
+Check 0.
+Check 000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0.0012.
+Check 42e3.
+Check 42e-3.
+
+Open Scope hex_R_scope.
+
+Check 0x0.
+Check 0x000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0x0.0012.
+Check 0x2ap3.
+Check 0x2ap-3.
+
+Close Scope hex_R_scope.
 
 Require Import Reals.