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

2 files changed, 69 insertions, 2 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 3d4b3d0568..1a7dadb2c3 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -16,6 +16,8 @@
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
+Require Import Datatypes.
+
 (** Unsigned integers are just lists of digits.
     For instance, ten is (D1 (D0 Nil)) *)
 
@@ -42,6 +44,15 @@ Notation zero := (D0 Nil).
 
 Variant int := Pos (d:uint) | Neg (d:uint).
 
+(** For decimal numbers, we use two constructors [Decimal] and
+    [DecimalExp], depending on whether or not they are given with an
+    exponent (e.g., 1.02e+01). [i] is the integral part while [f] is
+    the fractional part (beware that leading zeroes do matter). *)
+
+Variant decimal :=
+ | Decimal (i:int) (f:uint)
+ | DecimalExp (i:int) (f:uint) (e:int).
+
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
@@ -52,6 +63,14 @@ Bind Scope dec_int_scope with int.
 
 Register uint as num.uint.type.
 Register int as num.int.type.
+Register decimal as num.decimal.type.
+
+Fixpoint nb_digits d :=
+  match d with
+  | Nil => O
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d =>
+    S (nb_digits d)
+  end.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
@@ -115,6 +134,28 @@ Fixpoint revapp (d d' : uint) :=
 
 Definition rev d := revapp d Nil.
 
+Definition app d d' := revapp (rev d) d'.
+
+Definition app_int d1 d2 :=
+  match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end.
+
+(** [nztail] removes all trailing zero digits and return both the
+    result and the number of removed digits. *)
+
+Definition nztail d :=
+  let fix aux d_rev :=
+    match d_rev with
+    | D0 d_rev => let (r, n) := aux d_rev in pair r (S n)
+    | _ => pair d_rev O
+    end in
+  let (r, n) := aux (rev d) in pair (rev r) n.
+
+Definition nztail_int d :=
+  match d with
+  | Pos d => let (r, n) := nztail d in pair (Pos r) n
+  | Neg d => let (r, n) := nztail d in pair (Neg r) n
+  end.
+
 Module Little.
 
 (** Successor of little-endian numbers *)
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.