# Module PrintPos

Require Import ZArith NArith List Zpower.

Inductive hex_digit : Set :=
| Hx0 | Hx1 | Hx2 | Hx3
| Hx4 | Hx5 | Hx6 | Hx7
| Hx8 | Hx9 | HxA | HxB
| HxC | HxD | HxE | HxF
.

Inductive hex_digit_partial : Set :=
| HDP0 | HDP1 (b: bool)
| HDP2 (b1 b0: bool)
| HDP3 (b2 b1 b0: bool)
.

Definition hex_partial_as_digit (hp: hex_digit_partial) : hex_digit :=
match hp with
| HDP0
| HDP1 false
| HDP2 false false
| HDP3 false false false => Hx0
| HDP1 true
| HDP2 false true
| HDP3 false false true => Hx1
| HDP2 true false
| HDP3 false true false => Hx2
| HDP2 true true
| HDP3 false true true => Hx3
| HDP3 true false false => Hx4
| HDP3 true false true => Hx5
| HDP3 true true false => Hx6
| HDP3 true true true => Hx7
end.

Definition set_next_bit (bh: hex_digit_partial)
: hex_digit + hex_digit_partial :=
match bh with
| HDP0 => inr _ (HDP1 true)
| HDP1 b => inr _ (HDP2 true b)
| HDP2 b1 b0 => inr _ (HDP3 true b1 b0)
| HDP3 b2 b1 b0 => inl _
(match b2, b1, b0 with
| false, false, false => Hx8
| false, false, true => Hx9
| false, true , false => HxA
| false, true , true => HxB
| true , false, false => HxC
| true , false, true => HxD
| true , true , false => HxE
| true , true , true => HxF
end)
end.

Definition reset_next_bit (bh: hex_digit_partial)
: hex_digit + hex_digit_partial :=
match bh with
| HDP0 => inr _ (HDP1 false)
| HDP1 b => inr _ (HDP2 false b)
| HDP2 b1 b0 => inr _ (HDP3 false b1 b0)
| HDP3 b2 b1 b0 => inl _
(match b2, b1, b0 with
| false, false, false => Hx0
| false, false, true => Hx1
| false, true , false => Hx2
| false, true , true => Hx3
| true , false, false => Hx4
| true , false, true => Hx5
| true , true , false => Hx6
| true , true , true => Hx7
end)
end.

Definition hex_num : Set := list hex_digit.

Fixpoint hex_of_pos' (p: positive) (curr: hex_digit_partial) (acc: hex_num)
{struct p} : hex_num :=
match p with
| xH => match set_next_bit curr with
| inl d => d
| inr hp => hex_partial_as_digit hp
end :: acc
| xO p' => match reset_next_bit curr with
| inl d => hex_of_pos' p' HDP0 (d::acc)
| inr hp => hex_of_pos' p' hp acc
end
| xI p' => match set_next_bit curr with
| inl d => hex_of_pos' p' HDP0 (d::acc)
| inr hp => hex_of_pos' p' hp acc
end
end.

Definition hex_of_pos (p: positive) : hex_num :=
hex_of_pos' p HDP0 nil.

Section PRINT.

Require Import Ascii String.
Local Open Scope char_scope.

Definition hex_digit_ascii (hx: hex_digit) : ascii :=
match hx with
| Hx0 => "0" | Hx1 => "1"
| Hx2 => "2" | Hx3 => "3"
| Hx4 => "4" | Hx5 => "5"
| Hx6 => "6" | Hx7 => "7"
| Hx8 => "8" | Hx9 => "9"
| HxA => "A" | HxB => "B"
| HxC => "C" | HxD => "D"
| HxE => "E" | HxF => "F"
end.

Fixpoint hex_num_string (hn: hex_num) {struct hn} : string :=
match hn with
| d :: hn' => String (hex_digit_ascii d) (hex_num_string hn')
| nil => EmptyString
end.

Definition print_pos (p: positive) : string :=
("0x" ++ hex_num_string (hex_of_pos p))%string.

Definition string_of_z (z: Z) : string :=
(match z with
| Z0 => "0"
| Zpos p => print_pos p
| Zneg p => "-" ++ print_pos p
end)%string.

End PRINT.