Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)

3 files changed, 38 insertions, 3 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/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/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 139c4bf432..790bdf9ed6 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -29,12 +29,38 @@ Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.
 
 Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 
+Definition of_decimal (d:Decimal.decimal) : Q :=
+  let '(i, f, e) :=
+    match d with
+    | Decimal.Decimal i f => (i, f, Decimal.Pos Decimal.Nil)
+    | Decimal.DecimalExp i f e => (i, f, e)
+    end in
+  let num := Z.of_int (Decimal.app_int i f) in
+  let e := Z.sub (Z.of_int e) (Z.of_nat (Decimal.nb_digits f)) in
+  match e with
+  | Z0 => Qmake num 1
+  | Zpos e => Qmake (Pos.iter (Z.mul 10) num e) 1
+  | Zneg e => Qmake num (Pos.iter (Pos.mul 10) 1%positive e)
+  end.
+
+Definition to_decimal (q:Q) : option Decimal.decimal :=
+  let num := Z.to_int (Qnum q) in
+  let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in
+  match den with
+  | Decimal.D1 Decimal.Nil =>
+    match Z.of_nat e_den with
+    | Z0 => Some (Decimal.Decimal num Decimal.Nil)
+    | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e)))
+    end
+  | _ => None
+  end.
+
+Numeral Notation Q of_decimal to_decimal : Q_scope.
+
 Definition inject_Z (x : Z) := Qmake x 1.
 Arguments inject_Z x%Z.
 
 Notation QDen p := (Zpos (Qden p)).
-Notation " 0 " := (0#1) : Q_scope.
-Notation " 1 " := (1#1) : Q_scope.
 
 Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
 Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.