module Stdlib.Data.Byte;

import Stdlib.Data.Byte.Base open using {Byte} public;
import Stdlib.Data.Byte.Base as Byte public;
import Stdlib.Function open;
import Stdlib.Data.Nat open;
import Stdlib.Data.String.Base open;
import Stdlib.Debug.Fail open;

import Stdlib.Trait.Eq open public;
import Stdlib.Trait.FromNatural open;
import Stdlib.Trait.Show open public;

{-# specialize: true, inline: case #-}
instance
eqByteI : Eq Byte := Eq.mk (Byte.==);

instance
showByteI : Show Byte :=
  Show.mk@{
    show (x : Byte) : String :=
      let
        nibble (n : Nat) : String :=
          if 
            | n <= 9 := Show.show n
            | n == 10 := "A"
            | n == 11 := "B"
            | n == 12 := "C"
            | n == 13 := "D"
            | n == 14 := "E"
            | n == 15 := "F"
            | else := impossible;
        nat := Byte.toNat x;
      in "0x" ++str nibble (div nat 16) ++str nibble (mod nat 16);
  };

{-# specialize: true, inline: case #-}
instance
fromNaturalByteI : FromNatural Byte :=
  mkFromNatural@{
    fromNat := Byte.fromNat;
  };