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 | |
parent | 7895d276146496648d576914aab4aded4b4a32cd (diff) | |
parent | 63da69cff704be2da61f3cd311fa7a67dca6fc51 (diff) |
Merge PR #6599: Decimals in prelude
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Decimal.v | 161 | ||||
-rw-r--r-- | theories/Init/Nat.v | 58 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 1 |
3 files changed, 219 insertions, 1 deletions
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v new file mode 100644 index 000000000..fa462f147 --- /dev/null +++ b/theories/Init/Decimal.v @@ -0,0 +1,161 @@ +(************************************************************************) +(* 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). *) + +(** [nzhead] removes all head zero digits *) + +Fixpoint nzhead d := + match d with + | D0 d => nzhead d + | _ => d + end. + +(** [unorm] : normalization of unsigned integers *) + +Definition unorm d := + match nzhead d with + | Nil => zero + | d => d + end. + +(** [norm] : normalization of signed integers *) + +Definition norm d := + match d with + | Pos d => Pos (unorm d) + | Neg d => + match nzhead 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 revapp (d d' : uint) := + match d with + | Nil => d' + | D0 d => revapp d (D0 d') + | D1 d => revapp d (D1 d') + | D2 d => revapp d (D2 d') + | D3 d => revapp d (D3 d') + | D4 d => revapp d (D4 d') + | D5 d => revapp d (D5 d') + | D6 d => revapp d (D6 d') + | D7 d => revapp d (D7 d') + | D8 d => revapp d (D8 d') + | D9 d => revapp d (D9 d') + end. + +Definition rev d := revapp d Nil. + +Module Little. + +(** Successor of little-endian numbers *) + +Fixpoint succ d := + match d with + | Nil => D1 Nil + | D0 d => D1 d + | D1 d => D2 d + | D2 d => D3 d + | D3 d => D4 d + | D4 d => D5 d + | D5 d => D6 d + | D6 d => D7 d + | D7 d => D8 d + | D8 d => D9 d + | D9 d => D0 (succ d) + end. + +(** Doubling little-endian numbers *) + +Fixpoint double d := + match d with + | Nil => Nil + | D0 d => D0 (double d) + | D1 d => D2 (double d) + | D2 d => D4 (double d) + | D3 d => D6 (double d) + | D4 d => D8 (double d) + | D5 d => D0 (succ_double d) + | D6 d => D2 (succ_double d) + | D7 d => D4 (succ_double d) + | D8 d => D6 (succ_double d) + | D9 d => D8 (succ_double d) + end + +with succ_double d := + match d with + | Nil => D1 Nil + | D0 d => D1 (double d) + | D1 d => D3 (double d) + | D2 d => D5 (double d) + | D3 d => D7 (double d) + | D4 d => D9 (double d) + | D5 d => D1 (succ_double d) + | D6 d => D3 (succ_double d) + | D7 d => D5 (succ_double d) + | D8 d => D7 (succ_double d) + | D9 d => D9 (succ_double d) + end. + +End Little. 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. 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. |