diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:29:26 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-24 09:29:26 +0100 |
commit | 89bd76b6f6a534613b03aaa970baf513b7c9b76b (patch) | |
tree | bfba682b6121778a64fcf1f593c37e4a6674990f /theories/Init/Nat.v | |
parent | 7895d276146496648d576914aab4aded4b4a32cd (diff) | |
parent | 63da69cff704be2da61f3cd311fa7a67dca6fc51 (diff) |
Merge PR #6599: Decimals in prelude
Diffstat (limited to 'theories/Init/Nat.v')
-rw-r--r-- | theories/Init/Nat.v | 58 |
1 files changed, 57 insertions, 1 deletions
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index e942ca562..8f2648269 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,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. |