Library HoTT.Basics.Numerals.Decimal

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    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)         *)
(************************************************************************)

(************************************************************************)
(* This file has been modified for use in the HoTT library              *)
(************************************************************************)

Require Import Basics.Overture.

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))

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.

Variant int : Type0 := Pos (d:uint) | Neg (d:uint).

For decimal numbers, we use two constructors Decimal and DecimalExp, depending on whether or not they are given with an exponent (e.g., 1.02e+01). i is the integral part while f is the fractional part (beware that leading zeroes do matter).

Variant decimal : Type0 :=
| Decimal (i:int) (f:uint)
| DecimalExp (i:int) (f:uint) (e:int).

Declare Scope dec_uint_scope.
Delimit Scope dec_uint_scope with uint.
Bind Scope dec_uint_scope with uint.

Declare Scope dec_int_scope.
Delimit Scope dec_int_scope with int.
Bind Scope dec_int_scope with int.

Register uint as num.uint.type.
Register int as num.int.type.
Register decimal as num.decimal.type.

Fixpoint nb_digits d :=
  match d with
  | Nil ⇒ O
  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d ⇒
    S (nb_digits d)
  end.

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.

nztail removes all trailing zero digits and return both the result and the number of removed digits.

Definition nztail d :=
  let fix aux d_rev :=
    match d_rev with
    | D0 d_rev ⇒ let (r, n) := aux d_rev in pair r (S n)
    | _ ⇒ pair d_rev O
    end in
  let (r, n) := aux (rev d) in pair (rev r) n.

Definition nztail_int d :=
  match d with
  | Pos d ⇒ let (r, n) := nztail d in pair (Pos r) n
  | Neg d ⇒ let (r, n) := nztail d in pair (Neg r) n
  end.

Module Little.

Successor of little-endian numbers

Doubling little-endian numbers

Pseudo-conversion functions used when declaring Numeral Notations on uint and int.

Definition uint_of_uint (i:uint) := i.
Definition int_of_int (i:int) := i.