Library 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.