aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Init/Decimal.v153
-rw-r--r--theories/Init/Nat.v62
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--theories/NArith/BinNatDef.v18
-rw-r--r--theories/PArith/BinPosDef.v55
-rw-r--r--theories/ZArith/BinIntDef.v17
6 files changed, 305 insertions, 1 deletions
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.