From 960d48790121b876e6be7ca033138f5d28eae0cb Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Mon, 27 Feb 2017 19:56:27 +0100
Subject: Decimal: simple representation of base-10 numbers

---
 theories/Init/Decimal.v     | 153 ++++++++++++++++++++++++++++++++++++++++++++
 theories/Init/Nat.v         |  62 +++++++++++++++++-
 theories/Init/Prelude.v     |   1 +
 theories/NArith/BinNatDef.v |  18 ++++++
 theories/PArith/BinPosDef.v |  55 ++++++++++++++++
 theories/ZArith/BinIntDef.v |  17 +++++
 6 files changed, 305 insertions(+), 1 deletion(-)
 create mode 100644 theories/Init/Decimal.v

(limited to 'theories')

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
new file mode 100644
index 000000000..bf4764895
--- /dev/null
+++ b/theories/Init/Decimal.v
@@ -0,0 +1,153 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Decimal numbers *)
+
+(** These numbers coded in base 10 will be used for parsing and printing
+    other Coq numeral datatypes in an human-readable way.
+    See the [Numeral Notation] command.
+    We represent numbers in base 10 as lists of decimal digits,
+    in big-endian order (most significant digit comes first). *)
+
+(** Unsigned integers are just lists of digits.
+    For instance, ten is (D1 (D0 Nil)) *)
+
+Inductive uint :=
+ | Nil
+ | D0 (_:uint)
+ | D1 (_:uint)
+ | D2 (_:uint)
+ | D3 (_:uint)
+ | D4 (_:uint)
+ | D5 (_:uint)
+ | D6 (_:uint)
+ | D7 (_:uint)
+ | D8 (_:uint)
+ | D9 (_:uint).
+
+(** [Nil] is the number terminator. Taken alone, it behaves as zero,
+    but rather use [D0 Nil] instead, since this form will be denoted
+    as [0], while [Nil] will be printed as [Nil]. *)
+
+Notation zero := (D0 Nil).
+
+(** For signed integers, we use two constructors [Pos] and [Neg]. *)
+
+Inductive int := Pos (d:uint) | Neg (d:uint).
+
+Delimit Scope uint_scope with uint.
+Bind Scope uint_scope with uint.
+Delimit Scope int_scope with int.
+Bind Scope int_scope with int.
+
+(** This representation favors simplicity over canonicity.
+    For normalizing numbers, we need to remove head zero digits,
+    and choose our canonical representation of 0 (here [D0 Nil]
+    for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *)
+
+Fixpoint nonzero_head d :=
+  match d with
+  | D0 d => nonzero_head d
+  | _ => d
+  end.
+
+Definition unorm d :=
+  match nonzero_head d with
+  | Nil => zero
+  | d => d
+  end.
+
+Definition norm d :=
+  match d with
+  | Pos d => Pos (unorm d)
+  | Neg d =>
+    match nonzero_head d with
+    | Nil => Pos zero
+    | d => Neg d
+    end
+  end.
+
+(** A few easy operations. For more advanced computations, use the conversions
+    with other Coq numeral datatypes (e.g. Z) and the operations on them. *)
+
+Definition opp (d:int) :=
+  match d with
+  | Pos d => Neg d
+  | Neg d => Pos d
+  end.
+
+(** For conversions with binary numbers, it is easier to operate
+    on little-endian numbers. *)
+
+Fixpoint rev (l l' : uint) :=
+  match l with
+  | Nil => l'
+  | D0 l => rev l (D0 l')
+  | D1 l => rev l (D1 l')
+  | D2 l => rev l (D2 l')
+  | D3 l => rev l (D3 l')
+  | D4 l => rev l (D4 l')
+  | D5 l => rev l (D5 l')
+  | D6 l => rev l (D6 l')
+  | D7 l => rev l (D7 l')
+  | D8 l => rev l (D8 l')
+  | D9 l => rev l (D9 l')
+  end.
+
+Module Little.
+
+(** Successor of little-endian numbers *)
+
+Fixpoint succ d :=
+  match d with
+  | Nil => D1 Nil
+  | D0 l => D1 l
+  | D1 l => D2 l
+  | D2 l => D3 l
+  | D3 l => D4 l
+  | D4 l => D5 l
+  | D5 l => D6 l
+  | D6 l => D7 l
+  | D7 l => D8 l
+  | D8 l => D9 l
+  | D9 l => D0 (succ l)
+  end.
+
+(** Doubling little-endian numbers *)
+
+Fixpoint double d :=
+  match d with
+  | Nil => Nil
+  | D0 l => D0 (double l)
+  | D1 l => D2 (double l)
+  | D2 l => D4 (double l)
+  | D3 l => D6 (double l)
+  | D4 l => D8 (double l)
+  | D5 l => D0 (succ_double l)
+  | D6 l => D2 (succ_double l)
+  | D7 l => D4 (succ_double l)
+  | D8 l => D6 (succ_double l)
+  | D9 l => D8 (succ_double l)
+  end
+
+with succ_double d :=
+  match d with
+  | Nil => D1 Nil
+  | D0 l => D1 (double l)
+  | D1 l => D3 (double l)
+  | D2 l => D5 (double l)
+  | D3 l => D7 (double l)
+  | D4 l => D9 (double l)
+  | D5 l => D1 (succ_double l)
+  | D6 l => D3 (succ_double l)
+  | D7 l => D5 (succ_double l)
+  | D8 l => D7 (succ_double l)
+  | D9 l => D9 (succ_double l)
+  end.
+
+End Little.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index e942ca562..72d35827e 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import Notations Logic Datatypes.
-
+Require Decimal.
 Local Open Scope nat_scope.
 
 (**********************************************************************)
@@ -134,6 +134,66 @@ Fixpoint pow n m :=
 
 where "n ^ m" := (pow n m) : nat_scope.
 
+(** ** Tail-recursive versions of [add] and [mul] *)
+
+Module Tail.
+
+Fixpoint add n m :=
+  match n with
+    | O => m
+    | S n => add n (S m)
+  end.
+
+(** [addmul r n m] is [r + n * m]. *)
+
+Fixpoint addmul r n m :=
+  match n with
+    | O => r
+    | S n => addmul (add m r) n m
+  end.
+
+Definition mul n m := addmul 0 n m.
+
+End Tail.
+
+(** ** Conversion with a decimal representation for printing/parsing *)
+
+Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).
+
+Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
+  match d with
+  | Decimal.Nil => acc
+  | Decimal.D0 d => of_uint_acc d (Tail.mul ten acc)
+  | Decimal.D1 d => of_uint_acc d (S (Tail.mul ten acc))
+  | Decimal.D2 d => of_uint_acc d (S (S (Tail.mul ten acc)))
+  | Decimal.D3 d => of_uint_acc d (S (S (S (Tail.mul ten acc))))
+  | Decimal.D4 d => of_uint_acc d (S (S (S (S (Tail.mul ten acc)))))
+  | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (Tail.mul ten acc))))))
+  | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (Tail.mul ten acc)))))))
+  | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (Tail.mul ten acc))))))))
+  | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (Tail.mul ten acc)))))))))
+  | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (Tail.mul ten acc))))))))))
+  end.
+
+Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
+
+Fixpoint to_little_uint n acc :=
+  match n with
+  | O => acc
+  | S n => to_little_uint n (Decimal.Little.succ acc)
+  end.
+
+Definition to_uint n :=
+  Decimal.rev (to_little_uint n Decimal.zero) Decimal.Nil.
+
+Definition of_int (d:Decimal.int) : option nat :=
+  match Decimal.norm d with
+    | Decimal.Pos u => Some (of_uint u)
+    | _ => None
+  end.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
 (** ** Euclidean division *)
 
 (** This division is linear and tail-recursive.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index f0867a034..63c431e8e 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -11,6 +11,7 @@ Require Export Logic.
 Require Export Logic_Type.
 Require Export Datatypes.
 Require Export Specif.
+Require Coq.Init.Decimal.
 Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 6771e57ad..e07758914 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -378,4 +378,22 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
     | pos p => Pos.iter f x p
   end.
 
+(** Conversion with a decimal representation for printing/parsing *)
+
+Definition of_uint (d:Decimal.uint) := Pos.of_uint d.
+
+Definition of_int (d:Decimal.int) :=
+  match Decimal.norm d with
+  | Decimal.Pos d => Some (Pos.of_uint d)
+  | Decimal.Neg _ => None
+  end.
+
+Definition to_uint n :=
+  match n with
+  | 0 => Decimal.zero
+  | pos p => Pos.to_uint p
+  end.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
 End N.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 2b647555c..85c401cf4 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -557,4 +557,59 @@ Fixpoint of_succ_nat (n:nat) : positive :=
     | S x => succ (of_succ_nat x)
   end.
 
+(** ** Conversion with a decimal representation for printing/parsing *)
+
+Local Notation ten := 1~0~1~0.
+
+Fixpoint of_uint_acc (d:Decimal.uint)(acc:positive) :=
+  match d with
+  | Decimal.Nil => acc
+  | Decimal.D0 l => of_uint_acc l (mul ten acc)
+  | Decimal.D1 l => of_uint_acc l (add 1 (mul ten acc))
+  | Decimal.D2 l => of_uint_acc l (add 1~0 (mul ten acc))
+  | Decimal.D3 l => of_uint_acc l (add 1~1 (mul ten acc))
+  | Decimal.D4 l => of_uint_acc l (add 1~0~0 (mul ten acc))
+  | Decimal.D5 l => of_uint_acc l (add 1~0~1 (mul ten acc))
+  | Decimal.D6 l => of_uint_acc l (add 1~1~0 (mul ten acc))
+  | Decimal.D7 l => of_uint_acc l (add 1~1~1 (mul ten acc))
+  | Decimal.D8 l => of_uint_acc l (add 1~0~0~0 (mul ten acc))
+  | Decimal.D9 l => of_uint_acc l (add 1~0~0~1 (mul ten acc))
+  end.
+
+Fixpoint of_uint (d:Decimal.uint) : N :=
+  match d with
+  | Decimal.Nil => N0
+  | Decimal.D0 l => of_uint l
+  | Decimal.D1 l => Npos (of_uint_acc l 1)
+  | Decimal.D2 l => Npos (of_uint_acc l 1~0)
+  | Decimal.D3 l => Npos (of_uint_acc l 1~1)
+  | Decimal.D4 l => Npos (of_uint_acc l 1~0~0)
+  | Decimal.D5 l => Npos (of_uint_acc l 1~0~1)
+  | Decimal.D6 l => Npos (of_uint_acc l 1~1~0)
+  | Decimal.D7 l => Npos (of_uint_acc l 1~1~1)
+  | Decimal.D8 l => Npos (of_uint_acc l 1~0~0~0)
+  | Decimal.D9 l => Npos (of_uint_acc l 1~0~0~1)
+  end.
+
+Definition of_int (d:Decimal.int) : option positive :=
+  match d with
+  | Decimal.Pos d =>
+    match of_uint d with
+    | N0 => None
+    | Npos p => Some p
+    end
+  | Decimal.Neg _ => None
+  end.
+
+Fixpoint to_little_uint p :=
+  match p with
+  | 1 => Decimal.D1 Decimal.Nil
+  | p~1 => Decimal.Little.succ_double (to_little_uint p)
+  | p~0 => Decimal.Little.double (to_little_uint p)
+  end.
+
+Definition to_uint p := Decimal.rev (to_little_uint p) Decimal.Nil.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
 End Pos.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 443667f48..a0393f318 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -299,6 +299,23 @@ Definition to_pos (z:Z) : positive :=
     | _ => 1%positive
   end.
 
+(** Conversion with a decimal representation for printing/parsing *)
+
+Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d).
+
+Definition of_int (d:Decimal.int) :=
+  match d with
+  | Decimal.Pos d => of_uint d
+  | Decimal.Neg d => opp (of_uint d)
+  end.
+
+Definition to_int n :=
+  match n with
+  | 0 => Decimal.Pos Decimal.zero
+  | pos p => Decimal.Pos (Pos.to_uint p)
+  | neg p => Decimal.Neg (Pos.to_uint p)
+  end.
+
 (** ** Iteration of a function
 
     By convention, iterating a negative number of times is identity.
-- 
cgit v1.2.3