Library HoTT.Basics.Nat

Require Import Basics.Overture Basics.Numeral.

Notation "n .+1" := (S n) : nat_scope.
Notation "n .+2" := (n.+1.+1)%nat : nat_scope.
Notation "n .+3" := (n.+1.+2)%nat : nat_scope.
Notation "n .+4" := (n.+1.+3)%nat : nat_scope.
Notation "n .+5" := (n.+1.+4)%nat : nat_scope.

Tail-recursive versions of add and mul


Fixpoint tail_add n m :=
  match n with
    | Om
    | S ntail_add n (S m)
  end.

tail_addmul r n m is r + n × m.

Fixpoint tail_addmul r n m :=
  match n with
    | Or
    | S ntail_addmul (tail_add m r) n m
  end.

Definition tail_mul n m := tail_addmul O 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.Nilacc
  | Decimal.D0 dof_uint_acc d (tail_mul ten acc)
  | Decimal.D1 dof_uint_acc d (S (tail_mul ten acc))
  | Decimal.D2 dof_uint_acc d (S (S (tail_mul ten acc)))
  | Decimal.D3 dof_uint_acc d (S (S (S (tail_mul ten acc))))
  | Decimal.D4 dof_uint_acc d (S (S (S (S (tail_mul ten acc)))))
  | Decimal.D5 dof_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
  | Decimal.D6 dof_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
  | Decimal.D7 dof_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
  | Decimal.D8 dof_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
  | Decimal.D9 dof_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.

Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).

Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
  match d with
  | Hexadecimal.Nilacc
  | Hexadecimal.D0 dof_hex_uint_acc d (tail_mul sixteen acc)
  | Hexadecimal.D1 dof_hex_uint_acc d (S (tail_mul sixteen acc))
  | Hexadecimal.D2 dof_hex_uint_acc d (S (S (tail_mul sixteen acc)))
  | Hexadecimal.D3 dof_hex_uint_acc d (S (S (S (tail_mul sixteen acc))))
  | Hexadecimal.D4 dof_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc)))))
  | Hexadecimal.D5 dof_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc))))))
  | Hexadecimal.D6 dof_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc)))))))
  | Hexadecimal.D7 dof_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))
  | Hexadecimal.D8 dof_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))
  | Hexadecimal.D9 dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))
  | Hexadecimal.Da dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))
  | Hexadecimal.Db dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))
  | Hexadecimal.Dc dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))
  | Hexadecimal.Dd dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))
  | Hexadecimal.De dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))
  | Hexadecimal.Df dof_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))))
  end.

Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.

Definition of_num_uint (d:Numeral.uint) :=
  match d with
  | Numeral.UIntDec dof_uint d
  | Numeral.UIntHex dof_hex_uint d
  end.

Fixpoint to_little_uint n acc :=
  match n with
  | Oacc
  | S nto_little_uint n (Decimal.Little.succ acc)
  end.

Definition to_uint n :=
  Decimal.rev (to_little_uint n Decimal.zero).

Definition to_num_uint n := Numeral.UIntDec (to_uint n).

Definition of_int (d:Decimal.int) : option nat :=
  match Decimal.norm d with
    | Decimal.Pos uSome (of_uint u)
    | _None
  end.

Definition of_hex_int (d:Hexadecimal.int) : option nat :=
  match Hexadecimal.norm d with
    | Hexadecimal.Pos uSome (of_hex_uint u)
    | _None
  end.

Definition of_num_int (d:Numeral.int) : option nat :=
  match d with
  | Numeral.IntDec dof_int d
  | Numeral.IntHex dof_hex_int d
  end.

Definition to_int n := Decimal.Pos (to_uint n).

Definition to_num_int n := Numeral.IntDec (to_int n).

Arguments of_uint d%_dec_uint_scope.
Arguments of_int d%_dec_int_scope.

(* Parsing / printing of nat numbers *)
Number Notation nat of_num_uint to_num_uint (abstract after 5001) : nat_scope.