Require Import List Arith NArith NPeano Ascii String.
Set Implicit Arguments.
Local Open Scope string_scope.
Local Definition natToDigit (n : nat) : string :=
match n with
| 0 => "0"
| 1 => "1"
| 2 => "2"
| 3 => "3"
| 4 => "4"
| 5 => "5"
| 6 => "6"
| 7 => "7"
| 8 => "8"
| _ => "9"
end.
Local Definition NToDigit (n : N) := natToDigit (N.to_nat n).
Local Fixpoint writeNatAux (time n : nat) (acc : string) : string :=
let acc' := natToDigit (n mod 10) ++ acc in
match time with
| 0 => acc'
| S time' =>
match n / 10 with
| 0 => acc'
| n' => writeNatAux time' n' acc'
end
end.
Local Fixpoint writeNAux (time : nat) (n : N) (acc : string) : string :=
let acc' := NToDigit (n mod 10)%N ++ acc in
match time with
| 0 => acc'
| S time' =>
match (n / 10)%N with
| N0 => acc'
| n' => writeNAux time' n' acc'
end
end.
Section N_to_string.
Let loop := fix loop l n s :=
let (d,r) := N.div_eucl n 10 in
let s' := String (ascii_of_N (48+r)) s
in match d, l with
| N0, _ => s'
| _ , 0 => s'
| _ , S l => loop l d s'
end.
Definition string_of_N n :=
match n with
| N0 => "0"
| _ => loop 12 n EmptyString
end.
End N_to_string.
Definition string_of_nat n := writeNatAux n n "".