From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Init/Nat.v | 68 +++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 63 insertions(+), 5 deletions(-)

(limited to 'theories/Init/Nat.v')

diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index b8920586..ad1bc717 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -1,13 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 Require Import Notations Logic Datatypes.
-
+Require Decimal.
 Local Open Scope nat_scope.
 
 (**********************************************************************)
@@ -134,6 +136,62 @@ Fixpoint pow n m :=
 
 where "n ^ m" := (pow n m) : nat_scope.
 
+(** ** Tail-recursive versions of [add] and [mul] *)
+
+Fixpoint tail_add n m :=
+  match n with
+    | O => m
+    | S n => tail_add n (S m)
+  end.
+
+(** [tail_addmul r n m] is [r + n * m]. *)
+
+Fixpoint tail_addmul r n m :=
+  match n with
+    | O => r
+    | S n => tail_addmul (tail_add m r) n m
+  end.
+
+Definition tail_mul n m := tail_addmul 0 n m.
+
+(** ** 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).
+
+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.
-- 
cgit v1.2.3