From ec24b26be7795af27256d39431e1c4e3d42fe3b7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:16:00 +0200
Subject: [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).
---
 test-suite/output/QArithSyntax.v | 34 +++++++++++++++++++++++++++++-----
 1 file changed, 29 insertions(+), 5 deletions(-)

(limited to 'test-suite/output/QArithSyntax.v')

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.
-- 
cgit v1.2.3