Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01

4 files changed, 38 insertions, 9 deletions

diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 7266b662fa..9efb81a901 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -54,7 +54,7 @@ Qed.
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by
+ assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index b0ac9ea29f..4cd0ffb1dc 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -19,30 +19,31 @@ Nat.div2: nat -> nat
 Nat.log2: nat -> nat
 Nat.succ: nat -> nat
 Nat.sqrt: nat -> nat
+S: nat -> nat
 Nat.pred: nat -> nat
 Nat.double: nat -> nat
 Nat.square: nat -> nat
-S: nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.tail_add: nat -> nat -> nat
 Nat.land: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
 Nat.tail_mul: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
-Nat.mul: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-Nat.add: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.of_uint: Decimal.uint -> nat
+Decimal.nb_digits: Decimal.uint -> nat
 Nat.tail_addmul: nat -> nat -> nat -> nat
 Nat.of_uint_acc: Decimal.uint -> nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
 length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 Nat.div2: nat -> nat
diff --git a/test-suite/success/QArithSyntax.v b/test-suite/success/QArithSyntax.v
new file mode 100644
index 0000000000..2f2ee0134a
--- /dev/null
+++ b/test-suite/success/QArithSyntax.v
@@ -0,0 +1,9 @@
+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 (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = -1 # 10000).
+Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v
new file mode 100644
index 0000000000..2765200991
--- /dev/null
+++ b/test-suite/success/RealSyntax.v
@@ -0,0 +1,19 @@
+Require Import Reals.
+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 (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
+Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)).
+
+Goal 254e3 = 2540 * 10 ^ 2.
+ring.
+Qed.
+
+Require Import Psatz.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+lra.
+Qed.