[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, 44 insertions, 0 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 025264ab01..bb12f9ca3e 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -118,6 +118,12 @@ Definition opp (d:int) :=
   | Neg d => Pos d
   end.
 
+Definition abs (d:int) : uint :=
+  match d with
+  | Pos d => d
+  | Neg d => d
+  end.
+
 (** For conversions with binary numbers, it is easier to operate
     on little-endian numbers. *)
 
diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v
index 36f5e5ad1f..7467aa1262 100644
--- a/theories/Init/Hexadecimal.v
+++ b/theories/Init/Hexadecimal.v
@@ -125,6 +125,12 @@ Definition opp (d:int) :=
   | Neg d => Pos d
   end.
 
+Definition abs (d:int) : uint :=
+  match d with
+  | Pos d => d
+  | Neg d => d
+  end.
+
 (** For conversions with binary numbers, it is easier to operate
     on little-endian numbers. *)
 
@@ -173,6 +179,38 @@ Definition nztail_int d :=
   | Neg d => let (r, n) := nztail d in pair (Neg r) n
   end.
 
+(** [del_head n d] removes [n] digits at beginning of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Fixpoint del_head n d :=
+  match n with
+  | O => d
+  | S n =>
+    match d with
+    | Nil => zero
+    | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d
+    | Da d | Db d | Dc d | Dd d | De d | Df d =>
+      del_head n d
+    end
+  end.
+
+Definition del_head_int n d :=
+  match d with
+  | Pos d => del_head n d
+  | Neg d => del_head n d
+  end.
+
+(** [del_tail n d] removes [n] digits at end of [d]
+    or returns [zero] if [d] has less than [n] digits. *)
+
+Definition del_tail n d := rev (del_head n (rev d)).
+
+Definition del_tail_int n d :=
+  match d with
+  | Pos d => Pos (del_tail n d)
+  | Neg d => Neg (del_tail n d)
+  end.
+
 Module Little.
 
 (** Successor of little-endian numbers *)