[numeral notation] Q

Previously rationals were all parsed as a pair numerator, denominator.
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 still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).

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

A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).

2 files changed, 97 insertions, 27 deletions

diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index 9b5c076cb4..ced52524f2 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -1,26 +1,72 @@
 eq_refl : 1.02 = 1.02
      : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 1020 = 1020
-     : 1020 = 1020
-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
+1.02e1
+     : Q
+10.2
+     : Q
+1.02e3
+     : Q
+1020
+     : Q
+1.02e2
+     : Q
+102
+     : Q
+eq_refl : 10.2e-1 = 1.02
+     : 10.2e-1 = 1.02
+eq_refl : -0.0001 = -0.0001
+     : -0.0001 = -0.0001
 eq_refl : -0.50 = -0.50
      : -0.50 = -0.50
-eq_refl : -26 = -26
-     : -26 = -26
-eq_refl : 2860 # 256 = 2860 # 256
-     : 2860 # 256 = 2860 # 256
-eq_refl : -6882 = -6882
-     : -6882 = -6882
-eq_refl : 2860 # 64 = 2860 # 64
-     : 2860 # 64 = 2860 # 64
-eq_refl : 2860 = 2860
-     : 2860 = 2860
-eq_refl : -2860 # 1024 = -2860 # 1024
-     : -2860 # 1024 = -2860 # 1024
+0
+     : Q
+0
+     : Q
+42
+     : Q
+42
+     : Q
+1.23
+     : Q
+0x1.23%xQ
+     : Q
+0.0012
+     : Q
+42e3
+     : Q
+42e-3
+     : Q
+eq_refl : -0x1a = -0x1a
+     : -0x1a = -0x1a
+eq_refl : 0xb.2c = 0xb.2c
+     : 0xb.2c = 0xb.2c
+eq_refl : -0x1ae2 = -0x1ae2
+     : -0x1ae2 = -0x1ae2
+0xb.2cp2
+     : Q
+2860 # 64
+     : Q
+0xb.2cp8
+     : Q
+0xb2c
+     : Q
+eq_refl : -0xb.2cp-2 = -2860 # 1024
+     : -0xb.2cp-2 = -2860 # 1024
+0x0
+     : Q
+0x0
+     : Q
+0x2a
+     : Q
+0x2a
+     : Q
+1.23%Q
+     : Q
+0x1.23
+     : Q
+0x0.0012
+     : Q
+0x2ap3
+     : Q
+0x2ap-3
+     : Q
diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v
index b5c6222bba..e979abca66 100644
--- a/test-suite/output/QArithSyntax.v
+++ b/test-suite/output/QArithSyntax.v
@@ -1,15 +1,39 @@
 Require Import QArith.
 Open Scope Q_scope.
 Check (eq_refl : 1.02 = 102 # 100).
-Check (eq_refl : 1.02e1 = 102 # 10).
-Check (eq_refl : 1.02e+03 = 1020).
-Check (eq_refl : 1.02e+02 = 102 # 1).
+Check 1.02e1.
+Check 102 # 10.
+Check 1.02e+03.
+Check 1020.
+Check 1.02e+02.
+Check 102 # 1.
 Check (eq_refl : 10.2e-1 = 1.02).
 Check (eq_refl : -0.0001 = -1 # 10000).
 Check (eq_refl : -0.50 = - 50 # 100).
+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_Q_scope.
 Check (eq_refl : -0x1a = - 26 # 1).
 Check (eq_refl : 0xb.2c = 2860 # 256).
 Check (eq_refl : -0x1ae2 = -6882).
-Check (eq_refl : 0xb.2cp2 = 2860 # 64).
-Check (eq_refl : 0xb.2cp8 = 2860).
+Check 0xb.2cp2.
+Check 2860 # 64.
+Check 0xb.2cp8.
+Check 2860.
 Check (eq_refl : -0xb.2cp-2 = -2860 # 1024).
+Check 0x0.
+Check 0x00.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0x0.0012.
+Check 0x2ap3.
+Check 0x2ap-3.